Make new-tc monomorphisation actually work

4 files changed, 39 insertions, 25 deletions

diff --git a/src/monomorphise_new.ml b/src/monomorphise_new.ml
index f73ecb13..e0e06158 100644
--- a/src/monomorphise_new.ml
+++ b/src/monomorphise_new.ml
@@ -65,13 +65,16 @@ let subst_src_typ substs t =
 (* Based on current type checker's behaviour *)
 let pat_id_is_variable env id =
   match Env.lookup_id id env with
+  | Unbound
+  (* TODO: are the next two possible in typechecked code?  What
+     would they do? *)
   | Register _
   | Local _
     -> true
   | Enum _
   | Union _
     -> false
-  | Unbound -> failwith "unbound var"
+
 
 let rec is_value (E_aux (e,(l,annot))) =
   match e with
@@ -381,7 +384,7 @@ type split =
   | VarSplit of (tannot pat * (id * tannot Ast.exp)) list
   | ConstrSplit of (tannot pat * nexp KSubst.t) list
 
-let split_defs splits (Type_check.Env (d_env,t_env,b_env,tp_env)) defs =
+let split_defs splits defs =
   let split_constructors (Defs defs) =
     let sc_type_union q (Tu_aux (tu,l) as tua) =
       match tu with
@@ -689,32 +692,38 @@ let split_defs splits (Type_check.Env (d_env,t_env,b_env,tp_env)) defs =
       nexp_subst_exp nsubsts refinements exp'
   in
     
-let env_some_enum_lookup _ _ = None in
   (* Split a variable pattern into every possible value *)
 
-  let split var env (Typ_aux (ty,l) as typ) =
-    let new_l = Generated l in
-    let new_id i = Id_aux (Id i, new_l) in
+  let split var annot =
     let v = string_of_id var in
+    let (env, (Typ_aux (ty,l) as typ), eff) =
+      match annot with
+      | Some ann -> ann
+      | None -> raise (Reporting_basic.err_general Unknown
+                         ("Missing type environment when splitting " ^ v))
+    in
+    let new_l = Generated l in
+    let renew_id (Id_aux (id,l)) = Id_aux (id,new_l) in
     let cannot () =
       raise (Reporting_basic.err_general l
                ("Cannot split type " ^ string_of_typ typ ^ " for variable " ^ v))
     in
     match ty with
     | Typ_id id ->
-       (match env_some_enum_lookup id env with
-          (* enumerations *)
-       | Some ns -> List.map (fun n -> (P_aux (P_id (new_id n),(l,None)),
-                                        (var,E_aux (E_id (new_id n),(new_l,None))))) ns
-       | None ->
-          if id_to_string id = "bit" then
-            List.map (fun b ->
-              P_aux (P_lit (L_aux (b,new_l)),(l,None)),
-              (var,E_aux (E_lit (L_aux (b,new_l)),(new_l, None))))
-              [L_zero; L_one]
-          else cannot ())
-       (*|  vectors TODO *)
-       (*|  numbers TODO *)
+       (try
+         (* enumerations *)
+         let ns = Env.get_enum id env in
+         List.map (fun n -> (P_aux (P_id (renew_id n),(l,annot)),
+                             (var,E_aux (E_id (renew_id n),(new_l,annot))))) ns
+       with Type_error _ ->
+         if id_to_string id = "bit" then
+           List.map (fun b ->
+             P_aux (P_lit (L_aux (b,new_l)),(l,annot)),
+             (var,E_aux (E_lit (L_aux (b,new_l)),(new_l, annot))))
+             [L_zero; L_one]
+         else cannot ())
+    (*|  vectors TODO *)
+    (*|  numbers TODO *)
     | _ -> cannot ()
   in
   
@@ -769,11 +778,7 @@ let env_some_enum_lookup _ _ = None in
         | P_id id ->
            let i = id_to_string id in
            if i = var
-           then
-             match annot with
-             | Some (env,ty,_) -> Some (split id env ty)
-             | None -> raise (Reporting_basic.err_general l
-                                ("Missing type environment when splitting " ^ var))
+           then Some (split id annot)
            else None
         | P_app (id,ps) ->
            relist spl (fun ps -> P_app (id,ps)) ps
diff --git a/src/process_file.ml b/src/process_file.ml
index 090332fd..efa2ec55 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -89,6 +89,7 @@ let opt_new_typecheck = ref false
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
 let opt_dno_cast = ref false
+let opt_mono_split = ref ([]:((string * int) * string) list)
 
 let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs =
   let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
@@ -103,6 +104,14 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
   then
     let ienv = if !opt_dno_cast then Type_check_new.Env.no_casts Type_check_new.initial_env else Type_check_new.initial_env in
     let ast, _ = Type_check_new.check ienv defs in
+    let ast = match !opt_mono_split with
+      | [] -> ast
+      | l ->
+         let ast = Monomorphise_new.split_defs l ast in
+         let ienv = Type_check_new.Env.no_casts Type_check_new.initial_env in
+         let ast, _ = Type_check_new.check ienv ast in
+         ast
+    in
     if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else ()
   else ();
   if !opt_just_check
diff --git a/src/process_file.mli b/src/process_file.mli
index 7ddd49ad..9620712a 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -51,6 +51,7 @@ val opt_new_typecheck : bool ref
 val opt_just_check : bool ref
 val opt_ddump_tc_ast : bool ref
 val opt_dno_cast : bool ref
+val opt_mono_split : ((string * int) * string) list ref
 
 type out_type =
   | Lem_ast_out
diff --git a/src/sail.ml b/src/sail.ml
index bff1f58b..007a3208 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -53,7 +53,6 @@ let opt_print_ocaml = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_ocaml = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
-let opt_mono_split = ref ([]:((string * int) * string) list)
 let options = Arg.align ([
   ( "-o",
     Arg.String (fun f -> opt_file_out := Some f),