Merge funcls for Lem output, making it suitable for testing with OCaml

2 files changed, 24 insertions, 0 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f2136f07..4bb3b553 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1198,6 +1198,9 @@ let get_id = function
 
 module StringSet = Set.Make(String)
 
+(* Strictly speaking, Lem doesn't support multiple clauses for a single function
+   joined by "and", although it has worked for Isabelle before.  However, all
+   the funcls should have been merged by the merge_funcls rewrite now. *)   
 let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) =
   separate_map (hardline ^^ string "and ") doc_funcl_lem funcls
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 0b4a864c..d6144755 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2952,6 +2952,26 @@ let rewrite_defs_remove_e_assign (Defs defs) =
     ; rewrite_defs = rewrite_defs_base
     } (Defs (loop_specs @ defs))
 
+let merge_funcls (Defs defs) =
+  let merge_function (FD_aux (FD_function (r,t,e,fcls),ann) as f) =
+    match fcls with
+    | [] | [_] -> f
+    | (FCL_aux (FCL_Funcl (id,_),(l,_)))::_ ->
+       let var = mk_id "merge#var" in
+       let l_g = Parse_ast.Generated l in
+       let ann_g : _ * tannot = (l_g,None) in
+       let clauses = List.map (fun (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp) fcls in
+       FD_aux (FD_function (r,t,e,[
+         FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (P_aux (P_id var,ann_g),
+                                                  E_aux (E_case (E_aux (E_id var,ann_g),clauses),ann_g)),ann_g)),
+                  (l,None))]),ann)
+  in
+  let merge_in_def = function
+    | DEF_fundef f -> DEF_fundef (merge_function f)
+    | DEF_internal_mutrec fs -> DEF_internal_mutrec (List.map merge_function fs)
+    | d -> d
+  in Defs (List.map merge_in_def defs)
+
 let recheck_defs defs = fst (check initial_env defs)
 
 let rewrite_defs_lem = [
@@ -2980,6 +3000,7 @@ let rewrite_defs_lem = [
   ("internal_lets", rewrite_defs_internal_lets);
   ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
   ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns);
+  ("merge function clauses", merge_funcls);
   ("recheck_defs", recheck_defs)
   ]