All of the generated code is syntactically correct

4 files changed, 22 insertions, 11 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index e1b2b23f..24f8d141 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -476,10 +476,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   in
   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)
-      (missing_body: bool)
       : string =
     let fname = fun_name_to_snake_case fname in
-    let fname = if !backend = Lean && missing_body then "opaque_defs." ^ fname else fname in
     (* Compute the suffix *)
     let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
     (* Concatenate *)
@@ -1581,7 +1579,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
       (* Open a box for the function call *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* Print the function name *)
-      let fun_name = ctx_get_function fun_id ctx in
+      let fun_name = Option.value
+        ~default:(ctx_get_function fun_id ctx)
+        (ctx_maybe_get (DeclaredId fun_id) ctx)
+      in
       F.pp_print_string fmt fun_name;
       (* Print the type parameters *)
       List.iter
@@ -2612,7 +2613,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "=";
         F.pp_print_space fmt ();
         let success = ctx_get_variant (Assumed Result) result_return_id ctx in
-        F.pp_print_string fmt (success ^ " ())")
+        F.pp_print_string fmt ("." ^ success ^ " ())")
     );
     (* Close the box for the test *)
     F.pp_close_box fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 98a29daf..4c4a9959 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -168,7 +168,6 @@ type formatter = {
     int ->
     region_group_info option ->
     bool * int ->
-    bool ->
     string;
       (** Compute the name of a regular (non-assumed) function.
 
@@ -188,7 +187,6 @@ type formatter = {
               The number of extracted backward functions if not necessarily
               equal to the number of region groups, because we may have
               filtered some of them.
-          - whether there is a body or not (indicates assumed function)
           TODO: use the fun id for the assumed functions.
        *)
   decreases_clause_name :
@@ -296,6 +294,7 @@ type formatter = {
 type id =
   | GlobalId of A.GlobalDeclId.id
   | FunId of fun_id
+  | DeclaredId of fun_id
   | DecreasesClauseId of (A.fun_id * LoopId.id option)
       (** The definition which provides the decreases/termination clause.
           We insert calls to this clause to prove/reason about termination:
@@ -472,6 +471,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | GlobalId gid ->
       let name = (A.GlobalDeclId.Map.find gid global_decls).name in
       "global name: " ^ Print.global_name_to_string name
+  | DeclaredId fid
   | FunId fid -> (
       match fid with
       | FromLlbc (fid, lp_id, rg_id) ->
@@ -584,8 +584,11 @@ let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
   let names_map = names_map_add id_to_string id name ctx.names_map in
   { ctx with names_map }
 
+let ctx_maybe_get (id : id) (ctx : extraction_ctx) : string option =
+  IdMap.find_opt id ctx.names_map.id_to_name
+
 let ctx_get (id : id) (ctx : extraction_ctx) : string =
-  match IdMap.find_opt id ctx.names_map.id_to_name with
+  match ctx_maybe_get id ctx with
   | Some s -> s
   | None ->
       log#serror ("Could not find: " ^ id_to_string id ctx);
@@ -776,7 +779,14 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   in
   let name =
     ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
-      (keep_fwd, num_backs) (def.body = None)
+      (keep_fwd, num_backs)
+  in
+  let ctx = if def.body = None && !Config.backend = Lean then
+    ctx_add
+      (DeclaredId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
+      ("opaque_defs." ^ name) ctx
+  else
+    ctx
   in
   ctx_add
     (FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index ffe3416a..b0c4d683 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -5,7 +5,7 @@ import HashmapMain.Types
 import HashmapMain.Opaque
 import HashmapMain.Clauses.Template
 
-section variable (opaque_defs: OpaqueDecls)
+section variable (opaque_defs: OpaqueDefs)
 
 /- [hashmap_main::hashmap::hash_key] -/
 def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k
@@ -654,5 +654,5 @@ def insert_on_disk_fwd
 def main_fwd : result Unit := result.ret ()
 
 /- Unit test for [hashmap_main::main] -/
-#assert (main_fwd = ret ())
+#assert (main_fwd = .ret ())
 
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
index 8b41934d..ce618a6c 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
@@ -3,7 +3,7 @@
 import Base.Primitives
 import HashmapMain.Types
 
-structure OpaqueDecls where
+structure OpaqueDefs where
   
   /- [hashmap_main::hashmap_utils::deserialize] -/
   hashmap_utils_deserialize_fwd