New directory structure and corresponding extraction, + misc fixes, for Lean

3 files changed, 49 insertions, 38 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 9496fcf9..af510a84 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -175,8 +175,8 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | Lean ->
       [
-        (Result, result_return_id, "ret");
-        (Result, result_fail_id, "fail_"); (* TODO: why the _ *)
+        (Result, result_return_id, "result.ret");
+        (Result, result_fail_id, "result.fail");
         (Error, error_failure_id, "panic");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
@@ -218,7 +218,7 @@ let assumed_pure_functions : (pure_assumed_fun_id * string) list =
   | Lean ->
       [
         (Return, "return");
-        (Fail, "fail_");
+        (Fail, "fail");
         (Assert, "massert");
         (* TODO: figure out how to deal with this *)
         (FuelDecrease, "decrease");
@@ -296,7 +296,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
   if inside then F.pp_print_string fmt ")"
 
 let type_decl_kind_to_qualif (kind : decl_kind)
-    (type_kind : type_decl_kind option) (is_rec: bool): string =
+    (type_kind : type_decl_kind option): string =
   match !backend with
   | FStar -> (
       match kind with
@@ -321,8 +321,7 @@ let type_decl_kind_to_qualif (kind : decl_kind)
       | _ -> raise (Failure "Unexpected"))
   | Lean -> (
       match kind with
-      | SingleNonRec ->
-          if type_kind = Some Struct && not is_rec then "structure" else "inductive"
+      | SingleNonRec -> if type_kind = Some Struct then "structure" else "inductive"
       | SingleRec -> "inductive"
       | MutRecFirst -> "mutual inductive"
       | MutRecInner -> "inductive"
@@ -640,7 +639,8 @@ let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
     F.pp_print_cut fmt ();
     F.pp_print_string fmt ".")
 
-let unit_name = match !backend with | Lean -> "Unit" | Coq | FStar -> "unit"
+let unit_name () =
+  match !backend with | Lean -> "Unit" | Coq | FStar -> "unit"
 
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
@@ -653,7 +653,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       | Tuple ->
           (* This is a bit annoying, but in F*/Coq [()] is not the unit type:
            * we have to write [unit]... *)
-          if tys = [] then F.pp_print_string fmt unit_name
+          if tys = [] then F.pp_print_string fmt (unit_name ())
           else (
             F.pp_print_string fmt "(";
             Collections.List.iter_link
@@ -882,7 +882,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
   let _ =
     if !backend = FStar && fields = [] then (
       F.pp_print_space fmt ();
-      F.pp_print_string fmt unit_name)
+      F.pp_print_string fmt (unit_name ()))
     else if (not is_rec) || !backend = FStar then (
       F.pp_print_space fmt ();
       (* If Coq: print the constructor name *)
@@ -983,8 +983,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "type TYPE_NAME" *)
-  let is_rec = decl_is_from_rec_group kind in
-  let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind is_rec in
+  let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   (* Print the type parameters *)
   let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in
@@ -1011,7 +1010,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
     let eq = match !backend with
       | FStar -> "="
       | Coq -> ":="
-      | Lean -> if type_kind = Some Struct && not is_rec then "where" else ":="
+      | Lean -> if type_kind = Some Struct && kind = SingleNonRec then "where" else ":="
     in
     F.pp_print_string fmt eq)
   else (
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index c8094128..3ad55d37 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -118,7 +118,7 @@ type formatter = {
   char_name : string;
   int_name : integer_type -> string;
   str_name : string;
-  type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> bool -> string;
+  type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string;
       (** Compute the qualified for a type definition/declaration.
     
           For instance: "type", "and", etc.
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6b3d00f3..b2162b20 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -708,7 +708,7 @@ 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 Primitives\nopen result\n\n";
+      Printf.fprintf out "import Base.Primitives\n";
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
       (* Add the custom includes *)
@@ -845,11 +845,30 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
          trans_funs)
   in
 
+  let mkdir_if dest_dir =
+    if not (Sys.file_exists dest_dir) then (
+      log#linfo (lazy ("Creating missing directory: " ^ dest_dir));
+      (* Create a directory with *default* permissions *)
+      Core_unix.mkdir_p dest_dir)
+  in
+
   (* Create the directory, if necessary *)
-  if not (Sys.file_exists dest_dir) then (
-    log#linfo (lazy ("Creating missing directory: " ^ dest_dir));
-    (* Create a directory with *default* permissions *)
-    Core_unix.mkdir_p dest_dir);
+  mkdir_if dest_dir;
+
+  let needs_clauses_module =
+    !Config.extract_decreases_clauses
+    && not (PureUtils.FunLoopIdSet.is_empty rec_functions)
+  in
+
+  (* Lean reflects the module hierarchy within the filesystem, so we need to
+     create more directories *)
+  if !Config.backend = Lean then begin
+    let (^^) = Filename.concat in
+    mkdir_if (dest_dir ^^ "Base");
+    mkdir_if (dest_dir ^^ module_name);
+    if needs_clauses_module then
+      mkdir_if (dest_dir ^^ module_name ^^ "Clauses");
+  end;
 
   (* Copy the "Primitives" file *)
   let _ =
@@ -859,7 +878,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       match !Config.backend with
       | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst")
       | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v")
-      | Config.Lean -> ("/backends/lean/Primitives.lean", "Primitives.lean")
+      | Config.Lean -> ("/backends/lean/Primitives.lean", "Base/Primitives.lean")
     in
     let src = open_in (exe_dir ^ primitives_src) in
     let tgt_filename = Filename.concat dest_dir primitives_destname in
@@ -889,7 +908,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
   in
 
   let module_delimiter =
-    match !Config.backend with FStar | Lean -> "." | Coq -> "_"
+    match !Config.backend with FStar -> "." | Coq -> "_" | Lean -> "."
+  in
+  let file_delimiter =
+    if !Config.backend = Lean then "/" else module_delimiter
   in
   let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in
 
@@ -922,11 +944,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       | Coq -> ".v"
       | Lean -> ".lean"
     in
-    let types_file_suffix = module_delimiter ^ "Types" in
     let types_filename =
-      extract_filebasename ^ types_file_suffix ^ types_filename_ext
+      extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
     in
-    let types_module = module_name ^ types_file_suffix in
+    let types_module = module_name ^ module_delimiter ^ "Types" in
     let types_config =
       {
         base_gen_config with
@@ -940,16 +961,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       ": type definitions" [] [];
 
     (* Extract the template clauses *)
-    let needs_clauses_module =
-      !Config.extract_decreases_clauses
-      && not (PureUtils.FunLoopIdSet.is_empty rec_functions)
-    in
     if needs_clauses_module && !Config.extract_template_decreases_clauses then (
-      let clauses_file_suffix =
-        module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"
-      in
-      let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in
-      let clauses_module = module_name ^ clauses_file_suffix in
+      let clauses_filename = extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter ^ "Template" ^ ext in
+      let clauses_module = module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" in
       let clauses_config =
         { base_gen_config with extract_template_decreases_clauses = true }
       in
@@ -960,9 +974,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     (* Extract the opaque functions, if needed *)
     let opaque_funs_module =
       if has_opaque_funs then (
-        let opaque_file_suffix = module_delimiter ^ "Opaque" in
-        let opaque_filename = extract_filebasename ^ opaque_file_suffix ^ ext in
-        let opaque_module = module_name ^ opaque_file_suffix in
+        let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ ext in
+        let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
         let opaque_config =
           {
             base_gen_config with
@@ -979,9 +992,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     in
 
     (* Extract the functions *)
-    let fun_file_suffix = module_delimiter ^ "Funs" in
-    let fun_filename = extract_filebasename ^ fun_file_suffix ^ ext in
-    let fun_module = module_name ^ fun_file_suffix in
+    let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in
+    let fun_module = module_name ^ module_delimiter ^ "Funs" in
     let fun_config =
       {
         base_gen_config with