summaryrefslogtreecommitdiff
path: root/compiler/ExtractBase.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/ExtractBase.ml')
-rw-r--r--compiler/ExtractBase.ml828
1 files changed, 515 insertions, 313 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index d733c763..31b1a447 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -5,9 +5,10 @@ open TranslateCore
module C = Contexts
module RegionVarId = T.RegionVarId
module F = Format
+open ExtractBuiltin
(** The local logger *)
-let log = L.pure_to_extract_log
+let log = L.extract_log
type region_group_info = {
id : RegionGroupId.id;
@@ -21,8 +22,8 @@ type region_group_info = {
*)
}
-module StringSet = Collections.MakeSet (Collections.OrderedString)
-module StringMap = Collections.MakeMap (Collections.OrderedString)
+module StringSet = Collections.StringSet
+module StringMap = Collections.StringMap
type name = Names.name
type type_name = Names.type_name
@@ -77,6 +78,7 @@ type decl_kind =
F*: [val x : Type0]
Coq: [Axiom x : Type.]
*)
+[@@deriving show]
(** Return [true] if the declaration is the last from its group of declarations.
@@ -111,9 +113,9 @@ let decl_is_first_from_group (kind : decl_kind) : bool =
let decl_is_not_last_from_group (kind : decl_kind) : bool =
not (decl_is_last_from_group kind)
-(* TODO: this should a module we give to a functor! *)
+type type_decl_kind = Enum | Struct [@@deriving show]
-type type_decl_kind = Enum | Struct
+(* TODO: this should be a module we give to a functor! *)
(** A formatter's role is twofold:
1. Come up with name suggestions.
@@ -125,6 +127,9 @@ type type_decl_kind = Enum | Struct
snake case, adding prefixes/suffixes, etc.
2. Format some specific terms, like constants.
+
+ TODO: unclear that this is useful now that all the backends are so much
+ entangled in Extract.ml
*)
type formatter = {
bool_name : string;
@@ -239,37 +244,14 @@ type formatter = {
the same purpose as in {!field:fun_name}.
- loop identifier, if this is for a loop
*)
- 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.
- *)
+ trait_decl_name : trait_decl -> string;
+ trait_impl_name : trait_decl -> trait_impl -> string;
+ trait_decl_constructor : trait_decl -> string;
+ trait_parent_clause_name : trait_decl -> trait_clause -> string;
+ trait_const_name : trait_decl -> string -> string;
+ trait_type_name : trait_decl -> string -> string;
+ trait_method_name : trait_decl -> string -> string;
+ trait_type_clause_name : trait_decl -> string -> trait_clause -> string;
var_basename : StringSet.t -> string option -> ty -> string;
(** Generates a variable basename.
@@ -288,6 +270,14 @@ type formatter = {
(** Generates a type variable basename. *)
const_generic_var_basename : StringSet.t -> string -> string;
(** Generates a const generic variable basename. *)
+ trait_self_clause_basename : string;
+ trait_clause_basename : StringSet.t -> trait_clause -> string;
+ (** Return a base name for a trait clause. We might add a suffix to prevent
+ collisions.
+
+ In the traduction we explicitely manipulate the trait clause instances,
+ that is we introduce one input variable for each trait clause.
+ *)
append_index : string -> int -> string;
(** Appends an index to a name - we use this to generate unique
names: when doing so, the role of the formatter is just to concatenate
@@ -396,10 +386,60 @@ type id =
| TypeVarId of TypeVarId.id
| ConstGenericVarId of ConstGenericVarId.id
| VarId of VarId.id
+ | TraitDeclId of TraitDeclId.id
+ | TraitImplId of TraitImplId.id
+ | LocalTraitClauseId of TraitClauseId.id
+ | TraitDeclConstructorId of TraitDeclId.id
+ | TraitMethodId of TraitDeclId.id * string * T.RegionGroupId.id option
+ (** Something peculiar with trait methods: because we have to take into
+ account forward/backward functions, we may need to generate fields
+ items per method.
+ *)
+ | TraitItemId of TraitDeclId.id * string
+ (** A trait associated item which is not a method *)
+ | TraitParentClauseId of TraitDeclId.id * TraitClauseId.id
+ | TraitItemClauseId of TraitDeclId.id * string * TraitClauseId.id
+ | TraitSelfClauseId
+ (** Specifically for the clause: [Self : Trait].
+
+ For now, we forbid provided methods (methods in trait declarations
+ with a default implementation) from being overriden in trait implementations.
+ We extract trait provided methods such that they take an instance of
+ the trait as input: this instance is given by the trait self clause.
+
+ For instance:
+ {[
+ //
+ // Rust
+ //
+ trait ToU64 {
+ fn to_u64(&self) -> u64;
+
+ // Provided method
+ fn is_pos(&self) -> bool {
+ self.to_u64() > 0
+ }
+ }
+
+ //
+ // Generated code
+ //
+ struct ToU64 (T : Type) {
+ to_u64 : T -> u64;
+ }
+
+ // The trait self clause
+ // vvvvvvvvvvvvvvvvvvvvvv
+ let is_pos (T : Type) (trait_self : ToU64 T) (self : T) : bool =
+ trait_self.to_u64 self > 0
+ ]}
+ *)
| UnknownId
(** Used for stored various strings like keywords, definitions which
should always be in context, etc. and which can't be linked to one
of the above.
+
+ TODO: rename to "keyword"
*)
[@@deriving show, ord]
@@ -429,69 +469,64 @@ 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.
+let empty_names_map : names_map =
+ {
+ id_to_name = IdMap.empty;
+ name_to_id = StringMap.empty;
+ names_set = StringSet.empty;
+ }
- See {!formatter.opaque_pre} for detailed explanations about why
- we need to know which definitions are opaque to compute names.
+(** Small helper to report name collision *)
+let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
+ (name : string) : unit =
+ let id1 = "\n- " ^ id_to_string id1 in
+ let id2 = "\n- " ^ id_to_string id2 in
+ let err =
+ "Name clash detected: the following identifiers are bound to the same name \
+ \"" ^ name ^ "\":" ^ id1 ^ id2
+ ^ "\nYou may want to rename some of your definitions, or report an issue."
+ in
+ log#serror err;
+ (* If we fail hard on errors, raise an exception *)
+ if !Config.fail_hard then raise (Failure err)
- 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 names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+ StringMap.find_opt name nm.name_to_id
-let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
- (name : string) (nm : names_map) : names_map =
- (* Check if there is a clash *)
- (match StringMap.find_opt name nm.name_to_id with
+let names_map_check_collision (id_to_string : id -> string) (id : id)
+ (name : string) (nm : names_map) : unit =
+ match names_map_get_id_from_name name nm with
| None -> () (* Ok *)
| Some clash ->
(* There is a clash: print a nice debugging message for the user *)
- let id1 = "\n- " ^ id_to_string clash in
- let id2 = "\n- " ^ id_to_string id in
- let err =
- "Name clash detected: the following identifiers are bound to the same \
- name \"" ^ name ^ "\":" ^ id1 ^ id2
- in
- log#serror err;
- raise (Failure err));
- (* Sanity check *)
- assert (not (StringSet.mem name nm.names_set));
+ report_name_collision id_to_string clash id name
+
+(** Insert bindings in a names map without checking for collisions *)
+let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
+ names_map =
(* Insert *)
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 }
-
-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
-
-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
+ { id_to_name; name_to_id; names_set }
-let names_map_add_assumed_variant (id_to_string : id -> string)
- (id : assumed_ty) (variant_id : VariantId.id) (name : string)
+let names_map_add (id_to_string : id -> string) (id : 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
-
-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
+ (* Check if there is a clash *)
+ names_map_check_collision id_to_string id name nm;
+ (* Sanity check *)
+ if StringSet.mem name nm.names_set then (
+ let err =
+ "Error when registering the name for id: " ^ id_to_string id
+ ^ ":\nThe chosen name is already in the names set: " ^ name
+ in
+ log#serror err;
+ (* If we fail hard on errors, raise an exception *)
+ if !Config.fail_hard then raise (Failure err));
+ (* Insert *)
+ names_map_add_unchecked id 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
@@ -503,6 +538,8 @@ let names_map_add_function (id_to_string : id -> string) (is_opaque : bool)
*)
type unsafe_names_map = { id_to_name : string IdMap.t }
+let empty_unsafe_names_map = { id_to_name = IdMap.empty }
+
let unsafe_names_map_add (id : id) (name : string) (nm : unsafe_names_map) :
unsafe_names_map =
{ id_to_name = IdMap.add id name nm.id_to_name }
@@ -541,6 +578,24 @@ let basename_to_unique (names_set : StringSet.t)
type fun_name_info = { keep_fwd : bool; num_backs : int }
+type names_maps = {
+ names_map : names_map;
+ (** The map for id to names, where we forbid name collisions
+ (ex.: we always forbid function name collisions). *)
+ unsafe_names_map : unsafe_names_map;
+ (** The map for id to names, where we allow name collisions
+ (ex.: we might allow record field name collisions). *)
+ strict_names_map : names_map;
+ (** This map is a sub-map of [names_map]. For the ids in this map we also
+ forbid collisions with names in the [unsafe_names_map].
+
+ We do so for keywords for instance, but also for types (in a dependently
+ typed language, we might have an issue if the field of a record has, say,
+ the name "u32", and another field of the same record refers to "u32"
+ (for instance in its type).
+ *)
+}
+
(** Extraction context.
Note that the extraction context contains information coming from the
@@ -549,24 +604,12 @@ type fun_name_info = { keep_fwd : bool; num_backs : int }
functions, etc.
*)
type extraction_ctx = {
+ crate : A.crate;
trans_ctx : trans_ctx;
- names_map : names_map;
- (** The map for id to names, where we forbid name collisions
- (ex.: we always forbid function name collisions). *)
- unsafe_names_map : unsafe_names_map;
- (** The map for id to names, where we allow name collisions
- (ex.: we might allow record field name collisions). *)
+ names_maps : names_maps;
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?
@@ -586,6 +629,29 @@ type extraction_ctx = {
in case a Rust function only has one backward translation
and we filter the forward function because it returns unit.
*)
+ trait_decl_id : trait_decl_id option;
+ (** If we are extracting a trait declaration, identifies it *)
+ is_provided_method : bool;
+ trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
+ trans_funs : pure_fun_translation A.FunDeclId.Map.t;
+ functions_with_decreases_clause : PureUtils.FunLoopIdSet.t;
+ trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t;
+ trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t;
+ types_filter_type_args_map : bool list TypeDeclId.Map.t;
+ (** The map to filter the type arguments for the builtin type
+ definitions.
+
+ We need this for type `Vec`, for instance, which takes a useless
+ (in the context of the type translation) type argument for the
+ allocator which is used, and which we want to remove.
+
+ TODO: it would be cleaner to filter those types in a micro-pass,
+ rather than at code generation time.
+ *)
+ funs_filter_type_args_map : bool list FunDeclId.Map.t;
+ (** Same as {!types_filter_type_args_map}, but for functions *)
+ trait_impls_filter_type_args_map : bool list TraitImplId.Map.t;
+ (** Same as {!types_filter_type_args_map}, but for trait implementations *)
}
(** Debugging function, used when communicating name collisions to the user,
@@ -593,9 +659,16 @@ type extraction_ctx = {
instance).
*)
let id_to_string (id : id) (ctx : extraction_ctx) : string =
- let global_decls = ctx.trans_ctx.global_context.global_decls in
- let fun_decls = ctx.trans_ctx.fun_context.fun_decls in
- let type_decls = ctx.trans_ctx.type_context.type_decls in
+ let global_decls = ctx.trans_ctx.global_ctx.global_decls in
+ let fun_decls = ctx.trans_ctx.fun_ctx.fun_decls in
+ let type_decls = ctx.trans_ctx.type_ctx.type_decls in
+ let trait_decls = ctx.trans_ctx.trait_decls_ctx.trait_decls in
+ let trait_decl_id_to_string (id : A.TraitDeclId.id) : string =
+ let trait_name =
+ Print.fun_name_to_string (A.TraitDeclId.Map.find id trait_decls).name
+ in
+ "trait_decl: " ^ trait_name ^ " (id: " ^ A.TraitDeclId.to_string id ^ ")"
+ in
(* TODO: factorize the pretty-printing with what is in PrintPure *)
let get_type_name (id : type_id) : string =
match id with
@@ -614,10 +687,17 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| FromLlbc (fid, lp_id, rg_id) ->
let fun_name =
match fid with
- | Regular fid ->
+ | FunId (Regular fid) ->
Print.fun_name_to_string
(A.FunDeclId.Map.find fid fun_decls).name
- | Assumed aid -> A.show_assumed_fun_id aid
+ | FunId (Assumed aid) -> A.show_assumed_fun_id aid
+ | TraitMethod (trait_ref, method_name, _) ->
+ (* Shouldn't happen *)
+ if !Config.fail_hard then raise (Failure "Unexpected")
+ else
+ "Trait method: decl: "
+ ^ TraitDeclId.to_string trait_ref.trait_decl_ref.trait_decl_id
+ ^ ", method_name: " ^ method_name
in
let lp_kind =
@@ -673,12 +753,16 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
if variant_id = error_failure_id then "@error::Failure"
else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel"
else raise (Failure "Unreachable")
- | Assumed Option ->
- if variant_id = option_some_id then "@option::Some"
- else if variant_id = option_none_id then "@option::None"
+ | Assumed Fuel ->
+ if variant_id = fuel_zero_id then "@fuel::0"
+ else if variant_id = fuel_succ_id then "@fuel::Succ"
else raise (Failure "Unreachable")
- | Assumed (State | Vec | Fuel | Array | Slice | Str | Range) ->
- raise (Failure "Unreachable")
+ | Assumed (State | Array | Slice | Str | RawPtr _) ->
+ raise
+ (Failure
+ ("Unreachable: variant id ("
+ ^ VariantId.to_string variant_id
+ ^ ") for " ^ show_type_id id))
| AdtId id -> (
let def = TypeDeclId.Map.find id type_decls in
match def.kind with
@@ -693,8 +777,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
match id with
| Tuple -> raise (Failure "Unreachable")
| Assumed
- ( State | Result | Error | Fuel | Option | Vec | Array | Slice | Str
- | Range ) ->
+ (State | Result | Error | Fuel | Array | Slice | Str | RawPtr _) ->
(* We can't directly have access to the fields of those types *)
raise (Failure "Unreachable")
| AdtId id -> (
@@ -716,134 +799,265 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| ConstGenericVarId id ->
"const_generic_var_id: " ^ ConstGenericVarId.to_string id
| VarId id -> "var_id: " ^ VarId.to_string id
+ | TraitDeclId id -> "trait_decl_id: " ^ TraitDeclId.to_string id
+ | TraitImplId id -> "trait_impl_id: " ^ TraitImplId.to_string id
+ | LocalTraitClauseId id ->
+ "local_trait_clause_id: " ^ TraitClauseId.to_string id
+ | TraitDeclConstructorId id ->
+ "trait_decl_constructor: " ^ trait_decl_id_to_string id
+ | TraitParentClauseId (id, clause_id) ->
+ "trait_parent_clause_id: " ^ trait_decl_id_to_string id ^ ", clause_id: "
+ ^ TraitClauseId.to_string clause_id
+ | TraitItemClauseId (id, item_name, clause_id) ->
+ "trait_item_clause_id: " ^ trait_decl_id_to_string id ^ ", item name: "
+ ^ item_name ^ ", clause_id: "
+ ^ TraitClauseId.to_string clause_id
+ | TraitItemId (id, name) ->
+ "trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name
+ | TraitMethodId (trait_decl_id, fun_name, rg_id) ->
+ let fwd_back_kind =
+ match rg_id with
+ | None -> "forward"
+ | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
+ in
+ trait_decl_id_to_string trait_decl_id
+ ^ ", method name (" ^ fwd_back_kind ^ "): " ^ fun_name
+ | TraitSelfClauseId -> "trait_self_clause"
+
+(** Return [true] if we are strict on collisions for this id (i.e., we forbid
+ collisions even with the ids in the unsafe names map) *)
+let strict_collisions (id : id) : bool =
+ match id with UnknownId | TypeId _ -> true | _ -> false
(** We might not check for collisions for some specific ids (ex.: field names) *)
let allow_collisions (id : id) : bool =
match id with
- | FieldId (_, _) -> !Config.record_fields_short_names
+ | FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _
+ | TraitMethodId _ ->
+ !Config.record_fields_short_names
+ | FunId (Pure _ | FromLlbc (FunId (Assumed _), _, _)) ->
+ (* We map several assumed functions to the same id *)
+ true
| _ -> false
-let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
- : extraction_ctx =
- (* We do not use the same name map if we allow/disallow collisions *)
+(** The [id_to_string] function to print nice debugging messages if there are
+ collisions *)
+let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
+ (nm : names_maps) : names_maps =
+ (* We do not use the same name map if we allow/disallow collisions.
+ We notably use it for field names: some backends like Lean can use the
+ type information to disambiguate field projections.
+
+ Remark: we still need to check that those "unsafe" ids don't collide with
+ the ids that we mark as "strict on collision".
+
+ For instance, we don't allow naming a field "let". We enforce this by
+ not checking collision between ids for which we permit collisions (ex.:
+ between fields), but still checking collisions between those ids and the
+ 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 nm.strict_names_map;
{
- ctx with
- unsafe_names_map = unsafe_names_map_add id name ctx.unsafe_names_map;
+ nm with
+ unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
})
else
- (* 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
- let names_map =
- names_map_add id_to_string is_opaque id name ctx.names_map
+ (* Remark: if we are strict on collisions:
+ - we add the id to the strict collisions map
+ - we check that the id doesn't collide with the unsafe map
+ TODO: we might not check that:
+ - a user defined function doesn't collide with an assumed function
+ - two trait decl items don't collide with each other
+ *)
+ let strict_names_map =
+ if strict_collisions id then
+ names_map_add id_to_string id name nm.strict_names_map
+ else nm.strict_names_map
in
- { ctx with names_map }
+ let names_map = names_map_add id_to_string id name nm.names_map in
+ { nm with strict_names_map; names_map }
+
+let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
+ let id_to_string (id : id) : string = id_to_string id ctx in
+ let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+ { ctx with names_maps }
-(** [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 =
+(** The [id_to_string] function to print nice debugging messages if there are
+ collisions *)
+let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
+ string =
(* We do not use the same name map if we allow/disallow collisions *)
- if allow_collisions id then IdMap.find id ctx.unsafe_names_map.id_to_name
+ let map_to_string (m : string IdMap.t) : string =
+ "[\n"
+ ^ String.concat ","
+ (List.map
+ (fun (id, n) -> "\n " ^ id_to_string id ^ " -> " ^ n)
+ (IdMap.bindings m))
+ ^ "\n]"
+ in
+ if allow_collisions id then (
+ let m = nm.unsafe_names_map.id_to_name in
+ match IdMap.find_opt id m with
+ | Some s -> s
+ | None ->
+ let err =
+ "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
+ ^ map_to_string m
+ in
+ log#serror err;
+ if !Config.fail_hard then raise (Failure err)
+ else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
else
- match IdMap.find_opt id ctx.names_map.id_to_name 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
+ let m = nm.names_map.id_to_name in
+ match IdMap.find_opt id m with
+ | Some s -> s
| None ->
- log#serror ("Could not find: " ^ id_to_string id ctx);
- raise Not_found
+ let err =
+ "Could not find: " ^ id_to_string id ^ "\nNames map:\n"
+ ^ map_to_string m
+ in
+ log#serror err;
+ if !Config.fail_hard then raise (Failure err)
+ else "(ERROR: \"" ^ id_to_string id ^ "\")"
+
+let ctx_get (id : id) (ctx : extraction_ctx) : string =
+ let id_to_string (id : id) : string = id_to_string id ctx in
+ names_maps_get id_to_string id ctx.names_maps
+
+let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
+ (name : string) (nm : names_maps) : names_maps =
+ names_maps_add id_to_string (TypeId (Assumed id)) name nm
+
+let names_maps_add_assumed_struct (id_to_string : id -> string)
+ (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
+ names_maps_add id_to_string (StructId (Assumed id)) name nm
-let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id)
+let names_maps_add_assumed_variant (id_to_string : id -> string)
+ (id : assumed_ty) (variant_id : VariantId.id) (name : string)
+ (nm : names_maps) : names_maps =
+ names_maps_add id_to_string (VariantId (Assumed id, variant_id)) name nm
+
+let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
+ (name : string) (nm : names_maps) : names_maps =
+ names_maps_add id_to_string (FunId fid) name nm
+
+let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
+ ctx_get (GlobalId id) ctx
+
+let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string =
+ ctx_get (FunId id) 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 (id : type_id) (ctx : extraction_ctx) : string =
+ assert (id <> Tuple);
+ ctx_get (TypeId 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 =
+ ctx_get_type (Assumed id) ctx
+
+let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) :
+ string =
+ ctx_get (TraitDeclConstructorId id) ctx
+
+let ctx_get_trait_self_clause (ctx : extraction_ctx) : string =
+ ctx_get TraitSelfClauseId ctx
+
+let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
+ ctx_get (TraitDeclId 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 =
- ctx_get with_opaque_pre (GlobalId id) ctx
+ ctx_get (TraitItemId (id, item_name)) ctx
-let ctx_get_function (with_opaque_pre : bool) (id : fun_id)
+let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (FunId id) ctx
+ ctx_get_trait_item id item_name ctx
-let ctx_get_local_function (with_opaque_pre : bool) (id : A.FunDeclId.id)
- (lp : LoopId.id option) (rg : RegionGroupId.id option)
+let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- ctx_get_function with_opaque_pre (FromLlbc (Regular id, lp, rg)) ctx
+ ctx_get_trait_item id item_name ctx
-let ctx_get_type (with_opaque_pre : bool) (id : type_id) (ctx : extraction_ctx)
- : string =
- assert (id <> Tuple);
- ctx_get with_opaque_pre (TypeId id) ctx
+let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
+ (rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string =
+ ctx_get (TraitMethodId (id, item_name, rg_id)) ctx
-let ctx_get_local_type (with_opaque_pre : bool) (id : TypeDeclId.id)
+let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
(ctx : extraction_ctx) : string =
- ctx_get_type with_opaque_pre (AdtId id) ctx
+ ctx_get (TraitParentClauseId (id, clause)) 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
+let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
+ (clause : trait_clause_id) (ctx : extraction_ctx) : string =
+ 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 =
+ 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
+ ctx.fmt.type_var_basename ctx.names_maps.names_map.names_set basename
+ in
+ let name =
+ basename_to_unique ctx.names_maps.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
+ ctx.fmt.const_generic_var_basename ctx.names_maps.names_map.names_set
+ basename
in
let name =
- basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
+ basename_to_unique ctx.names_maps.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} *)
@@ -856,11 +1070,31 @@ 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
+ basename_to_unique ctx.names_maps.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 basename = ctx.fmt.trait_self_clause_basename in
+ let name =
+ basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+ basename
+ 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 name =
+ basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+ basename
+ in
+ let ctx = ctx_add (LocalTraitClauseId id) name ctx in
(ctx, name)
(** See {!ctx_add_var} *)
@@ -868,7 +1102,9 @@ let ctx_add_vars (vars : var list) (ctx : extraction_ctx) :
extraction_ctx * string list =
List.fold_left_map
(fun ctx (v : var) ->
- let name = ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty in
+ let name =
+ ctx.fmt.var_basename ctx.names_maps.names_map.names_set v.basename v.ty
+ in
ctx_add_var name v.id ctx)
ctx vars
@@ -885,142 +1121,105 @@ let ctx_add_const_generic_params (vars : const_generic_var list)
ctx_add_const_generic_var var.name var.index ctx)
ctx vars
-let ctx_add_type_const_generic_params (tvars : type_var list)
- (cgvars : const_generic_var list) (ctx : extraction_ctx) :
- extraction_ctx * string list * string list =
- let ctx, tys = ctx_add_type_params tvars ctx in
- let ctx, cgs = ctx_add_const_generic_params cgvars ctx in
- (ctx, tys, cgs)
-
-let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
- extraction_ctx * string =
- assert (match def.kind with Struct _ -> true | _ -> false);
- let is_opaque = false in
- let cons_name = ctx.fmt.struct_constructor def.name in
- let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx in
- (ctx, cons_name)
-
-let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx
- =
- let is_opaque = def.kind = Opaque in
- let def_name = ctx.fmt.type_name def.name in
- let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
- ctx
-
-let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field)
- (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
- let name = ctx.fmt.field_name def.name field_id field.field_name in
- let ctx = ctx_add is_opaque (FieldId (AdtId def.def_id, field_id)) name ctx in
- (ctx, name)
-
-let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list)
+let ctx_add_local_trait_clauses (clauses : trait_clause list)
(ctx : extraction_ctx) : extraction_ctx * string list =
List.fold_left_map
- (fun ctx (vid, v) -> ctx_add_field def vid v ctx)
- ctx fields
-
-let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
- (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
- let name = ctx.fmt.variant_name def.name variant.variant_name in
- (* Add the type name prefix for Lean *)
- let name =
- if !Config.backend = Lean then
- let type_name = ctx.fmt.type_name def.name in
- type_name ^ "." ^ name
- else name
- in
- let ctx =
- ctx_add is_opaque (VariantId (AdtId def.def_id, variant_id)) name ctx
- in
- (ctx, name)
-
-let ctx_add_variants (def : type_decl)
- (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) :
- extraction_ctx * string list =
- List.fold_left_map
- (fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
- ctx variants
+ (fun ctx (c : trait_clause) ->
+ let basename =
+ ctx.fmt.trait_clause_basename ctx.names_maps.names_map.names_set c
+ in
+ ctx_add_local_trait_clause basename c.clause_id ctx)
+ ctx clauses
-let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
- extraction_ctx * string =
- assert (match def.kind with Struct _ -> true | _ -> false);
- let is_opaque = false in
- let name = ctx.fmt.struct_constructor def.name in
- let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) name ctx in
- (ctx, name)
+(** Returns the lists of names for:
+ - the type variables
+ - the const generic variables
+ - the trait clauses
+ *)
+let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
+ extraction_ctx * string list * string list * string list =
+ let { types; const_generics; trait_clauses } = generics in
+ let ctx, tys = ctx_add_type_params types ctx in
+ let ctx, cgs = ctx_add_const_generic_params const_generics ctx in
+ let ctx, tcs = ctx_add_local_trait_clauses trait_clauses ctx in
+ (ctx, tys, cgs, tcs)
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 name = ctx.fmt.global_name def.name in
let decl = GlobalId def.def_id in
- let body = FunId (FromLlbc (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
- ctx
-let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
- (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
- (* Sanity check: the function should not be a global body - those are handled
- * separately *)
- assert (not def.is_global_decl_body);
+ (* Check if the global corresponds to an assumed global that we should map
+ to a custom definition in our standard library (for instance, happens
+ with "core::num::usize::MAX") *)
+ let sname = name_to_simple_name def.name in
+ match SimpleNameMap.find_opt sname builtin_globals_map with
+ | Some name ->
+ (* Yes: register the custom binding *)
+ 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 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)
+ (ctx : extraction_ctx) : string =
(* Lookup the LLBC def to compute the region group information *)
let def_id = def.def_id in
- let llbc_def =
- A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
- in
+ let llbc_def = A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_ctx.fun_decls in
let sg = llbc_def.signature in
let num_rgs = List.length sg.regions_hierarchy in
- let keep_fwd, (_, backs) = trans_group in
+ let { keep_fwd; fwd = _; backs } = trans_group in
let num_backs = List.length backs in
let rg_info =
match def.back_id with
| None -> None
| Some rg_id ->
let rg = T.RegionGroupId.nth sg.regions_hierarchy rg_id in
- let regions =
+ let region_names =
List.map
- (fun rid -> T.RegionVarId.nth sg.region_params rid)
+ (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name)
rg.regions
in
- let region_names =
- List.map (fun (r : T.region_var) -> r.name) regions
- in
Some { id = rg_id; region_names }
in
- let is_opaque = def.body = None in
(* Add the function name *)
- let def_name =
- ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
- (keep_fwd, num_backs)
- in
- let fun_id = (A.Regular def_id, def.loop_id, def.back_id) in
- let ctx = ctx_add is_opaque (FunId (FromLlbc fun_id)) def_name ctx in
+ ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
+ (keep_fwd, num_backs)
+
+(* TODO: move to Extract *)
+let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
+ (ctx : extraction_ctx) : extraction_ctx =
+ (* Sanity check: the function should not be a global body - those are handled
+ * separately *)
+ assert (not def.is_global_decl_body);
+ (* Lookup the LLBC def to compute the region group information *)
+ let def_id = def.def_id in
+ let { keep_fwd; fwd = _; backs } = trans_group in
+ let num_backs = List.length backs 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 (FunId (FromLlbc fun_id)) def_name ctx in
(* Add the name info *)
{
ctx with
@@ -1039,9 +1238,10 @@ type names_map_init = {
assumed_pure_functions : (pure_assumed_fun_id * string) list;
}
-(** Initialize a names map with a proper set of keywords/names coming from the
+(** Initialize names maps with a proper set of keywords/names coming from the
target language/prover. *)
-let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
+let initialize_names_maps (fmt : formatter) (init : names_map_init) : names_maps
+ =
let int_names = List.map fmt.int_name T.all_int_types in
let keywords =
List.concat
@@ -1049,20 +1249,30 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
[ fmt.bool_name; fmt.char_name; fmt.str_name ]; int_names; init.keywords;
]
in
- let names_set = StringSet.of_list keywords in
- let name_to_id =
- StringMap.of_list (List.map (fun x -> (x, UnknownId)) keywords)
- in
- let opaque_ids = IdSet.empty in
+ let names_set = StringSet.empty in
+ let name_to_id = StringMap.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 names_map = { id_to_name; name_to_id; names_set } in
+ let unsafe_names_map = empty_unsafe_names_map in
+ let strict_names_map = empty_names_map 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) *)
let id_to_string = show_id in
+ (* Add the keywords as strict collisions *)
+ let strict_names_map =
+ List.fold_left
+ (fun nm name ->
+ (* There is duplication in the keywords so we don't check the collisions
+ while registering them (what is important is that there are no collisions
+ between keywords and user-defined identifiers) *)
+ names_map_add_unchecked UnknownId name nm)
+ strict_names_map keywords
+ in
+ let nm = { names_map; unsafe_names_map; strict_names_map } in
(* Then we add:
* - the assumed types
* - the assumed struct constructors
@@ -1072,37 +1282,31 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
let nm =
List.fold_left
(fun nm (type_id, name) ->
- names_map_add_assumed_type id_to_string type_id name nm)
+ names_maps_add_assumed_type id_to_string type_id name nm)
nm init.assumed_adts
in
let nm =
List.fold_left
(fun nm (type_id, name) ->
- names_map_add_assumed_struct id_to_string type_id name nm)
+ names_maps_add_assumed_struct id_to_string type_id name nm)
nm init.assumed_structs
in
let nm =
List.fold_left
(fun nm (type_id, variant_id, name) ->
- names_map_add_assumed_variant id_to_string type_id variant_id name nm)
+ names_maps_add_assumed_variant id_to_string type_id variant_id name nm)
nm init.assumed_variants
in
let assumed_functions =
List.map
- (fun (fid, rg, name) -> (FromLlbc (A.Assumed fid, None, rg), name))
+ (fun (fid, rg, name) ->
+ (FromLlbc (Pure.FunId (Assumed fid), None, rg), name))
init.assumed_llbc_functions
@ 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_maps_add_function id_to_string fid name nm)
nm assumed_functions
in
(* Return *)
@@ -1150,22 +1354,20 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
let rg_suff =
(* TODO: make all the backends match what is done for Lean *)
match rg with
- | None -> (
- match !Config.backend with
- | FStar | Coq | HOL4 -> "_fwd"
- | Lean ->
- (* In order to avoid name conflicts:
- * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
- * - otherwise, no suffix (because the backward functions will have a suffix)
- *)
- if num_backs = 1 && not keep_fwd then "_fwd" else "")
+ | None ->
+ if
+ (* In order to avoid name conflicts:
+ * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
+ * - otherwise, no suffix (because the backward functions will have a suffix)
+ *)
+ num_backs = 1 && not keep_fwd
+ then "_fwd"
+ else ""
| Some rg ->
assert (num_region_groups > 0 && num_backs > 0);
if num_backs = 1 then
(* Exactly one backward function *)
- match !Config.backend with
- | FStar | Coq | HOL4 -> if not keep_fwd then "_fwd_back" else "_back"
- | Lean -> if not keep_fwd then "" else "_back"
+ if not keep_fwd then "" else "_back"
else if
(* Several region groups/backward functions:
- if all the regions in the group have names, we use those names
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 20:55:47 +0000