From 91d62c6e73cd67236848c3efa85f85ae152d0d4e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 8 Feb 2024 09:42:00 +0100 Subject: Update following changes in Charon --- compiler/AssociatedTypes.ml | 25 +++++++++---------------- compiler/Extract.ml | 6 +----- compiler/ExtractBase.ml | 2 +- compiler/ExtractTypes.ml | 7 +------ compiler/InterpreterExpressions.ml | 6 ++---- compiler/PrintPure.ml | 18 ++++-------------- compiler/Pure.ml | 6 ++---- compiler/RegionsHierarchy.ml | 2 +- compiler/SymbolicAst.ml | 3 +-- compiler/SymbolicToPure.ml | 28 +++++++++++----------------- compiler/TypesUtils.ml | 3 +-- 11 files changed, 34 insertions(+), 72 deletions(-) (limited to 'compiler') diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 054c8169..7b928566 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -51,9 +51,10 @@ let compute_norm_trait_types_from_preds that it would be enough to only visit the field [ty] of the trait type constraint, but for safety we visit all the fields *) assert (trait_type_constraint_no_regions c); - let trait_ty = TTraitType (c.trait_ref, c.generics, c.type_name) in + let { trait_ref; type_name; ty } : trait_type_constraint = c in + let trait_ty = TTraitType (trait_ref, type_name) in let trait_ty_ref = get_ref trait_ty in - let ty_ref = get_ref c.ty in + let ty_ref = get_ref ty in let new_repr = UnionFind.get ty_ref in let merged = UnionFind.union trait_ty_ref ty_ref in (* Not sure the set operation is necessary, but I want to control which @@ -72,9 +73,7 @@ let compute_norm_trait_types_from_preds List.filter_map (fun (k, v) -> match k with - | TTraitType (trait_ref, generics, type_name) -> - assert (generics = empty_generic_args); - Some ({ trait_ref; type_name }, v) + | TTraitType (trait_ref, type_name) -> Some ({ trait_ref; type_name }, v) | _ -> None) rbindings in @@ -225,20 +224,15 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in let output = norm_ctx_normalize_ty ctx output in TArrow (regions, inputs, output) - | TTraitType (trait_ref, generics, type_name) -> ( + | TTraitType (trait_ref, type_name) -> ( log#ldebug (lazy ("norm_ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty ^ "\n- trait_ref: " ^ trait_ref_to_string ctx trait_ref - ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref - ^ "\n- generics:\n" - ^ generic_args_to_string ctx generics)); + ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* Normalize and attempt to project the type from the trait ref *) let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in - let generics = norm_ctx_normalize_generic_args ctx generics in - (* For now, we don't support higher order types *) - assert (generics = empty_generic_args); let ty : ty = match trait_ref.trait_id with | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ } @@ -284,7 +278,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* We can't project *) assert (trait_instance_id_is_local_clause trait_ref.trait_id); - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) in let tr : trait_type_ref = { trait_ref; type_name } in (* Lookup the representative, if there is *) @@ -484,11 +478,10 @@ and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx) let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx) (ttc : trait_type_constraint) : trait_type_constraint = - let { trait_ref; generics; type_name; ty } = ttc in + let { trait_ref; type_name; ty } : trait_type_constraint = ttc in let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in - let generics = norm_ctx_normalize_generic_args ctx generics in let ty = norm_ctx_normalize_ty ctx ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let mk_norm_ctx (ctx : eval_ctx) : norm_ctx = { diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 46f6a1ca..a93ed6e4 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -326,11 +326,8 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args | Proj proj -> extract_field_projector ctx fmt inside app proj qualif.generics args - | TraitConst (trait_ref, generics, const_name) -> - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; + | TraitConst (trait_ref, const_name) -> extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref; - extract_generic_args ctx fmt TypeDeclId.Set.empty generics; let name = ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id const_name ctx @@ -338,7 +335,6 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets name)) | _ -> (* "Regular" expression *) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 5e97cd21..297a1d22 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1682,7 +1682,7 @@ let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option) | TLiteral lty -> ( match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") | TArrow _ -> "f" - | TTraitType (_, _, name) -> name_from_type_ident name) + | TTraitType (_, name) -> name_from_type_ident name) (** Generates a type variable basename. *) let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 9d4131d2..bbd5fae4 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -528,7 +528,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_rec false ret_ty; if inside then F.pp_print_string fmt ")" - | TTraitType (trait_ref, generics, type_name) -> ( + | TTraitType (trait_ref, type_name) -> ( if !parameterize_trait_types then raise (Failure "Unimplemented") else let type_name = @@ -547,7 +547,6 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) *) match trait_ref.trait_id with | Self -> - assert (generics = empty_generic_args); assert (trait_ref.generics = empty_generic_args); extract_trait_instance_id_with_dot ctx fmt no_params_tys false trait_ref.trait_id; @@ -555,11 +554,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) | _ -> (* HOL4 doesn't have 1st class types *) assert (!backend <> HOL4); - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; extract_trait_ref ctx fmt no_params_tys false trait_ref; - extract_generic_args ctx fmt no_params_tys generics; - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets type_name)) and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 8536b4ab..dc100fe3 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -263,8 +263,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) match cv.value with | CLiteral lit -> cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx - | CTraitConst (trait_ref, generics, const_name) -> ( - assert (generics = empty_generic_args); + | CTraitConst (trait_ref, const_name) -> ( match trait_ref.trait_id with | TraitImpl _ -> (* This shouldn't happen: if we refer to a concrete implementation, we @@ -294,8 +293,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaTraitConstValue - (trait_ref, generics, const_name), + SymbolicAst.VaTraitConstValue (trait_ref, const_name), e )))) | CVar vid -> ( let ctx0 = ctx in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 21ca7f08..a401594d 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -159,14 +159,9 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string = ty_to_string env true arg_ty ^ " -> " ^ ty_to_string env false ret_ty in if inside then "(" ^ ty ^ ")" else ty - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = trait_ref_to_string env false trait_ref in - let s = - if generics = empty_generic_args then trait_ref ^ "::" ^ type_name - else - let generics = generic_args_to_string env generics in - "(" ^ trait_ref ^ " " ^ generics ^ ")::" ^ type_name - in + let s = trait_ref ^ "::" ^ type_name in if inside then "(" ^ s ^ ")" else s and generic_args_to_strings (env : fmt_env) (inside : bool) @@ -624,14 +619,9 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) let field_s = adt_field_to_string env adt_id field_id in (* Adopting an F*-like syntax *) (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) - | TraitConst (trait_ref, generics, const_name) -> + | TraitConst (trait_ref, const_name) -> let trait_ref = trait_ref_to_string env true trait_ref in - let generics_s = generic_args_to_string env generics in - let qualif = - if generics <> empty_generic_args then - "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name - else trait_ref ^ "." ^ const_name - in + let qualif = trait_ref ^ "." ^ const_name in (qualif, [])) | _ -> (* "Regular" expression case *) diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 33c23cc3..a735667e 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -283,7 +283,7 @@ type ty = | TVar of type_var_id | TLiteral of literal_type | TArrow of ty * ty - | TTraitType of trait_ref * generic_args * string + | TTraitType of trait_ref * string (** The string is for the name of the associated type *) and trait_ref = { @@ -374,7 +374,6 @@ type generic_params = { type trait_type_constraint = { trait_ref : trait_ref; - generics : generic_args; type_name : trait_item_name; ty : ty; } @@ -599,8 +598,7 @@ type qualif_id = | Global of global_decl_id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) - | TraitConst of trait_ref * generic_args * string - (** A trait associated constant *) + | TraitConst of trait_ref * string (** A trait associated constant *) [@@deriving show] (** An instantiated qualifier. diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 80b67a54..0b589453 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -169,7 +169,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (* Continue *) explore_ty outer ty | TRawPtr (ty, _) -> explore_ty outer ty - | TTraitType (trait_ref, _generic_args, _) -> + | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) assert ( diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 7252a020..79c03e58 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -251,8 +251,7 @@ and value_aggregate = | VaCgValue of const_generic_var_id (** This is used when evaluating a const generic value: in the interpreter, we introduce a fresh symbolic value. *) - | VaTraitConstValue of trait_ref * generic_args * string - (** A trait constant value *) + | VaTraitConstValue of trait_ref * string (** A trait constant value *) [@@deriving show, visitors diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 922f0375..27279327 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -474,10 +474,9 @@ let rec translate_sty (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_sgeneric_args (generics : T.generic_args) : generic_args = @@ -497,11 +496,10 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause = let translate_strait_type_constraint (ttc : T.trait_type_constraint) : trait_type_constraint = - let { T.trait_ref; generics; type_name; ty } = ttc in + let { T.trait_ref; type_name; ty } = ttc in let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in let ty = translate_sty ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let translate_predicates (preds : T.predicates) : predicates = let trait_type_constraints = @@ -638,10 +636,9 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_fwd_generic_args (type_infos : type_infos) @@ -737,16 +734,14 @@ let rec translate_back_ty (type_infos : type_infos) | TRawPtr _ -> (* TODO: not sure what to do here *) None - | TTraitType (trait_ref, generics, type_name) -> - assert (generics.regions = []); + | TTraitType (trait_ref, type_name) -> assert ( AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); if inside_mut then - (* Translate the trait ref and the generics as "forward" generics - + (* Translate the trait ref as a "forward" trait ref - we do not want to filter any type *) let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - Some (TTraitType (trait_ref, generics, type_name)) + Some (TTraitType (trait_ref, type_name)) else None | TArrow _ -> raise (Failure "TODO") @@ -2956,11 +2951,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) in { e = StructUpdate su; ty = var.ty } | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } - | VaTraitConstValue (trait_ref, generics, const_name) -> + | VaTraitConstValue (trait_ref, const_name) -> let type_infos = ctx.type_ctx.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - let qualif_id = TraitConst (trait_ref, generics, const_name) in + let qualif_id = TraitConst (trait_ref, const_name) in let qualif = { id = qualif_id; generics = empty_generic_args } in { e = Qualif qualif; ty = var.ty } in diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index 28db59ec..f5dd7df4 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -105,9 +105,8 @@ let generic_args_no_regions (x : generic_args) : bool = (** Return [true] if the trait type constraint doesn't contain regions (including erased regions) *) let trait_type_constraint_no_regions (x : trait_type_constraint) : bool = try - let { trait_ref; generics; type_name = _; ty } = x in + let { trait_ref; type_name = _; ty } = x in raise_if_region_ty_visitor#visit_trait_ref () trait_ref; - raise_if_region_ty_visitor#visit_generic_args () generics; raise_if_region_ty_visitor#visit_ty () ty; true with Found -> false -- cgit v1.2.3