diff options
| -rw-r--r-- | compiler/Config.ml | 27 | ||||
| -rw-r--r-- | compiler/Extract.ml | 47 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 1635 | ||||
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 25 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 980 | ||||
| -rw-r--r-- | compiler/Main.ml | 5 | ||||
| -rw-r--r-- | compiler/Translate.ml | 19 |
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; |