Reorganize the Lean tests

5 files changed, 62 insertions, 43 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index ce9b0e0c..bfb9d161 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -162,6 +162,11 @@ let backward_no_state_update = ref false
  *)
 let split_files = ref true
 
+(** For Lean, controls whether we generate a lakefile or not.
+
+ *)
+let lean_gen_lakefile = ref false
+
 (** If true, treat the unit functions (function taking no inputs and returning
     no outputs) as unit tests: evaluate them with the interpreter and check that
     they don't panic.
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 2ff9e295..f935a717 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -107,6 +107,9 @@ let () =
         Arg.Clear check_invariants,
         " Deactivate the invariant sanity checks performed at every evaluation \
          step. Dramatically increases speed." );
+      ( "-lean-default-lakefile",
+        Arg.Clear lean_gen_lakefile,
+        " Generate a default lakefile.lean (Lean only)" );
     ]
   in
 
@@ -130,6 +133,9 @@ let () =
     (not !use_fuel)
     || (not !extract_decreases_clauses)
        && not !extract_template_decreases_clauses);
+  if !lean_gen_lakefile && not (!backend = Lean) then
+    log#error
+      "The -lean-default-lakefile option is valid only for the Lean backend";
 
   (* Check that the user specified a backend *)
   let _ =
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index d624d9ca..a54a2299 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -505,10 +505,10 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
   | Lean -> (
       match kind with
       | SingleNonRec -> Some "def"
-      | SingleRec -> Some "def"
-      | MutRecFirst -> Some "mutual def"
-      | MutRecInner -> Some "def"
-      | MutRecLast -> Some "def"
+      | SingleRec -> Some "divergent def"
+      | MutRecFirst -> Some "mutual divergent def"
+      | MutRecInner -> Some "divergent def"
+      | MutRecLast -> Some "divergent def"
       | Assumed -> Some "axiom"
       | Declared -> Some "axiom")
   | HOL4 -> None
@@ -2327,9 +2327,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           match !backend with
           | FStar -> "="
           | Coq -> ":="
-          | Lean ->
-              (* TODO: switch to ⟵ once issues are fixed *)
-              if monadic then "←" else ":="
+          | Lean -> if monadic then "←" else ":="
           | HOL4 -> if monadic then "<-" else "="
         in
         F.pp_print_string fmt eq;
@@ -2409,7 +2407,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
       (* Open a box for the [if e] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       F.pp_print_string fmt "if";
-      if !backend = Lean then F.pp_print_string fmt " h:";
+      if !backend = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
       F.pp_print_space fmt ();
       let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 0a5d7df2..14ce4119 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -539,6 +539,16 @@ type extraction_ctx = {
           use it.
           Also see {!names_map.opaque_ids}.
        *)
+  use_dep_ite : bool;
+      (** For Lean: do we use dependent-if then else expressions?
+
+          Example:
+          {[
+            if h: b then ... else ...
+            -- ^^
+            -- makes the if then else dependent
+          ]}
+        *)
 }
 
 (** Debugging function, used when communicating name collisions to the user,
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 75fc7fe9..39b169c9 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -834,11 +834,13 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
         custom_includes;
       Printf.fprintf out "Module %s.\n" module_name
   | Lean ->
-      Printf.fprintf out "import Base.Primitives\n";
+      Printf.fprintf out "import Base\n";
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
       (* Add the custom includes *)
-      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes
+      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes;
+      (* Always open the Primitives namespace *)
+      Printf.fprintf out "open Primitives\n"
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
       (* Add the custom imports and includes *)
@@ -903,6 +905,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       fmt;
       indent_incr = 2;
       use_opaque_pre = !Config.split_files;
+      use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
     }
   in
 
@@ -1019,7 +1022,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
      create more directories *)
   if !Config.backend = Lean then (
     let ( ^^ ) = Filename.concat in
-    mkdir_if (dest_dir ^^ "Base");
     if !Config.split_files then mkdir_if (dest_dir ^^ module_name);
     if needs_clauses_module then (
       assert !Config.split_files;
@@ -1033,7 +1035,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       match !Config.backend with
       | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
-      | Lean -> Some ("/backends/lean/Primitives.lean", "Base/Primitives.lean")
+      | Lean -> None
       | HOL4 -> None
     in
     match primitives_src_dest with
@@ -1265,38 +1267,36 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         log#linfo (lazy ("Generated: " ^ filename)));
 
       (*
-       * Generate the lakefile.lean file
+       * Generate the lakefile.lean file, if the user asks for it
        *)
+      if !Config.lean_gen_lakefile then (
+        (* Open the file *)
+        let filename = Filename.concat dest_dir "lakefile.lean" in
+        let out = open_out filename in
 
-      (* Open the file *)
-      let filename = Filename.concat dest_dir "lakefile.lean" in
-      let out = open_out filename in
-
-      (* Generate the content *)
-      Printf.fprintf out "import Lake\nopen Lake DSL\n\n";
-      Printf.fprintf out "require mathlib from git\n";
-      Printf.fprintf out
-        "  \"https://github.com/leanprover-community/mathlib4.git\"\n\n";
-
-      let package_name = StringUtils.to_snake_case module_name in
-      Printf.fprintf out "package «%s» {}\n\n" package_name;
-
-      Printf.fprintf out "lean_lib «Base» {}\n\n";
-
-      Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" module_name;
-
-      (* No default target for now.
-         Format would be:
-         {[
-           @[default_target]
-           lean_exe «package_name» {
-             root := `Main
-           }
-         ]}
-      *)
+        (* Generate the content *)
+        Printf.fprintf out "import Lake\nopen Lake DSL\n\n";
+        Printf.fprintf out "require mathlib from git\n";
+        Printf.fprintf out
+          "  \"https://github.com/leanprover-community/mathlib4.git\"\n\n";
+
+        let package_name = StringUtils.to_snake_case module_name in
+        Printf.fprintf out "package «%s» {}\n\n" package_name;
+
+        Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" module_name;
+
+        (* No default target for now.
+           Format would be:
+           {[
+             @[default_target]
+               lean_exe «package_name» {
+               root := `Main
+             }
+           ]}
+        *)
 
-      (* Flush and close the file *)
-      close_out out;
+        (* Flush and close the file *)
+        close_out out;
 
-      (* Logging *)
-      log#linfo (lazy ("Generated: " ^ filename))
+        (* Logging *)
+        log#linfo (lazy ("Generated: " ^ filename)))