Add top-level pattern match guards internally

Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.

4 files changed, 8 insertions, 7 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index b49646ea..11947c17 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -103,7 +103,8 @@ end
 let rec extract_from_decode decoder = 
   match decoder with
     | [] -> []
-    | (FCL_aux (FCL_Funcl _ pat exp) _)::decoder ->
+    | (FCL_aux (FCL_Funcl _ (Pat_aux pexp _)) _)::decoder ->
+      let exp = match pexp with Pat_exp _ exp -> exp | Pat_when _ _ exp -> exp end in
       (match exp with
 	| E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_,_))) ->
 	  Instr_form id (List.map extract_parm parms) []
@@ -112,7 +113,7 @@ end
 
 let rec extract_effects_of_fcl id execute = match execute with
   | [] -> []
-  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) _) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _,_))) :: executes ->
+  | FCL_aux (FCL_Funcl _ (Pat_aux (Pat_exp (P_aux (P_app (Id_aux (Id i) _) _) _) _) _)) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _,_))) :: executes ->
     if i = id 
     then efs
     else extract_effects_of_fcl id executes
@@ -134,7 +135,7 @@ let rec extract_patt_parm (P_aux p (_,tannot)) =
 
 let rec extract_from_execute fcls = match fcls with
   | [] -> []
-  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) parms) _) _) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls ->
+  | FCL_aux (FCL_Funcl _ (Pat_aux (Pat_exp (P_aux (P_app (Id_aux (Id i) _) parms) _) _) _)) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls ->
      (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls
   | _ :: fcls ->
      (* AA: Find out what breaks this *)
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 486728d9..431c1a08 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -639,7 +639,7 @@ let rec to_fdefs (Defs defs) =
             | FD_aux (FD_function _ _ _ fcls) _ ->
               match fcls with
                 | [] -> to_fdefs (Defs defs)
-                | (FCL_aux (FCL_Funcl name _ _) _)::_  ->
+                | (FCL_aux (FCL_Funcl name _) _)::_  ->
                   Map.insert (get_id name) fcls (to_fdefs (Defs defs)) end end)
         | _ -> to_fdefs (Defs defs) end end
 
@@ -1625,7 +1625,7 @@ val find_funcl : top_level -> list (funcl tannot) -> value -> list (lenv * bool
 let rec find_funcl t_level funcls value =
   match funcls with
   | [] -> []
-  | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
+  | (FCL_aux (FCL_Funcl id (Pat_aux (Pat_exp pat exp) _)) _)::funcls ->
     let (is_matching,used_unknown,env) = match_pattern t_level pat value in
     if (is_matching && used_unknown)
     then (env,used_unknown,exp)::(find_funcl t_level funcls value)
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index a178df61..1e6c59ff 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -178,7 +178,7 @@ val find_type_def : defs tannot -> id -> maybe (type_def tannot)
 val find_function : defs tannot -> id -> maybe (list (funcl tannot))
 
 let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
-  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
+  List.filter (fun (FCL_aux (FCL_Funcl name pexp) _) -> (get_id id) = (get_id name)) fcls
 
 let rec find_function (Defs defs) id =
   match defs with 
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 129b74c0..bf42795b 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -657,7 +657,7 @@ let doc_effects_opt (Effect_opt_aux(e,_)) = match e with
   | Effect_opt_pure -> string "pure"
   | Effect_opt_effect e -> doc_effects e
 
-let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,Pat_aux (Pat_exp (pat, exp), _)),_)) =
   group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env mem add_red false exp))
 
 let doc_fundef env mem add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) =