summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml7
-rw-r--r--compiler/Extract.ml167
-rw-r--r--compiler/ExtractBase.ml233
-rw-r--r--compiler/Translate.ml34
4 files changed, 111 insertions, 330 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 62f6c300..cd0903b6 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -306,13 +306,6 @@ let filter_useless_monadic_calls = ref true
*)
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
-
(** Use short names for the record fields.
Some backends can't disambiguate records when their field names have collisions.
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a1c9605b..275cb3b9 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -758,12 +758,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
fname ^ lp_suffix ^ suffix
in
- let opaque_pre () =
- match !Config.backend with
- | FStar | Coq | HOL4 -> ""
- | Lean -> if !Config.wrap_opaque_in_sig then "opaque_defs." else ""
- in
-
let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
: string =
(* Small helper to derive var names from ADT type names.
@@ -934,7 +928,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
trait_type_name;
trait_method_name;
trait_type_clause_name;
- opaque_pre;
var_basename;
type_var_basename;
const_generic_var_basename;
@@ -983,11 +976,8 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(* In HOL4, opaque functions have a special treatment *)
if is_single_opaque_fun_decl_group dg then ()
else
- let with_opaque_pre = false in
let compute_fun_def_name (def : Pure.fun_decl) : string =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
- ^ "_def"
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx ^ "_def"
in
let names = List.map compute_fun_def_name dg in
(* Add a break before *)
@@ -1110,7 +1100,7 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
(inside : bool) (cg : const_generic) : unit =
match cg with
| ConstGenericGlobal id ->
- let s = ctx_get_global ctx.use_opaque_pre id ctx in
+ let s = ctx_get_global id ctx in
F.pp_print_string fmt s
| ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v
| ConstGenericVar id ->
@@ -1178,14 +1168,13 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
In HOL4 we would write:
`('a, 'b) tree`
*)
- let with_opaque_pre = false in
match !backend with
| FStar | Coq | Lean ->
let print_paren = inside && has_params in
if print_paren then F.pp_print_string fmt "(";
(* TODO: for now, only the opaque *functions* are extracted in the
opaque module. The opaque *types* are assumed. *)
- F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+ F.pp_print_string fmt (ctx_get_type type_id ctx);
extract_generic_args ctx fmt no_params_tys generics;
if print_paren then F.pp_print_string fmt ")"
| HOL4 ->
@@ -1208,7 +1197,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
(extract_rec true) types;
if print_paren then F.pp_print_string fmt ")";
F.pp_print_space fmt ());
- F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+ F.pp_print_string fmt (ctx_get_type type_id ctx);
if trait_refs <> [] then (
F.pp_print_space fmt ();
Collections.List.iter_link (F.pp_print_space fmt)
@@ -1273,8 +1262,7 @@ and extract_trait_decl_ref (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) :
unit =
let use_brackets = tr.decl_generics <> empty_generic_args && inside in
- let is_opaque = false in
- let name = ctx_get_trait_decl is_opaque tr.trait_decl_id ctx in
+ let name = ctx_get_trait_decl tr.trait_decl_id ctx in
if use_brackets then F.pp_print_string fmt "(";
F.pp_print_string fmt name;
(* There is something subtle here: the trait obligations for the implemented
@@ -1307,14 +1295,13 @@ and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter)
and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id)
: unit =
- let with_opaque_pre = false in
match id with
| Self ->
(* This has specific treatment depending on the item we're extracting
(associated type, etc.). We should have caught this elsewhere. *)
raise (Failure "Unexpected")
| TraitImpl id ->
- let name = ctx_get_trait_impl with_opaque_pre id ctx in
+ let name = ctx_get_trait_impl id ctx in
F.pp_print_string fmt name
| Clause id ->
let name = ctx_get_local_trait_clause id ctx in
@@ -1354,8 +1341,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
| None -> ctx.fmt.type_name def.name
| Some info -> String.concat "." info.rust_name
in
- let is_opaque = def.kind = Opaque in
- let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
+ let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
(* Compute and register:
* - the variant names, if this is an enumeration
* - the field names, if this is a structure
@@ -1392,11 +1378,11 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let ctx =
List.fold_left
(fun ctx (fid, name) ->
- ctx_add is_opaque (FieldId (AdtId def.def_id, fid)) name ctx)
+ ctx_add (FieldId (AdtId def.def_id, fid)) name ctx)
ctx field_names
in
(* Add the constructor name *)
- ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx
+ ctx_add (StructId (AdtId def.def_id)) cons_name ctx
| Enum variants ->
let variant_names =
match info with
@@ -1432,7 +1418,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
in
List.fold_left
(fun ctx (vid, vname) ->
- ctx_add is_opaque (VariantId (AdtId def.def_id, vid)) vname ctx)
+ ctx_add (VariantId (AdtId def.def_id, vid)) vname ctx)
ctx variant_names
| Opaque ->
(* Nothing to do *)
@@ -1635,9 +1621,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* If Coq: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
if !backend = Coq && not is_rec then (
- let with_opaque_pre = false in
- F.pp_print_string fmt
- (ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx);
+ F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
F.pp_print_string fmt " ");
(match !backend with
| Lean -> ()
@@ -1681,16 +1665,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* We extract for Coq or Lean, and we have a recursive record, or a record in
a group of mutually recursive types: we extract it as an inductive type *)
assert (is_rec && (!backend = Coq || !backend = Lean));
- let with_opaque_pre = false in
(* Small trick: in Lean we use namespaces, meaning we don't need to prefix
the constructor name with the name of the type at definition site,
i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
we generate `inductive Foo := | mk ... *)
let cons_name =
- if !backend = Lean then "mk"
- else ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx
+ if !backend = Lean then "mk" else ctx_get_struct (AdtId def.def_id) ctx
in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
cg_params cons_name fields)
in
@@ -1720,8 +1702,7 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
- let with_opaque_pre = false in
- let trait_name = ctx_get_trait_decl with_opaque_pre clause.trait_id ctx in
+ let trait_name = ctx_get_trait_decl clause.trait_id ctx in
F.pp_print_string fmt trait_name;
extract_generic_args ctx fmt no_params_tys clause.generics
@@ -1743,8 +1724,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- let with_opaque_pre = false in
- let trait_id = ctx_get_trait_decl with_opaque_pre trait_decl.def_id ctx in
+ let trait_id = ctx_get_trait_decl trait_decl.def_id ctx in
F.pp_print_string fmt trait_id;
List.iter
(fun p ->
@@ -1913,8 +1893,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let is_opaque_coq = !backend = Coq && is_opaque in
let use_forall = is_opaque_coq && def.generics <> empty_generic_params in
(* Retrieve the definition name *)
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx_body, type_params, cg_params, trait_clauses =
@@ -2001,8 +1980,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : type_decl) : unit =
(* Retrieve the definition name *)
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
(* Generic parameters are unsupported *)
assert (def.generics.const_generics = []);
(* Trait clauses on type definitions are unsupported *)
@@ -2027,8 +2005,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
(fmt : F.formatter) (def : type_decl) : unit =
(* Retrieve the definition name *)
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
(* Sanity check *)
assert (def.generics = empty_generic_params);
(* Generate the declaration *)
@@ -2111,8 +2088,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
| Struct fields ->
let adt_id = AdtId decl.def_id in
(* Generate the instruction for the record constructor *)
- let with_opaque_pre = false in
- let cons_name = ctx_get_struct with_opaque_pre adt_id ctx in
+ let cons_name = ctx_get_struct adt_id ctx in
extract_arguments_info cons_name fields;
(* Generate the instruction for the record projectors, if there are *)
let is_rec = decl_is_from_rec_group kind in
@@ -2156,11 +2132,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
in
let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre decl.def_id ctx in
- let cons_name =
- ctx_get_struct with_opaque_pre (AdtId decl.def_id) ctx
- in
+ let def_name = ctx_get_local_type decl.def_id ctx in
+ let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in
let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
F.pp_print_space fmt ();
(* Outer box for the projector definition *)
@@ -2391,7 +2364,6 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
| Some (_filter, info) ->
let backs = List.map (fun f -> f.f) def.backs in
let funs = if def.keep_fwd then def.fwd.f :: backs else backs in
- let is_opaque = false in
List.fold_left
(fun ctx (f : fun_decl) ->
let open ExtractBuiltin in
@@ -2404,7 +2376,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
info)
.extract_name
in
- ctx_add is_opaque (FunId (FromLlbc fun_id)) fun_name ctx)
+ ctx_add (FunId (FromLlbc fun_id)) fun_name ctx)
ctx funs
| None ->
let fwd = def.fwd in
@@ -2509,18 +2481,14 @@ let extract_adt_g_value
* [{ field0=...; ...; fieldn=...; }] in case of structures.
*)
let cons =
- (* The ADT shouldn't be opaque *)
- let with_opaque_pre = false in
match variant_id with
| Some vid -> (
(* In the case of Lean, we might have to add the type name as a prefix *)
match (!backend, adt_id) with
| Lean, Assumed _ ->
- ctx_get_type with_opaque_pre adt_id ctx
- ^ "."
- ^ ctx_get_variant adt_id vid ctx
+ ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
| _ -> ctx_get_variant adt_id vid ctx)
- | None -> ctx_get_struct with_opaque_pre adt_id ctx
+ | None -> ctx_get_struct adt_id ctx
in
let use_parentheses = inside && field_values <> [] in
if use_parentheses then F.pp_print_string fmt "(";
@@ -2539,8 +2507,7 @@ let extract_adt_g_value
(* Extract globals in the same way as variables *)
let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
(id : A.GlobalDeclId.id) : unit =
- let with_opaque_pre = ctx.use_opaque_pre in
- F.pp_print_string fmt (ctx_get_global with_opaque_pre id ctx)
+ F.pp_print_string fmt (ctx_get_global id ctx)
(** [inside]: see {!extract_ty}.
@@ -2676,9 +2643,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
if inside then F.pp_print_string fmt "(";
(* Open a box for the function call *)
F.pp_open_hovbox fmt ctx.indent_incr;
- (* Print the function name *)
- let with_opaque_pre = ctx.use_opaque_pre in
- (* For the function name: the id is not the same depending on whether
+ (* Print the function name.
+
+ For the function name: the id is not the same depending on whether
we call a trait method and a "regular" function (remark: trait
method *implementations* are considered as regular functions here;
only calls to method of traits which are parameterized in a where
@@ -2751,7 +2718,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
let fun_id =
FromLlbc (FunId (Regular method_id.id), lp_id, rg_id)
in
- let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
+ let fun_name = ctx_get_function fun_id ctx in
F.pp_print_string fmt fun_name;
(* Note that we do not need to print the generics for the trait
@@ -2762,7 +2729,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref
| _ ->
- let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
+ let fun_name = ctx_get_function fun_id ctx in
F.pp_print_string fmt fun_name);
(* Sanity check: HOL4 doesn't support const generics *)
@@ -3260,7 +3227,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the box for `Array.replicate T N [` *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the array constructor *)
- let cs = ctx_get_struct false (Assumed Array) ctx in
+ let cs = ctx_get_struct (Assumed Array) ctx in
F.pp_print_string fmt cs;
(* Print the parameters *)
let _, generics = ty_as_adt e_ty in
@@ -3613,10 +3580,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
assert (not def.is_global_decl_body);
(* Retrieve the function name *)
- let with_opaque_pre = false in
let def_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
- ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
(* Add a break before *)
if !backend <> HOL4 || not (decl_is_first_from_group kind) then
@@ -3649,8 +3614,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
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
+ (if not (kind = Assumed || kind = Declared) then
let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
match qualif with
| Some qualif ->
@@ -3867,10 +3831,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_decl) : unit =
(* Retrieve the definition name *)
- let with_opaque_pre = false in
let def_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
- ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
assert (def.signature.generics.const_generics = []);
(* Add the type/const gen parameters - note that we need those bindings
@@ -4065,10 +4027,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ];
F.pp_print_space fmt ();
- let with_opaque_pre = false in
- let decl_name = ctx_get_global with_opaque_pre global.def_id ctx in
+ let decl_name = ctx_get_global global.def_id ctx in
let body_name =
- ctx_get_function with_opaque_pre
+ ctx_get_function
(FromLlbc (Pure.FunId (Regular global.body_id), None, None))
ctx
in
@@ -4111,7 +4072,6 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
(trait_decl : trait_decl)
(builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
extraction_ctx =
- let is_opaque = false in
let generics = trait_decl.generics in
(* Compute the clause names *)
let clause_names =
@@ -4135,7 +4095,7 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (cid, cname) ->
- ctx_add is_opaque (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx)
+ ctx_add (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx)
ctx clause_names
(** Similar to {!extract_trait_decl_register_names} *)
@@ -4143,7 +4103,6 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
(trait_decl : trait_decl)
(builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
extraction_ctx =
- let is_opaque = false in
let consts = trait_decl.consts in
(* Compute the names *)
let constant_names =
@@ -4169,7 +4128,7 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (item_name, name) ->
- ctx_add is_opaque (TraitItemId (trait_decl.def_id, item_name)) name ctx)
+ ctx_add (TraitItemId (trait_decl.def_id, item_name)) name ctx)
ctx constant_names
(** Similar to {!extract_trait_decl_register_names} *)
@@ -4177,7 +4136,6 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
(trait_decl : trait_decl)
(builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
extraction_ctx =
- let is_opaque = false in
let types = trait_decl.types in
(* Compute the names *)
let type_names =
@@ -4227,13 +4185,11 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
List.fold_left
(fun ctx (item_name, (type_name, clauses)) ->
let ctx =
- ctx_add is_opaque
- (TraitItemId (trait_decl.def_id, item_name))
- type_name ctx
+ ctx_add (TraitItemId (trait_decl.def_id, item_name)) type_name ctx
in
List.fold_left
(fun ctx (clause_id, clause_name) ->
- ctx_add is_opaque
+ ctx_add
(TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
clause_name ctx)
ctx clauses)
@@ -4244,7 +4200,6 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(trait_decl : trait_decl)
(builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
extraction_ctx =
- let is_opaque = false in
let required_methods = trait_decl.required_methods in
(* Compute the names *)
let method_names =
@@ -4305,7 +4260,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(* We add one field per required forward/backward function *)
List.fold_left
(fun ctx (rg, fun_name) ->
- ctx_add is_opaque
+ ctx_add
(TraitMethodId (trait_decl.def_id, item_name, rg))
fun_name ctx)
ctx funs)
@@ -4326,8 +4281,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
| None -> ctx.fmt.trait_decl_name trait_decl
| Some info -> info.extract_name
in
- let is_opaque = false in
- ctx_add is_opaque (TraitDeclId trait_decl.def_id) trait_name ctx
+ ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx
in
(* Parent clauses *)
let ctx =
@@ -4369,8 +4323,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
| None -> ctx.fmt.trait_impl_name trait_decl trait_impl
| Some name -> name
in
- let is_opaque = false in
- ctx_add is_opaque (TraitImplId trait_impl.def_id) name ctx
+ ctx_add (TraitImplId trait_impl.def_id) name ctx
(** Small helper.
@@ -4446,8 +4399,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(decl : trait_decl) : unit =
(* Retrieve the trait name *)
- let with_opaque_pre = false in
- let decl_name = ctx_get_trait_decl with_opaque_pre decl.def_id ctx in
+ let decl_name = ctx_get_trait_decl decl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -4592,7 +4544,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
if use_forall then F.pp_print_string fmt ",";
(* Extract the function call *)
F.pp_print_space fmt ();
- let id = ctx_get_local_function false f.def_id None f.back_id ctx in
+ let id = ctx_get_local_function f.def_id None f.back_id ctx in
F.pp_print_string fmt id;
let all_generics =
let i_tys, i_cgs, i_tcs = impl_generics in
@@ -4613,8 +4565,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name));
(* Retrieve the impl name *)
- let with_opaque_pre = false in
- let impl_name = ctx_get_trait_impl with_opaque_pre impl.def_id ctx in
+ let impl_name = ctx_get_trait_impl impl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -4690,7 +4641,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
let item_name = ctx_get_trait_const trait_decl_id name ctx in
let ty () =
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_global false id ctx)
+ F.pp_print_string fmt (ctx_get_global id ctx)
in
extract_trait_impl_item ctx fmt item_name ty)
@@ -4776,12 +4727,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "assert_norm";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -4796,12 +4743,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "Check";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -4813,12 +4756,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "#assert";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -4832,12 +4771,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
| HOL4 ->
F.pp_print_string fmt "val _ = assert_return (";
F.pp_print_string fmt "“";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 3ff299f2..f26beeb6 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -251,37 +251,6 @@ type formatter = {
trait_type_name : trait_decl -> string -> string;
trait_method_name : trait_decl -> string -> string;
trait_type_clause_name : trait_decl -> string -> trait_clause -> string;
- opaque_pre : unit -> string;
- (** 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
- definitions requires to prefix them with a module parameter name (such
- as "opaque_defs.").
-
- For instance, if we have an opaque function [f : int -> int], which
- is used by the non-opaque function [g], we would generate (in Coq):
- {[
- (* The module signature declaring the opaque definitions *)
- module type OpaqueDefs = {
- f_fwd : int -> int
- ... (* Other definitions *)
- }
-
- (* The definitions generated for the non-opaque definitions *)
- module Funs (opaque: OpaqueDefs) = {
- let g ... =
- ...
- opaque_defs.f_fwd
- ...
- }
- ]}
-
- Upon using [f] in [g], we don't directly use the the name "f_fwd",
- but prefix it with the "opaque_defs." identifier.
- *)
var_basename : StringSet.t -> string option -> ty -> string;
(** Generates a variable basename.
@@ -498,20 +467,6 @@ type names_map = {
precisely which identifiers are mapped to the same name...
*)
names_set : StringSet.t;
- opaque_ids : IdSet.t;
- (** TODO: this is obsolete. Remove.
-
- The set of opaque definitions.
-
- See {!formatter.opaque_pre} for detailed explanations about why
- we need to know which definitions are opaque to compute names.
-
- Also note that the opaque ids don't contain the ids of the assumed
- definitions. In practice, assumed definitions are opaque_defs. However, they
- are not grouped in the opaque module, meaning we never need to
- prefix them (with, say, "opaque_defs."): we thus consider them as non-opaque
- with regards to the names map.
- *)
}
let empty_names_map : names_map =
@@ -519,7 +474,6 @@ let empty_names_map : names_map =
id_to_name = IdMap.empty;
name_to_id = StringMap.empty;
names_set = StringSet.empty;
- opaque_ids = IdSet.empty;
}
(** Small helper to report name collision *)
@@ -547,8 +501,8 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
(* There is a clash: print a nice debugging message for the user *)
report_name_collision id_to_string clash id name
-let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
- (name : string) (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+ (nm : names_map) : names_map =
(* Check if there is a clash *)
names_map_check_collision id_to_string id name nm;
(* Sanity check *)
@@ -564,32 +518,24 @@ let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
let id_to_name = IdMap.add id name nm.id_to_name in
let name_to_id = StringMap.add name id nm.name_to_id in
let names_set = StringSet.add name nm.names_set in
- let opaque_ids =
- if is_opaque then IdSet.add id nm.opaque_ids else nm.opaque_ids
- in
- { id_to_name; name_to_id; names_set; opaque_ids }
+ { id_to_name; name_to_id; names_set }
let names_map_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_map) : names_map =
- let is_opaque = false in
- names_map_add id_to_string is_opaque (TypeId (Assumed id)) name nm
+ names_map_add id_to_string (TypeId (Assumed id)) name nm
let names_map_add_assumed_struct (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_map) : names_map =
- let is_opaque = false in
- names_map_add id_to_string is_opaque (StructId (Assumed id)) name nm
+ names_map_add id_to_string (StructId (Assumed id)) name nm
let names_map_add_assumed_variant (id_to_string : id -> string)
(id : assumed_ty) (variant_id : VariantId.id) (name : string)
(nm : names_map) : names_map =
- let is_opaque = false in
- names_map_add id_to_string is_opaque
- (VariantId (Assumed id, variant_id))
- name nm
+ names_map_add id_to_string (VariantId (Assumed id, variant_id)) name nm
-let names_map_add_function (id_to_string : id -> string) (is_opaque : bool)
- (fid : fun_id) (name : string) (nm : names_map) : names_map =
- names_map_add id_to_string is_opaque (FunId fid) name nm
+let names_map_add_function (id_to_string : id -> string) (fid : fun_id)
+ (name : string) (nm : names_map) : names_map =
+ names_map_add id_to_string (FunId fid) name nm
(** The unsafe names map stores mappings from identifiers to names which might
collide. For some backends and some names, it might be acceptable to have
@@ -667,14 +613,6 @@ type extraction_ctx = {
fmt : formatter;
indent_incr : int;
(** The indent increment we insert whenever we need to indent more *)
- use_opaque_pre : bool;
- (** Do we use the "opaque_defs." prefix for the opaque definitions?
-
- Opaque function definitions might refer opaque types: if we are in the
- opaque module, we musn't use the "opaque_defs." prefix, otherwise we
- use it.
- Also see {!names_map.opaque_ids}.
- *)
use_dep_ite : bool;
(** For Lean: do we use dependent-if then else expressions?
@@ -884,8 +822,7 @@ let allow_collisions (id : id) : bool =
!Config.record_fields_short_names
| _ -> false
-let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
- : extraction_ctx =
+let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
(* The id_to_string function to print nice debugging messages if there are
* collisions *)
let id_to_string (id : id) : string = id_to_string id ctx in
@@ -902,7 +839,6 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
others (ex.: fields and keywords).
*)
if allow_collisions id then (
- assert (not is_opaque);
(* Check with the ids which are considered to be strict on collisions *)
names_map_check_collision id_to_string id name ctx.strict_names_map;
{
@@ -916,16 +852,13 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
*)
let strict_names_map =
if strict_collisions id then
- names_map_add id_to_string is_opaque id name ctx.strict_names_map
+ names_map_add id_to_string id name ctx.strict_names_map
else ctx.strict_names_map
in
- let names_map =
- names_map_add id_to_string is_opaque id name ctx.names_map
- in
+ let names_map = names_map_add id_to_string id name ctx.names_map in
{ ctx with strict_names_map; names_map }
-(** [with_opaque_pre]: if [true] and the definition is opaque, add the opaque prefix *)
-let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
+let ctx_get (id : id) (ctx : extraction_ctx) : string =
(* We do not use the same name map if we allow/disallow collisions *)
let map_to_string (m : string IdMap.t) : string =
"[\n"
@@ -951,9 +884,7 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
else
let m = ctx.names_map.id_to_name in
match IdMap.find_opt id m with
- | Some s ->
- let is_opaque = IdSet.mem id ctx.names_map.opaque_ids in
- if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s
+ | Some s -> s
| None ->
let err =
"Could not find: " ^ id_to_string id ctx ^ "\nNames map:\n"
@@ -963,53 +894,38 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
if !Config.extract_fail_hard then raise (Failure err)
else "(ERROR: \"" ^ id_to_string id ctx ^ "\")"
-let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (GlobalId id) ctx
+let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
+ ctx_get (GlobalId id) ctx
-let ctx_get_function (with_opaque_pre : bool) (id : fun_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (FunId id) ctx
+let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string =
+ ctx_get (FunId id) ctx
-let ctx_get_local_function (with_opaque_pre : bool) (id : A.FunDeclId.id)
- (lp : LoopId.id option) (rg : RegionGroupId.id option)
- (ctx : extraction_ctx) : string =
- ctx_get_function with_opaque_pre (FromLlbc (FunId (Regular id), lp, rg)) ctx
+let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option)
+ (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string =
+ ctx_get_function (FromLlbc (FunId (Regular id), lp, rg)) ctx
-let ctx_get_type (with_opaque_pre : bool) (id : type_id) (ctx : extraction_ctx)
- : string =
+let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
assert (id <> Tuple);
- ctx_get with_opaque_pre (TypeId id) ctx
+ ctx_get (TypeId id) ctx
-let ctx_get_local_type (with_opaque_pre : bool) (id : TypeDeclId.id)
- (ctx : extraction_ctx) : string =
- ctx_get_type with_opaque_pre (AdtId id) ctx
+let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
+ ctx_get_type (AdtId id) ctx
let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
- (* In practice, the assumed types are opaque. However, assumed types
- are never grouped in the opaque module, meaning we never need to
- prefix them: we thus consider them as non-opaque with regards to the
- names map.
- *)
- let is_opaque = false in
- ctx_get_type is_opaque (Assumed id) ctx
+ ctx_get_type (Assumed id) ctx
let ctx_get_trait_self_clause (ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre TraitSelfClauseId ctx
+ ctx_get TraitSelfClauseId ctx
-let ctx_get_trait_decl (with_opaque_pre : bool) (id : trait_decl_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (TraitDeclId id) ctx
+let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
+ ctx_get (TraitDeclId id) ctx
-let ctx_get_trait_impl (with_opaque_pre : bool) (id : trait_impl_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (TraitImplId id) ctx
+let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string =
+ ctx_get (TraitImplId id) ctx
let ctx_get_trait_item (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (TraitItemId (id, item_name)) ctx
+ ctx_get (TraitItemId (id, item_name)) ctx
let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
@@ -1021,83 +937,69 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
(rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre (TraitMethodId (id, item_name, rg_id)) ctx
+ ctx_get (TraitMethodId (id, item_name, rg_id)) ctx
let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
(ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre (TraitParentClauseId (id, clause)) ctx
+ ctx_get (TraitParentClauseId (id, clause)) ctx
let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
(clause : trait_clause_id) (ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre (TraitItemClauseId (id, item, clause)) ctx
+ ctx_get (TraitItemClauseId (id, item, clause)) ctx
let ctx_get_var (id : VarId.id) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (VarId id) ctx
+ ctx_get (VarId id) ctx
let ctx_get_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (TypeVarId id) ctx
+ ctx_get (TypeVarId id) ctx
let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx)
: string =
- let is_opaque = false in
- ctx_get is_opaque (ConstGenericVarId id) ctx
+ ctx_get (ConstGenericVarId id) ctx
let ctx_get_local_trait_clause (id : TraitClauseId.id) (ctx : extraction_ctx) :
string =
- let is_opaque = false in
- ctx_get is_opaque (LocalTraitClauseId id) ctx
+ ctx_get (LocalTraitClauseId id) ctx
let ctx_get_field (type_id : type_id) (field_id : FieldId.id)
(ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (FieldId (type_id, field_id)) ctx
+ ctx_get (FieldId (type_id, field_id)) ctx
-let ctx_get_struct (with_opaque_pre : bool) (def_id : type_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (StructId def_id) ctx
+let ctx_get_struct (def_id : type_id) (ctx : extraction_ctx) : string =
+ ctx_get (StructId def_id) ctx
let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
(ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (VariantId (def_id, variant_id)) ctx
+ ctx_get (VariantId (def_id, variant_id)) ctx
let ctx_get_decreases_proof (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (DecreasesProofId (Regular def_id, loop_id)) ctx
+ ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx
let ctx_get_termination_measure (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (TerminationMeasureId (Regular def_id, loop_id)) ctx
+ ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx
(** Generate a unique type variable name and add it to the context *)
let ctx_add_type_var (basename : string) (id : TypeVarId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let name = ctx.fmt.type_var_basename ctx.names_map.names_set basename in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
in
- let ctx = ctx_add is_opaque (TypeVarId id) name ctx in
+ let ctx = ctx_add (TypeVarId id) name ctx in
(ctx, name)
(** Generate a unique const generic variable name and add it to the context *)
let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let name =
ctx.fmt.const_generic_var_basename ctx.names_map.names_set basename
in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
in
- let ctx = ctx_add is_opaque (ConstGenericVarId id) name ctx in
+ let ctx = ctx_add (ConstGenericVarId id) name ctx in
(ctx, name)
(** See {!ctx_add_type_var} *)
@@ -1110,31 +1012,28 @@ let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
(** Generate a unique variable name and add it to the context *)
let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
extraction_ctx * string =
- let is_opaque = false in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
in
- let ctx = ctx_add is_opaque (VarId id) name ctx in
+ let ctx = ctx_add (VarId id) name ctx in
(ctx, name)
(** Generate a unique variable name for the trait self clause and add it to the context *)
let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let basename = ctx.fmt.trait_self_clause_basename in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
in
- let ctx = ctx_add is_opaque TraitSelfClauseId name ctx in
+ let ctx = ctx_add TraitSelfClauseId name ctx in
(ctx, name)
(** Generate a unique trait clause name and add it to the context *)
let ctx_add_local_trait_clause (basename : string) (id : TraitClauseId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
in
- let ctx = ctx_add is_opaque (LocalTraitClauseId id) name ctx in
+ let ctx = ctx_add (LocalTraitClauseId id) name ctx in
(ctx, name)
(** See {!ctx_add_var} *)
@@ -1182,30 +1081,23 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
- let is_opaque = false in
let name =
ctx.fmt.decreases_proof_name def.def_id def.basename def.num_loops
def.loop_id
in
- ctx_add is_opaque
- (DecreasesProofId (Regular def.def_id, def.loop_id))
- name ctx
+ ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx
let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
- let is_opaque = false in
let name =
ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops
def.loop_id
in
- ctx_add is_opaque
- (TerminationMeasureId (Regular def.def_id, def.loop_id))
- name ctx
+ ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx
let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
extraction_ctx =
(* TODO: update once the body id can be an option *)
- let is_opaque = false in
let decl = GlobalId def.def_id in
(* Check if the global corresponds to an assumed global that we should map
@@ -1215,13 +1107,13 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
match SimpleNameMap.find_opt sname builtin_globals_map with
| Some name ->
(* Yes: register the custom binding *)
- ctx_add is_opaque decl name ctx
+ ctx_add decl name ctx
| None ->
(* Not the case: "standard" registration *)
let name = ctx.fmt.global_name def.name in
let body = FunId (FromLlbc (FunId (Regular def.body_id), None, None)) in
- let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in
- let ctx = ctx_add is_opaque body (name ^ "_body") ctx in
+ let ctx = ctx_add decl (name ^ "_c") ctx in
+ let ctx = ctx_add body (name ^ "_body") ctx in
ctx
let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
@@ -1259,11 +1151,10 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
let def_id = def.def_id in
let { keep_fwd; fwd = _; backs } = trans_group in
let num_backs = List.length backs in
- let is_opaque = def.body = None in
(* Add the function name *)
let def_name = ctx_compute_fun_name trans_group def ctx in
let fun_id = (Pure.FunId (Regular def_id), def.loop_id, def.back_id) in
- let ctx = ctx_add is_opaque (FunId (FromLlbc fun_id)) def_name ctx in
+ let ctx = ctx_add (FunId (FromLlbc fun_id)) def_name ctx in
(* Add the name info *)
{
ctx with
@@ -1296,12 +1187,11 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
let name_to_id =
StringMap.of_list (List.map (fun x -> (x, UnknownId)) keywords)
in
- let opaque_ids = IdSet.empty in
(* We fist initialize [id_to_name] as empty, because the id of a keyword is [UnknownId].
* Also note that we don't need this mapping for keywords: we insert keywords only
* to check collisions. *)
let id_to_name = IdMap.empty in
- let nm = { id_to_name; name_to_id; names_set; opaque_ids } in
+ let nm = { id_to_name; name_to_id; names_set } in
(* For debugging - we are creating bindings for assumed types and functions, so
* it is ok if we simply use the "show" function (those aren't simply identified
* by numbers) *)
@@ -1338,15 +1228,8 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
@ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
in
let nm =
- (* In practice, the assumed function are opaque. However, assumed functions
- are never grouped in the opaque module, meaning we never need to
- prefix them: we thus consider them as non-opaque with regards to the
- names map.
- *)
- let is_opaque = false in
List.fold_left
- (fun nm (fid, name) ->
- names_map_add_function id_to_string is_opaque fid name nm)
+ (fun nm (fid, name) -> names_map_add_function id_to_string fid name nm)
nm assumed_functions
in
(* Return *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 74a8537f..b3269aa2 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -851,37 +851,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
if config.extract_state_type && config.extract_fun_decls then
export_state_type ();
- (* 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.wrap_opaque_in_sig
- &&
- let _, opaque_funs = crate_has_opaque_decls ctx true in
- opaque_funs
- in
- if wrap_in_sig then (
- (* We change the name of the structure depending on whether we *only*
- extract opaque definitions, or if we extract all definitions *)
- let struct_name =
- if config.extract_transparent then "Definitions" else "OpaqueDefs"
- in
- Format.pp_print_break fmt 0 0;
- Format.pp_open_vbox fmt ctx.indent_incr;
- Format.pp_print_string fmt ("structure " ^ struct_name ^ " where");
- Format.pp_print_break fmt 0 0);
List.iter export_decl_group ctx.crate.declarations;
if config.extract_state_type && not config.extract_fun_decls then
- export_state_type ();
-
- if wrap_in_sig then Format.pp_close_box fmt ()
+ export_state_type ()
type extract_file_info = {
filename : string;
@@ -1029,10 +1002,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(fun (id, _) -> strict_collisions id)
(IdMap.bindings names_map.id_to_name)
in
- let is_opaque = false in
List.fold_left
(* id_to_string: we shouldn't need to use it *)
- (fun m (id, n) -> names_map_add show_id is_opaque id n m)
+ (fun m (id, n) -> names_map_add show_id id n m)
empty_names_map ids
in
@@ -1093,7 +1065,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
strict_names_map;
fmt;
indent_incr = 2;
- use_opaque_pre = !Config.split_files;
use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
fun_name_info = PureUtils.RegularFunIdMap.empty;
trait_decl_id = None (* None by default *);
@@ -1389,7 +1360,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
interface = true;
}
in
- let ctx = { ctx with use_opaque_pre = false } in
let file_info =
{
filename = opaque_filename;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 07:02:31 +0000