summaryrefslogtreecommitdiff
path: root/compiler/ExtractBase.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBase.ml1917
1 files changed, 1270 insertions, 647 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 31b1a447..c6158847 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1,14 +1,15 @@
(** Define base utilities for the extraction *)
+open Contexts
open Pure
-open TranslateCore
-module C = Contexts
-module RegionVarId = T.RegionVarId
+open StringUtils
+open Config
module F = Format
open ExtractBuiltin
+open TranslateCore
(** The local logger *)
-let log = L.extract_log
+let log = Logging.extract_log
type region_group_info = {
id : RegionGroupId.id;
@@ -25,11 +26,6 @@ type region_group_info = {
module StringSet = Collections.StringSet
module StringMap = Collections.StringMap
-type name = Names.name
-type type_name = Names.type_name
-type global_name = Names.global_name
-type fun_name = Names.fun_name
-
(** Characterizes a declaration.
Is in particular useful to derive the proper keywords to introduce the
@@ -115,225 +111,6 @@ let decl_is_not_last_from_group (kind : decl_kind) : bool =
type type_decl_kind = Enum | Struct [@@deriving show]
-(* TODO: this should be a module we give to a functor! *)
-
-(** A formatter's role is twofold:
- 1. Come up with name suggestions.
- For instance, provided some information about a function (its basename,
- information about the region group, etc.) it should come up with an
- appropriate name for the forward/backward function.
-
- It can of course apply many transformations, like changing to camel case/
- 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;
- char_name : string;
- int_name : integer_type -> string;
- str_name : string;
- type_decl_kind_to_qualif :
- decl_kind -> type_decl_kind option -> string option;
- (** Compute the qualified for a type definition/declaration.
-
- For instance: "type", "and", etc.
-
- Remark: can return [None] for some backends like HOL4.
- *)
- fun_decl_kind_to_qualif : decl_kind -> string option;
- (** Compute the qualified for a function definition/declaration.
-
- For instance: "let", "let rec", "and", etc.
-
- Remark: can return [None] for some backends like HOL4.
- *)
- field_name : name -> FieldId.id -> string option -> string;
- (** Inputs:
- - type name
- - field id
- - field name
-
- Note that fields don't always have names, but we still need to
- generate some names if we want to extract the structures to records...
- We might want to extract such structures to tuples, later, but field
- access then causes trouble because not all provers accept syntax like
- [x.3] where [x] is a tuple.
- *)
- variant_name : name -> string -> string;
- (** Inputs:
- - type name
- - variant name
- *)
- struct_constructor : name -> string;
- (** Structure constructors are used when constructing structure values.
-
- For instance, in F*:
- {[
- type pair = { x : nat; y : nat }
- let p : pair = Mkpair 0 1
- ]}
-
- Inputs:
- - type name
- *)
- type_name : type_name -> string;
- (** Provided a basename, compute a type name. *)
- global_name : global_name -> string;
- (** Provided a basename, compute a global name. *)
- fun_name :
- fun_name ->
- int ->
- LoopId.id option ->
- int ->
- region_group_info option ->
- bool * int ->
- string;
- (** Compute the name of a regular (non-assumed) function.
-
- Inputs:
- - function basename (TODO: shouldn't appear for assumed functions?...)
- - number of loops in the function (useful to check if we need to use
- indices to derive unique names for the loops for instance - if there is
- exactly one loop, we don't need to use indices)
- - loop id (if pertinent)
- - number of region groups
- - region group information in case of a backward function
- ([None] if forward function)
- - pair:
- - do we generate the forward function (it may have been filtered)?
- - the number of *extracted backward functions* (same comment as for
- the number of loops)
- The number of extracted backward functions if not necessarily
- equal to the number of region groups, because we may have
- filtered some of them.
- TODO: use the fun id for the assumed functions.
- *)
- termination_measure_name :
- A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
- (** Generates the name of the termination measure used to prove/reason about
- termination. The generated code uses this clause where needed,
- but its body must be defined by the user.
-
- F* and Lean only.
-
- Inputs:
- - function id: this is especially useful to identify whether the
- function is an assumed function or a local function
- - function basename
- - the number of loops in the parent function. This is used for
- the same purpose as in {!field:fun_name}.
- - loop identifier, if this is for a loop
- *)
- decreases_proof_name :
- A.FunDeclId.id -> fun_name -> int -> LoopId.id option -> string;
- (** Generates the name of the proof used to prove/reason about
- termination. The generated code uses this clause where needed,
- but its body must be defined by the user.
-
- Lean only.
-
- Inputs:
- - function id: this is especially useful to identify whether the
- function is an assumed function or a local function
- - function basename
- - the number of loops in the parent function. This is used for
- the same purpose as in {!field:fun_name}.
- - loop identifier, if this is for a loop
- *)
- 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.
-
- Inputs:
- - the set of names used in the context so far
- - the basename we got from the symbolic execution, if we have one
- - the type of the variable (can be useful for heuristics, in order
- not to always use "x" for instance, whenever naming anonymous
- variables)
-
- Note that once the formatter generated a basename, we add an index
- if necessary to prevent name clashes: the burden of name clashes checks
- is thus on the caller's side.
- *)
- type_var_basename : StringSet.t -> string -> string;
- (** 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
- indices to names, the responsability of finding a proper index is
- delegated to helper functions.
- *)
- extract_literal : F.formatter -> bool -> literal -> unit;
- (** Format a constant value.
-
- Inputs:
- - formatter
- - [inside]: if [true], the value should be wrapped in parentheses
- if it is made of an application (ex.: [U32 3])
- - the constant value
- *)
- extract_unop :
- (bool -> texpression -> unit) ->
- F.formatter ->
- bool ->
- unop ->
- texpression ->
- unit;
- (** Format a unary operation
-
- Inputs:
- - a formatter for expressions (called on the argument of the unop)
- - extraction context (see below)
- - formatter
- - expression formatter
- - [inside]
- - unop
- - argument
- *)
- extract_binop :
- (bool -> texpression -> unit) ->
- F.formatter ->
- bool ->
- E.binop ->
- integer_type ->
- texpression ->
- texpression ->
- unit;
- (** Format a binary operation
-
- Inputs:
- - a formatter for expressions (called on the arguments of the binop)
- - extraction context (see below)
- - formatter
- - expression formatter
- - [inside]
- - binop
- - argument 0
- - argument 1
- *)
-}
-
(** We use identifiers to look for name clashes *)
type id =
| GlobalId of A.GlobalDeclId.id
@@ -596,6 +373,152 @@ type names_maps = {
*)
}
+(** 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 _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _
+ | TraitMethodId _ ->
+ !Config.record_fields_short_names
+ | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _, _)) ->
+ (* We map several assumed functions to the same id *)
+ true
+ | _ -> false
+
+(** 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 (
+ (* 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;
+ {
+ nm with
+ unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
+ })
+ else
+ (* 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
+ let names_map = names_map_add id_to_string id name nm.names_map in
+ { nm with strict_names_map; names_map }
+
+(** 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 *)
+ 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
+ let m = nm.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: \"" ^ id_to_string id ^ "\")"
+
+type names_map_init = {
+ keywords : string list;
+ assumed_adts : (assumed_ty * string) list;
+ assumed_structs : (assumed_ty * string) list;
+ assumed_variants : (assumed_ty * VariantId.id * string) list;
+ assumed_llbc_functions :
+ (A.assumed_fun_id * RegionGroupId.id option * string) list;
+ assumed_pure_functions : (pure_assumed_fun_id * string) list;
+}
+
+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 (TAssumed 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 (TAssumed id)) name nm
+
+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 (TAssumed 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 bool_name () = if !backend = Lean then "Bool" else "bool"
+let char_name () = if !backend = Lean then "Char" else "char"
+let str_name () = if !backend = Lean then "String" else "string"
+
+(** Small helper to compute the name of an int type *)
+let int_name (int_ty : integer_type) =
+ let isize, usize, i_format, u_format =
+ match !backend with
+ | FStar | Coq | HOL4 ->
+ ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
+ | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
+ in
+ match int_ty with
+ | Isize -> isize
+ | I8 -> Printf.sprintf i_format 8
+ | I16 -> Printf.sprintf i_format 16
+ | I32 -> Printf.sprintf i_format 32
+ | I64 -> Printf.sprintf i_format 64
+ | I128 -> Printf.sprintf i_format 128
+ | Usize -> usize
+ | U8 -> Printf.sprintf u_format 8
+ | U16 -> Printf.sprintf u_format 16
+ | U32 -> Printf.sprintf u_format 32
+ | U64 -> Printf.sprintf u_format 64
+ | U128 -> Printf.sprintf u_format 128
+
(** Extraction context.
Note that the extraction context contains information coming from the
@@ -607,7 +530,6 @@ type extraction_ctx = {
crate : A.crate;
trans_ctx : trans_ctx;
names_maps : names_maps;
- fmt : formatter;
indent_incr : int;
(** The indent increment we insert whenever we need to indent more *)
use_dep_ite : bool;
@@ -654,72 +576,47 @@ type extraction_ctx = {
(** Same as {!types_filter_type_args_map}, but for trait implementations *)
}
+let extraction_ctx_to_fmt_env (ctx : extraction_ctx) : PrintPure.fmt_env =
+ TranslateCore.trans_ctx_to_pure_fmt_env ctx.trans_ctx
+
+let name_to_string (ctx : extraction_ctx) =
+ PrintPure.name_to_string (extraction_ctx_to_fmt_env ctx)
+
+let trait_decl_id_to_string (ctx : extraction_ctx) =
+ PrintPure.trait_decl_id_to_string (extraction_ctx_to_fmt_env ctx)
+
+let type_id_to_string (ctx : extraction_ctx) =
+ PrintPure.type_id_to_string (extraction_ctx_to_fmt_env ctx)
+
+let global_decl_id_to_string (ctx : extraction_ctx) =
+ PrintPure.global_decl_id_to_string (extraction_ctx_to_fmt_env ctx)
+
+let llbc_fun_id_to_string (ctx : extraction_ctx) =
+ PrintPure.llbc_fun_id_to_string (extraction_ctx_to_fmt_env ctx)
+
+let fun_id_to_string (ctx : extraction_ctx) =
+ PrintPure.regular_fun_id_to_string (extraction_ctx_to_fmt_env ctx)
+
+let adt_variant_to_string (ctx : extraction_ctx) =
+ PrintPure.adt_variant_to_string (extraction_ctx_to_fmt_env ctx)
+
+let adt_field_to_string (ctx : extraction_ctx) =
+ PrintPure.adt_field_to_string (extraction_ctx_to_fmt_env ctx)
+
(** Debugging function, used when communicating name collisions to the user,
and also to print ids for internal debugging (in case of lookup miss for
instance).
*)
let id_to_string (id : id) (ctx : extraction_ctx) : string =
- 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
+ let trait_name = trait_decl_id_to_string ctx id 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
- | AdtId id ->
- let def = TypeDeclId.Map.find id type_decls in
- Print.name_to_string def.name
- | Assumed aty -> show_assumed_ty aty
- | Tuple -> raise (Failure "Unreachable")
- in
match id with
- | GlobalId gid ->
- let name = (A.GlobalDeclId.Map.find gid global_decls).name in
- "global name: " ^ Print.global_name_to_string name
- | FunId fid -> (
- match fid with
- | FromLlbc (fid, lp_id, rg_id) ->
- let fun_name =
- match fid with
- | FunId (Regular fid) ->
- Print.fun_name_to_string
- (A.FunDeclId.Map.find fid fun_decls).name
- | 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 =
- match lp_id with
- | None -> ""
- | Some lp_id -> "loop " ^ LoopId.to_string lp_id ^ ", "
- in
-
- let fwd_back_kind =
- match rg_id with
- | None -> "forward"
- | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
- in
- "fun name (" ^ lp_kind ^ fwd_back_kind ^ "): " ^ fun_name
- | Pure fid -> PrintPure.pure_assumed_fun_id_to_string fid)
+ | GlobalId gid -> global_decl_id_to_string ctx gid
+ | FunId fid -> fun_id_to_string ctx fid
| DecreasesProofId (fid, lid) ->
- let fun_name =
- match fid with
- | Regular fid ->
- Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name
- | Assumed aid -> A.show_assumed_fun_id aid
- in
+ let fun_name = llbc_fun_id_to_string ctx fid in
let loop =
match lid with
| None -> ""
@@ -727,72 +624,20 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
in
"decreases proof for function: " ^ fun_name ^ loop
| TerminationMeasureId (fid, lid) ->
- let fun_name =
- match fid with
- | Regular fid ->
- Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name
- | Assumed aid -> A.show_assumed_fun_id aid
- in
+ let fun_name = llbc_fun_id_to_string ctx fid in
let loop =
match lid with
| None -> ""
| Some lid -> ", loop: " ^ LoopId.to_string lid
in
"termination measure for function: " ^ fun_name ^ loop
- | TypeId id -> "type name: " ^ get_type_name id
- | StructId id -> "struct constructor of: " ^ get_type_name id
+ | TypeId id -> "type name: " ^ type_id_to_string ctx id
+ | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id
| VariantId (id, variant_id) ->
- let variant_name =
- match id with
- | Tuple -> raise (Failure "Unreachable")
- | Assumed Result ->
- if variant_id = result_return_id then "@result::Return"
- else if variant_id = result_fail_id then "@result::Fail"
- else raise (Failure "Unreachable")
- | Assumed Error ->
- 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 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 | 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
- | Struct _ | Opaque -> raise (Failure "Unreachable")
- | Enum variants ->
- let variant = VariantId.nth variants variant_id in
- Print.name_to_string def.name ^ "::" ^ variant.variant_name)
- in
+ let variant_name = adt_variant_to_string ctx id (Some variant_id) in
"variant name: " ^ variant_name
| FieldId (id, field_id) ->
- let field_name =
- match id with
- | Tuple -> raise (Failure "Unreachable")
- | Assumed
- (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 -> (
- let def = TypeDeclId.Map.find id type_decls in
- match def.kind with
- | Enum _ | Opaque -> raise (Failure "Unreachable")
- | Struct fields ->
- let field = FieldId.nth fields field_id in
- let field_name =
- match field.field_name with
- | None -> FieldId.to_string field_id
- | Some name -> name
- in
- Print.name_to_string def.name ^ "." ^ field_name)
- in
+ let field_name = adt_field_to_string ctx id field_id in
"field name: " ^ field_name
| UnknownId -> "keyword"
| TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
@@ -824,125 +669,15 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
^ ", 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 _ | 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
-
-(** 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 (
- (* 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;
- {
- nm with
- unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
- })
- else
- (* 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
- 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 }
-(** 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 *)
- 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
- let m = nm.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: \"" ^ 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 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
@@ -951,17 +686,17 @@ let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string =
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
+ ctx_get_function (FromLlbc (FunId (FRegular id), lp, rg)) ctx
let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
- assert (id <> Tuple);
+ assert (id <> TTuple);
ctx_get (TypeId id) ctx
let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
- ctx_get_type (AdtId id) ctx
+ ctx_get_type (TAdtId id) ctx
let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
- ctx_get_type (Assumed id) ctx
+ ctx_get_type (TAssumed id) ctx
let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) :
string =
@@ -1027,21 +762,1043 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
let ctx_get_decreases_proof (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx
+ ctx_get (DecreasesProofId (FRegular def_id, loop_id)) ctx
let ctx_get_termination_measure (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx
+ ctx_get (TerminationMeasureId (FRegular def_id, loop_id)) ctx
+
+(** Small helper to compute the name of a unary operation *)
+let unop_name (unop : unop) : string =
+ match unop with
+ | Not -> (
+ match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~")
+ | Neg (int_ty : integer_type) -> (
+ match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg")
+ | Cast _ ->
+ (* We never directly use the unop name in this case *)
+ raise (Failure "Unsupported")
+
+(** Small helper to compute the name of a binary operation (note that many
+ binary operations like "less than" are extracted to primitive operations,
+ like [<]).
+ *)
+let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
+ let binop =
+ match binop with
+ | Div -> "div"
+ | Rem -> "rem"
+ | Add -> "add"
+ | Sub -> "sub"
+ | Mul -> "mul"
+ | Lt -> "lt"
+ | Le -> "le"
+ | Ge -> "ge"
+ | Gt -> "gt"
+ | BitXor -> "xor"
+ | BitAnd -> "and"
+ | BitOr -> "or"
+ | Shl -> "lsl"
+ | Shr ->
+ "asr"
+ (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *)
+ | _ -> raise (Failure "Unreachable")
+ in
+ (* Remark: the Lean case is actually not used *)
+ match !backend with
+ | Lean -> int_name int_ty ^ "." ^ binop
+ | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop
+
+(** A list of keywords/identifiers used by the backend and with which we
+ want to check collision.
+
+ Remark: this is useful mostly to look for collisions when generating
+ names for *variables*.
+ *)
+let keywords () =
+ let named_unops =
+ unop_name Not
+ :: List.map (fun it -> unop_name (Neg it)) T.all_signed_int_types
+ in
+ let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
+ let named_binops =
+ List.concat_map
+ (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
+ named_binops
+ in
+ let misc =
+ match !backend with
+ | FStar ->
+ [
+ "assert";
+ "assert_norm";
+ "assume";
+ "else";
+ "fun";
+ "fn";
+ "FStar";
+ "FStar.Mul";
+ "if";
+ "in";
+ "include";
+ "int";
+ "let";
+ "list";
+ "match";
+ "open";
+ "rec";
+ "scalar_cast";
+ "then";
+ "type";
+ "Type0";
+ "Type";
+ "unit";
+ "val";
+ "with";
+ ]
+ | Coq ->
+ [
+ "assert";
+ "Arguments";
+ "Axiom";
+ "char_of_byte";
+ "Check";
+ "Declare";
+ "Definition";
+ "else";
+ "End";
+ "fun";
+ "Fixpoint";
+ "if";
+ "in";
+ "int";
+ "Inductive";
+ "Import";
+ "let";
+ "Lemma";
+ "match";
+ "Module";
+ "not";
+ "Notation";
+ "Proof";
+ "Qed";
+ "rec";
+ "Record";
+ "Require";
+ "Scope";
+ "Search";
+ "SearchPattern";
+ "Set";
+ "then";
+ (* [tt] is unit *)
+ "tt";
+ "type";
+ "Type";
+ "unit";
+ "with";
+ ]
+ | Lean ->
+ [
+ "by";
+ "class";
+ "decreasing_by";
+ "def";
+ "deriving";
+ "do";
+ "else";
+ "end";
+ "for";
+ "have";
+ "if";
+ "inductive";
+ "instance";
+ "import";
+ "let";
+ "macro";
+ "match";
+ "namespace";
+ "opaque";
+ "open";
+ "run_cmd";
+ "set_option";
+ "simp";
+ "structure";
+ "syntax";
+ "termination_by";
+ "then";
+ "Type";
+ "unsafe";
+ "where";
+ "with";
+ "opaque_defs";
+ ]
+ | HOL4 ->
+ [
+ "Axiom";
+ "case";
+ "Definition";
+ "else";
+ "End";
+ "fix";
+ "fix_exec";
+ "fn";
+ "fun";
+ "if";
+ "in";
+ "int";
+ "Inductive";
+ "let";
+ "of";
+ "Proof";
+ "QED";
+ "then";
+ "Theorem";
+ ]
+ in
+ List.concat [ named_unops; named_binops; misc ]
+
+let assumed_adts () : (assumed_ty * string) list =
+ match !backend with
+ | Lean ->
+ [
+ (TState, "State");
+ (TResult, "Result");
+ (TError, "Error");
+ (TFuel, "Nat");
+ (TArray, "Array");
+ (TSlice, "Slice");
+ (TStr, "Str");
+ (TRawPtr Mut, "MutRawPtr");
+ (TRawPtr Const, "ConstRawPtr");
+ ]
+ | Coq | FStar | HOL4 ->
+ [
+ (TState, "state");
+ (TResult, "result");
+ (TError, "error");
+ (TFuel, if !backend = HOL4 then "num" else "nat");
+ (TArray, "array");
+ (TSlice, "slice");
+ (TStr, "str");
+ (TRawPtr Mut, "mut_raw_ptr");
+ (TRawPtr Const, "const_raw_ptr");
+ ]
+
+let assumed_struct_constructors () : (assumed_ty * string) list =
+ match !backend with
+ | Lean -> [ (TArray, "Array.make") ]
+ | Coq -> [ (TArray, "mk_array") ]
+ | FStar -> [ (TArray, "mk_array") ]
+ | HOL4 -> [ (TArray, "mk_array") ]
+
+let assumed_variants () : (assumed_ty * VariantId.id * string) list =
+ match !backend with
+ | FStar ->
+ [
+ (TResult, result_return_id, "Return");
+ (TResult, result_fail_id, "Fail");
+ (TError, error_failure_id, "Failure");
+ (TError, error_out_of_fuel_id, "OutOfFuel");
+ (* No Fuel::Zero on purpose *)
+ (* No Fuel::Succ on purpose *)
+ ]
+ | Coq ->
+ [
+ (TResult, result_return_id, "Return");
+ (TResult, result_fail_id, "Fail_");
+ (TError, error_failure_id, "Failure");
+ (TError, error_out_of_fuel_id, "OutOfFuel");
+ (TFuel, fuel_zero_id, "O");
+ (TFuel, fuel_succ_id, "S");
+ ]
+ | Lean ->
+ [
+ (TResult, result_return_id, "ret");
+ (TResult, result_fail_id, "fail");
+ (TError, error_failure_id, "panic");
+ (* No Fuel::Zero on purpose *)
+ (* No Fuel::Succ on purpose *)
+ ]
+ | HOL4 ->
+ [
+ (TResult, result_return_id, "Return");
+ (TResult, result_fail_id, "Fail");
+ (TError, error_failure_id, "Failure");
+ (* No Fuel::Zero on purpose *)
+ (* No Fuel::Succ on purpose *)
+ ]
+
+let assumed_llbc_functions () :
+ (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+ let rg0 = Some T.RegionGroupId.zero in
+ match !backend with
+ | FStar | Coq | HOL4 ->
+ [
+ (ArrayIndexShared, None, "array_index_usize");
+ (ArrayIndexMut, None, "array_index_usize");
+ (ArrayIndexMut, rg0, "array_update_usize");
+ (ArrayToSliceShared, None, "array_to_slice");
+ (ArrayToSliceMut, None, "array_to_slice");
+ (ArrayToSliceMut, rg0, "array_from_slice");
+ (ArrayRepeat, None, "array_repeat");
+ (SliceIndexShared, None, "slice_index_usize");
+ (SliceIndexMut, None, "slice_index_usize");
+ (SliceIndexMut, rg0, "slice_update_usize");
+ ]
+ | Lean ->
+ [
+ (ArrayIndexShared, None, "Array.index_usize");
+ (ArrayIndexMut, None, "Array.index_usize");
+ (ArrayIndexMut, rg0, "Array.update_usize");
+ (ArrayToSliceShared, None, "Array.to_slice");
+ (ArrayToSliceMut, None, "Array.to_slice");
+ (ArrayToSliceMut, rg0, "Array.from_slice");
+ (ArrayRepeat, None, "Array.repeat");
+ (SliceIndexShared, None, "Slice.index_usize");
+ (SliceIndexMut, None, "Slice.index_usize");
+ (SliceIndexMut, rg0, "Slice.update_usize");
+ ]
+
+let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
+ match !backend with
+ | FStar ->
+ [
+ (Return, "return");
+ (Fail, "fail");
+ (Assert, "massert");
+ (FuelDecrease, "decrease");
+ (FuelEqZero, "is_zero");
+ ]
+ | Coq ->
+ (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+ [ (Return, "return_"); (Fail, "fail_"); (Assert, "massert") ]
+ | Lean ->
+ (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+ [ (Return, "return"); (Fail, "fail_"); (Assert, "massert") ]
+ | HOL4 ->
+ (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+ [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+
+let names_map_init () : names_map_init =
+ {
+ keywords = keywords ();
+ assumed_adts = assumed_adts ();
+ assumed_structs = assumed_struct_constructors ();
+ assumed_variants = assumed_variants ();
+ assumed_llbc_functions = assumed_llbc_functions ();
+ assumed_pure_functions = assumed_pure_functions ();
+ }
+
+(** Initialize names maps with a proper set of keywords/names coming from the
+ target language/prover. *)
+let initialize_names_maps () : names_maps =
+ let init = names_map_init () in
+ let int_names = List.map int_name T.all_int_types in
+ let keywords =
+ List.concat
+ [ [ bool_name (); char_name (); str_name () ]; int_names; init.keywords ]
+ 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 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
+ * - the assumed variants
+ * - the assumed functions
+ *)
+ let nm =
+ List.fold_left
+ (fun nm (type_id, name) ->
+ 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_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_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 (Pure.FunId (FAssumed fid), None, rg), name))
+ init.assumed_llbc_functions
+ @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+ in
+ let nm =
+ List.fold_left
+ (fun nm (fid, name) -> names_maps_add_function id_to_string fid name nm)
+ nm assumed_functions
+ in
+ (* Return *)
+ nm
+
+(** Compute the qualified for a type definition/declaration.
+
+ For instance: "type", "and", etc.
+
+ Remark: can return [None] for some backends like HOL4.
+ *)
+let type_decl_kind_to_qualif (kind : decl_kind)
+ (type_kind : type_decl_kind option) : string option =
+ match !backend with
+ | FStar -> (
+ match kind with
+ | SingleNonRec -> Some "type"
+ | SingleRec -> Some "type"
+ | MutRecFirst -> Some "type"
+ | MutRecInner -> Some "and"
+ | MutRecLast -> Some "and"
+ | Assumed -> Some "assume type"
+ | Declared -> Some "val")
+ | Coq -> (
+ match (kind, type_kind) with
+ | SingleNonRec, Some Enum -> Some "Inductive"
+ | SingleNonRec, Some Struct -> Some "Record"
+ | (SingleRec | MutRecFirst), Some _ -> Some "Inductive"
+ | (MutRecInner | MutRecLast), Some _ ->
+ (* Coq doesn't support groups of mutually recursive definitions which mix
+ * records and inducties: we convert everything to records if this happens
+ *)
+ Some "with"
+ | (Assumed | Declared), None -> Some "Axiom"
+ | SingleNonRec, None ->
+ (* This is for traits *)
+ Some "Record"
+ | _ ->
+ raise
+ (Failure
+ ("Unexpected: (" ^ show_decl_kind kind ^ ", "
+ ^ Print.option_to_string show_type_decl_kind type_kind
+ ^ ")")))
+ | Lean -> (
+ match kind with
+ | SingleNonRec ->
+ if type_kind = Some Struct then Some "structure" else Some "inductive"
+ | SingleRec -> Some "inductive"
+ | MutRecFirst -> Some "inductive"
+ | MutRecInner -> Some "inductive"
+ | MutRecLast -> Some "inductive"
+ | Assumed -> Some "axiom"
+ | Declared -> Some "axiom")
+ | HOL4 -> None
+
+(** Compute the qualified for a function definition/declaration.
+
+ For instance: "let", "let rec", "and", etc.
+
+ Remark: can return [None] for some backends like HOL4.
+ *)
+let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
+ match !backend with
+ | FStar -> (
+ match kind with
+ | SingleNonRec -> Some "let"
+ | SingleRec -> Some "let rec"
+ | MutRecFirst -> Some "let rec"
+ | MutRecInner -> Some "and"
+ | MutRecLast -> Some "and"
+ | Assumed -> Some "assume val"
+ | Declared -> Some "val")
+ | Coq -> (
+ match kind with
+ | SingleNonRec -> Some "Definition"
+ | SingleRec -> Some "Fixpoint"
+ | MutRecFirst -> Some "Fixpoint"
+ | MutRecInner -> Some "with"
+ | MutRecLast -> Some "with"
+ | Assumed -> Some "Axiom"
+ | Declared -> Some "Axiom")
+ | Lean -> (
+ match kind with
+ | SingleNonRec -> Some "def"
+ | SingleRec -> Some "divergent def"
+ | MutRecFirst -> Some "mutual divergent def"
+ | MutRecInner -> Some "divergent def"
+ | MutRecLast -> Some "divergent def"
+ | Assumed -> Some "axiom"
+ | Declared -> Some "axiom")
+ | HOL4 -> None
+
+(** The type of types.
+
+ TODO: move inside the formatter?
+ *)
+let type_keyword () =
+ match !backend with
+ | FStar -> "Type0"
+ | Coq | Lean -> "Type"
+ | HOL4 -> raise (Failure "Unexpected")
+
+(** Helper *)
+let name_last_elem_as_ident (n : llbc_name) : string =
+ match Collections.List.last n with
+ | PeIdent (s, _) -> s
+ | PeImpl _ -> raise (Failure "Unexpected")
+
+(** Helper
+
+ Prepare a name.
+ The first id elem is always the crate: if it is the local crate,
+ we remove it. We ignore disambiguators (there may be collisions, but we
+ check if there are).
+ *)
+let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
+ string list =
+ (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+ match name with
+ | (PeIdent (crate, _) as id) :: name ->
+ let name = if crate = ctx.crate.name then name else id :: name in
+ name_to_simple_name ctx.trans_ctx name
+ | _ ->
+ raise
+ (Failure
+ ("Unexpected name shape: "
+ ^ TranslateCore.name_to_string ctx.trans_ctx name))
+
+(** Helper *)
+let ctx_compute_simple_type_name = ctx_compute_simple_name
+
+(** Helper *)
+let ctx_compute_type_name_no_suffix (ctx : extraction_ctx) (name : llbc_name) :
+ string =
+ flatten_name (ctx_compute_simple_type_name ctx name)
+
+(** Provided a basename, compute a type name. *)
+let ctx_compute_type_name (ctx : extraction_ctx) (name : llbc_name) =
+ let name = ctx_compute_type_name_no_suffix ctx name in
+ match !backend with
+ | FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
+ | Coq | HOL4 -> name ^ "_t"
+ | Lean -> name
+
+(** Inputs:
+ - type name
+ - field id
+ - field name
+
+ Note that fields don't always have names, but we still need to
+ generate some names if we want to extract the structures to records...
+ We might want to extract such structures to tuples, later, but field
+ access then causes trouble because not all provers accept syntax like
+ [x.3] where [x] is a tuple.
+ *)
+let ctx_compute_field_name (ctx : extraction_ctx) (def_name : llbc_name)
+ (field_id : FieldId.id) (field_name : string option) : string =
+ let field_name_s =
+ match field_name with
+ | Some field_name -> field_name
+ | None ->
+ (* TODO: extract structs with no field names to tuples *)
+ FieldId.to_string field_id
+ in
+ if !Config.record_fields_short_names then
+ if field_name = None then (* TODO: this is a bit ugly *)
+ "_" ^ field_name_s
+ else field_name_s
+ else
+ let def_name =
+ ctx_compute_type_name_no_suffix ctx def_name ^ "_" ^ field_name_s
+ in
+ match !backend with
+ | Lean | HOL4 -> def_name
+ | Coq | FStar -> StringUtils.lowercase_first_letter def_name
+
+(** Inputs:
+ - type name
+ - variant name
+ *)
+let ctx_compute_variant_name (ctx : extraction_ctx) (def_name : llbc_name)
+ (variant : string) : string =
+ match !backend with
+ | FStar | Coq | HOL4 ->
+ let variant = to_camel_case variant in
+ if !variant_concatenate_type_name then
+ StringUtils.capitalize_first_letter
+ (ctx_compute_type_name_no_suffix ctx def_name ^ "_" ^ variant)
+ else variant
+ | Lean -> variant
+
+(** Structure constructors are used when constructing structure values.
+
+ For instance, in F*:
+ {[
+ type pair = { x : nat; y : nat }
+ let p : pair = Mkpair 0 1
+ ]}
+
+ Inputs:
+ - type name
+*)
+let ctx_compute_struct_constructor (ctx : extraction_ctx) (basename : llbc_name)
+ : string =
+ let tname = ctx_compute_type_name ctx basename in
+ ExtractBuiltin.mk_struct_constructor tname
+
+let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) :
+ string =
+ let fname = ctx_compute_simple_name ctx fname in
+ (* TODO: don't convert to snake case for Coq, HOL4, F* *)
+ let fname = flatten_name fname in
+ match !backend with
+ | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
+ | Lean -> fname
+
+(** Provided a basename, compute the name of a global declaration. *)
+let ctx_compute_global_name (ctx : extraction_ctx) (name : llbc_name) : string =
+ (* Converting to snake case also lowercases the letters (in Rust, global
+ * names are written in capital letters). *)
+ let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in
+ String.concat "_" parts
+
+(** Helper function: generate a suffix for a function name, i.e., generates
+ a suffix like "_loop", "loop1", etc. to append to a function name.
+ *)
+let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
+ string =
+ match loop_id with
+ | None -> ""
+ | Some loop_id ->
+ (* If this is for a loop, generally speaking, we append the loop index.
+ If this function admits only one loop, we omit it. *)
+ if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
+
+(** A helper function: generates a function suffix from a region group
+ information.
+ TODO: move all those helpers.
+*)
+let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
+ (num_region_groups : int) (rg : region_group_info option)
+ ((keep_fwd, num_backs) : bool * int) : string =
+ let lp_suff = default_fun_loop_suffix num_loops loop_id in
+
+ (* There are several cases:
+ - [rg] is [Some]: this is a forward function:
+ - we add "_fwd"
+ - [rg] is [None]: this is a backward function:
+ - this function has one extracted backward function:
+ - if the forward function has been filtered, we add "_fwd_back":
+ the forward function is useless, so the unique backward function
+ takes its place, in a way
+ - otherwise we add "_back"
+ - this function has several backward functions: we add "_back" and an
+ additional suffix to identify the precise backward function
+ Note that we always add a suffix (in case there are no region groups,
+ we could not add the "_fwd" suffix) to prevent name clashes between
+ definitions (in particular between type and function definitions).
+ *)
+ let rg_suff =
+ (* TODO: make all the backends match what is done for Lean *)
+ match rg with
+ | 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 *)
+ 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
+ - otherwise we use an index
+ *)
+ List.for_all Option.is_some rg.region_names
+ then
+ (* Concatenate the region names *)
+ "_back" ^ String.concat "" (List.map Option.get rg.region_names)
+ else (* Use the region index *)
+ "_back" ^ RegionGroupId.to_string rg.id
+ in
+ lp_suff ^ rg_suff
+
+(** Compute the name of a regular (non-assumed) function.
+
+ Inputs:
+ - function basename (TODO: shouldn't appear for assumed functions?...)
+ - number of loops in the function (useful to check if we need to use
+ indices to derive unique names for the loops for instance - if there is
+ exactly one loop, we don't need to use indices)
+ - loop id (if pertinent)
+ - number of region groups
+ - region group information in case of a backward function
+ ([None] if forward function)
+ - pair:
+ - do we generate the forward function (it may have been filtered)?
+ - the number of *extracted backward functions* (same comment as for
+ the number of loops)
+ The number of extracted backward functions if not necessarily
+ equal to the number of region groups, because we may have
+ filtered some of them.
+ TODO: use the fun id for the assumed functions.
+ *)
+let ctx_compute_fun_name (ctx : extraction_ctx) (fname : llbc_name)
+ (num_loops : int) (loop_id : LoopId.id option) (num_rgs : int)
+ (rg : region_group_info option) (filter_info : bool * int) : string =
+ let fname = ctx_compute_fun_name_no_suffix ctx fname in
+ (* Compute the suffix *)
+ let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
+ (* Concatenate *)
+ fname ^ suffix
+
+let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
+ : string =
+ ctx_compute_type_name ctx trait_decl.llbc_name
+
+let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
+ (trait_impl : trait_impl) : string =
+ (* We derive the trait impl name from the implemented trait.
+ For instance, if this implementation is an instance of `trait::Trait`
+ for `<foo::Foo, u32>`, we generate the name: "trait.TraitFooFooU32Inst".
+ Importantly, it is to be noted that the name is independent of the place
+ where the instance has been defined (it is indepedent of the file, etc.).
+ *)
+ let name =
+ let params = trait_impl.llbc_generics in
+ let args = trait_impl.llbc_impl_trait.decl_generics in
+ trait_name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name
+ params args
+ in
+ let name = flatten_name name in
+ match !backend with
+ | FStar -> StringUtils.lowercase_first_letter name
+ | Coq | HOL4 | Lean -> name
+
+let ctx_compute_trait_decl_constructor (ctx : extraction_ctx)
+ (trait_decl : trait_decl) : string =
+ let name = ctx_compute_trait_decl_name ctx trait_decl in
+ ExtractBuiltin.mk_struct_constructor name
+
+(** Helper to derive names for parent trait clauses and for variables
+ for trait instances.
+
+ We derive the name from the type of the clause (i.e., the trait ref
+ the clause implements).
+ For instance, if a trait clause is for the trait ref "Trait<Box<usize>",
+ we generate a name like "traitBoxUsizeInst". This is more meaningful
+ that giving it a generic name with an index (such as "parent_clause_1"
+ or "inst3").
+
+ Because we want to be precise when deriving the name, we use the
+ original LLBC types, that is the types from before the translation
+ to pure, which simplifies types like boxes and references.
+ *)
+let ctx_compute_trait_clause_name (ctx : extraction_ctx)
+ (current_def_name : Types.name) (params : Types.generic_params)
+ (clauses : Types.trait_clause list) (clause_id : trait_clause_id) : string =
+ (* We derive the name of the clause from the trait instance.
+ For instance, if the clause gives us an instance of `Foo<u32>`,
+ we generate a name along the lines of "fooU32Inst".
+ *)
+ let clause =
+ (* If the current def and the trait decl referenced by the clause
+ are in the same namespace, we try to simplify the names. We do so by
+ removing the common prefixes in their names.
+
+ For instance, if we have:
+ {[
+ // This is file traits.rs
+ trait Parent {}
+
+ trait Child : Parent {}
+ ]}
+ For the parent clause of trait [Child] we would like to generate
+ the name: "ParentInst", rather than "traitParentInst".
+ *)
+ let prefix = Some current_def_name in
+ let clause =
+ List.find
+ (fun (c : Types.trait_clause) -> c.clause_id = clause_id)
+ clauses
+ in
+ let trait_id = clause.trait_id in
+ let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
+ let args = clause.clause_generics in
+ trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
+ impl_trait_decl.name params args
+ in
+ String.concat "" clause
+
+let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
+ (trait_decl : trait_decl) (clause : trait_clause) : string =
+ (* We derive the name of the clause from the trait instance.
+ For instance, if the clause gives us an instance of `Foo<u32>`,
+ we generate a name along the lines of "fooU32Inst".
+ *)
+ (* We need to lookup the LLBC definitions, to have the original instantiation *)
+ let clause =
+ let current_def_name = trait_decl.llbc_name in
+ let params = trait_decl.llbc_generics in
+ ctx_compute_trait_clause_name ctx current_def_name params
+ trait_decl.llbc_parent_clauses clause.clause_id
+ in
+ let clause =
+ if !Config.record_fields_short_names then clause
+ else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
+ in
+ match !backend with
+ | FStar -> StringUtils.lowercase_first_letter clause
+ | Coq | HOL4 | Lean -> clause
+
+let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
+ (item : string) : string =
+ let name =
+ if !Config.record_fields_short_names then item
+ else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
+ in
+ (* Constants are usually all capital letters.
+ Some backends do not support field names starting with a capital letter,
+ and it may be weird to lowercase everything (especially as it may lead
+ to more name collisions): we add a prefix when necessary.
+ For instance, it gives: "U" -> "tU"
+ Note that for some backends we prepend the type name (because those backends
+ can't disambiguate fields coming from different ADTs if they have the same
+ names), and thus don't need to add a prefix starting with a lowercase.
+ *)
+ match !backend with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+
+let ctx_compute_trait_const_name (ctx : extraction_ctx)
+ (trait_decl : trait_decl) (item : string) : string =
+ let name =
+ if !Config.record_fields_short_names then item
+ else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
+ in
+ (* See [trait_type_name] *)
+ match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+
+let ctx_compute_trait_method_name (ctx : extraction_ctx)
+ (trait_decl : trait_decl) (item : string) : string =
+ if !Config.record_fields_short_names then item
+ else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
+
+let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
+ (trait_decl : trait_decl) (item : string) (clause : trait_clause) : string =
+ (* TODO: improve - it would be better to not use indices *)
+ ctx_compute_trait_type_name ctx trait_decl item
+ ^ "_clause_"
+ ^ TraitClauseId.to_string clause.clause_id
+
+(** Generates the name of the termination measure used to prove/reason about
+ termination. The generated code uses this clause where needed,
+ but its body must be defined by the user.
+
+ F* and Lean only.
+
+ Inputs:
+ - function id: this is especially useful to identify whether the
+ function is an assumed function or a local function
+ - function basename
+ - the number of loops in the parent function. This is used for
+ the same purpose as in {!field:llbc_name}.
+ - loop identifier, if this is for a loop
+ *)
+let ctx_compute_termination_measure_name (ctx : extraction_ctx)
+ (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int)
+ (loop_id : LoopId.id option) : string =
+ let fname = ctx_compute_fun_name_no_suffix ctx fname in
+ let lp_suffix = default_fun_loop_suffix num_loops loop_id in
+ (* Compute the suffix *)
+ let suffix =
+ match !Config.backend with
+ | FStar -> "_decreases"
+ | Lean -> "_terminates"
+ | Coq | HOL4 -> raise (Failure "Unexpected")
+ in
+ (* Concatenate *)
+ fname ^ lp_suffix ^ suffix
+
+(** Generates the name of the proof used to prove/reason about
+ termination. The generated code uses this clause where needed,
+ but its body must be defined by the user.
+
+ Lean only.
+
+ Inputs:
+ - function id: this is especially useful to identify whether the
+ function is an assumed function or a local function
+ - function basename
+ - the number of loops in the parent function. This is used for
+ the same purpose as in {!field:llbc_name}.
+ - loop identifier, if this is for a loop
+ *)
+let ctx_compute_decreases_proof_name (ctx : extraction_ctx)
+ (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int)
+ (loop_id : LoopId.id option) : string =
+ let fname = ctx_compute_fun_name_no_suffix ctx fname in
+ let lp_suffix = default_fun_loop_suffix num_loops loop_id in
+ (* Compute the suffix *)
+ let suffix =
+ match !Config.backend with
+ | Lean -> "_decreases"
+ | FStar | Coq | HOL4 -> raise (Failure "Unexpected")
+ in
+ (* Concatenate *)
+ fname ^ lp_suffix ^ suffix
+
+(** Generates a variable basename.
+
+ Inputs:
+ - the set of names used in the context so far
+ - the basename we got from the symbolic execution, if we have one
+ - the type of the variable (can be useful for heuristics, in order
+ not to always use "x" for instance, whenever naming anonymous
+ variables)
+
+ Note that once the formatter generated a basename, we add an index
+ if necessary to prevent name clashes: the burden of name clashes checks
+ is thus on the caller's side.
+ *)
+let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option)
+ (ty : ty) : string =
+ (* Small helper to derive var names from ADT type names.
+
+ We do the following:
+ - convert the type name to snake case
+ - take the first letter of every "letter group"
+ Ex.: "HashMap" -> "hash_map" -> "hm"
+ *)
+ let name_from_type_ident (name : string) : string =
+ let cl = to_snake_case name in
+ let cl = String.split_on_char '_' cl in
+ let cl = List.filter (fun s -> String.length s > 0) cl in
+ assert (List.length cl > 0);
+ let cl = List.map (fun s -> s.[0]) cl in
+ StringUtils.string_of_chars cl
+ in
+ (* If there is a basename, we use it *)
+ match basename with
+ | Some basename ->
+ (* This should be a no-op *)
+ to_snake_case basename
+ | None -> (
+ (* No basename: we use the first letter of the type *)
+ match ty with
+ | TAdt (type_id, generics) -> (
+ match type_id with
+ | TTuple ->
+ (* The "pair" case is frequent enough to have its special treatment *)
+ if List.length generics.types = 2 then "p" else "t"
+ | TAssumed TResult -> "r"
+ | TAssumed TError -> ConstStrings.error_basename
+ | TAssumed TFuel -> ConstStrings.fuel_basename
+ | TAssumed TArray -> "a"
+ | TAssumed TSlice -> "s"
+ | TAssumed TStr -> "s"
+ | TAssumed TState -> ConstStrings.state_basename
+ | TAssumed (TRawPtr _) -> "p"
+ | TAdtId adt_id ->
+ let def =
+ TypeDeclId.Map.find adt_id ctx.trans_ctx.type_ctx.type_decls
+ in
+ (* Derive the var name from the last ident of the type name
+ Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
+ *)
+ (* The name shouldn't be empty, and its last element should
+ * be an ident *)
+ let cl = Collections.List.last def.name in
+ name_from_type_ident (TypesUtils.as_ident cl))
+ | TVar _ -> (
+ (* TODO: use "t" also for F* *)
+ match !backend with
+ | FStar -> "x" (* lacking inspiration here... *)
+ | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
+ | TLiteral lty -> (
+ match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
+ | TArrow _ -> "f"
+ | TTraitType (_, _, name) -> name_from_type_ident name)
+
+(** Generates a type variable basename. *)
+let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
+ string =
+ (* Rust type variables are snake-case and start with a capital letter *)
+ match !backend with
+ | FStar ->
+ (* This is *not* a no-op: this removes the capital letter *)
+ to_snake_case basename
+ | HOL4 ->
+ (* In HOL4, type variable names must start with "'" *)
+ "'" ^ to_snake_case basename
+ | Coq | Lean -> basename
+
+(** Generates a const generic variable basename. *)
+let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx)
+ (basename : string) : string =
+ (* Rust type variables are snake-case and start with a capital letter *)
+ match !backend with
+ | FStar | HOL4 ->
+ (* This is *not* a no-op: this removes the capital letter *)
+ to_snake_case basename
+ | Coq | Lean -> basename
+
+(** 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.
+ *)
+let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
+ (current_def_name : Types.name) (params : Types.generic_params)
+ (clause_id : trait_clause_id) : string =
+ (* This is similar to {!ctx_compute_trait_parent_clause_name}: we
+ derive the name from the trait reference (i.e., from the type) *)
+ let clause =
+ ctx_compute_trait_clause_name ctx current_def_name params
+ params.trait_clauses clause_id
+ in
+ match !backend with
+ | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
+ | Lean -> clause
+
+let trait_self_clause_basename = "self_clause"
+
+(** 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
+ indices to names, the responsability of finding a proper index is
+ delegated to helper functions.
+ *)
+let name_append_index (basename : string) (i : int) : string =
+ basename ^ string_of_int i
(** 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 name = ctx_compute_type_var_basename ctx basename in
let 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
+ basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
in
let ctx = ctx_add (TypeVarId id) name ctx in
(ctx, name)
@@ -1049,13 +1806,9 @@ let ctx_add_type_var (basename : string) (id : TypeVarId.id)
(** 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 name = ctx_compute_const_generic_var_basename ctx basename in
let name =
- ctx.fmt.const_generic_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
+ basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
in
let ctx = ctx_add (ConstGenericVarId id) name ctx in
(ctx, name)
@@ -1071,7 +1824,7 @@ let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
extraction_ctx * string =
let name =
- basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+ basename_to_unique ctx.names_maps.names_map.names_set name_append_index
basename
in
let ctx = ctx_add (VarId id) name ctx in
@@ -1079,9 +1832,9 @@ let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
(** 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 basename = trait_self_clause_basename in
let name =
- basename_to_unique ctx.names_maps.names_map.names_set ctx.fmt.append_index
+ basename_to_unique ctx.names_maps.names_map.names_set name_append_index
basename
in
let ctx = ctx_add TraitSelfClauseId name ctx in
@@ -1091,7 +1844,7 @@ let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string =
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_to_unique ctx.names_maps.names_map.names_set name_append_index
basename
in
let ctx = ctx_add (LocalTraitClauseId id) name ctx in
@@ -1102,9 +1855,7 @@ 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_maps.names_map.names_set v.basename v.ty
- in
+ let name = ctx_compute_var_basename ctx v.basename v.ty in
ctx_add_var name v.id ctx)
ctx vars
@@ -1121,12 +1872,23 @@ 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_local_trait_clauses (clauses : trait_clause list)
+(** Returns the lists of names for:
+ - the type variables
+ - the const generic variables
+ - the trait clauses
+
+ For the [current_name_def] and the [llbc_generics]: we use them to derive
+ pretty names for the trait clauses. See {!ctx_compute_trait_clause_name}
+ for additional information.
+ *)
+let ctx_add_local_trait_clauses (current_def_name : Types.name)
+ (llbc_generics : Types.generic_params) (clauses : trait_clause list)
(ctx : extraction_ctx) : extraction_ctx * string list =
List.fold_left_map
(fun ctx (c : trait_clause) ->
let basename =
- ctx.fmt.trait_clause_basename ctx.names_maps.names_map.names_set c
+ ctx_compute_trait_clause_basename ctx current_def_name llbc_generics
+ c.clause_id
in
ctx_add_local_trait_clause basename c.clause_id ctx)
ctx clauses
@@ -1135,30 +1897,38 @@ let ctx_add_local_trait_clauses (clauses : trait_clause list)
- the type variables
- the const generic variables
- the trait clauses
+
+ For the [current_name_def] and the [llbc_generics]: we use them to derive
+ pretty names for the trait clauses. See {!ctx_compute_trait_clause_name}
+ for additional information.
*)
-let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
+let ctx_add_generic_params (current_def_name : Types.name)
+ (llbc_generics : Types.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
+ let ctx, tcs =
+ ctx_add_local_trait_clauses current_def_name llbc_generics trait_clauses ctx
+ in
(ctx, tys, cgs, tcs)
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let name =
- ctx.fmt.decreases_proof_name def.def_id def.basename def.num_loops
+ ctx_compute_decreases_proof_name ctx def.def_id def.llbc_name def.num_loops
def.loop_id
in
- ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx
+ ctx_add (DecreasesProofId (FRegular def.def_id, def.loop_id)) name ctx
let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let name =
- ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops
- def.loop_id
+ ctx_compute_termination_measure_name ctx def.def_id def.llbc_name
+ def.num_loops def.loop_id
in
- ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx
+ ctx_add (TerminationMeasureId (FRegular def.def_id, def.loop_id)) name ctx
let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
extraction_ctx =
@@ -1168,15 +1938,14 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
(* 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
+ match match_name_find_opt ctx.trans_ctx def.name 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 name = ctx_compute_global_name ctx def.name in
+ let body = FunId (FromLlbc (FunId (FRegular def.body), None, None)) in
let ctx = ctx_add decl (name ^ "_c") ctx in
let ctx = ctx_add body (name ^ "_body") ctx in
ctx
@@ -1187,24 +1956,28 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
let def_id = def.def_id 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 regions_hierarchy =
+ LlbcAstUtils.FunIdMap.find (FRegular def_id)
+ ctx.trans_ctx.fun_ctx.regions_hierarchies
+ in
+ let num_rgs = List.length regions_hierarchy 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 rg = T.RegionGroupId.nth regions_hierarchy rg_id in
let region_names =
List.map
- (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name)
+ (fun rid -> (T.RegionId.nth sg.generics.regions rid).name)
rg.regions
in
Some { id = rg_id; region_names }
in
(* Add the function name *)
- ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
- (keep_fwd, num_backs)
+ ctx_compute_fun_name ctx def.llbc_name 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)
@@ -1218,7 +1991,7 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
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 fun_id = (Pure.FunId (FRegular 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 *)
{
@@ -1228,156 +2001,6 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
ctx.fun_name_info;
}
-type names_map_init = {
- keywords : string list;
- assumed_adts : (assumed_ty * string) list;
- assumed_structs : (assumed_ty * string) list;
- assumed_variants : (assumed_ty * VariantId.id * string) list;
- assumed_llbc_functions :
- (A.assumed_fun_id * RegionGroupId.id option * string) list;
- assumed_pure_functions : (pure_assumed_fun_id * string) list;
-}
-
-(** Initialize names maps with a proper set of keywords/names coming from the
- target language/prover. *)
-let initialize_names_maps (fmt : formatter) (init : names_map_init) : names_maps
+let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
=
- let int_names = List.map fmt.int_name T.all_int_types in
- let keywords =
- List.concat
- [
- [ fmt.bool_name; fmt.char_name; fmt.str_name ]; int_names; init.keywords;
- ]
- 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 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
- * - the assumed variants
- * - the assumed functions
- *)
- let nm =
- List.fold_left
- (fun nm (type_id, name) ->
- 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_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_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 (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 =
- List.fold_left
- (fun nm (fid, name) -> names_maps_add_function id_to_string fid name nm)
- nm assumed_functions
- in
- (* Return *)
- nm
-
-let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
- fmt.type_name def.name
-
-(** Helper function: generate a suffix for a function name, i.e., generates
- a suffix like "_loop", "loop1", etc. to append to a function name.
- *)
-let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
- string =
- match loop_id with
- | None -> ""
- | Some loop_id ->
- (* If this is for a loop, generally speaking, we append the loop index.
- If this function admits only one loop, we omit it. *)
- if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id
-
-(** A helper function: generates a function suffix from a region group
- information.
- TODO: move all those helpers.
-*)
-let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
- (num_region_groups : int) (rg : region_group_info option)
- ((keep_fwd, num_backs) : bool * int) : string =
- let lp_suff = default_fun_loop_suffix num_loops loop_id in
-
- (* There are several cases:
- - [rg] is [Some]: this is a forward function:
- - we add "_fwd"
- - [rg] is [None]: this is a backward function:
- - this function has one extracted backward function:
- - if the forward function has been filtered, we add "_fwd_back":
- the forward function is useless, so the unique backward function
- takes its place, in a way
- - otherwise we add "_back"
- - this function has several backward functions: we add "_back" and an
- additional suffix to identify the precise backward function
- Note that we always add a suffix (in case there are no region groups,
- we could not add the "_fwd" suffix) to prevent name clashes between
- definitions (in particular between type and function definitions).
- *)
- let rg_suff =
- (* TODO: make all the backends match what is done for Lean *)
- match rg with
- | 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 *)
- 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
- - otherwise we use an index
- *)
- List.for_all Option.is_some rg.region_names
- then
- (* Concatenate the region names *)
- "_back" ^ String.concat "" (List.map Option.get rg.region_names)
- else (* Use the region index *)
- "_back" ^ RegionGroupId.to_string rg.id
- in
- lp_suff ^ rg_suff
+ ctx_compute_type_name ctx def.llbc_name
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 05:31:15 +0000