diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 9 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 18 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 2 |
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 |