diff --git a/backend/cn/indexTerms.ml b/backend/cn/indexTerms.ml index d8ce2c329..624ccab14 100644 --- a/backend/cn/indexTerms.ml +++ b/backend/cn/indexTerms.ml @@ -36,7 +36,13 @@ let pp ?(atomic=false) = Terms.pp ~atomic - +let rec bound_by_pattern = function + | PSym s -> SymSet.singleton s + | PWild -> SymSet.empty + | PConstructor (_s, args) -> + List.fold_right SymSet.union + (List.map (fun (_id, pat) -> bound_by_pattern pat) args) + SymSet.empty let rec free_vars_ = function | Const _ -> SymSet.empty @@ -76,6 +82,11 @@ let rec free_vars_ = function | MapDef ((s, _bt), t) -> SymSet.remove s (free_vars t) | Apply (_pred, ts) -> free_vars_list ts | Let ((nm, t1), t2) -> SymSet.union (free_vars t1) (SymSet.remove nm (free_vars t2)) + | Match (e, cases) -> + List.fold_right (fun (pattern, body) acc -> + SymSet.union acc (SymSet.diff (free_vars body) (bound_by_pattern pattern)) + ) cases (free_vars e) + | Constructor (_s, args) -> free_vars_list (List.map snd args) and free_vars (IT (term_, _bt)) = free_vars_ term_ @@ -127,6 +138,8 @@ let rec fold_ f binders acc = function | Let ((nm, IT (t1_, bt)), t2) -> let acc' = fold f binders acc (IT (t1_, bt)) in fold f (binders @ [(nm, bt)]) acc' t2 + | Match _ -> failwith "todo" + | Constructor _ -> failwith "todo" and fold f binders acc (IT (term_, _bt)) = let acc' = fold_ f binders acc term_ in @@ -265,6 +278,10 @@ let rec subst (su : typed subst) (IT (it, bt)) = | Let ((name, t1), t2) -> let name, t2 = suitably_alpha_rename su.relevant (name, basetype t1) t2 in IT (Let ((name, subst su t1), subst su t2), bt) + | Match _ -> + failwith "todo" + | Constructor _ -> + failwith "todo" and alpha_rename (s, bt) body = let s' = Sym.fresh_same s in diff --git a/backend/cn/main.ml b/backend/cn/main.ml index 42a62a652..647fb277d 100644 --- a/backend/cn/main.ml +++ b/backend/cn/main.ml @@ -151,6 +151,7 @@ let main let open Resultat in let@ prog5 = Core_to_mucore.normalise_file (markers_env, ail_prog) prog4 in (* let instrumentation = Core_to_mucore.collect_instrumentation prog5 in *) + (* for constructor base type information, for now see prog5.mu_datatypes and prog5.mu_constructors *) print_log_file ("mucore", MUCORE prog5); let@ res = Typing.run Context.empty (Check.check prog5 statement_locs lemmata) in begin match output_decorated with diff --git a/backend/cn/terms.ml b/backend/cn/terms.ml index face92086..2655b36ef 100644 --- a/backend/cn/terms.ml +++ b/backend/cn/terms.ml @@ -47,6 +47,12 @@ type binop = | Subset [@@deriving eq, ord, show] +type pattern = + | PSym of Sym.t + | PWild + | PConstructor of Sym.t * (Id.t * pattern) list +[@@deriving eq, ord, map] + (* over integers and reals *) type 'bt term_ = | Const of const @@ -64,9 +70,10 @@ type 'bt term_ = | Record of (Id.t * 'bt term) list | RecordMember of 'bt term * Id.t | RecordUpdate of ('bt term * Id.t) * 'bt term - | DatatypeCons of Sym.t * 'bt term - | DatatypeMember of 'bt term * Id.t - | DatatypeIsCons of Sym.t * 'bt term + | DatatypeCons of Sym.t * 'bt term (* TODO: will be removed *) + | DatatypeMember of 'bt term * Id.t (* TODO: will be removed *) + | DatatypeIsCons of Sym.t * 'bt term (* TODO: will be removed *) + | Constructor of Sym.t * (Id.t * 'bt term) list | MemberOffset of Sym.t * Id.t | ArrayOffset of Sctypes.t (*element ct*) * 'bt term (*index*) | Nil @@ -86,6 +93,7 @@ type 'bt term_ = | MapDef of (Sym.t * 'bt) * 'bt term | Apply of Sym.t * ('bt term) list | Let of (Sym.t * 'bt term) * 'bt term + | Match of 'bt term * (pattern * 'bt term) list | Cast of BaseTypes.t * 'bt term and 'bt term = @@ -96,17 +104,31 @@ and 'bt term = let equal = equal_term let compare = compare_term + + +let rec pp_pattern = function + | PSym s -> + Sym.pp s + | PWild -> + underscore + | PConstructor (c, args) -> + Sym.pp c ^^^ + braces (separate_map (comma ^^ space) (fun (id, pat) -> + Id.pp id ^^ colon ^^^ pp_pattern pat + ) args) + let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term -> Pp.doc = fun ?(atomic=false) ?(f=fun _ x -> x) -> let rec aux atomic (IT (it, _)) = let aux b x = f x (aux b x) in (* Without the `lparen` inside `nest 2`, the printed `rparen` is indented by 2 (wrt to the lparen). I don't quite understand it, but it works. *) + let parens pped = + Pp.group ((nest 2 @@ lparen ^^ break 0 ^^ pped) ^^ break 0 ^^ rparen) in + let braces pped = + Pp.group ((nest 2 @@ lbrace ^^ break 0 ^^ pped) ^^ break 0 ^^ rbrace) in let mparens pped = - if atomic then - Pp.group ((nest 2 @@ lparen ^^ break 0 ^^ pped) ^^ break 0 ^^ rparen) - else - Pp.group pped in + if atomic then parens pped else Pp.group pped in let break_op x = break 1 ^^ x ^^ space in match it with | Const const -> @@ -308,6 +330,17 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term - c_app (Sym.pp name) (List.map (aux false) args) | Let ((name, x1), x2) -> parens (!^ "let" ^^^ Sym.pp name ^^^ Pp.equals ^^^ aux false x1 ^^^ !^ "in" ^^^ aux false x2) + | Match (e, cases) -> + !^"match" ^^^ aux false e ^^^ braces ( + (* copying from mparens *) + Pp.group (nest 2 @@ ( + separate_map (break 0) (fun (pattern, body) -> + pp_pattern pattern ^^^ !^"=>" ^^^ + braces (aux false body) + ) cases)) + ) + | Constructor (s, args) -> + Sym.pp s ^^^ braces (separate_map (comma ^^ space) (fun (id, e) -> Id.pp id ^^ colon ^^^ aux false e) args) in fun (it : 'bt term) -> aux atomic it diff --git a/backend/cn/wellTyped.ml b/backend/cn/wellTyped.ml index dbb533715..e3016ffee 100644 --- a/backend/cn/wellTyped.ml +++ b/backend/cn/wellTyped.ml @@ -586,6 +586,8 @@ module WIT = struct let@ t2 = infer loc t2 in return (IT (Let ((name, t1), t2), IT.bt t2)) end + | Match _ -> failwith "todo" + | Constructor _ -> failwith "todo" and check = fun loc ls it ->