From 535f4736f3632e8959a7ebc7f5f43c8d6abc1325 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 13 Mar 2018 14:39:05 +0000
Subject: Merge funcls for Lem output, making it suitable for testing with
 OCaml

---
 src/pretty_print_lem.ml        |  3 +++
 src/rewrites.ml                | 21 +++++++++++++++++++++
 test/mono/not-yet/control_deps |  1 -
 test/mono/pass/control_deps    |  1 +
 4 files changed, 25 insertions(+), 1 deletion(-)
 delete mode 100644 test/mono/not-yet/control_deps
 create mode 100644 test/mono/pass/control_deps

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)
   ]
 
diff --git a/test/mono/not-yet/control_deps b/test/mono/not-yet/control_deps
deleted file mode 100644
index e173c42f..00000000
--- a/test/mono/not-yet/control_deps
+++ /dev/null
@@ -1 +0,0 @@
-control_deps.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/control_deps b/test/mono/pass/control_deps
new file mode 100644
index 00000000..e173c42f
--- /dev/null
+++ b/test/mono/pass/control_deps
@@ -0,0 +1 @@
+control_deps.sail -auto_mono
\ No newline at end of file
-- 
cgit v1.2.3