added the preliminary lem output option that for now uses ocaml pp

5 files changed, 54 insertions, 10 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 2b6ef616..5b6c8ee5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -48,6 +48,7 @@ open Type_internal
 
 type out_type =
   | Lem_ast_out
+  | Lem_out of string option
   | Ocaml_out of string option
 
 (* let r = Ulib.Text.of_latin1 *)
@@ -102,6 +103,7 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs 
 
 let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
+let rewrite_ast_lem (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs
 let rewrite_ast_ocaml (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs
 
 let open_output_with_check file_name =
@@ -170,6 +172,15 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
 	  Pretty_print.pp_lem_defs o defs;
 	  close_output_with_check ext_o
 	end
+      | Lem_out None ->
+        let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in
+	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"];
+        close_output_with_check ext_o
+        end
+      | Lem_out (Some lib) ->
+        let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in
+	Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"; lib];
+        close_output_with_check ext_o
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
 	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"];
diff --git a/src/process_file.mli b/src/process_file.mli
index 232727f1..38ac057f 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -48,10 +48,12 @@ val parse_file : string -> Parse_ast.defs
 val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
 val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs
 val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
+val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 
 type out_type =
   | Lem_ast_out
+  | Lem_out of string option (* If present, the string is a file to open in the lem backend*)
   | Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*)
 
 val output :
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 3df257aa..402f8208 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -499,6 +499,7 @@ and fold_letbind_aux alg = function
 and fold_letbind alg (LB_aux (letbind_aux,annot)) = alg.lB_aux (fold_letbind_aux alg letbind_aux, annot)
 
 
+let remove_vector_concat_pat_counter = ref 0
 let remove_vector_concat_pat pat =
   (* ivc: bool that indicates whether the exp is in a vector_concat pattern *)
   let remove_tannot_in_vector_concats = 
@@ -528,10 +529,9 @@ let remove_vector_concat_pat pat =
 
   let pat = (fold_pat remove_tannot_in_vector_concats pat) false in
 
-  let counter = ref 0 in
   let fresh_name () =
-    let current = !counter in
-    let () = counter := (current + 1) in
+    let current = !remove_vector_concat_pat_counter in
+    let () = remove_vector_concat_pat_counter := (current + 1) in
     Id_aux (Id ("__v" ^ string_of_int current), Parse_ast.Unknown) in
   
   (* expects that P_typ elements have been removed from AST,
@@ -799,14 +799,14 @@ let rewrite_defs_ocaml defs =
   defs_lifted_assign
 
 
-let normalise_exp exp =
+let sequentialise_effects_counter = ref 0
+let sequentialise_effects exp =
 
   let compose f g x = f (g x) in
 
-  let counter = ref 0 in
   let fresh_name () =
-    let current = !counter in
-    let () = counter := (current + 1) in
+    let current = !sequentialise_effects_counter in
+    let () = sequentialise_effects_counter := (current + 1) in
     Id_aux (Id ("__w" ^ string_of_int current), Parse_ast.Unknown) in
   
   let aux (((E_aux (_,annot)) as e,b) : ('a exp * bool)) : (('a exp -> 'a exp) * 'a exp * bool) =
@@ -834,7 +834,8 @@ let normalise_exp exp =
        (compose acc_decl decl, acc_es @ [e], acc_b || b))
       ((fun x -> x), [], false) es in
             
-  (* for each expression e: return a tuple (normalised e, does e contain effectful terms) *)
+  (* for each expression e: return a tuple (e',b) where e' is e rewritten, 
+     b indicates whether e contains effectful terms) *)
   fold_exp 
     { e_block =
         (fun es ->
@@ -1038,3 +1039,18 @@ let normalise_exp exp =
     ; lB_aux = (fun ((lb,b),a) -> (LB_aux (lb,a),b))
     ; pat_alg = id_pat_alg
     } exp
+
+let rewrite_defs_sequentialise_effects (Defs defs) = rewrite_defs_base
+  {rewrite_exp = (fun _ _ exp -> fst (sequentialise_effects exp));
+   rewrite_pat = rewrite_pat;
+   rewrite_let = rewrite_let;
+   rewrite_lexp = rewrite_lexp;
+   rewrite_fun = rewrite_fun;
+   rewrite_def = rewrite_def;
+   rewrite_defs = rewrite_defs_base} (Defs defs)
+
+let rewrite_defs_lem defs =
+  let defs = rewrite_defs_remove_vector_concat defs in
+  let defs = rewrite_defs_exp_lift_assign defs in
+  let defs = rewrite_defs_sequentialise_effects defs in
+  defs
diff --git a/src/rewriter.mli b/src/rewriter.mli
index dfde1d76..c258a342 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -18,6 +18,7 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> nexp_map option -> 'a exp ->
 val rewrite_exp : tannot rewriters -> nexp_map option -> tannot exp -> tannot exp
 val rewrite_defs : tannot defs -> tannot defs
 val rewrite_defs_ocaml : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
+val rewrite_defs_lem : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*)
 
 (* the type of interpretations of pattern-matching expressions *)
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
diff --git a/src/sail.ml b/src/sail.ml
index 0fa383ef..d91d229b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -49,8 +49,10 @@ open Process_file
 let lib = ref []
 let opt_print_version = ref false
 let opt_print_verbose = ref false
+let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
 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 options = Arg.align ([
@@ -61,14 +63,20 @@ let options = Arg.align ([
     Arg.Unit (fun b -> opt_print_verbose := true),
     " pretty-print out the file");
   ( "-lem_ast",
-    Arg.Unit (fun b -> opt_print_lem := true),
+    Arg.Unit (fun b -> opt_print_lem_ast := true),
     " pretty-print a Lem AST representation of the file");
+  ( "-lem",
+    Arg.Unit (fun b -> opt_print_lem := true),
+    " print a Lem translated version of the specification");
   ( "-ocaml",
     Arg.Unit (fun b -> opt_print_ocaml := true),
     " print an Ocaml translated version of the specification");
   ( "-skip_constraints",
     Arg.Clear Type_internal.do_resolve_constraints,
     " skip constraint resolution in type-checking");
+  ( "-lem_lib",
+    Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
+    " provide additional library to open in Lem output");
   ( "-ocaml_lib",
     Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
     " provide additional library to open in Ocaml output");
@@ -104,7 +112,7 @@ let main() =
       (if !(opt_print_verbose)
        then ((Pretty_print.pp_defs stdout) ast)
        else ());
-      (if !(opt_print_lem)
+      (if !(opt_print_lem_ast)
        then output "" Lem_ast_out [(fst (List.hd parsed)),ast]
        else ());
       (if !(opt_print_ocaml)
@@ -113,6 +121,12 @@ let main() =
          then output "" (Ocaml_out None) [(fst (List.hd parsed)),ast_ocaml]
          else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [(fst (List.hd parsed)),ast_ocaml]
        else ());
+      (if !(opt_print_lem)
+       then let ast_lem = rewrite_ast_lem ast in
+         if !(opt_libs_lem) = []
+         then output "" (Lem_out None) [(fst (List.hd parsed)),ast_lem]
+         else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [(fst (List.hd parsed)),ast_lem]
+       else ())
     end
 
 let _ =  try