Start using namespaces in the Lean backend

5 files changed, 84 insertions, 45 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index bfb9d161..f58ba89b 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -297,3 +297,10 @@ let filter_useless_monadic_calls = ref true
       dynamically check for that).
  *)
 let filter_useless_functions = ref true
+
+(** Obsolete. TODO: remove.
+
+    For Lean we used to parameterize the entire development by a section variable
+    called opaque_defs, of type OpaqueDefs.
+  *)
+let wrap_opaque_in_sig = ref false
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 7d00dd73..50215dac 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -625,13 +625,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     in
     prefix ^ tname ^ suffix
   in
-  let get_fun_name = get_name in
-  let fun_name_to_snake_case (fname : fun_name) : string =
-    let fname = get_fun_name fname in
-    (* Converting to snake case should be a no-op, but it doesn't cost much *)
-    let fname = List.map to_snake_case fname in
-    (* Concatenate the elements *)
-    String.concat "_" fname
+  let get_fun_name fname =
+    let fname = get_name fname in
+    (* TODO: don't convert to snake case for Coq, HOL4, F* *)
+    match !backend with
+    | FStar | Coq | HOL4 -> String.concat "_" (List.map to_snake_case fname)
+    | Lean -> String.concat "." fname
   in
   let global_name (name : global_name) : string =
     (* Converting to snake case also lowercases the letters (in Rust, global
@@ -642,7 +641,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option)
       (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int)
       : string =
-    let fname = fun_name_to_snake_case fname in
+    let fname = get_fun_name fname in
     (* Compute the suffix *)
     let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
     (* Concatenate *)
@@ -651,7 +650,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
 
   let termination_measure_name (_fid : A.FunDeclId.id) (fname : fun_name)
       (num_loops : int) (loop_id : LoopId.id option) : string =
-    let fname = fun_name_to_snake_case fname in
+    let fname = get_fun_name fname in
     let lp_suffix = default_fun_loop_suffix num_loops loop_id in
     (* Compute the suffix *)
     let suffix =
@@ -666,7 +665,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
 
   let decreases_proof_name (_fid : A.FunDeclId.id) (fname : fun_name)
       (num_loops : int) (loop_id : LoopId.id option) : string =
-    let fname = fun_name_to_snake_case fname in
+    let fname = get_fun_name fname in
     let lp_suffix = default_fun_loop_suffix num_loops loop_id in
     (* Compute the suffix *)
     let suffix =
@@ -681,7 +680,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   let opaque_pre () =
     match !Config.backend with
     | FStar | Coq | HOL4 -> ""
-    | Lean -> "opaque_defs."
+    | Lean -> if !Config.wrap_opaque_in_sig then "opaque_defs." else ""
   in
 
   let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
@@ -2981,8 +2980,11 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   let use_forall = is_opaque_coq && def.signature.type_params <> [] in
   (* Print the qualifier ("assume", etc.).
 
-     For Lean: we generate a record of assumed functions *)
-  (if not (!backend = Lean && (kind = Assumed || kind = Declared)) then
+     if `wrap_opaque_in_sig`: we generate a record of assumed funcions.
+     TODO: this is obsolete.
+  *)
+  (if not (!Config.wrap_opaque_in_sig && (kind = Assumed || kind = Declared))
+   then
      let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
      match qualif with
      | Some qualif ->
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 14ce4119..feab7706 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -240,7 +240,9 @@ type formatter = {
           - loop identifier, if this is for a loop
        *)
   opaque_pre : unit -> string;
-      (** The prefix to use for opaque definitions.
+      (** TODO: obsolete, remove.
+
+          The prefix to use for opaque definitions.
 
           We need this because for some backends like Lean and Coq, we group
           opaque definitions in module signatures, meaning that using those
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 4a00dfb2..b251a005 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -18,16 +18,19 @@ module GlobalDeclId = A.GlobalDeclId
     (they monotonically increase across functions) while in {!module:Pure} we want
     the indices to start at 0 for every function.
  *)
-module LoopId = IdGen ()
+module LoopId =
+IdGen ()
 
 type loop_id = LoopId.id [@@deriving show, ord]
 
 (** We give an identifier to every phase of the synthesis (forward, backward
     for group of regions 0, etc.) *)
-module SynthPhaseId = IdGen ()
+module SynthPhaseId =
+IdGen ()
 
 (** Pay attention to the fact that we also define a {!E.VarId} module in Values *)
-module VarId = IdGen ()
+module VarId =
+IdGen ()
 
 type integer_type = T.integer_type [@@deriving show, ord]
 
@@ -723,6 +726,7 @@ type fun_sig_info = {
  *)
 type fun_sig = {
   type_params : type_var list;
+      (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *)
   inputs : ty list;
       (** The input types.
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 5827b4a8..795674b4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -750,18 +750,17 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   if config.extract_state_type && config.extract_fun_decls then
     export_state_type ();
 
-  (* For Lean, we parameterize the entire development by a section variable
-     called opaque_defs, of type OpaqueDefs. The code below emits the type
-     definition for OpaqueDefs, which is a structure, in which each field is one
-     of the functions marked as Opaque. We emit the `structure ...` bit here,
-     then rely on `extract_fun_decl` to be aware of this, and skip the keyword
-     (e.g. "axiom" or "val") so as to generate valid syntax for records.
-
-     We also generate such a structure only if there actually are opaque
-     definitions.
-  *)
+  (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section
+     variable called opaque_defs, of type OpaqueDefs. The code below emits the type
+     definition for OpaqueDefs, which is a structure, in which each field is one of the
+     functions marked as Opaque. We emit the `structure ...` bit here, then rely on
+     `extract_fun_decl` to be aware of this, and skip the keyword (e.g. "axiom" or "val")
+     so as to generate valid syntax for records.
+
+     We also generate such a structure only if there actually are opaque definitions. *)
   let wrap_in_sig =
-    config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean
+    config.extract_opaque && config.extract_fun_decls
+    && !Config.wrap_opaque_in_sig
     &&
     let _, opaque_funs = module_has_opaque_decls ctx in
     opaque_funs
@@ -785,6 +784,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
 
 type extract_file_info = {
   filename : string;
+  namespace : string;
+  in_namespace : bool;
   crate_name : string;
   rust_module_name : string;
   module_name : string;
@@ -852,9 +853,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       (* Add the custom includes *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
       (* Always open the Primitives namespace *)
-      Printf.fprintf out "open Primitives\n\n";
-      (* Open the namespace *)
-      Printf.fprintf out "namespace %s\n" fi.crate_name
+      Printf.fprintf out "open Primitives\n";
+      (* If we are inside the namespace: declare it, otherwise: open it *)
+      if fi.in_namespace then Printf.fprintf out "namespace %s\n" fi.namespace
+      else Printf.fprintf out "open %s\n" fi.namespace
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
       (* Add the custom imports and includes *)
@@ -884,7 +886,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   (* Close the module *)
   (match !Config.backend with
   | FStar -> ()
-  | Lean -> Printf.fprintf out "end %s\n" fi.crate_name
+  | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
   | Coq -> Printf.fprintf out "End %s .\n" fi.module_name);
 
@@ -986,7 +988,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   (* Open the output file *)
   (* First compute the filename by replacing the extension and converting the
    * case (rust module names are snake case) *)
-  let crate_name, extract_filebasename =
+  let namespace, crate_name, extract_filebasename =
     match Filename.chop_suffix_opt ~suffix:".llbc" filename with
     | None ->
         (* Note that we already checked the suffix upon opening the file *)
@@ -1001,8 +1003,14 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
             StringUtils.lowercase_first_letter crate_name
           else crate_name
         in
+        (* We use the raw crate name for the namespaces *)
+        let namespace =
+          match !Config.backend with
+          | FStar | Coq | HOL4 -> crate.name
+          | Lean -> crate.name
+        in
         (* Concatenate *)
-        (crate_name, Filename.concat dest_dir crate_name)
+        (namespace, crate_name, Filename.concat dest_dir crate_name)
   in
 
   (* Put the translated definitions in maps *)
@@ -1134,6 +1142,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
      (* Extract the types *)
      (* If there are opaque types, we extract in an interface *)
+     (* TODO: for Lean and Coq: generate a template file *)
      let types_filename_ext =
        match !Config.backend with
        | FStar -> if has_opaque_types then ".fsti" else ".fst"
@@ -1157,6 +1166,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
      let file_info =
        {
          filename = types_filename;
+         namespace;
+         in_namespace = true;
          crate_name;
          rust_module_name = crate.A.name;
          module_name = types_module;
@@ -1183,6 +1194,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         let file_info =
           {
             filename = template_clauses_filename;
+            namespace;
+            in_namespace = true;
             crate_name;
             rust_module_name = crate.A.name;
             module_name = template_clauses_module;
@@ -1196,20 +1209,25 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
      (* Extract the opaque functions, if needed *)
      let opaque_funs_module =
        if has_opaque_funs then (
+         (* In the case of Lean we generate a template file *)
+         let module_suffix, opaque_imported_suffix, custom_msg =
+           match !Config.backend with
+           | FStar | Coq | HOL4 ->
+               ("Opaque", "Opaque", ": external function declarations")
+           | Lean ->
+               ( "FunsExternal_Template",
+                 "FunsExternal",
+                 ": external functions.\n\
+                  -- This is a template file: rename it to \
+                  \"FunsExternal.lean\" and fill the holes." )
+         in
          let opaque_filename =
-           extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
+           extract_filebasename ^ file_delimiter ^ module_suffix ^ opaque_ext
          in
-         let opaque_module = crate_name ^ module_delimiter ^ "Opaque" in
+         let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
          let opaque_imported_module =
-           (* In the case of Lean, we declare an interface (a record) containing
-              the opaque definitions, and we leave it to the user to provide an
-              instance of this module.
-
-              TODO: do the same for Coq.
-              TODO: do the same for the type definitions.
-           *)
            if !Config.backend = Lean then
-             crate_name ^ module_delimiter ^ "ExternalFuns"
+             crate_name ^ module_delimiter ^ opaque_imported_suffix
            else opaque_module
          in
          let opaque_config =
@@ -1230,10 +1248,12 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          let file_info =
            {
              filename = opaque_filename;
+             namespace;
+             in_namespace = false;
              crate_name;
              rust_module_name = crate.A.name;
              module_name = opaque_module;
-             custom_msg = ": opaque function definitions";
+             custom_msg;
              custom_imports = [];
              custom_includes = [ types_module ];
            }
@@ -1266,6 +1286,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
      let file_info =
        {
          filename = fun_filename;
+         namespace;
+         in_namespace = true;
          crate_name;
          rust_module_name = crate.A.name;
          module_name = fun_module;
@@ -1295,6 +1317,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
      let file_info =
        {
          filename = extract_filebasename ^ ext;
+         namespace;
+         in_namespace = true;
          crate_name;
          rust_module_name = crate.A.name;
          module_name = crate_name;