diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/ExtractBase.ml | 275 |
1 files changed, 139 insertions, 136 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 297a1d22..f6b891cc 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -7,6 +7,7 @@ open Config module F = Format open ExtractBuiltin open TranslateCore +open Errors (** The local logger *) let log = Logging.extract_log @@ -263,7 +264,7 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) in log#serror err; (* If we fail hard on errors, raise an exception *) - if !Config.fail_hard then raise (Failure err) + craise_opt_meta None err let names_map_get_id_from_name (name : string) (nm : names_map) : id option = StringMap.find_opt name nm.name_to_id @@ -297,7 +298,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string) in log#serror err; (* If we fail hard on errors, raise an exception *) - if !Config.fail_hard then raise (Failure err)); + craise_opt_meta None err); (* Insert *) names_map_add_unchecked id name nm @@ -424,7 +425,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string) (** The [id_to_string] function to print nice debugging messages if there are collisions *) -let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) : +let names_maps_get (meta : Meta.meta) (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 = @@ -445,7 +446,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) : ^ map_to_string m in log#serror err; - if !Config.fail_hard then raise (Failure err) + if !Config.fail_hard then craise meta err else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)") else let m = nm.names_map.id_to_name in @@ -457,7 +458,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) : ^ map_to_string m in log#serror err; - if !Config.fail_hard then raise (Failure err) + if !Config.fail_hard then craise meta err else "(ERROR: \"" ^ id_to_string id ^ "\")" type names_map_init = { @@ -528,6 +529,7 @@ let scalar_name (ty : literal_type) : string = functions, etc. *) type extraction_ctx = { + (* mutable _meta : Meta.meta; *) crate : A.crate; trans_ctx : trans_ctx; names_maps : names_maps; @@ -589,17 +591,17 @@ let llbc_fun_id_to_string (ctx : extraction_ctx) = let fun_id_to_string (ctx : extraction_ctx) = PrintPure.regular_fun_id_to_string (extraction_ctx_to_fmt_env ctx) -let adt_variant_to_string (ctx : extraction_ctx) = - PrintPure.adt_variant_to_string (extraction_ctx_to_fmt_env ctx) +let adt_variant_to_string (meta : Meta.meta) (ctx : extraction_ctx) = + PrintPure.adt_variant_to_string meta (extraction_ctx_to_fmt_env ctx) -let adt_field_to_string (ctx : extraction_ctx) = - PrintPure.adt_field_to_string (extraction_ctx_to_fmt_env ctx) +let adt_field_to_string (meta : Meta.meta) (ctx : extraction_ctx) = + PrintPure.adt_field_to_string meta (extraction_ctx_to_fmt_env ctx) (** Debugging function, used when communicating name collisions to the user, and also to print ids for internal debugging (in case of lookup miss for instance). *) -let id_to_string (id : id) (ctx : extraction_ctx) : string = +let id_to_string (meta : Meta.meta) (id : id) (ctx : extraction_ctx) : string = let trait_decl_id_to_string (id : A.TraitDeclId.id) : string = let trait_name = trait_decl_id_to_string ctx id in "trait_decl: " ^ trait_name ^ " (id: " ^ A.TraitDeclId.to_string id ^ ")" @@ -627,11 +629,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id | VariantId (id, variant_id) -> let type_name = type_id_to_string ctx id in - let variant_name = adt_variant_to_string ctx id (Some variant_id) in + let variant_name = adt_variant_to_string meta ctx id (Some variant_id) in "type name: " ^ type_name ^ ", variant name: " ^ variant_name | FieldId (id, field_id) -> let type_name = type_id_to_string ctx id in - let field_name = adt_field_to_string ctx id field_id in + let field_name = adt_field_to_string meta ctx id field_id in "type name: " ^ type_name ^ ", field name: " ^ field_name | UnknownId -> "keyword" | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id @@ -657,51 +659,55 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name | TraitSelfClauseId -> "trait_self_clause" -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 ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = + let id_to_string (id : id) : string = id_to_string meta id ctx in let names_maps = names_maps_add id_to_string id name ctx.names_maps in { ctx with names_maps } -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 ctx_get (meta : Meta.meta) (id : id) (ctx : extraction_ctx) : string = + let id_to_string (id : id) : string = id_to_string meta id ctx in + names_maps_get meta id_to_string id ctx.names_maps (* TODO check if we can remove the meta arg, same for following functions*) -let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = - ctx_get (GlobalId id) ctx +let ctx_get_global (meta : Meta.meta) (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get meta (GlobalId id) ctx -let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string = - ctx_get (FunId id) ctx +let ctx_get_function (meta : Meta.meta) (id : fun_id) (ctx : extraction_ctx) : string = + ctx_get meta (FunId id) ctx -let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option) +let ctx_get_local_function (meta : Meta.meta) (id : A.FunDeclId.id) (lp : LoopId.id option) (ctx : extraction_ctx) : string = - ctx_get_function (FromLlbc (FunId (FRegular id), lp)) ctx + ctx_get_function meta (FromLlbc (FunId (FRegular id), lp)) ctx -let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string = - assert (id <> TTuple); - ctx_get (TypeId id) ctx +let ctx_get_type (meta : Meta.meta) (id : type_id) (ctx : extraction_ctx) : string = + cassert (id <> TTuple) meta "T"; + ctx_get meta (TypeId id) ctx -let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string = - ctx_get_type (TAdtId id) ctx +let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id) (ctx : extraction_ctx) : string = + ctx_get_type meta (TAdtId id) ctx -let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string = - ctx_get_type (TAssumed id) ctx +let ctx_get_assumed_type (meta : Meta.meta) (id : assumed_ty) (ctx : extraction_ctx) : string = + ctx_get_type meta (TAssumed id) ctx let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) : string = - ctx_get (TraitDeclConstructorId id) ctx + let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in + ctx_get meta (TraitDeclConstructorId id) ctx -let ctx_get_trait_self_clause (ctx : extraction_ctx) : string = - ctx_get TraitSelfClauseId ctx +let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string = + ctx_get meta TraitSelfClauseId ctx let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string = - ctx_get (TraitDeclId id) ctx + let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in + ctx_get meta (TraitDeclId id) ctx let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string = - ctx_get (TraitImplId id) ctx + let meta = (TraitImplId.Map.find id ctx.trans_trait_impls).meta in + ctx_get meta (TraitImplId id) ctx let ctx_get_trait_item (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = - ctx_get (TraitItemId (id, item_name)) ctx + let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in + ctx_get meta (TraitItemId (id, item_name)) ctx let ctx_get_trait_const (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = @@ -713,48 +719,52 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string) let ctx_get_trait_method (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = - ctx_get (TraitMethodId (id, item_name)) ctx + let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in + ctx_get meta (TraitMethodId (id, item_name)) ctx let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id) (ctx : extraction_ctx) : string = - ctx_get (TraitParentClauseId (id, clause)) ctx + let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in + ctx_get meta (TraitParentClauseId (id, clause)) ctx let ctx_get_trait_item_clause (id : trait_decl_id) (item : string) (clause : trait_clause_id) (ctx : extraction_ctx) : string = - ctx_get (TraitItemClauseId (id, item, clause)) ctx + let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in + ctx_get meta (TraitItemClauseId (id, item, clause)) ctx -let ctx_get_var (id : VarId.id) (ctx : extraction_ctx) : string = - ctx_get (VarId id) ctx +let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) : string = + ctx_get meta (VarId id) ctx -let ctx_get_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string = - ctx_get (TypeVarId id) ctx +let ctx_get_type_var (meta : Meta.meta) (id : TypeVarId.id) (ctx : extraction_ctx) : string = + ctx_get meta (TypeVarId id) ctx -let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx) +let ctx_get_const_generic_var (meta : Meta.meta) (id : ConstGenericVarId.id) (ctx : extraction_ctx) : string = - ctx_get (ConstGenericVarId id) ctx + ctx_get meta (ConstGenericVarId id) ctx -let ctx_get_local_trait_clause (id : TraitClauseId.id) (ctx : extraction_ctx) : +let ctx_get_local_trait_clause (meta : Meta.meta) (id : TraitClauseId.id) (ctx : extraction_ctx) : string = - ctx_get (LocalTraitClauseId id) ctx + ctx_get meta (LocalTraitClauseId id) ctx -let ctx_get_field (type_id : type_id) (field_id : FieldId.id) +let ctx_get_field (meta : Meta.meta) (type_id : type_id) (field_id : FieldId.id) (ctx : extraction_ctx) : string = - ctx_get (FieldId (type_id, field_id)) ctx + (* let meta = (TypeDeclId.Map.find type_id ctx.trans_types).meta in TODO : check how to get meta *) + ctx_get meta (FieldId (type_id, field_id)) ctx -let ctx_get_struct (def_id : type_id) (ctx : extraction_ctx) : string = - ctx_get (StructId def_id) ctx +let ctx_get_struct (meta : Meta.meta) (def_id : type_id) (ctx : extraction_ctx) : string = + ctx_get meta (StructId def_id) ctx -let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id) +let ctx_get_variant (meta : Meta.meta) (def_id : type_id) (variant_id : VariantId.id) (ctx : extraction_ctx) : string = - ctx_get (VariantId (def_id, variant_id)) ctx + ctx_get meta (VariantId (def_id, variant_id)) ctx -let ctx_get_decreases_proof (def_id : A.FunDeclId.id) +let ctx_get_decreases_proof (meta : Meta.meta) (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = - ctx_get (DecreasesProofId (FRegular def_id, loop_id)) ctx + ctx_get meta (DecreasesProofId (FRegular def_id, loop_id)) ctx -let ctx_get_termination_measure (def_id : A.FunDeclId.id) +let ctx_get_termination_measure (meta : Meta.meta) (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = - ctx_get (TerminationMeasureId (FRegular def_id, loop_id)) ctx + ctx_get meta (TerminationMeasureId (FRegular def_id, loop_id)) ctx (** Small helper to compute the name of a unary operation *) let unop_name (unop : unop) : string = @@ -1161,7 +1171,7 @@ let initialize_names_maps () : names_maps = Remark: can return [None] for some backends like HOL4. *) -let type_decl_kind_to_qualif (kind : decl_kind) +let type_decl_kind_to_qualif (meta : Meta.meta) (kind : decl_kind) (type_kind : type_decl_kind option) : string option = match !backend with | FStar -> ( @@ -1189,11 +1199,11 @@ let type_decl_kind_to_qualif (kind : decl_kind) (* This is for traits *) Some "Record" | _ -> - raise - (Failure + craise + meta ("Unexpected: (" ^ show_decl_kind kind ^ ", " ^ Print.option_to_string show_type_decl_kind type_kind - ^ ")"))) + ^ ")")) | Lean -> ( match kind with | SingleNonRec -> ( @@ -1247,17 +1257,17 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option = TODO: move inside the formatter? *) -let type_keyword () = +let type_keyword (meta : Meta.meta) = match !backend with | FStar -> "Type0" | Coq | Lean -> "Type" - | HOL4 -> raise (Failure "Unexpected") + | HOL4 -> craise meta "Unexpected" (** Helper *) -let name_last_elem_as_ident (n : llbc_name) : string = +let name_last_elem_as_ident (meta : Meta.meta) (n : llbc_name) : string = match Collections.List.last n with | PeIdent (s, _) -> s - | PeImpl _ -> raise (Failure "Unexpected") + | PeImpl _ -> craise meta "Unexpected" (** Helper @@ -1266,35 +1276,28 @@ let name_last_elem_as_ident (n : llbc_name) : string = we remove it. We ignore disambiguators (there may be collisions, but we check if there are). *) -let ctx_prepare_name (ctx : extraction_ctx) (name : llbc_name) : llbc_name = +let ctx_prepare_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) : llbc_name = (* Rmk.: initially we only filtered the disambiguators equal to 0 *) match name with | (PeIdent (crate, _) as id) :: name -> if crate = ctx.crate.name then name else id :: name | _ -> - raise - (Failure + craise + meta ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx.trans_ctx name)) (** Helper *) -let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) : - string list = - (* Rmk.: initially we only filtered the disambiguators equal to 0 *) - let name = ctx_prepare_name ctx name in - name_to_simple_name 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) : +let ctx_compute_type_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) : string = - flatten_name (ctx_compute_simple_type_name ctx name) + flatten_name (ctx_compute_simple_type_name meta 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 +let ctx_compute_type_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) = + let name = ctx_compute_type_name_no_suffix meta ctx name in match !backend with | FStar -> StringUtils.lowercase_first_letter (name ^ "_t") | Coq | HOL4 -> name ^ "_t" @@ -1311,7 +1314,7 @@ let ctx_compute_type_name (ctx : extraction_ctx) (name : llbc_name) = 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) +let ctx_compute_field_name (meta : Meta.meta) (ctx : extraction_ctx) (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option) : string = let field_name_s = match field_name with @@ -1326,7 +1329,7 @@ let ctx_compute_field_name (ctx : extraction_ctx) (def_name : llbc_name) else field_name_s else let def_name = - ctx_compute_type_name_no_suffix ctx def_name ^ "_" ^ field_name_s + ctx_compute_type_name_no_suffix meta ctx def_name ^ "_" ^ field_name_s in match !backend with | Lean | HOL4 -> def_name @@ -1336,14 +1339,14 @@ let ctx_compute_field_name (ctx : extraction_ctx) (def_name : llbc_name) - type name - variant name *) -let ctx_compute_variant_name (ctx : extraction_ctx) (def_name : llbc_name) +let ctx_compute_variant_name (meta : Meta.meta) (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) + (ctx_compute_type_name_no_suffix meta ctx def_name ^ "_" ^ variant) else variant | Lean -> variant @@ -1358,14 +1361,14 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def_name : llbc_name) Inputs: - type name *) -let ctx_compute_struct_constructor (ctx : extraction_ctx) (basename : llbc_name) +let ctx_compute_struct_constructor (meta : Meta.meta) (ctx : extraction_ctx) (basename : llbc_name) : string = - let tname = ctx_compute_type_name ctx basename in + let tname = ctx_compute_type_name meta ctx basename in ExtractBuiltin.mk_struct_constructor tname -let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) : +let ctx_compute_fun_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx) (fname : llbc_name) : string = - let fname = ctx_compute_simple_name ctx fname in + let fname = ctx_compute_simple_name meta ctx fname in (* TODO: don't convert to snake case for Coq, HOL4, F* *) let fname = flatten_name fname in match !backend with @@ -1373,10 +1376,10 @@ let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) : | Lean -> fname (** Provided a basename, compute the name of a global declaration. *) -let ctx_compute_global_name (ctx : extraction_ctx) (name : llbc_name) : string = +let ctx_compute_global_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) : string = match !Config.backend with | Coq | FStar | HOL4 -> - let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in + let parts = List.map to_snake_case (ctx_compute_simple_name meta ctx name) in String.concat "_" parts | Lean -> flatten_name (ctx_compute_simple_name ctx name) @@ -1395,7 +1398,7 @@ let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) : (** A helper function: generates a function suffix. TODO: move all those helpers. *) -let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string = +let default_fun_suffix (meta : Meta.meta) (num_loops : int) (loop_id : LoopId.id option) : string = (* We only generate a suffix for the functions we generate from the loops *) default_fun_loop_suffix num_loops loop_id @@ -1409,17 +1412,17 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string = - loop id (if pertinent) TODO: use the fun id for the assumed functions. *) -let ctx_compute_fun_name (ctx : extraction_ctx) (fname : llbc_name) +let ctx_compute_fun_name (meta : Meta.meta) (ctx : extraction_ctx) (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string = - let fname = ctx_compute_fun_name_no_suffix ctx fname in + let fname = ctx_compute_fun_name_no_suffix meta ctx fname in (* Compute the suffix *) - let suffix = default_fun_suffix num_loops loop_id in + let suffix = default_fun_suffix meta num_loops loop_id 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 + ctx_compute_type_name trait_decl.meta ctx trait_decl.llbc_name let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) (trait_impl : trait_impl) : string = @@ -1569,17 +1572,17 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx) the same purpose as in [llbc_name]. - loop identifier, if this is for a loop *) -let ctx_compute_termination_measure_name (ctx : extraction_ctx) +let ctx_compute_termination_measure_name (meta : Meta.meta) (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 fname = ctx_compute_fun_name_no_suffix meta 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") + | Coq | HOL4 -> craise meta "Unexpected" in (* Concatenate *) fname ^ lp_suffix ^ suffix @@ -1598,16 +1601,16 @@ let ctx_compute_termination_measure_name (ctx : extraction_ctx) the same purpose as in [llbc_name]. - loop identifier, if this is for a loop *) -let ctx_compute_decreases_proof_name (ctx : extraction_ctx) +let ctx_compute_decreases_proof_name (meta : Meta.meta) (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 fname = ctx_compute_fun_name_no_suffix meta 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") + | FStar | Coq | HOL4 -> craise meta "Unexpected" in (* Concatenate *) fname ^ lp_suffix ^ suffix @@ -1625,7 +1628,7 @@ let ctx_compute_decreases_proof_name (ctx : extraction_ctx) 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) +let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) (basename : string option) (ty : ty) : string = (* Small helper to derive var names from ADT type names. @@ -1638,7 +1641,7 @@ let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option) 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); + cassert (List.length cl > 0) meta "T"; let cl = List.map (fun s -> s.[0]) cl in StringUtils.string_of_chars cl in @@ -1738,82 +1741,82 @@ 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) +let ctx_add_type_var (meta : Meta.meta) (basename : string) (id : TypeVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx_compute_type_var_basename ctx basename in let 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 + let ctx = ctx_add meta (TypeVarId id) name ctx in (ctx, name) (** Generate a unique const generic variable name and add it to the context *) -let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id) +let ctx_add_const_generic_var (meta : Meta.meta) (basename : string) (id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx_compute_const_generic_var_basename ctx basename in let 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 + let ctx = ctx_add meta (ConstGenericVarId id) name ctx in (ctx, name) (** See {!ctx_add_type_var} *) -let ctx_add_type_vars (vars : (string * TypeVarId.id) list) +let ctx_add_type_vars (meta : Meta.meta) (vars : (string * TypeVarId.id) list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map - (fun ctx (name, id) -> ctx_add_type_var name id ctx) + (fun ctx (name, id) -> ctx_add_type_var meta name id ctx) ctx vars (** Generate a unique variable name and add it to the context *) -let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) : +let ctx_add_var (meta : Meta.meta) (basename : string) (id : VarId.id) (ctx : extraction_ctx) : extraction_ctx * string = let name = basename_to_unique ctx.names_maps.names_map.names_set name_append_index basename in - let ctx = ctx_add (VarId id) name ctx in + let ctx = ctx_add meta (VarId id) name ctx in (ctx, name) (** Generate a unique variable name for the trait self clause and add it to the context *) -let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string = +let ctx_add_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : extraction_ctx * string = let basename = trait_self_clause_basename in let name = basename_to_unique ctx.names_maps.names_map.names_set name_append_index basename in - let ctx = ctx_add TraitSelfClauseId name ctx in + let ctx = ctx_add meta TraitSelfClauseId name ctx in (ctx, name) (** Generate a unique trait clause name and add it to the context *) -let ctx_add_local_trait_clause (basename : string) (id : TraitClauseId.id) +let ctx_add_local_trait_clause (meta : Meta.meta) (basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string = let name = basename_to_unique ctx.names_maps.names_map.names_set name_append_index basename in - let ctx = ctx_add (LocalTraitClauseId id) name ctx in + let ctx = ctx_add meta (LocalTraitClauseId id) name ctx in (ctx, name) (** See {!ctx_add_var} *) -let ctx_add_vars (vars : var list) (ctx : extraction_ctx) : +let ctx_add_vars (meta : Meta.meta) (vars : var list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map (fun ctx (v : var) -> - let name = ctx_compute_var_basename ctx v.basename v.ty in - ctx_add_var name v.id ctx) + let name = ctx_compute_var_basename meta ctx v.basename v.ty in + ctx_add_var meta name v.id ctx) ctx vars -let ctx_add_type_params (vars : type_var list) (ctx : extraction_ctx) : +let ctx_add_type_params (meta : Meta.meta) (vars : type_var list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map - (fun ctx (var : type_var) -> ctx_add_type_var var.name var.index ctx) + (fun ctx (var : type_var) -> ctx_add_type_var meta var.name var.index ctx) ctx vars -let ctx_add_const_generic_params (vars : const_generic_var list) +let ctx_add_const_generic_params (meta : Meta.meta) (vars : const_generic_var list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map (fun ctx (var : const_generic_var) -> - ctx_add_const_generic_var var.name var.index ctx) + ctx_add_const_generic_var meta var.name var.index ctx) ctx vars (** Returns the lists of names for: @@ -1825,7 +1828,7 @@ let ctx_add_const_generic_params (vars : const_generic_var list) pretty names for the trait clauses. See {!ctx_compute_trait_clause_name} for additional information. *) -let ctx_add_local_trait_clauses (current_def_name : Types.name) +let ctx_add_local_trait_clauses (meta : Meta.meta) (current_def_name : Types.name) (llbc_generics : Types.generic_params) (clauses : trait_clause list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map @@ -1834,7 +1837,7 @@ let ctx_add_local_trait_clauses (current_def_name : Types.name) ctx_compute_trait_clause_basename ctx current_def_name llbc_generics c.clause_id in - ctx_add_local_trait_clause basename c.clause_id ctx) + ctx_add_local_trait_clause meta basename c.clause_id ctx) ctx clauses (** Returns the lists of names for: @@ -1846,33 +1849,33 @@ let ctx_add_local_trait_clauses (current_def_name : Types.name) pretty names for the trait clauses. See {!ctx_compute_trait_clause_name} for additional information. *) -let ctx_add_generic_params (current_def_name : Types.name) +let ctx_add_generic_params (meta : Meta.meta) (current_def_name : Types.name) (llbc_generics : Types.generic_params) (generics : generic_params) (ctx : extraction_ctx) : extraction_ctx * string list * string list * string list = let { types; const_generics; trait_clauses } = generics in - let ctx, tys = ctx_add_type_params types ctx in - let ctx, cgs = ctx_add_const_generic_params const_generics ctx in + let ctx, tys = ctx_add_type_params meta types ctx in + let ctx, cgs = ctx_add_const_generic_params meta const_generics ctx in let ctx, tcs = - ctx_add_local_trait_clauses current_def_name llbc_generics trait_clauses ctx + ctx_add_local_trait_clauses meta current_def_name llbc_generics trait_clauses ctx in (ctx, tys, cgs, tcs) let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = let name = - ctx_compute_decreases_proof_name ctx def.def_id def.llbc_name def.num_loops + ctx_compute_decreases_proof_name def.meta 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 + ctx_add def.meta (DecreasesProofId (FRegular def.def_id, def.loop_id)) name ctx let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = let name = - ctx_compute_termination_measure_name ctx def.def_id def.llbc_name + ctx_compute_termination_measure_name def.meta 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 + ctx_add def.meta (TerminationMeasureId (FRegular def.def_id, def.loop_id)) name ctx let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = @@ -1885,7 +1888,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with | Some name -> (* Yes: register the custom binding *) - ctx_add decl name ctx + ctx_add def.meta decl name ctx | None -> (* Not the case: "standard" registration *) let name = ctx_compute_global_name ctx def.name in @@ -1903,20 +1906,20 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = (* Add the function name *) - ctx_compute_fun_name ctx def.llbc_name def.num_loops def.loop_id + ctx_compute_fun_name def.meta ctx def.llbc_name def.num_loops def.loop_id (* TODO: move to Extract *) let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Sanity check: the function should not be a global body - those are handled * separately *) - assert (not def.is_global_decl_body); + cassert (not def.is_global_decl_body) def.meta "The function should not be a global body - those are handled separately"; (* Lookup the LLBC def to compute the region group information *) let def_id = def.def_id in (* Add the function name *) let def_name = ctx_compute_fun_name def ctx in let fun_id = (Pure.FunId (FRegular def_id), def.loop_id) in - ctx_add (FunId (FromLlbc fun_id)) def_name ctx + ctx_add def.meta (FunId (FromLlbc fun_id)) def_name ctx let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string = - ctx_compute_type_name ctx def.llbc_name + ctx_compute_type_name def.meta ctx def.llbc_name |