WIP lots of stuff

3 files changed, 47 insertions, 27 deletions

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 4350c9ae..f460f73d 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -95,28 +95,19 @@ let () =
         " Forbid backward functions from updating the state" );
       ( "-template-clauses",
         Arg.Set extract_template_decreases_clauses,
-        " Generate templates for the required decreases clauses, in a\n\
-        \                         dedicated file. Reauires -decreases-clauses"
+        " Generate templates for the required decreases clauses, in a \
+          dedicated file. Implies -decreases-clauses"
       );
       ( "-no-split-files",
         Arg.Clear split_files,
-        " Don't split the definitions between different files for types,\n\
-        \                         functions, etc." );
+        " Don't split the definitions between different files for types, \
+          functions, etc." );
       ( "-no-check-inv",
         Arg.Clear check_invariants,
-        " Deactivate the invariant sanity checks performed at every step of\n\
-        \                         evaluation. Dramatically saves speed." );
+        " Deactivate the invariant sanity checks performed at every step of \
+          evaluation. Dramatically saves speed." );
     ]
   in
-  (* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
-  assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
-  (* Sanity check: -backward-no-state-update ==> not -no-state *)
-  assert ((not !backward_no_state_update) || !use_state);
-  (* Sanity check: the use of decrease clauses is not compatible with the use of fuel *)
-  assert (
-    (not !use_fuel)
-    || (not !extract_decreases_clauses)
-       && not !extract_template_decreases_clauses);
 
   let spec = Arg.align spec in
   let filenames = ref [] in
@@ -127,6 +118,19 @@ let () =
     exit 1
   in
 
+  if !extract_template_decreases_clauses then
+    extract_decreases_clauses := true;
+
+  (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
+  assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
+  (* Sanity check: -backward-no-state-update ==> -state *)
+  assert ((not !backward_no_state_update) || !use_state);
+  (* Sanity check: the use of decrease clauses is not compatible with the use of fuel *)
+  assert (
+    (not !use_fuel)
+    || (not !extract_decreases_clauses)
+       && not !extract_template_decreases_clauses);
+
   (* Check that the user specified a backend *)
   let _ =
     match !opt_backend with
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 0207d1ea..7670c753 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1992,6 +1992,11 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
   in
   List.iter extract_param def.signature.inputs
 
+let assert_backend_supports_decreases_clauses () =
+  match !backend with
+  | FStar | Lean -> ()
+  | _ -> failwith "decreases clauses only supported for the Lean & F* backends"
+
 (** Extract a decrease clause function template body.
 
     Only for F*.
@@ -2010,7 +2015,8 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
  *)
 let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_decl) : unit =
-  assert (!backend = FStar);
+  assert_backend_supports_decreases_clauses ();
+
   (* Retrieve the function name *)
   let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
   (* Add a break before *)
@@ -2022,14 +2028,16 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
    * one line *)
   F.pp_open_hvbox fmt 0;
   (* Add the [unfold] keyword *)
-  F.pp_print_string fmt "unfold";
-  F.pp_print_space fmt ();
+  if !backend = FStar then begin
+    F.pp_print_string fmt "unfold";
+    F.pp_print_space fmt ();
+  end;
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
   F.pp_open_hvbox fmt ctx.indent_incr;
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
-  F.pp_print_string fmt ("let " ^ def_name);
+  F.pp_print_string fmt ((if !backend = FStar then "let " else "def ") ^ def_name);
   F.pp_print_space fmt ();
   (* Extract the parameters *)
   let space = ref true in
@@ -2038,15 +2046,15 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_string fmt ":";
   (* Print the signature *)
   F.pp_print_space fmt ();
-  F.pp_print_string fmt "nat";
+  F.pp_print_string fmt (if !backend = FStar then "nat" else "Nat");
   (* Print the "=" *)
   F.pp_print_space fmt ();
-  F.pp_print_string fmt "=";
+  F.pp_print_string fmt (if !backend = FStar then "=" else ":=");
   (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
   F.pp_print_space fmt ();
   (* Print the "admit ()" *)
-  F.pp_print_string fmt "admit ()";
+  F.pp_print_string fmt (if !backend = FStar then "admit ()" else "sorry");
   (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
   F.pp_close_box fmt ();
   (* Close the box for the whole definition *)
@@ -2128,7 +2136,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     if is_opaque then extract_fun_input_parameters_types ctx fmt def;
     (* [Tot] *)
     if has_decreases_clause then (
-      assert (!backend = FStar);
+      assert_backend_supports_decreases_clauses ();
       F.pp_print_string fmt "Tot";
       F.pp_print_space fmt ());
     extract_ty ctx fmt has_decreases_clause def.signature.output;
@@ -2137,7 +2145,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (* Print the decrease clause - rk.: a function with a decreases clause
      * is necessarily a transparent function *)
     if has_decreases_clause then (
-      assert (!backend = FStar);
+      assert_backend_supports_decreases_clauses ();
       F.pp_print_space fmt ();
       (* Open a box for the decreases clause *)
       F.pp_open_hovbox fmt ctx.indent_incr;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index b2162b20..4ca9eff2 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -353,6 +353,9 @@ type gen_config = {
       (** If [true], extract the opaque declarations, otherwise ignore. *)
   extract_state_type : bool;
       (** If [true], generate a definition/declaration for the state type *)
+  extract_globals : bool;
+      (** If [true], generate a definition/declaration for top-level (global)
+          declarations *)
   interface : bool;
       (** [true] if we generate an interface file, [false] otherwise.
           For now, this only impacts whether we use [val] or [assume val] for the
@@ -463,8 +466,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
 
   let is_opaque = Option.is_none body.Pure.body in
   if
-    ((not is_opaque) && config.extract_transparent)
-    || (is_opaque && config.extract_opaque)
+    config.extract_globals && (
+      ((not is_opaque) && config.extract_transparent)
+      || (is_opaque && config.extract_opaque)
+    )
   then
     Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface
 
@@ -926,6 +931,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
         extract_transparent = true;
         extract_opaque = false;
         extract_state_type = false;
+        extract_globals = false;
         interface = false;
         test_trans_unit_functions = false;
       }
@@ -998,12 +1004,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       {
         base_gen_config with
         extract_fun_decls = true;
+        extract_globals = true;
         test_trans_unit_functions = !Config.test_trans_unit_functions;
       }
     in
     let clauses_module =
       if needs_clauses_module then
-        [ module_name ^ module_delimiter ^ "Clauses" ]
+        [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"]
       else []
     in
     extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
@@ -1020,6 +1027,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
         extract_transparent = true;
         extract_opaque = true;
         extract_state_type = !Config.use_state;
+        extract_globals = true;
         interface = false;
         test_trans_unit_functions = !Config.test_trans_unit_functions;
       }