summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-21 17:24:50 +0100
committerSon Ho2023-11-21 17:24:50 +0100
commitb916f696c5265dc4f5af4a67b118b005a7ed8612 (patch)
tree671dd4b1f207dc7bce18060af86dc92013b2e3d9
parent137cc7335e64fcb70c254e7fd2a6fa353fb43e61 (diff)
Reorganize the "Extract" files
-rw-r--r--compiler/Config.ml27
-rw-r--r--compiler/Extract.ml47
-rw-r--r--compiler/ExtractBase.ml1635
-rw-r--r--compiler/ExtractBuiltin.ml25
-rw-r--r--compiler/ExtractTypes.ml980
-rw-r--r--compiler/Main.ml5
-rw-r--r--compiler/Translate.ml19
7 files changed, 1299 insertions, 1439 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index a487f9e2..fe110ee4 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -336,3 +336,30 @@ let type_check_pure_code = ref false
(** Shall we fail hard if we encounter an issue, or should we attempt to go
as far as possible while leaving "holes" in the generated code? *)
let fail_hard = ref true
+
+(** if true, add the type name as a prefix
+ to the variant names.
+ Ex.:
+ In Rust:
+ {[
+ enum List = {
+ Cons(u32, Box<List>),x
+ Nil,
+ }
+ ]}
+
+ F*, if option activated:
+ {[
+ type list =
+ | ListCons : u32 -> list -> list
+ | ListNil : list
+ ]}
+
+ F*, if option not activated:
+ {[
+ type list =
+ | Cons : u32 -> list -> list
+ | Nil : list
+ ]}
+ *)
+let variant_concatenate_type_name = ref true
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index d7b4c152..16262c91 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -6,7 +6,6 @@
open Pure
open PureUtils
open TranslateCore
-open ExtractBase
open Config
include ExtractTypes
@@ -236,12 +235,10 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
(is_let : bool) (inside : bool) (v : typed_pattern) : extraction_ctx =
match v.value with
| PatConstant cv ->
- ctx.fmt.extract_literal fmt inside cv;
+ extract_literal fmt inside cv;
ctx
| PatVar (v, _) ->
- let vname =
- ctx.fmt.var_basename ctx.names_maps.names_map.names_set v.basename v.ty
- in
+ let vname = ctx_compute_var_basename ctx v.basename v.ty in
let ctx, vname = ctx_add_var vname v.id ctx in
F.pp_print_string fmt vname;
ctx
@@ -274,7 +271,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
| CVar var_id ->
let var_name = ctx_get_const_generic_var var_id ctx in
F.pp_print_string fmt var_name
- | Const cv -> ctx.fmt.extract_literal fmt inside cv
+ | Const cv -> extract_literal fmt inside cv
| App _ ->
let app, args = destruct_apps e in
extract_App ctx fmt inside app args
@@ -354,10 +351,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
* Note that the way we generate the translation, we shouldn't get the
* case where we have no argument (all functions are fully instantiated,
* and no AST transformation introduces partial calls). *)
- ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
+ extract_unop (extract_texpression ctx fmt) fmt inside unop arg
| Binop (binop, int_ty), [ arg0; arg1 ] ->
(* Number of arguments: similar to unop *)
- ctx.fmt.extract_binop
+ extract_binop
(extract_texpression ctx fmt)
fmt inside binop int_ty arg0 arg1
| Fun fun_id, _ ->
@@ -1359,7 +1356,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
is_opaque_coq && def.signature.generics <> empty_generic_params
in
(* Print the qualifier ("assume", etc.). *)
- let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
+ let qualif = fun_decl_kind_to_qualif kind in
(match qualif with
| Some qualif ->
F.pp_print_string fmt qualif;
@@ -1655,7 +1652,7 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open "QUALIF NAME : TYPE =" box (depth=1) *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print "QUALIF NAME " *)
- (match ctx.fmt.fun_decl_kind_to_qualif kind with
+ (match fun_decl_kind_to_qualif kind with
| Some qualif ->
F.pp_print_string fmt qualif;
F.pp_print_space fmt ()
@@ -1824,11 +1821,11 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
| None ->
List.map
(fun (c : trait_clause) ->
- let name = ctx.fmt.trait_parent_clause_name trait_decl c in
+ let name = ctx_compute_trait_parent_clause_name ctx trait_decl c in
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name trait_decl ^ name
+ else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(c.clause_id, name))
trait_decl.parent_clauses
@@ -1855,11 +1852,11 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
| None ->
List.map
(fun (item_name, _) ->
- let name = ctx.fmt.trait_const_name trait_decl item_name in
+ let name = ctx_compute_trait_const_name ctx trait_decl item_name in
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name trait_decl ^ name
+ else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(item_name, name))
consts
@@ -1887,19 +1884,21 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
match builtin_info with
| None ->
let compute_type_name (item_name : string) : string =
- let type_name = ctx.fmt.trait_type_name trait_decl item_name in
+ let type_name =
+ ctx_compute_trait_type_name ctx trait_decl item_name
+ in
if !Config.record_fields_short_names then type_name
- else ctx.fmt.trait_decl_name trait_decl ^ type_name
+ else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
in
let compute_clause_name (item_name : string) (clause : trait_clause) :
TraitClauseId.id * string =
let name =
- ctx.fmt.trait_type_clause_name trait_decl item_name clause
+ ctx_compute_trait_type_clause_name ctx trait_decl item_name clause
in
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name trait_decl ^ name
+ else ctx_compute_trait_decl_name ctx trait_decl ^ name
in
(clause.clause_id, name)
in
@@ -1971,7 +1970,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(* Add a prefix if necessary *)
let name =
if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name trait_decl ^ "_" ^ name
+ else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ name
in
(f.back_id, name)
in
@@ -2036,8 +2035,8 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
let trait_name, trait_constructor =
match builtin_info with
| None ->
- ( ctx.fmt.trait_decl_name trait_decl,
- ctx.fmt.trait_decl_constructor trait_decl )
+ ( ctx_compute_trait_decl_name ctx trait_decl,
+ ctx_compute_trait_decl_constructor ctx trait_decl )
| Some info -> (info.extract_name, info.constructor)
in
let ctx = ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx in
@@ -2101,7 +2100,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
(* Compute the name *)
let name =
match builtin_info with
- | None -> ctx.fmt.trait_impl_name trait_decl trait_impl
+ | None -> ctx_compute_trait_impl_name ctx trait_decl trait_impl
| Some name -> name
in
ctx_add (TraitImplId trait_impl.def_id) name ctx
@@ -2214,7 +2213,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the box for the name + generics *)
F.pp_open_hovbox fmt ctx.indent_incr;
let qualif =
- Option.get (ctx.fmt.type_decl_kind_to_qualif SingleNonRec (Some Struct))
+ Option.get (type_decl_kind_to_qualif SingleNonRec (Some Struct))
in
(* When checking if the trait declaration is empty: we ignore the provided
methods, because for now they are extracted separately *)
@@ -2505,7 +2504,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* `let (....) : Trait ... =` *)
(* Open the box for the name + generics *)
F.pp_open_hovbox fmt ctx.indent_incr;
- (match ctx.fmt.fun_decl_kind_to_qualif SingleNonRec with
+ (match fun_decl_kind_to_qualif SingleNonRec with
| Some qualif ->
F.pp_print_string fmt qualif;
F.pp_print_space fmt ()
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index f1ba35a2..0b9908b2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -2,9 +2,11 @@
open Contexts
open Pure
-open TranslateCore
+open StringUtils
+open Config
module F = Format
open ExtractBuiltin
+open TranslateCore
(** The local logger *)
let log = Logging.extract_log
@@ -109,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 : llbc_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 : llbc_name -> string -> string;
- (** Inputs:
- - type name
- - variant name
- *)
- struct_constructor : llbc_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 : llbc_name -> string;
- (** Provided a basename, compute a type name. *)
- global_name : llbc_name -> string;
- (** Provided a basename, compute a global name. *)
- fun_name :
- llbc_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 -> llbc_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:llbc_name}.
- - loop identifier, if this is for a loop
- *)
- decreases_proof_name :
- A.FunDeclId.id -> llbc_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:llbc_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
@@ -590,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
@@ -601,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;
@@ -741,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 (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 }
-
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 (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 ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
ctx_get (GlobalId id) ctx
@@ -950,15 +768,970 @@ let ctx_get_termination_measure (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
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 =
+ (* We need to lookup the LLBC definitions, to have the original instantiation *)
+ let trait_impl =
+ TraitImplId.Map.find trait_impl.def_id
+ ctx.trans_ctx.trait_impls_ctx.trait_impls
+ in
+ let params = trait_impl.generics in
+ let args = trait_impl.impl_trait.decl_generics in
+ 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
+
+let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
+ (trait_decl : trait_decl) (clause : trait_clause) : string =
+ (* TODO: improve - it would be better to not use indices *)
+ let clause = "parent_clause_" ^ TraitClauseId.to_string clause.clause_id in
+ if !Config.record_fields_short_names then clause
+ else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ 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)
+ (_clause : trait_clause) : string =
+ (* TODO: actually use the clause to derive the name *)
+ "inst"
+
+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)
@@ -966,13 +1739,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)
@@ -988,7 +1757,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
@@ -996,9 +1765,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
@@ -1008,7 +1777,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
@@ -1019,9 +1788,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
@@ -1042,9 +1809,7 @@ let ctx_add_local_trait_clauses (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
- in
+ let basename = ctx_compute_trait_clause_basename ctx c in
ctx_add_local_trait_clause basename c.clause_id ctx)
ctx clauses
@@ -1064,7 +1829,7 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
let name =
- ctx.fmt.decreases_proof_name def.def_id def.llbc_name 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 (FRegular def.def_id, def.loop_id)) name ctx
@@ -1072,8 +1837,8 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_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.llbc_name 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 (FRegular def.def_id, def.loop_id)) name ctx
@@ -1091,7 +1856,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
ctx_add decl name ctx
| None ->
(* Not the case: "standard" registration *)
- let name = ctx.fmt.global_name def.name 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
@@ -1123,8 +1888,8 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
Some { id = rg_id; region_names }
in
(* Add the function name *)
- ctx.fmt.fun_name def.llbc_name 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)
@@ -1148,156 +1913,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 (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
-
-let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
- fmt.type_name def.llbc_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
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index b0a5159f..ef746ddf 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -26,6 +26,11 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a =
let split_on_separator (s : string) : string list =
Str.split (Str.regexp "\\(::\\|\\.\\)") s
+let flatten_name (name : string list) : string =
+ match !backend with
+ | FStar | Coq | HOL4 -> String.concat "_" name
+ | Lean -> String.concat "." name
+
let () =
assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]);
assert (split_on_separator "x.y.z" = [ "x"; "y"; "z" ])
@@ -124,10 +129,7 @@ let mk_struct_constructor (type_name : string) : string =
let builtin_types () : builtin_type_info list =
let mk_type (rust_name : string) ?(keep_params : bool list option = None)
?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
- let extract_name =
- let sep = backend_choice "_" "." in
- String.concat sep (split_on_separator rust_name)
- in
+ let extract_name = flatten_name (split_on_separator rust_name) in
let body_info : builtin_type_body_info option =
match kind with
| KOpaque -> None
@@ -231,11 +233,7 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
| None -> pattern_to_fun_extract_name rust_name
| Some name -> split_on_separator name
in
- let basename =
- match !backend with
- | FStar | Coq | HOL4 -> String.concat "_" extract_name
- | Lean -> String.concat "." extract_name
- in
+ let basename = flatten_name extract_name in
let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in
let fwd = [ { rg = None; extract_name = basename ^ fwd_suffix } ] in
let back_suffix = if with_back && back_no_suffix then "" else "_back" in
@@ -400,11 +398,9 @@ let builtin_trait_decls_info () =
let extract_name =
match extract_name with
| Some n -> n
- | None -> (
+ | None ->
let rust_name = pattern_to_fun_extract_name rust_name in
- match !backend with
- | Coq | FStar | HOL4 -> String.concat "_" rust_name
- | Lean -> String.concat "." rust_name)
+ flatten_name rust_name
in
let constructor = mk_struct_constructor extract_name in
let consts = [] in
@@ -502,13 +498,12 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
pattern * (bool list option * string) =
let rust_name = parse_pattern rust_name in
let name =
- let sep = backend_choice "_" "." in
let name =
match extract_name with
| None -> pattern_to_trait_impl_extract_name rust_name
| Some name -> split_on_separator name
in
- String.concat sep name
+ flatten_name name
in
(rust_name, (filter, name))
in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 3a81e6fe..c9be5abe 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -6,354 +6,88 @@
open Pure
open PureUtils
open TranslateCore
-open ExtractBase
-open StringUtils
open Config
-module F = Format
+include ExtractBase
-(** 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
-
-(** 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
+(** Format a constant value.
-(** 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*.
+ 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
*)
-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 extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit =
+ match cv with
+ | VScalar sv -> (
+ match !backend with
+ | FStar -> F.pp_print_string fmt (Z.to_string sv.value)
+ | Coq | HOL4 | Lean ->
+ let print_brackets = inside && !backend = HOL4 in
+ if print_brackets then F.pp_print_string fmt "(";
+ (match !backend with
+ | Coq | Lean -> ()
+ | HOL4 ->
+ F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty);
+ F.pp_print_space fmt ()
+ | _ -> raise (Failure "Unreachable"));
+ (* We need to add parentheses if the value is negative *)
+ if sv.value >= Z.of_int 0 then
+ F.pp_print_string fmt (Z.to_string sv.value)
+ else if !backend = Lean then
+ (* TODO: parsing issues with Lean because there are ambiguous
+ interpretations between int values and nat values *)
+ F.pp_print_string fmt
+ ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))")
+ else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
+ (match !backend with
+ | Coq ->
+ let iname = int_name sv.int_ty in
+ F.pp_print_string fmt ("%" ^ iname)
+ | Lean ->
+ let iname = String.lowercase_ascii (int_name sv.int_ty) in
+ F.pp_print_string fmt ("#" ^ iname)
+ | HOL4 -> ()
+ | _ -> raise (Failure "Unreachable"));
+ if print_brackets then F.pp_print_string fmt ")")
+ | VBool b ->
+ let b =
+ match !backend with
+ | HOL4 -> if b then "T" else "F"
+ | Coq | FStar | Lean -> if b then "true" else "false"
+ in
+ F.pp_print_string fmt b
+ | VChar c -> (
+ match !backend with
+ | HOL4 ->
+ (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
+ F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
+ | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+ | Coq ->
+ if inside then F.pp_print_string fmt "(";
+ F.pp_print_string fmt "char_of_byte";
+ F.pp_print_space fmt ();
+ (* Convert the the char to ascii *)
+ let c =
+ let i = Char.code c in
+ let x0 = i / 16 in
+ let x1 = i mod 16 in
+ "Coq.Init.Byte.x" ^ string_of_int x0 ^ string_of_int x1
+ in
+ F.pp_print_string fmt c;
+ if inside then F.pp_print_string fmt ")")
-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 ();
- }
+(** 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
+ *)
let extract_unop (extract_expr : bool -> texpression -> unit)
(fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit
=
@@ -409,7 +143,18 @@ let extract_unop (extract_expr : bool -> texpression -> unit)
extract_expr true arg;
if inside then F.pp_print_string fmt ")")
-(** [extract_expr] : the boolean argument is [inside] *)
+(** 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
+ *)
let extract_binop (extract_expr : bool -> texpression -> unit)
(fmt : F.formatter) (inside : bool) (binop : E.binop)
(int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
@@ -451,523 +196,6 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
extract_expr true arg1);
if inside then F.pp_print_string fmt ")"
-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
-
-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")
-
-let name_last_elem_as_ident (n : llbc_name) : string =
- match Collections.List.last n with
- | PeIdent (s, _) -> s
- | PeImpl _ -> raise (Failure "Unexpected")
-
-(**
- [ctx]: we use the context to lookup type definitions, to retrieve type names.
- This is used to compute variable names, when they have no basenames: in this
- case we use the first letter of the type name.
-
- [variant_concatenate_type_name]: if true, add the type name as a prefix
- to the variant names.
- Ex.:
- In Rust:
- {[
- enum List = {
- Cons(u32, Box<List>),x
- Nil,
- }
- ]}
-
- F*, if option activated:
- {[
- type list =
- | ListCons : u32 -> list -> list
- | ListNil : list
- ]}
-
- F*, if option not activated:
- {[
- type list =
- | Cons : u32 -> list -> list
- | Nil : list
- ]}
-
- Rk.: this should be true by default, because in Rust all the variant names
- are actively uniquely identifier by the type name [List::Cons(...)], while
- in other languages it is not necessarily the case, and thus clashes can mess
- up type checking. Note that some languages actually forbids the name clashes
- (it is the case of F* ).
- *)
-let mk_formatter (ctx : trans_ctx) (crate_name : string)
- (variant_concatenate_type_name : bool) : formatter =
- let int_name = int_name in
-
- (* 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 name_to_simple_name (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 = crate_name then name else id :: name in
- name_to_simple_name ctx name
- | _ ->
- raise
- (Failure
- ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
- in
- let flatten_name (name : string list) : string =
- match !backend with
- | FStar | Coq | HOL4 -> String.concat "_" name
- | Lean -> String.concat "." name
- in
- let get_name name : string list = name_to_simple_name name in
- let get_type_name = get_name in
- let get_type_name_no_suffix name =
- match !backend with
- | FStar | Coq | HOL4 -> String.concat "_" (get_type_name name)
- | Lean -> String.concat "." (get_type_name name)
- in
- let type_name name =
- match !backend with
- | FStar ->
- StringUtils.lowercase_first_letter (get_type_name_no_suffix name ^ "_t")
- | Coq | HOL4 -> get_type_name_no_suffix name ^ "_t"
- | Lean -> get_type_name_no_suffix name
- in
- let field_name (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 = get_type_name_no_suffix def_name ^ "_" ^ field_name_s in
- match !backend with
- | Lean | HOL4 -> def_name
- | Coq | FStar -> StringUtils.lowercase_first_letter def_name
- in
- let variant_name (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
- (get_type_name_no_suffix def_name ^ "_" ^ variant)
- else variant
- | Lean -> variant
- in
- let struct_constructor (basename : llbc_name) : string =
- let tname = type_name basename in
- ExtractBuiltin.mk_struct_constructor tname
- in
- let get_fun_name fname =
- let fname = get_name 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
- in
- let global_name (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 (get_name name) in
- String.concat "_" parts
- in
- let fun_name (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 = get_fun_name fname in
- (* Compute the suffix *)
- let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
- (* Concatenate *)
- fname ^ suffix
- in
-
- let trait_decl_name (trait_decl : trait_decl) : string =
- type_name trait_decl.llbc_name
- in
-
- let trait_impl_name (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 =
- (* We need to lookup the LLBC definitions, to have the original instantiation *)
- let trait_impl =
- TraitImplId.Map.find trait_impl.def_id ctx.trait_impls_ctx.trait_impls
- in
- let params = trait_impl.generics in
- let args = trait_impl.impl_trait.decl_generics in
- name_with_generics_to_simple_name 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
- in
-
- let trait_decl_constructor (trait_decl : trait_decl) : string =
- let name = trait_decl_name trait_decl in
- ExtractBuiltin.mk_struct_constructor name
- in
-
- let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause)
- : string =
- (* TODO: improve - it would be better to not use indices *)
- let clause = "parent_clause_" ^ TraitClauseId.to_string clause.clause_id in
- if !Config.record_fields_short_names then clause
- else trait_decl_name trait_decl ^ "_" ^ clause
- in
- let trait_type_name (trait_decl : trait_decl) (item : string) : string =
- let name =
- if !Config.record_fields_short_names then item
- else trait_decl_name 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
- in
- let trait_const_name (trait_decl : trait_decl) (item : string) : string =
- let name =
- if !Config.record_fields_short_names then item
- else trait_decl_name trait_decl ^ "_" ^ item
- in
- (* See [trait_type_name] *)
- match !backend with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
- in
- let trait_method_name (trait_decl : trait_decl) (item : string) : string =
- if !Config.record_fields_short_names then item
- else trait_decl_name trait_decl ^ "_" ^ item
- in
- let trait_type_clause_name (trait_decl : trait_decl) (item : string)
- (clause : trait_clause) : string =
- (* TODO: improve - it would be better to not use indices *)
- trait_type_name trait_decl item
- ^ "_clause_"
- ^ TraitClauseId.to_string clause.clause_id
- in
-
- let termination_measure_name (_fid : A.FunDeclId.id) (fname : llbc_name)
- (num_loops : int) (loop_id : LoopId.id option) : string =
- let fname = get_fun_name 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
- in
-
- let decreases_proof_name (_fid : A.FunDeclId.id) (fname : llbc_name)
- (num_loops : int) (loop_id : LoopId.id option) : string =
- let fname = get_fun_name 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
- in
-
- let var_basename (_varset : StringSet.t) (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.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)
- in
- let type_var_basename (_varset : StringSet.t) (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
- in
- let const_generic_var_basename (_varset : StringSet.t) (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
- in
- let trait_clause_basename (_varset : StringSet.t) (_clause : trait_clause) :
- string =
- (* TODO: actually use the clause to derive the name *)
- "inst"
- in
- let trait_self_clause_basename = "self_clause" in
- let append_index (basename : string) (i : int) : string =
- basename ^ string_of_int i
- in
-
- let extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit
- =
- match cv with
- | VScalar sv -> (
- match !backend with
- | FStar -> F.pp_print_string fmt (Z.to_string sv.value)
- | Coq | HOL4 | Lean ->
- let print_brackets = inside && !backend = HOL4 in
- if print_brackets then F.pp_print_string fmt "(";
- (match !backend with
- | Coq | Lean -> ()
- | HOL4 ->
- F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty);
- F.pp_print_space fmt ()
- | _ -> raise (Failure "Unreachable"));
- (* We need to add parentheses if the value is negative *)
- if sv.value >= Z.of_int 0 then
- F.pp_print_string fmt (Z.to_string sv.value)
- else if !backend = Lean then
- (* TODO: parsing issues with Lean because there are ambiguous
- interpretations between int values and nat values *)
- F.pp_print_string fmt
- ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))")
- else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
- (match !backend with
- | Coq ->
- let iname = int_name sv.int_ty in
- F.pp_print_string fmt ("%" ^ iname)
- | Lean ->
- let iname = String.lowercase_ascii (int_name sv.int_ty) in
- F.pp_print_string fmt ("#" ^ iname)
- | HOL4 -> ()
- | _ -> raise (Failure "Unreachable"));
- if print_brackets then F.pp_print_string fmt ")")
- | VBool b ->
- let b =
- match !backend with
- | HOL4 -> if b then "T" else "F"
- | Coq | FStar | Lean -> if b then "true" else "false"
- in
- F.pp_print_string fmt b
- | VChar c -> (
- match !backend with
- | HOL4 ->
- (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
- F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
- | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
- | Coq ->
- if inside then F.pp_print_string fmt "(";
- F.pp_print_string fmt "char_of_byte";
- F.pp_print_space fmt ();
- (* Convert the the char to ascii *)
- let c =
- let i = Char.code c in
- let x0 = i / 16 in
- let x1 = i mod 16 in
- "Coq.Init.Byte.x" ^ string_of_int x0 ^ string_of_int x1
- in
- F.pp_print_string fmt c;
- if inside then F.pp_print_string fmt ")")
- in
- let bool_name = if !backend = Lean then "Bool" else "bool" in
- let char_name = if !backend = Lean then "Char" else "char" in
- let str_name = if !backend = Lean then "String" else "string" in
- {
- bool_name;
- char_name;
- int_name;
- str_name;
- type_decl_kind_to_qualif;
- fun_decl_kind_to_qualif;
- field_name;
- variant_name;
- struct_constructor;
- type_name;
- global_name;
- fun_name;
- termination_measure_name;
- decreases_proof_name;
- trait_decl_name;
- trait_impl_name;
- trait_decl_constructor;
- trait_parent_clause_name;
- trait_const_name;
- trait_type_name;
- trait_method_name;
- trait_type_clause_name;
- var_basename;
- type_var_basename;
- const_generic_var_basename;
- trait_self_clause_basename;
- trait_clause_basename;
- append_index;
- extract_literal;
- extract_unop;
- extract_binop;
- }
-
-let mk_formatter_and_names_maps (ctx : trans_ctx) (crate_name : string)
- (variant_concatenate_type_name : bool) : formatter * names_maps =
- let fmt = mk_formatter ctx crate_name variant_concatenate_type_name in
- let names_maps = initialize_names_maps fmt (names_map_init ()) in
- (fmt, names_maps)
-
let is_single_opaque_fun_decl_group (dg : Pure.fun_decl list) : bool =
match dg with [ d ] -> d.body = None | _ -> false
@@ -1125,17 +353,17 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
| CgGlobal id ->
let s = ctx_get_global id ctx in
F.pp_print_string fmt s
- | CgValue v -> ctx.fmt.extract_literal fmt inside v
+ | CgValue v -> extract_literal fmt inside v
| CgVar id ->
let s = ctx_get_const_generic_var id ctx in
F.pp_print_string fmt s
-let extract_literal_type (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
(ty : literal_type) : unit =
match ty with
- | TBool -> F.pp_print_string fmt ctx.fmt.bool_name
- | TChar -> F.pp_print_string fmt ctx.fmt.char_name
- | TInteger int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
+ | TBool -> F.pp_print_string fmt (bool_name ())
+ | TChar -> F.pp_print_string fmt (char_name ())
+ | TInteger int_ty -> F.pp_print_string fmt (int_name int_ty)
(** [inside] constrols whether we should add parentheses or not around type
applications (if [true] we add parentheses).
@@ -1446,7 +674,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(* Compute and register the type def name *)
let def_name =
match info with
- | None -> ctx.fmt.type_name def.llbc_name
+ | None -> ctx_compute_type_name ctx def.llbc_name
| Some info -> info.extract_name
in
let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in
@@ -1464,10 +692,14 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let field_names =
FieldId.mapi
(fun fid (field : field) ->
- (fid, ctx.fmt.field_name def.llbc_name fid field.field_name))
+ ( fid,
+ ctx_compute_field_name ctx def.llbc_name fid
+ field.field_name ))
fields
in
- let cons_name = ctx.fmt.struct_constructor def.llbc_name in
+ let cons_name =
+ ctx_compute_struct_constructor ctx def.llbc_name
+ in
(field_names, cons_name)
| Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
let field_names =
@@ -1503,12 +735,13 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
VariantId.mapi
(fun variant_id (variant : variant) ->
let name =
- ctx.fmt.variant_name def.llbc_name variant.variant_name
+ ctx_compute_variant_name ctx def.llbc_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.llbc_name in
+ let type_name = ctx_compute_type_name ctx def.llbc_name in
type_name ^ "." ^ name
else name
in
@@ -1570,8 +803,7 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
| Some field_name ->
let var_id = VarId.of_int (FieldId.to_int fid) in
let field_name =
- ctx.fmt.var_basename ctx.names_maps.names_map.names_set
- (Some field_name) f.field_ty
+ ctx_compute_var_basename ctx (Some field_name) f.field_ty
in
let ctx, field_name = ctx_add_var field_name var_id ctx in
F.pp_print_string fmt (field_name ^ " :");
@@ -1652,7 +884,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
let print_variant _variant_id (v : variant) =
(* We don't lookup the name, because it may have a prefix for the type
id (in the case of Lean) *)
- let cons_name = ctx.fmt.variant_name def.llbc_name v.variant_name in
+ let cons_name = ctx_compute_variant_name ctx def.llbc_name v.variant_name in
let fields = v.fields in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
cg_params cons_name fields
@@ -2059,7 +1291,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* > "type TYPE_NAME" *)
- let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
+ let qualif = type_decl_kind_to_qualif kind type_kind in
(match qualif with
| Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name)
| None -> F.pp_print_string fmt def_name);
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 0daf454d..e350da8a 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -178,7 +178,10 @@ let () =
log#error "The Lean backend doesn't support the -use-fuel option";
fail ());
(* Lean can disambiguate the field names *)
- record_fields_short_names := true
+ record_fields_short_names := true;
+ (* We exploit the fact that the variant name should always be
+ prefixed with the type name to prevent collisions *)
+ variant_concatenate_type_name := false
| HOL4 ->
(* We don't support fuel for the HOL4 backend *)
if !use_fuel then (
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 271d19ad..05e48af5 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -993,20 +993,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
translate_crate_to_pure crate
in
- (* Initialize the extraction context - for now we extract only to F*.
- * We initialize the names map by registering the keywords used in the
- * language, as well as some primitive names ("u32", etc.) *)
- let variant_concatenate_type_name =
- (* For Lean, we exploit the fact that the variant name should always be
- prefixed with the type name to prevent collisions *)
- match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false
- in
- (* Initialize the names map (we insert the names of the "primitives"
- declarations, and insert the names of the local declarations later) *)
- let fmt, names_maps =
- Extract.mk_formatter_and_names_maps trans_ctx crate.name
- variant_concatenate_type_name
- in
+ (* Initialize the names map by registering the keywords used in the
+ language, as well as some primitive names ("u32", etc.).
+ We insert the names of the local declarations later. *)
+ let names_maps = Extract.initialize_names_maps () in
(* We need to compute which functions are recursive, in order to know
* whether we should generate a decrease clause or not. *)
@@ -1061,7 +1051,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
ExtractBase.crate;
trans_ctx;
names_maps;
- fmt;
indent_incr = 2;
use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
fun_name_info = PureUtils.RegularFunIdMap.empty;