From 8ae2d79250f65af1fdab2882a88e38c3f43e55eb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 8 Jan 2025 19:31:49 +0100 Subject: [PATCH] Let charon manage `Self` clauses --- charon-pin | 2 +- flake.lock | 12 +- src/Translate.ml | 1 - src/extract/Extract.ml | 112 +++++++-------- src/extract/ExtractBase.ml | 75 +--------- src/extract/ExtractTypes.ml | 113 ++------------- src/pure/Pure.ml | 30 ++-- src/pure/PureUtils.ml | 135 ++++++++++++++---- .../hashmap/Hashmap_FunsExternal_Template.v | 2 +- .../coq/misc/External_FunsExternal_Template.v | 2 +- tests/coq/rename_attribute/RenameAttribute.v | 6 +- tests/coq/traits/Traits.v | 9 +- tests/fstar/hashmap/Hashmap.FunsExternal.fsti | 2 +- tests/fstar/misc/External.FunsExternal.fsti | 2 +- .../rename_attribute/RenameAttribute.Funs.fst | 7 +- tests/fstar/traits/Traits.fst | 9 +- tests/lean/RenameAttribute.lean | 5 +- tests/lean/Traits.lean | 7 +- tests/src/mutually-recursive-traits.lean.out | 2 +- 19 files changed, 213 insertions(+), 320 deletions(-) diff --git a/charon-pin b/charon-pin index 8dbc03bb1..31c5cf1bc 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -8a17efc262ef3af377ab172efc865edcf1bb40ea +d7737574abf6adbabca3ff45c22d77b9d0bbc5f5 diff --git a/flake.lock b/flake.lock index 8a08ed8e0..b6625b88f 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1736180214, - "narHash": "sha256-BtyLLaWlN/b8SC/6eL0f9Imaoq71bHjAWh/ASugXxfk=", + "lastModified": 1736359539, + "narHash": "sha256-jwbX9fK7C6WrLM+xoOO89uWD4q1He0KQNBivxB4lyWQ=", "owner": "aeneasverif", "repo": "charon", - "rev": "8a17efc262ef3af377ab172efc865edcf1bb40ea", + "rev": "d7737574abf6adbabca3ff45c22d77b9d0bbc5f5", "type": "github" }, "original": { @@ -177,11 +177,11 @@ ] }, "locked": { - "lastModified": 1736216977, - "narHash": "sha256-EMueGrzBpryM8mgOyoyJ7DdNRRk09ug1ggcLLp0WrCQ=", + "lastModified": 1736303309, + "narHash": "sha256-IKrk7RL+Q/2NC6+Ql6dwwCNZI6T6JH2grTdJaVWHF0A=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "bbe7e4e7a70d235db4bbdcabbf8a2f6671881dd7", + "rev": "a0b81d4fa349d9af1765b0f0b4a899c13776f706", "type": "github" }, "original": { diff --git a/src/Translate.ml b/src/Translate.ml index cc0abc4a4..e1ed4b90f 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -1126,7 +1126,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : use_dep_ite = Config.backend () = Lean && !Config.extract_decreases_clauses; trait_decl_id = None (* None by default *); - is_provided_method = false (* false by default *); trans_trait_decls; trans_trait_impls; trans_types; diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 796cd29cd..4aa450e72 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -505,51 +505,63 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) true ]} *) - (match fun_id with - | FromLlbc (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id) -> - (* We have to check whether the trait method is required or provided *) - let trait_decl_id = trait_ref.trait_decl_ref.trait_decl_id in - let trait_decl = - TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls - in - let method_id = - PureUtils.trait_decl_get_method trait_decl method_name - in - - if not method_id.is_provided then ( - (* Required method *) - sanity_check __FILE__ __LINE__ (lp_id = None) - trait_decl.item_meta.span; - extract_trait_ref trait_decl.item_meta.span ctx fmt - TypeDeclId.Set.empty true trait_ref; - let fun_name = - ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id - method_name ctx - in - let add_brackets (s : string) = - if backend () = Coq then "(" ^ s ^ ")" else s + let generics = + match fun_id with + | FromLlbc (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id) + -> + (* We have to check whether the trait method is required or provided *) + let trait_decl_id = trait_ref.trait_decl_ref.trait_decl_id in + let trait_decl = + TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in - F.pp_print_string fmt ("." ^ add_brackets fun_name)) - else - (* Provided method: we see it as a regular function call, and use - the function name *) - let fun_id = FromLlbc (FunId (FRegular method_id.id), lp_id) in - let fun_name = - ctx_get_function trait_decl.item_meta.span fun_id ctx + let bound_method = + PureUtils.trait_decl_get_method trait_decl method_name in - F.pp_print_string fmt fun_name; - (* Note that we do not need to print the generics for the trait - declaration: they are always implicit as they can be deduced - from the trait self clause. + if not bound_method.is_provided then begin + (* Required method *) + sanity_check __FILE__ __LINE__ (lp_id = None) + trait_decl.item_meta.span; + extract_trait_ref trait_decl.item_meta.span ctx fmt + TypeDeclId.Set.empty true trait_ref; + let fun_name = + ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id + method_name ctx + in + let add_brackets (s : string) = + if backend () = Coq then "(" ^ s ^ ")" else s + in + F.pp_print_string fmt ("." ^ add_brackets fun_name); + generics + end + else begin + (* Provided method: we see it as a regular function call, and use + the function name. `generics` is generics for the method only; + we must substitute the bound method to get the correct + generics for the function item. *) + let subst = + make_subst_from_generics_including_methods trait_decl.generics + bound_method.bound_method.binder_generics trait_ref.trait_id + trait_ref.trait_decl_ref.decl_generics generics + in + let fn_ref = + subst_visitor#visit_fun_decl_ref subst + bound_method.bound_method.binder_value + in + let fun_id = FromLlbc (FunId (FRegular fn_ref.fun_id), lp_id) in + let fun_name = + ctx_get_function trait_decl.item_meta.span fun_id ctx + in + F.pp_print_string fmt fun_name; - Print the trait ref (to instantate the self clause) *) - F.pp_print_space fmt (); - extract_trait_ref trait_decl.item_meta.span ctx fmt - TypeDeclId.Set.empty true trait_ref - | _ -> - let fun_name = ctx_get_function span fun_id ctx in - F.pp_print_string fmt fun_name); + (* Return the newly-computed function item generics. *) + fn_ref.fun_generics + end + | _ -> + let fun_name = ctx_get_function span fun_id ctx in + F.pp_print_string fmt fun_name; + generics + in (* Sanity check: HOL4 doesn't support const generics *) sanity_check __FILE__ __LINE__ @@ -1296,21 +1308,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) About the order: we want to make sure the names are reserved for those (variable names might collide with them but it is ok, we will add suffixes to the variables). - - TODO: micro-pass to update what happens when calling trait provided - functions. *) - let ctx, trait_decl = - match def.kind with - | TraitDeclItem (trait_ref, _, true) -> - let trait_decl = - T.TraitDeclId.Map.find trait_ref.trait_decl_id ctx.trans_trait_decls - in - let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in - let ctx = { ctx with is_provided_method = true } in - (ctx, Some trait_decl) - | _ -> (ctx, None) - in (* Add the type parameters - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, type_params, cg_params, trait_clauses = @@ -1323,8 +1321,8 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) let explicit = def.signature.explicit_info in (let space = Some space in extract_generic_params def.item_meta.span ctx fmt TypeDeclId.Set.empty ~space - ~trait_decl Item def.signature.generics (Some explicit) type_params - cg_params trait_clauses); + Item def.signature.generics (Some explicit) type_params cg_params + trait_clauses); (* Close the box for the generics *) F.pp_close_box fmt (); (* The input parameters - note that doing this adds bindings to the context *) diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index 2c3835a94..ac327f9f6 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -112,16 +112,7 @@ let decl_is_not_last_from_group (kind : decl_kind) : bool = not (decl_is_last_from_group kind) type type_decl_kind = Enum | Struct | Tuple [@@deriving show] - -(** Generics can be bound in two places: each item has its generics, and - additionally within a trait decl or impl each method has its own generics. - We distinguish these two cases here. In charon, the distinction is made - thanks to `de_bruijn_var`. - Note that for the generics of a top-level `fun_decl` we always use `Item`; - `Method` only refers to the inner binder found in the list of methods in a - trait_decl/trait_impl. - *) -type generic_origin = Item | Method +type generic_origin = PureUtils.generic_origin (** We use identifiers to look for name clashes *) and id = @@ -183,41 +174,6 @@ and id = | TraitItemId of TraitDeclId.id * string (** A trait associated item which is not a method *) | TraitParentClauseId of TraitDeclId.id * TraitClauseId.id - | TraitSelfClauseId - (** Specifically for the clause: [Self : Trait]. - - For now, we forbid provided methods (methods in trait declarations - with a default implementation) from being overriden in trait implementations. - We extract trait provided methods such that they take an instance of - the trait as input: this instance is given by the trait self clause. - - For instance: - {[ - // - // Rust - // - trait ToU64 { - fn to_u64(&self) -> u64; - - // Provided method - fn is_pos(&self) -> bool { - self.to_u64() > 0 - } - } - - // - // Generated code - // - struct ToU64 (T : Type) { - to_u64 : T -> u64; - } - - // The trait self clause - // vvvvvvvvvvvvvvvvvvvvvv - let is_pos (T : Type) (trait_self : ToU64 T) (self : T) : bool = - trait_self.to_u64 self > 0 - ]} - *) | UnknownId (** Used for stored various strings like keywords, definitions which should always be in context, etc. and which can't be linked to one @@ -592,7 +548,6 @@ type extraction_ctx = { *) trait_decl_id : trait_decl_id option; (** If we are extracting a trait declaration, identifies it *) - is_provided_method : bool; trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; trans_funs : pure_fun_translation A.FunDeclId.Map.t; trans_globals : Pure.global_decl Pure.GlobalDeclId.Map.t; @@ -706,7 +661,6 @@ let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) : "trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name | TraitMethodId (trait_decl_id, fun_name) -> trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name - | TraitSelfClauseId -> "trait_self_clause" let ctx_add (span : Meta.span) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = @@ -750,10 +704,6 @@ let ctx_get_trait_constructor (span : Meta.span) (id : trait_decl_id) (ctx : extraction_ctx) : string = ctx_get (Some span) (TraitDeclConstructorId id) ctx -let ctx_get_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) : string - = - ctx_get (Some span) TraitSelfClauseId ctx - let ctx_get_trait_decl (span : Meta.span) (id : trait_decl_id) (ctx : extraction_ctx) : string = ctx_get (Some span) (TraitDeclId id) ctx @@ -786,21 +736,6 @@ let ctx_get_var (span : Meta.span) (id : VarId.id) (ctx : extraction_ctx) : string = ctx_get (Some span) (VarId id) ctx -(** This warrants explanations. Charon supports several levels of nested - binders; however there are currently only two cases where we bind - non-lifetime variables: at the top-level of each item, and for each method - inside a trait_decl/trait_impl. Moreover, we use `Free` vars to identify - item-bound vars. This means that we can identify which binder a variable - comes from without rigorously tracking binder levels, which is what this - function does. - Note that the `de_bruijn_id`s are wrong anyway because we kept charon's - binding levels but forgot all the region binders. - *) -let origin_from_de_bruijn_var (var : 'a de_bruijn_var) : generic_origin * 'a = - match var with - | Bound (_, id) -> (Method, id) - | Free id -> (Item, id) - let ctx_get_type_var (span : Meta.span) (origin : generic_origin) (id : TypeVarId.id) (ctx : extraction_ctx) : string = ctx_get (Some span) (TypeVarId (origin, id)) ctx @@ -2018,14 +1953,6 @@ let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id) let ctx = ctx_add span (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 (span : Meta.span) (ctx : extraction_ctx) : - extraction_ctx * string = - let basename = trait_self_clause_basename in - let name = basename_to_unique ctx basename in - let ctx = ctx_add span TraitSelfClauseId name ctx in - (ctx, name) - (** Generate a unique trait clause name and add it to the context *) let ctx_add_local_trait_clause (span : Meta.span) (origin : generic_origin) (basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) : diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index 3a73c55c6..3734aeddc 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -699,26 +699,9 @@ and extract_trait_instance_id_with_dot (span : Meta.span) (ctx : extraction_ctx) (id : trait_instance_id) : unit = match id with | Self -> - (* There are two situations: - - we are extracting a declared item and need to refer to another - item (for instance, we are extracting a method signature and - need to refer to an associated type). - We directly refer to the other item (we extract trait declarations - as structures, so we can refer to their fields) - - we are extracting a provided method for a trait declaration. We - refer to the item in the self trait clause (see {!SelfTraitClauseId}). - - Remark: we can't get there for trait *implementations* because then the - types should have been normalized. - *) - if ctx.is_provided_method then - (* Provided method: use the trait self clause *) - let self_clause = ctx_get_trait_self_clause span ctx in - F.pp_print_string fmt (self_clause ^ ".") - else - (* Declaration: nothing to print, we will directly refer to - the item. *) - () + (* This can only happen inside a trait (not inside its methods) so there + is nothing to print, we will directly refer to the item.*) + () | _ -> (* Other cases *) extract_trait_instance_id span ctx fmt no_params_tys inside id; @@ -1263,34 +1246,7 @@ let extract_trait_clause_type (span : Meta.span) (ctx : extraction_ctx) let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = if !space then space := false else F.pp_print_space fmt () -(** Extract the trait self clause. - - We add the trait self clause for provided methods (see {!TraitSelfClauseId}). - *) -let extract_trait_self_clause (insert_req_space : unit -> unit) - (ctx : extraction_ctx) (fmt : F.formatter) (trait_decl : trait_decl) - (params : string list) : unit = - insert_req_space (); - F.pp_print_string fmt "("; - let self_clause = ctx_get_trait_self_clause trait_decl.item_meta.span ctx in - F.pp_print_string fmt self_clause; - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - let trait_id = - ctx_get_trait_decl trait_decl.item_meta.span trait_decl.def_id ctx - in - F.pp_print_string fmt trait_id; - List.iter - (fun p -> - F.pp_print_space fmt (); - F.pp_print_string fmt p) - params; - F.pp_print_string fmt ")" - (** - - [trait_decl]: if [Some], it means we are extracting the generics for a provided - method and need to insert a trait self clause (see {!TraitSelfClauseId}). - [as_implicits]: if [explicit] is [None], then we use this parameter to control whether the parameters should be extract as explicit or implicit. *) @@ -1298,10 +1254,9 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) ?(use_forall = false) ?(use_forall_use_sep = true) ?(use_arrows = false) ?(as_implicits : bool = false) ?(space : bool ref option = None) - ?(trait_decl : trait_decl option = None) (origin : generic_origin) - (generics : generic_params) (explicit : explicit_info option) - (type_params : string list) (cg_params : string list) - (trait_clauses : string list) : unit = + (origin : generic_origin) (generics : generic_params) + (explicit : explicit_info option) (type_params : string list) + (cg_params : string list) (trait_clauses : string list) : unit = let all_params = List.concat [ type_params; cg_params; trait_clauses ] in (* HOL4 doesn't support const generics *) cassert __FILE__ __LINE__ @@ -1325,7 +1280,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx) | Some space -> insert_req_space fmt space in (* Print the type/const generic parameters *) - if all_params <> [] then ( + if all_params <> [] then begin if use_forall then ( if use_forall_use_sep then ( insert_req_space (); @@ -1410,58 +1365,8 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx) generics.const_generics, List.map (fun x -> (Explicit, x)) generics.trait_clauses ) in - (* If we extract the generics for a provided method for a trait declaration - (indicated by the trait decl given as input), we need to split the generics: - - we print the generics for the trait decl - - we print the trait self clause - - we print the generics for the trait method - *) - match trait_decl with - | None -> print_generics type_params const_generics trait_clauses - | Some trait_decl -> - (* Split the generics between the generics specific to the trait decl - and those specific to the trait method *) - let open Collections.List in - let dtype_params, mtype_params = - split_at type_params (length trait_decl.generics.types) - in - let dcgs, mcgs = - split_at const_generics (length trait_decl.generics.const_generics) - in - let dtrait_clauses, mtrait_clauses = - split_at trait_clauses (length trait_decl.generics.trait_clauses) - in - (* Extract the trait decl generics - note that we can always deduce - those parameters from the trait self clause: for this reason - they are always implicit *) - let dtype_params = - List.map (fun (_, x) -> (Implicit, x)) dtype_params - in - let dcgs = List.map (fun (_, x) -> (Implicit, x)) dcgs in - let dtrait_clauses = - List.map (fun (_, x) -> (Implicit, x)) dtrait_clauses - in - print_generics dtype_params dcgs dtrait_clauses; - (* Extract the trait self clause *) - let params = - concat - [ - map snd dtype_params; - map - (fun ((_, cg) : _ * const_generic_var) -> - ctx_get_const_generic_var trait_decl.item_meta.span origin - cg.index ctx) - dcgs; - map - (fun (_, c) -> - ctx_get_local_trait_clause trait_decl.item_meta.span origin - c.clause_id ctx) - dtrait_clauses; - ] - in - extract_trait_self_clause insert_req_space ctx fmt trait_decl params; - (* Extract the method generics *) - print_generics mtype_params mcgs mtrait_clauses) + print_generics type_params const_generics trait_clauses + end (** Extract a type declaration. diff --git a/src/pure/Pure.ml b/src/pure/Pure.ml index 1e41ab0bd..fab367e82 100644 --- a/src/pure/Pure.ml +++ b/src/pure/Pure.ml @@ -200,9 +200,6 @@ class ['self] iter_ty_base = object (_self : 'self) inherit [_] iter_type_id inherit! [_] T.iter_const_generic - - method visit_trait_item_name : 'env -> trait_item_name -> unit = - fun _ _ -> () end (** Ancestor for map visitor for [ty] *) @@ -210,30 +207,20 @@ class ['self] map_ty_base = object (_self : 'self) inherit [_] map_type_id inherit! [_] T.map_const_generic - - method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name = - fun _ x -> x end (** Ancestor for reduce visitor for [ty] *) class virtual ['self] reduce_ty_base = - object (self : 'self) + object (_self : 'self) inherit [_] reduce_type_id inherit! [_] T.reduce_const_generic - - method visit_trait_item_name : 'env -> trait_item_name -> 'a = - fun _ _ -> self#zero end (** Ancestor for mapreduce visitor for [ty] *) class virtual ['self] mapreduce_ty_base = - object (self : 'self) + object (_self : 'self) inherit [_] mapreduce_type_id inherit! [_] T.mapreduce_const_generic - - method visit_trait_item_name - : 'env -> trait_item_name -> trait_item_name * 'a = - fun _ x -> (x, self#zero) end type ty = @@ -343,6 +330,9 @@ class ['self] iter_type_decl_base = self#visit_literal_type e var.ty method visit_item_meta : 'env -> T.item_meta -> unit = fun _ _ -> () + + method visit_trait_item_name : 'env -> trait_item_name -> unit = + fun _ _ -> () end (** Ancestor for map visitor for [type_decl] *) @@ -367,6 +357,9 @@ class ['self] map_type_decl_base = } method visit_item_meta : 'env -> T.item_meta -> T.item_meta = fun _ x -> x + + method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name = + fun _ x -> x end (** Ancestor for reduce visitor for [type_decl] *) @@ -388,6 +381,9 @@ class virtual ['self] reduce_type_decl_base = self#plus (self#plus x0 x1) x2 method visit_item_meta : 'env -> T.item_meta -> 'a = fun _ _ -> self#zero + + method visit_trait_item_name : 'env -> trait_item_name -> 'a = + fun _ _ -> self#zero end (** Ancestor for mapreduce visitor for [type_decl] *) @@ -411,6 +407,10 @@ class virtual ['self] mapreduce_type_decl_base = method visit_item_meta : 'env -> T.item_meta -> T.item_meta * 'a = fun _ x -> (x, self#zero) + + method visit_trait_item_name + : 'env -> trait_item_name -> trait_item_name * 'a = + fun _ x -> (x, self#zero) end type field = { diff --git a/src/pure/PureUtils.ml b/src/pure/PureUtils.ml index af11fedea..07a367834 100644 --- a/src/pure/PureUtils.ml +++ b/src/pure/PureUtils.ml @@ -146,32 +146,68 @@ let empty_generic_args : generic_args = let mk_generic_args_from_types (types : ty list) : generic_args = { types; const_generics = []; trait_refs = [] } +(** Generics can be bound in two places: each item has its generics, and + additionally within a trait decl or impl each method has its own generics + (using `binder` above). We distinguish these two cases here. In charon, the + distinction is made thanks to `de_bruijn_var`. + Note that for the generics of a top-level `fun_decl` we always use `Item`; + `Method` only refers to the inner binder found in the list of methods in a + trait_decl/trait_impl. + *) +type generic_origin = Item | Method [@@deriving show, ord] + +(** Charon supports several levels of nested binders; however there are + currently only two cases where we bind non-lifetime variables: at the + top-level of each item, and for each method inside a trait_decl/trait_impl. + Moreover, we use `Free` vars to identify item-bound vars. This means that + we can identify which binder a variable comes from without rigorously + tracking binder levels, which is what this function does. + Note that the `de_bruijn_id`s are wrong anyway because we kept charon's + binding levels but forgot all the region binders. + *) +let origin_from_de_bruijn_var (var : 'a de_bruijn_var) : generic_origin * 'a = + match var with + | Bound (_, id) -> (Method, id) + | Free id -> (Item, id) + type subst = { ty_subst : TypeVarId.id -> ty; cg_subst : ConstGenericVarId.id -> const_generic; tr_subst : TraitClauseId.id -> trait_instance_id; + method_ty_subst : TypeVarId.id -> ty; + method_cg_subst : ConstGenericVarId.id -> const_generic; + method_tr_subst : TraitClauseId.id -> trait_instance_id; tr_self : trait_instance_id; } -(** Type substitution *) -let ty_substitute (subst : subst) (ty : ty) : ty = - let obj = - object - inherit [_] map_ty +let subst_visitor = + object + inherit [_] map_ty - method! visit_TVar _ var = - subst.ty_subst (Substitute.expect_free_var None var) + method! visit_TVar subst var = + let origin, id = origin_from_de_bruijn_var var in + match origin with + | Item -> subst.ty_subst id + | Method -> subst.method_ty_subst id - method! visit_CgVar _ var = - subst.cg_subst (Substitute.expect_free_var None var) + method! visit_CgVar subst var = + let origin, id = origin_from_de_bruijn_var var in + match origin with + | Item -> subst.cg_subst id + | Method -> subst.method_cg_subst id - method! visit_Clause _ var = - subst.tr_subst (Substitute.expect_free_var None var) + method! visit_Clause subst var = + let origin, id = origin_from_de_bruijn_var var in + match origin with + | Item -> subst.tr_subst id + | Method -> subst.method_tr_subst id - method! visit_Self _ = subst.tr_self - end - in - obj#visit_ty () ty + method! visit_Self subst = subst.tr_self + end + +(** Type substitution *) +let ty_substitute (subst : subst) (ty : ty) : ty = + subst_visitor#visit_ty subst ty let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty = @@ -190,6 +226,54 @@ let make_trait_subst (clauses : trait_clause list) (refs : trait_ref list) : let mp = TraitClauseId.Map.of_list (List.combine clauses refs) in fun id -> TraitClauseId.Map.find id mp +let make_subst_from_generics (params : generic_params) (args : generic_args) : + subst = + let ty_subst = make_type_subst params.types args.types in + let cg_subst = + make_const_generic_subst params.const_generics args.const_generics + in + let tr_subst = make_trait_subst params.trait_clauses args.trait_refs in + let err _ = + craise_opt_span __FILE__ __LINE__ None "Found unexpected bound variable" + in + { + ty_subst; + cg_subst; + tr_subst; + method_ty_subst = err; + method_cg_subst = err; + method_tr_subst = err; + tr_self = Self; + } + +let make_subst_from_generics_including_methods (item_params : generic_params) + (method_params : generic_params) (tr_self : trait_instance_id) + (item_args : generic_args) (method_args : generic_args) : subst = + let ty_subst = make_type_subst item_params.types item_args.types in + let cg_subst = + make_const_generic_subst item_params.const_generics item_args.const_generics + in + let tr_subst = + make_trait_subst item_params.trait_clauses item_args.trait_refs + in + let method_ty_subst = make_type_subst method_params.types method_args.types in + let method_cg_subst = + make_const_generic_subst method_params.const_generics + method_args.const_generics + in + let method_tr_subst = + make_trait_subst method_params.trait_clauses method_args.trait_refs + in + { + ty_subst; + cg_subst; + tr_subst; + method_ty_subst; + method_cg_subst; + method_tr_subst; + tr_self; + } + (** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}. Raises [Invalid_argument] if the arguments are incorrect. @@ -212,15 +296,6 @@ let type_decl_get_fields (def : type_decl) - def: " ^ show_type_decl def ^ "\n- opt_variant_id: " ^ opt_variant_id)) -let make_subst_from_generics (params : generic_params) (args : generic_args) : - subst = - let ty_subst = make_type_subst params.types args.types in - let cg_subst = - make_const_generic_subst params.const_generics args.const_generics - in - let tr_subst = make_trait_subst params.trait_clauses args.trait_refs in - { ty_subst; cg_subst; tr_subst; tr_self = Self } - (** Instantiate the type variables for the chosen variant in an ADT definition, and return the list of the types of its fields *) let type_decl_get_instantiated_fields_types (def : type_decl) @@ -779,23 +854,25 @@ let rec typed_pattern_to_texpression (span : Meta.span) (pat : typed_pattern) : | None -> None | Some e -> Some { e; ty = pat.ty } -type trait_decl_method_decl_id = { is_provided : bool; id : fun_decl_id } +type trait_decl_method = { + is_provided : bool; + bound_method : fun_decl_ref binder; +} let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) : - trait_decl_method_decl_id = + trait_decl_method = (* First look in the required methods *) let bound_method = List.find_opt (fun (s, _) -> s = method_name) trait_decl.required_methods in match bound_method with - | Some (_, bound_method) -> - { is_provided = false; id = bound_method.binder_value.fun_id } + | Some (_, bound_method) -> { is_provided = false; bound_method } | None -> (* Must be a provided method *) let _, bound_method = List.find (fun (s, _) -> s = method_name) trait_decl.provided_methods in - { is_provided = true; id = bound_method.binder_value.fun_id } + { is_provided = true; bound_method } let trait_decl_is_empty (trait_decl : trait_decl) : bool = let { diff --git a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v index d389498a5..2b25290fc 100644 --- a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v +++ b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v @@ -23,7 +23,7 @@ Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit). Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43 Name pattern: core::clone::Clone::clone_from *) Axiom core_clone_Clone_clone_from : - forall{Self : Type} (self_clause : core_clone_Clone Self), + forall{Self : Type} (cloneInst1 : core_clone_Clone Self), Self -> Self -> state -> result (state * Self) . diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index c3002326a..a920b43a6 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -32,7 +32,7 @@ Axiom core_cell_Cell_get_mut : Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43 Name pattern: core::clone::Clone::clone_from *) Axiom core_clone_Clone_clone_from : - forall{Self : Type} (self_clause : core_clone_Clone Self), + forall{Self : Type} (cloneInst1 : core_clone_Clone Self), Self -> Self -> state -> result (state * Self) . diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v index 8111a9bae..b7b0d4c6b 100644 --- a/tests/coq/rename_attribute/RenameAttribute.v +++ b/tests/coq/rename_attribute/RenameAttribute.v @@ -30,16 +30,14 @@ Definition BoolImpl : BoolTest_t bool := {| (** [rename_attribute::BoolTrait::ret_true]: Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) -Definition boolTrait_retTest - {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool := +Definition boolTrait_retTest {Self : Type} (self : Self) : result bool := Ok true . (** [rename_attribute::test_bool_trait]: Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *) Definition boolFn (T : Type) (x : bool) : result bool := - b <- boolTraitBool_getTest x; - if b then boolTrait_retTest BoolImpl x else Ok false + b <- boolTraitBool_getTest x; if b then boolTrait_retTest x else Ok false . (** [rename_attribute::SimpleEnum] diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index 4f9df3c9a..47e5756fb 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -30,16 +30,14 @@ Definition BoolTraitBool : BoolTrait_t bool := {| (** [traits::BoolTrait::ret_true]: Source: 'tests/src/traits.rs', lines 8:4-10:5 *) -Definition boolTrait_ret_true - {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool := +Definition boolTrait_ret_true {Self : Type} (self : Self) : result bool := Ok true . (** [traits::test_bool_trait_bool]: Source: 'tests/src/traits.rs', lines 19:0-21:1 *) Definition test_bool_trait_bool (x : bool) : result bool := - b <- boolTraitBool_get_bool x; - if b then boolTrait_ret_true BoolTraitBool x else Ok false + b <- boolTraitBool_get_bool x; if b then boolTrait_ret_true x else Ok false . (** [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: @@ -58,8 +56,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {| (** [traits::test_bool_trait_option]: Source: 'tests/src/traits.rs', lines 33:0-35:1 *) Definition test_bool_trait_option {T : Type} (x : option T) : result bool := - b <- boolTraitOption_get_bool x; - if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false + b <- boolTraitOption_get_bool x; if b then boolTrait_ret_true x else Ok false . (** [traits::test_bool_trait]: diff --git a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti index e94419c50..2769fc967 100644 --- a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti +++ b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti @@ -18,6 +18,6 @@ val utils_serialize : hashMap_t u64 -> state -> result (state & unit) Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43 Name pattern: core::clone::Clone::clone_from *) val core_clone_Clone_clone_from - (#self : Type0) (self_clause : core_clone_Clone self) : + (#self : Type0) (cloneInst : core_clone_Clone self) : self -> self -> state -> result (state & self) diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti index 9fca284e1..04467d2ff 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -25,6 +25,6 @@ val core_cell_Cell_get_mut Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43 Name pattern: core::clone::Clone::clone_from *) val core_clone_Clone_clone_from - (#self : Type0) (self_clause : core_clone_Clone self) : + (#self : Type0) (cloneInst : core_clone_Clone self) : self -> self -> state -> result (state & self) diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst index 1b9b63cc1..adc80c19b 100644 --- a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst +++ b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst @@ -18,17 +18,14 @@ let boolImpl : boolTest_t bool = { getTest = boolTraitBool_getTest; } (** [rename_attribute::BoolTrait::ret_true]: Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) -let boolTrait_retTest - (#self : Type0) (self_clause : boolTest_t self) (self1 : self) : - result bool - = +let boolTrait_retTest (#self : Type0) (self1 : self) : result bool = Ok true (** [rename_attribute::test_bool_trait]: Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *) let boolFn (t : Type0) (x : bool) : result bool = let* b = boolTraitBool_getTest x in - if b then boolTrait_retTest boolImpl x else Ok false + if b then boolTrait_retTest x else Ok false (** [rename_attribute::C] Source: 'tests/src/rename_attribute.rs', lines 50:0-50:28 *) diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 9f6cc5e75..0e42ccce2 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -20,17 +20,14 @@ let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; } (** [traits::BoolTrait::ret_true]: Source: 'tests/src/traits.rs', lines 8:4-10:5 *) -let boolTrait_ret_true - (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) : - result bool - = +let boolTrait_ret_true (#self : Type0) (self1 : self) : result bool = Ok true (** [traits::test_bool_trait_bool]: Source: 'tests/src/traits.rs', lines 19:0-21:1 *) let test_bool_trait_bool (x : bool) : result bool = let* b = boolTraitBool_get_bool x in - if b then boolTrait_ret_true boolTraitBool x else Ok false + if b then boolTrait_ret_true x else Ok false (** [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: Source: 'tests/src/traits.rs', lines 25:4-30:5 *) @@ -47,7 +44,7 @@ let boolTraitOption (t : Type0) : boolTrait_t (option t) = { Source: 'tests/src/traits.rs', lines 33:0-35:1 *) let test_bool_trait_option (#t : Type0) (x : option t) : result bool = let* b = boolTraitOption_get_bool x in - if b then boolTrait_ret_true (boolTraitOption t) x else Ok false + if b then boolTrait_ret_true x else Ok false (** [traits::test_bool_trait]: Source: 'tests/src/traits.rs', lines 37:0-39:1 *) diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean index ff7b746ab..f6ca2c332 100644 --- a/tests/lean/RenameAttribute.lean +++ b/tests/lean/RenameAttribute.lean @@ -27,8 +27,7 @@ def BoolImpl : BoolTest Bool := { /- [rename_attribute::BoolTrait::ret_true]: Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/ -def BoolTrait.retTest - {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool := +def BoolTrait.retTest {Self : Type} (self : Self) : Result Bool := Result.ok true /- [rename_attribute::test_bool_trait]: @@ -37,7 +36,7 @@ def BoolFn (T : Type) (x : Bool) : Result Bool := do let b ← BoolTraitBool.getTest x if b - then BoolTrait.retTest BoolImpl x + then BoolTrait.retTest x else Result.ok false /- [rename_attribute::SimpleEnum] diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 93b17b90c..9acd6c78f 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -27,8 +27,7 @@ def BoolTraitBool : BoolTrait Bool := { /- [traits::BoolTrait::ret_true]: Source: 'tests/src/traits.rs', lines 8:4-10:5 -/ -def BoolTrait.ret_true - {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := +def BoolTrait.ret_true {Self : Type} (self : Self) : Result Bool := Result.ok true /- [traits::test_bool_trait_bool]: @@ -37,7 +36,7 @@ def test_bool_trait_bool (x : Bool) : Result Bool := do let b ← BoolTraitBool.get_bool x if b - then BoolTrait.ret_true BoolTraitBool x + then BoolTrait.ret_true x else Result.ok false /- [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: @@ -60,7 +59,7 @@ def test_bool_trait_option {T : Type} (x : Option T) : Result Bool := do let b ← BoolTraitOption.get_bool x if b - then BoolTrait.ret_true (BoolTraitOption T) x + then BoolTrait.ret_true x else Result.ok false /- [traits::test_bool_trait]: diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 3277563cc..8e5bb740c 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -13,5 +13,5 @@ Called from Aeneas__Translate.extract_definitions.export_decl_group in file "Tra Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 886, characters 2-177 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1018, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1652, characters 5-42 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1651, characters 5-42 Called from Dune__exe__Main in file "Main.ml", line 493, characters 11-63