add ocaml types for patterns, pattern matching, and constructor appli…

…cation in terms.ml

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

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

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
 

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 ->