From dccf4fd1777cb65e74626b609e30c4ebd067c13e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 4 Dec 2024 14:59:45 +0100 Subject: [PATCH 1/9] Use a `RegionBinder` for `TyKind::Arrow` --- charon-ml/src/CharonVersion.ml | 2 +- charon-ml/src/GAstOfJson.ml | 12 ++++----- charon-ml/src/NameMatcher.ml | 27 ++++++++++++------- charon-ml/src/PrintTypes.ml | 5 ++-- charon-ml/src/Substitute.ml | 14 ---------- charon-ml/src/Types.ml | 2 +- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- charon/src/ast/types.rs | 2 +- charon/src/ast/types_utils.rs | 25 ++++++++++------- .../translate/translate_types.rs | 5 +++- charon/src/name_matcher/mod.rs | 14 +++++----- charon/src/pretty/fmt_with_ctx.rs | 13 ++++----- 13 files changed, 62 insertions(+), 63 deletions(-) diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 461ea417c..ed865877c 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.53" +let supported_charon_version = "0.1.54" diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index b71de0891..46096831c 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -1329,13 +1329,13 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result = | `Assoc [ ("DynTrait", dyn_trait) ] -> let* dyn_trait = existential_predicate_of_json ctx dyn_trait in Ok (TDynTrait dyn_trait) - | `Assoc [ ("Arrow", `List [ x_0; x_1; x_2 ]) ] -> - let* x_0 = - vector_of_json region_id_of_json region_var_of_json ctx x_0 + | `Assoc [ ("Arrow", arrow) ] -> + let* arrow = + region_binder_of_json + (pair_of_json (list_of_json ty_of_json) ty_of_json) + ctx arrow in - let* x_1 = list_of_json ty_of_json ctx x_1 in - let* x_2 = ty_of_json ctx x_2 in - Ok (TArrow (x_0, x_1, x_2)) + Ok (TArrow arrow) | _ -> Error "") and builtin_ty_of_json (ctx : of_json_ctx) (js : json) : diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 91e1c9b7e..6f6e54eba 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -551,15 +551,19 @@ and match_expr_with_ty (ctx : ctx) (c : match_config) (m : maps) (pty : expr) | EVar v, _ -> opt_update_tmap c m v ty | EComp pid, TTraitType (trait_ref, type_name) -> match_trait_type ctx c m pid trait_ref type_name - | EArrow (pinputs, pout), TArrow (regions, inputs, out) -> ( + | EArrow (pinputs, pout), TArrow binder -> begin (* Push a region group in the map, if necessary - TODO: make this more precise *) - let m = maps_push_bound_regions_group_if_nonempty m regions in + let m = + maps_push_bound_regions_group_if_nonempty m binder.binder_regions + in + let inputs, output = binder.binder_value in (* Match *) List.for_all2 (match_expr_with_ty ctx c m) pinputs inputs && match pout with - | None -> out = TypesUtils.mk_unit_ty - | Some pout -> match_expr_with_ty ctx c m pout out) + | None -> output = TypesUtils.mk_unit_ty + | Some pout -> match_expr_with_ty ctx c m pout output + end | ERawPtr (Mut, pty), TRawPtr (ty, RMut) -> match_expr_with_ty ctx c m pty ty | ERawPtr (Not, pty), TRawPtr (ty, RShared) -> match_expr_with_ty ctx c m pty ty @@ -969,15 +973,18 @@ and ty_to_pattern_aux (ctx : ctx) (c : to_pat_config) (m : constraints) TypesUtils.empty_generic_args in EComp name - | TArrow (regions, inputs, out) -> + | TArrow binder -> (* Push a regions map if necessary - TODO: make this more precise *) - let m = constraints_map_push_regions_map_if_nonempty m regions in + let m = + constraints_map_push_regions_map_if_nonempty m binder.binder_regions + in + let inputs, output = binder.binder_value in let inputs = List.map (ty_to_pattern_aux ctx c m) inputs in - let out = - if out = TypesUtils.mk_unit_ty then None - else Some (ty_to_pattern_aux ctx c m out) + let output = + if output = TypesUtils.mk_unit_ty then None + else Some (ty_to_pattern_aux ctx c m output) in - EArrow (inputs, out) + EArrow (inputs, output) | TRawPtr (ty, RMut) -> ERawPtr (Mut, ty_to_pattern_aux ctx c m ty) | TRawPtr (ty, RShared) -> ERawPtr (Not, ty_to_pattern_aux ctx c m ty) | TDynTrait _ -> raise (Failure "Unimplemented: DynTrait") diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 2f0305e9d..fdf4aeb77 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -183,8 +183,9 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = match ref_kind with | RMut -> "*mut " ^ ty_to_string env rty | RShared -> "*const " ^ ty_to_string env rty) - | TArrow (regions, inputs, output) -> - let env = { env with regions = regions :: env.regions } in + | TArrow binder -> + let env = { env with regions = binder.binder_regions :: env.regions } in + let inputs, output = binder.binder_value in let inputs = "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> " in diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index 7978edc44..a8722f8e2 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -34,20 +34,6 @@ let st_substitute_visitor = inherit [_] map_statement method! visit_region (subst : subst) r = subst.r_subst r - (** We need to properly handle the DeBruijn indices *) - method! visit_TArrow (subst : subst) regions inputs output = - (* Decrement the DeBruijn indices before calling the substitution *) - let r_subst r = - match r with - | RBVar (db, rid) -> subst.r_subst (RBVar (db - 1, rid)) - | _ -> subst.r_subst r - in - let subst = { subst with r_subst } in - (* Note that we ignore the bound regions variables *) - let inputs = List.map (self#visit_ty subst) inputs in - let output = self#visit_ty subst output in - TArrow (regions, inputs, output) - (** We need to properly handle the DeBruijn indices *) method! visit_region_binder visit_value (subst : subst) x = (* Decrement the DeBruijn indices before calling the substitution *) diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index baba5f4ae..3c902ff67 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -494,7 +494,7 @@ and ty = TODO: we don't translate this properly yet. *) - | TArrow of region_var list * ty list * ty + | TArrow of (ty list * ty) region_binder (** Arrow type, used in particular for the local function pointers. This is essentially a "constrained" function signature: arrow types can only contain generic lifetime parameters diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 9ed3b1c87..c6777b7c6 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -213,7 +213,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.53" +version = "0.1.54" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index bdfc0715e..ba679034a 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.53" +version = "0.1.54" authors = ["Son Ho "] edition = "2021" license = "Apache-2.0" diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 4b9fb2a94..985bd1c6c 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -755,7 +755,7 @@ pub enum TyKind { /// This is essentially a "constrained" function signature: /// arrow types can only contain generic lifetime parameters /// (no generic types), no predicates, etc. - Arrow(Vector, Vec, Ty), + Arrow(RegionBinder<(Vec, Ty)>), } /// Builtin types identifiers. diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 80d7fddd2..adfe76ebd 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -535,12 +535,15 @@ impl std::ops::DerefMut for VisitInsideTy { } } +type FnTys = (Vec, Ty); + /// Visitor for the [Ty::substitute] function. #[derive(VisitorMut)] #[visitor( PolyTraitDeclRef(enter, exit), + FnTys(enter, exit), Region(exit), - Ty(enter, exit), + Ty(exit), ConstGeneric(exit), TraitRef(exit) )] @@ -548,8 +551,9 @@ struct SubstVisitor<'a> { generics: &'a GenericArgs, // Tracks the depth of binders we're inside of. // Important: we must update it whenever we go inside a binder. Visitors are not generic so we - // must handle all the specific cases by hand. So far there's only `PolyTraitDeclRef` but there - // may be more in the future. + // must handle all the specific cases by hand. So far there's: + // - `PolyTraitDeclRef` + // - The contents of `TyKind::Arrow` binder_depth: DeBruijnId, } @@ -569,6 +573,14 @@ impl<'a> SubstVisitor<'a> { self.binder_depth = self.binder_depth.decr(); } + fn enter_fn_tys(&mut self, _: &mut FnTys) { + self.binder_depth = self.binder_depth.incr(); + } + + fn exit_fn_tys(&mut self, _: &mut FnTys) { + self.binder_depth = self.binder_depth.decr(); + } + fn exit_region(&mut self, r: &mut Region) { match r { Region::BVar(db, id) => { @@ -580,16 +592,9 @@ impl<'a> SubstVisitor<'a> { } } - fn enter_ty(&mut self, ty: &mut Ty) { - match ty.kind() { - TyKind::Arrow(_, _, _) => self.binder_depth = self.binder_depth.incr(), - _ => {} - } - } fn exit_ty(&mut self, ty: &mut Ty) { match ty.kind() { TyKind::TypeVar(id) => *ty = self.generics.types.get(*id).unwrap().clone(), - TyKind::Arrow(_, _, _) => self.binder_depth = self.binder_depth.decr(), _ => (), } } diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 2ecb52919..1dadcd6ed 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -323,7 +323,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { .map(|x| ctx.translate_ty(span, x)) .try_collect()?; let output = ctx.translate_ty(span, &sig.value.output)?; - Ok(TyKind::Arrow(regions, inputs, output)) + Ok(TyKind::Arrow(RegionBinder { + regions, + skip_binder: (inputs, output), + })) })? } hax::TyKind::Error => { diff --git a/charon/src/name_matcher/mod.rs b/charon/src/name_matcher/mod.rs index c467d5bf4..30d210178 100644 --- a/charon/src/name_matcher/mod.rs +++ b/charon/src/name_matcher/mod.rs @@ -96,14 +96,14 @@ impl Pattern { self.matches_with_generics(ctx, &name, args) } TyKind::Adt(TypeId::Tuple, _) - | TyKind::TypeVar(_) - | TyKind::Literal(_) + | TyKind::TypeVar(..) + | TyKind::Literal(..) | TyKind::Never - | TyKind::Ref(_, _, _) - | TyKind::RawPtr(_, _) - | TyKind::TraitType(_, _) - | TyKind::DynTrait(_) - | TyKind::Arrow(_, _, _) => false, + | TyKind::Ref(..) + | TyKind::RawPtr(..) + | TyKind::TraitType(..) + | TyKind::DynTrait(..) + | TyKind::Arrow(..) => false, } } diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index dda8f7ba7..a770d405f 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1346,22 +1346,19 @@ impl FmtWithCtx for Ty { format!("{}::{name}", trait_ref.fmt_with_ctx(ctx),) } TyKind::DynTrait(pred) => format!("dyn ({})", pred.with_ctx(ctx)), - TyKind::Arrow(regions, inputs, output) => { + TyKind::Arrow(io) => { // Update the bound regions - let ctx = &ctx.push_bound_regions(regions); + let ctx = &ctx.push_bound_regions(&io.regions); - let regions = if regions.is_empty() { + let regions = if io.regions.is_empty() { "".to_string() } else { format!( "<{}>", - regions - .iter() - .map(|r| ctx.format_object(r)) - .collect::>() - .join(", ") + io.regions.iter().map(|r| ctx.format_object(r)).join(", ") ) }; + let (inputs, output) = &io.skip_binder; let inputs = inputs .iter() .map(|x| x.fmt_with_ctx(ctx)) From 07367c56b82bd1caf7b7746b7051531fc723ea00 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 4 Dec 2024 15:18:51 +0100 Subject: [PATCH 2/9] Add `visit_{free,bound}_region` visitor methods In preparation for what comes next. --- charon-ml/src/Types.ml | 47 ++++++++++++++++++- charon/src/bin/generate-ml/main.rs | 2 +- charon/src/bin/generate-ml/templates/Types.ml | 42 +++++++++++++++++ 3 files changed, 88 insertions(+), 3 deletions(-) diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 3c902ff67..7a3860386 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -522,19 +522,62 @@ and builtin_ty = ord, visitors { - name = "iter_ty"; + name = "iter_ty_inner"; variety = "iter"; ancestors = [ "iter_ty_base_base" ]; nude = true (* Don't inherit VisitorsRuntime *); }, visitors { - name = "map_ty"; + name = "map_ty_inner"; variety = "map"; ancestors = [ "map_ty_base_base" ]; nude = true (* Don't inherit VisitorsRuntime *); }] +(** Ancestor for iter visitor for {!type: Types.ty} *) +class ['self] iter_ty = + object (self : 'self) + inherit [_] iter_ty_inner + + method! visit_RBVar env (db_id : region_db_id) (var_id : region_var_id) = + self#visit_bound_region env db_id var_id + + method visit_bound_region env (db_id : region_db_id) + (var_id : region_var_id) = + self#visit_region_db_id env db_id; + self#visit_region_var_id env var_id + + method! visit_RFVar env (var_id : region_id) = + self#visit_free_region env var_id + + method visit_free_region env (var_id : region_id) = + self#visit_region_id env var_id + end + +(** Ancestor for map visitor for {!type: Types.ty} *) +class virtual ['self] map_ty = + object (self : 'self) + inherit [_] map_ty_inner + + method! visit_RBVar env (db_id : region_db_id) (var_id : region_var_id) = + let db_id, var_id = self#visit_bound_region env db_id var_id in + RBVar (db_id, var_id) + + method visit_bound_region env (db_id : region_db_id) + (var_id : region_var_id) = + let db_id = self#visit_region_db_id env db_id in + let var_id = self#visit_region_var_id env var_id in + (db_id, var_id) + + method! visit_RFVar env (var_id : region_id) = + let var_id = self#visit_free_region env var_id in + RFVar var_id + + method visit_free_region env (var_id : region_id) = + self#visit_region_id env var_id + end + (* Ancestors for the generic_params visitors *) class ['self] iter_generic_params_base = object (self : 'self) diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 4a12a8515..6b751bc2f 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1352,7 +1352,7 @@ fn generate_ml( // Can't merge into above because aeneas uses the above alongside their own partial // copy of `ty`, which causes method type clashes. (GenerationKind::TypeDecl(Some(DeriveVisitors { - name: "ty", + name: "ty_inner", ancestor: Some("ty_base_base"), reduce: false, extra_types: &[], diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index a75df0c4e..91159fa56 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -162,6 +162,48 @@ class virtual ['self] map_ty_base_base = (* __REPLACE2__ *) +(** Ancestor for iter visitor for {!type: Types.ty} *) +class ['self] iter_ty = + object (self : 'self) + inherit [_] iter_ty_inner + + method! visit_RBVar env (db_id: region_db_id) (var_id: region_var_id) = + self#visit_bound_region env db_id var_id + + method visit_bound_region env (db_id: region_db_id) (var_id: region_var_id) = + self#visit_region_db_id env db_id; + self#visit_region_var_id env var_id + + method! visit_RFVar env (var_id: region_id) = + self#visit_free_region env var_id + + method visit_free_region env (var_id: region_id) = + self#visit_region_id env var_id + end + +(** Ancestor for map visitor for {!type: Types.ty} *) +class virtual ['self] map_ty = + object (self : 'self) + inherit [_] map_ty_inner + + method! visit_RBVar env (db_id: region_db_id) (var_id: region_var_id) = + let (db_id, var_id) = self#visit_bound_region env db_id var_id in + RBVar (db_id, var_id) + + method visit_bound_region env (db_id: region_db_id) (var_id: region_var_id) = + let db_id = self#visit_region_db_id env db_id in + let var_id = self#visit_region_var_id env var_id in + (db_id, var_id) + + method! visit_RFVar env (var_id: region_id) = + let var_id = self#visit_free_region env var_id in + RFVar var_id + + method visit_free_region env (var_id: region_id) = + self#visit_region_id env var_id + end + + (* __REPLACE3__ *) (* __REPLACE4__ *) From 94c4d97eea322a4b9d4320eec2ce1869e92541f6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 4 Dec 2024 17:03:50 +0100 Subject: [PATCH 3/9] Rename ocaml `region_id` to `free_region_id` --- charon-ml/src/PrintTypes.ml | 6 ++-- charon-ml/src/Types.ml | 29 ++++++++++--------- charon-ml/src/TypesUtils.ml | 16 +++++----- charon/src/ast/types.rs | 1 + charon/src/bin/generate-ml/main.rs | 5 ++-- charon/src/bin/generate-ml/templates/Types.ml | 15 +++++----- 6 files changed, 38 insertions(+), 34 deletions(-) diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index fdf4aeb77..637765f88 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -29,8 +29,8 @@ let region_var_id_to_pretty_string (db_id : region_db_id) (id : region_var_id) : string = "'" ^ show_region_db_id db_id ^ "_" ^ RegionVarId.to_string id -let region_id_to_pretty_string (id : region_id) : string = - "'" ^ RegionId.to_string id +let free_region_id_to_pretty_string (id : free_region_id) : string = + "'" ^ FreeRegionId.to_string id let type_var_id_to_pretty_string (id : type_var_id) : string = "T@" ^ TypeVarId.to_string id @@ -93,7 +93,7 @@ let region_to_string (env : 'a fmt_env) (r : region) : string = | RStatic -> "'static" | RErased -> "'_" | RBVar (db, rid) -> region_var_id_to_string env db rid - | RFVar rid -> region_id_to_pretty_string rid + | RFVar rid -> free_region_id_to_pretty_string rid let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 7a3860386..b3b8c5318 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -22,7 +22,7 @@ module TraitImplId = IdGen () module TraitClauseId = IdGen () module UnsolvedTraitId = IdGen () module RegionVarId = IdGen () -module RegionId = IdGen () +module FreeRegionId = IdGen () module RegionGroupId = IdGen () module Disambiguator = IdGen () module FunDeclId = IdGen () @@ -40,6 +40,7 @@ type region_db_id = int [@@deriving show, ord] *) type region_var_id = RegionVarId.id [@@deriving show, ord] +type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] type ('id, 'name) indexed_var = { @@ -57,7 +58,6 @@ and disambiguator = Disambiguator.id and type_var_id = TypeVarId.id and variant_id = VariantId.id and field_id = FieldId.id -and region_id = RegionId.id and const_generic_var_id = ConstGenericVarId.id and trait_clause_id = TraitClauseId.id [@@deriving show, ord] @@ -82,7 +82,7 @@ class ['self] iter_const_generic_base = method visit_fun_decl_id : 'env -> fun_decl_id -> unit = fun _ _ -> () method visit_global_decl_id : 'env -> global_decl_id -> unit = fun _ _ -> () method visit_region_db_id : 'env -> region_db_id -> unit = fun _ _ -> () - method visit_region_id : 'env -> region_id -> unit = fun _ _ -> () + method visit_free_region_id : 'env -> free_region_id -> unit = fun _ _ -> () method visit_region_var_id : 'env -> region_var_id -> unit = fun _ _ -> () method visit_trait_clause_id : 'env -> trait_clause_id -> unit = @@ -110,7 +110,8 @@ class ['self] map_const_generic_base = method visit_region_db_id : 'env -> region_db_id -> region_db_id = fun _ x -> x - method visit_region_id : 'env -> region_id -> region_id = fun _ x -> x + method visit_free_region_id : 'env -> free_region_id -> free_region_id = + fun _ x -> x method visit_region_var_id : 'env -> region_var_id -> region_var_id = fun _ x -> x @@ -145,7 +146,8 @@ class virtual ['self] reduce_const_generic_base = method visit_region_db_id : 'env -> region_db_id -> 'a = fun _ _ -> self#zero - method visit_region_id : 'env -> region_id -> 'a = fun _ _ -> self#zero + method visit_free_region_id : 'env -> free_region_id -> 'a = + fun _ _ -> self#zero method visit_region_var_id : 'env -> region_var_id -> 'a = fun _ _ -> self#zero @@ -183,7 +185,8 @@ class virtual ['self] mapreduce_const_generic_base = method visit_region_db_id : 'env -> region_db_id -> region_db_id * 'a = fun _ x -> (x, self#zero) - method visit_region_id : 'env -> region_id -> region_id * 'a = + method visit_free_region_id : 'env -> free_region_id -> free_region_id * 'a + = fun _ x -> (x, self#zero) method visit_region_var_id : 'env -> region_var_id -> region_var_id * 'a = @@ -353,7 +356,7 @@ and region = | RStatic (** Static region *) | RBVar of region_db_id * region_var_id (** Bound region. We use those in function signatures, type definitions, etc. *) - | RFVar of region_id + | RFVar of free_region_id (** Free region. We use those during the symbolic execution. *) | RErased (** Erased region *) @@ -548,11 +551,11 @@ class ['self] iter_ty = self#visit_region_db_id env db_id; self#visit_region_var_id env var_id - method! visit_RFVar env (var_id : region_id) = + method! visit_RFVar env (var_id : free_region_id) = self#visit_free_region env var_id - method visit_free_region env (var_id : region_id) = - self#visit_region_id env var_id + method visit_free_region env (var_id : free_region_id) = + self#visit_free_region_id env var_id end (** Ancestor for map visitor for {!type: Types.ty} *) @@ -570,12 +573,12 @@ class virtual ['self] map_ty = let var_id = self#visit_region_var_id env var_id in (db_id, var_id) - method! visit_RFVar env (var_id : region_id) = + method! visit_RFVar env (var_id : free_region_id) = let var_id = self#visit_free_region env var_id in RFVar var_id - method visit_free_region env (var_id : region_id) = - self#visit_region_id env var_id + method visit_free_region env (var_id : free_region_id) = + self#visit_free_region_id env var_id end (* Ancestors for the generic_params visitors *) diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml index d20113b9d..bc7492f8e 100644 --- a/charon-ml/src/TypesUtils.ml +++ b/charon-ml/src/TypesUtils.ml @@ -194,22 +194,22 @@ let mk_box_ty (ty : ty) : ty = This function should be used on non-erased and non-bound regions. For sanity, we raise exceptions if this is not the case. *) -let region_in_set (r : region) (rset : RegionId.Set.t) : bool = +let region_in_set (r : region) (rset : FreeRegionId.Set.t) : bool = match r with | RStatic -> false | RErased -> raise (Failure "region_in_set shouldn't be called on erased regions") | RBVar _ -> raise (Failure "region_in_set shouldn't be called on bound regions") - | RFVar id -> RegionId.Set.mem id rset + | RFVar id -> FreeRegionId.Set.mem id rset (** Return the set of regions in an type - TODO: add static? This function should be used on non-erased and non-bound regions. For sanity, we raise exceptions if this is not the case. *) -let ty_regions (ty : ty) : RegionId.Set.t = - let s = ref RegionId.Set.empty in +let ty_regions (ty : ty) : FreeRegionId.Set.t = + let s = ref FreeRegionId.Set.empty in let add_region (r : region) = match r with | RStatic -> () (* TODO: static? *) @@ -217,7 +217,7 @@ let ty_regions (ty : ty) : RegionId.Set.t = raise (Failure "ty_regions shouldn't be called on erased regions") | RBVar _ -> raise (Failure "region_in_set shouldn't be called on bound regions") - | RFVar rid -> s := RegionId.Set.add rid !s + | RFVar rid -> s := FreeRegionId.Set.add rid !s in let obj = object @@ -231,9 +231,9 @@ let ty_regions (ty : ty) : RegionId.Set.t = !s (* TODO: merge with ty_has_regions_in_set *) -let ty_regions_intersect (ty : ty) (regions : RegionId.Set.t) : bool = +let ty_regions_intersect (ty : ty) (regions : FreeRegionId.Set.t) : bool = let ty_regions = ty_regions ty in - not (RegionId.Set.disjoint ty_regions regions) + not (FreeRegionId.Set.disjoint ty_regions regions) (** Check if a {!type:Charon.Types.ty} contains regions from a given set *) let ty_has_regions_in_pred (pred : region -> bool) (ty : ty) : bool = @@ -249,5 +249,5 @@ let ty_has_regions_in_pred (pred : region -> bool) (ty : ty) : bool = with Found -> true (** Check if a {!type:Charon.Types.ty} contains regions from a given set *) -let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : ty) : bool = +let ty_has_regions_in_set (rset : FreeRegionId.Set.t) (ty : ty) : bool = ty_has_regions_in_pred (fun r -> region_in_set r rset) ty diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 985bd1c6c..6c70969eb 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -15,6 +15,7 @@ generate_index_type!(TypeVarId, "T"); generate_index_type!(VariantId, "Variant"); generate_index_type!(FieldId, "Field"); generate_index_type!(RegionId, "Region"); +generate_index_type!(FreeRegionId, "FreeRegion"); generate_index_type!(ConstGenericVarId, "Const"); /// Type variable. diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 6b751bc2f..16083d58d 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1018,7 +1018,7 @@ fn generate_ml( | RStatic (** Static region *) | RBVar of region_db_id * region_var_id (** Bound region. We use those in function signatures, type definitions, etc. *) - | RFVar of region_id + | RFVar of free_region_id (** Free region. We use those during the symbolic execution. *) | RErased (** Erased region *) " @@ -1321,7 +1321,6 @@ fn generate_ml( "FieldId", "FunDeclId", "GlobalDeclId", - "RegionId", "TraitClauseId", "TraitDeclId", "TraitImplId", @@ -1338,7 +1337,7 @@ fn generate_ml( "fun_decl_id", "global_decl_id", "region_db_id", - "region_id", + "free_region_id", "region_var_id", "trait_clause_id", "trait_decl_id", diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index 91159fa56..4b2d679de 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -23,7 +23,7 @@ module TraitImplId = IdGen () module TraitClauseId = IdGen () module UnsolvedTraitId = IdGen () module RegionVarId = IdGen () -module RegionId = IdGen () +module FreeRegionId = IdGen () module RegionGroupId = IdGen () module Disambiguator = IdGen () module FunDeclId = IdGen () @@ -41,6 +41,7 @@ type region_db_id = int [@@deriving show, ord] (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) type region_var_id = RegionVarId.id [@@deriving show, ord] +type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] type ('id, 'name) indexed_var = { @@ -174,11 +175,11 @@ class ['self] iter_ty = self#visit_region_db_id env db_id; self#visit_region_var_id env var_id - method! visit_RFVar env (var_id: region_id) = + method! visit_RFVar env (var_id: free_region_id) = self#visit_free_region env var_id - method visit_free_region env (var_id: region_id) = - self#visit_region_id env var_id + method visit_free_region env (var_id: free_region_id) = + self#visit_free_region_id env var_id end (** Ancestor for map visitor for {!type: Types.ty} *) @@ -195,12 +196,12 @@ class virtual ['self] map_ty = let var_id = self#visit_region_var_id env var_id in (db_id, var_id) - method! visit_RFVar env (var_id: region_id) = + method! visit_RFVar env (var_id: free_region_id) = let var_id = self#visit_free_region env var_id in RFVar var_id - method visit_free_region env (var_id: region_id) = - self#visit_region_id env var_id + method visit_free_region env (var_id: free_region_id) = + self#visit_free_region_id env var_id end From 1ea11100a3f1e5d9bea8d6658d68dcb16dd4096a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 4 Dec 2024 17:45:57 +0100 Subject: [PATCH 4/9] Rename ocaml `region_var_id` to `bound_region_id` --- charon-ml/src/GAstOfJson.ml | 19 +++++++--- charon-ml/src/NameMatcher.ml | 20 +++++----- charon-ml/src/PrintTypes.ml | 18 ++++----- charon-ml/src/Substitute.ml | 10 ++--- charon-ml/src/Types.ml | 37 ++++++++++--------- charon/src/ast/types.rs | 12 +++--- charon/src/ast/types_utils.rs | 2 +- .../charon-driver/translate/translate_ctx.rs | 12 +++--- charon/src/bin/generate-ml/main.rs | 7 ++-- .../bin/generate-ml/templates/GAstOfJson.ml | 2 +- charon/src/bin/generate-ml/templates/Types.ml | 24 ++++++------ charon/src/pretty/formatter.rs | 10 ++--- .../transform/update_closure_signatures.rs | 2 +- 13 files changed, 92 insertions(+), 83 deletions(-) diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 46096831c..2bccdee62 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -38,7 +38,7 @@ type of_json_ctx = id_to_file_map let de_bruijn_id_of_json = int_of_json let path_buf_of_json = string_of_json -let region_id_of_json = RegionVarId.id_of_json +let region_id_of_json = BoundRegionId.id_of_json let rec ___ = () @@ -873,6 +873,13 @@ and field_id_of_json (ctx : of_json_ctx) (js : json) : (field_id, string) result | x -> FieldId.id_of_json ctx x | _ -> Error "") +and bound_region_id_of_json (ctx : of_json_ctx) (js : json) : + (bound_region_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | x -> BoundRegionId.id_of_json ctx x + | _ -> Error "") + and const_generic_var_id_of_json (ctx : of_json_ctx) (js : json) : (const_generic_var_id, string) result = combine_error_msgs js __FUNCTION__ @@ -895,7 +902,7 @@ and region_var_of_json (ctx : of_json_ctx) (js : json) : combine_error_msgs js __FUNCTION__ (match js with | `Assoc [ ("index", index); ("name", name) ] -> - let* index = region_id_of_json ctx index in + let* index = bound_region_id_of_json ctx index in let* name = option_of_json string_of_json ctx name in Ok ({ index; name } : region_var) | _ -> Error "") @@ -917,7 +924,7 @@ and region_of_json (ctx : of_json_ctx) (js : json) : (region, string) result = | `String "Static" -> Ok RStatic | `Assoc [ ("BVar", `List [ x_0; x_1 ]) ] -> let* x_0 = de_bruijn_id_of_json ctx x_0 in - let* x_1 = region_id_of_json ctx x_1 in + let* x_1 = bound_region_id_of_json ctx x_1 in Ok (RBVar (x_0, x_1)) | `String "Erased" -> Ok RErased | _ -> Error "") @@ -1024,7 +1031,7 @@ and generic_args_of_json (ctx : of_json_ctx) (js : json) : ("trait_refs", trait_refs); ] -> let* regions = - vector_of_json region_id_of_json region_of_json ctx regions + vector_of_json bound_region_id_of_json region_of_json ctx regions in let* types = vector_of_json type_var_id_of_json ty_of_json ctx types in let* const_generics = @@ -1049,7 +1056,7 @@ and region_binder_of_json : (match js with | `Assoc [ ("regions", regions); ("skip_binder", skip_binder) ] -> let* binder_regions = - vector_of_json region_id_of_json region_var_of_json ctx regions + vector_of_json bound_region_id_of_json region_var_of_json ctx regions in let* binder_value = arg0_of_json ctx skip_binder in Ok ({ binder_regions; binder_value } : _ region_binder) @@ -1070,7 +1077,7 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) : ("trait_type_constraints", trait_type_constraints); ] -> let* regions = - vector_of_json region_id_of_json region_var_of_json ctx regions + vector_of_json bound_region_id_of_json region_var_of_json ctx regions in let* types = vector_of_json type_var_id_of_json type_var_of_json ctx types diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 6f6e54eba..136ef7956 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -287,7 +287,7 @@ type mexpr = MTy of T.ty | MCg of T.const_generic | MRegion of T.region type region_map = { regions : T.region VarMap.t ref; (** The map for "regular" regions *) - bound_regions : T.region T.RegionVarId.Map.t ref list; + bound_regions : T.region T.BoundRegionId.Map.t ref list; (** The stack of maps for bound regions. Note that the stack itself is not inside a reference: this allows us @@ -305,7 +305,7 @@ type maps = { let mk_empty_region_map () = { regions = ref VarMap.empty; - bound_regions = [ ref T.RegionVarId.Map.empty ]; + bound_regions = [ ref T.BoundRegionId.Map.empty ]; } let mk_empty_maps () = @@ -315,7 +315,7 @@ let maps_push_bound_regions_group (m : maps) : maps = let rmap = { m.rmap with - bound_regions = ref T.RegionVarId.Map.empty :: m.rmap.bound_regions; + bound_regions = ref T.BoundRegionId.Map.empty :: m.rmap.bound_regions; } in { m with rmap } @@ -356,8 +356,8 @@ let update_rmap (c : match_config) (m : maps) (id : var) (v : T.region) : bool = match List.nth_opt m.rmap.bound_regions db_id with | None -> raise (Failure "Unexpected bound variable") | Some brmap -> - update_map T.RegionVarId.Map.find_opt T.RegionVarId.Map.add brmap - rid v) + update_map T.BoundRegionId.Map.find_opt T.BoundRegionId.Map.add + brmap rid v) | _ -> update_map VarMap.find_opt VarMap.add m.rmap.regions id v let update_tmap (c : match_config) (m : maps) (id : var) (v : T.ty) : bool = @@ -777,7 +777,7 @@ let mk_name_matcher (ctx : ctx) (c : match_config) (pat : string) : (* We use this to store the constraints maps (the map from variable ids to option pattern variable ids) *) type constraints = { - rmap : var option T.RegionVarId.Map.t list; + rmap : var option T.BoundRegionId.Map.t list; (** Note that we have a stack of maps for the regions *) tmap : var option T.TypeVarId.Map.t; cmap : var option T.ConstGenericVarId.Map.t; @@ -785,7 +785,7 @@ type constraints = { let empty_constraints = { - rmap = [ T.RegionVarId.Map.empty ]; + rmap = [ T.BoundRegionId.Map.empty ]; tmap = T.TypeVarId.Map.empty; cmap = T.ConstGenericVarId.Map.empty; } @@ -802,7 +802,7 @@ let region_to_pattern (m : constraints) (r : T.region) : region = (match List.nth_opt m.rmap bdid with | None -> None | Some rmap -> ( - match T.RegionVarId.Map.find_opt r rmap with + match T.BoundRegionId.Map.find_opt r rmap with | Some r -> r | None -> None)) | RFVar _ -> @@ -832,14 +832,14 @@ let const_generic_var_to_pattern (m : constraints) (v : T.ConstGenericVarId.id) None let constraints_map_compute_regions_map (regions : T.region_var list) : - var option T.RegionVarId.Map.t = + var option T.BoundRegionId.Map.t = let fresh_id (gen : int ref) : int = let id = !gen in gen := id + 1; id in let rid_gen = ref 0 in - T.RegionVarId.Map.of_list + T.BoundRegionId.Map.of_list (List.map (fun (r : T.region_var) -> let v = diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 637765f88..13687cfdd 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -13,7 +13,7 @@ let const_generic_var_to_string (v : const_generic_var) : string = v.name let region_var_to_string (rv : region_var) : string = match rv.name with | Some name -> name - | None -> RegionVarId.to_string rv.index + | None -> BoundRegionId.to_string rv.index let ref_kind_to_string (rk : ref_kind) : string = match rk with @@ -25,9 +25,9 @@ let builtin_ty_to_string (_ : builtin_ty) : string = "Box" let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = "TraitClause@" ^ TraitClauseId.to_string id -let region_var_id_to_pretty_string (db_id : region_db_id) (id : region_var_id) : - string = - "'" ^ show_region_db_id db_id ^ "_" ^ RegionVarId.to_string id +let bound_region_id_to_pretty_string (db_id : region_db_id) + (id : bound_region_id) : string = + "'" ^ show_region_db_id db_id ^ "_" ^ BoundRegionId.to_string id let free_region_id_to_pretty_string (id : free_region_id) : string = "'" ^ FreeRegionId.to_string id @@ -59,14 +59,14 @@ let variant_id_to_pretty_string (id : variant_id) : string = let field_id_to_pretty_string (id : field_id) : string = "Field@" ^ FieldId.to_string id -let region_var_id_to_string (env : 'a fmt_env) (db_id : region_db_id) - (id : region_var_id) : string = +let bound_region_id_to_string (env : 'a fmt_env) (db_id : region_db_id) + (id : bound_region_id) : string = match List.nth_opt env.regions db_id with - | None -> region_var_id_to_pretty_string db_id id + | None -> bound_region_id_to_pretty_string db_id id | Some regions -> ( (* Note that the regions are not necessarily ordered following their indices *) match List.find_opt (fun (r : region_var) -> r.index = id) regions with - | None -> region_var_id_to_pretty_string db_id id + | None -> bound_region_id_to_pretty_string db_id id | Some r -> region_var_to_string r) let type_var_id_to_string (env : 'a fmt_env) (id : type_var_id) : string = @@ -92,7 +92,7 @@ let region_to_string (env : 'a fmt_env) (r : region) : string = match r with | RStatic -> "'static" | RErased -> "'_" - | RBVar (db, rid) -> region_var_id_to_string env db rid + | RBVar (db, rid) -> bound_region_id_to_string env db rid | RFVar rid -> free_region_id_to_pretty_string rid let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index a8722f8e2..684518a30 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -158,13 +158,13 @@ let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty) (** Create a region substitution from a list of region variable ids and a list of regions (with which to substitute the region variable ids *) -let make_region_subst (var_ids : RegionVarId.id list) (regions : region list) : - region -> region = +let make_region_subst (var_ids : BoundRegionId.id list) (regions : region list) + : region -> region = let ls = List.combine var_ids regions in let mp = List.fold_left - (fun mp (k, v) -> RegionVarId.Map.add k v mp) - RegionVarId.Map.empty ls + (fun mp (k, v) -> BoundRegionId.Map.add k v mp) + BoundRegionId.Map.empty ls in fun r -> match r with @@ -172,7 +172,7 @@ let make_region_subst (var_ids : RegionVarId.id list) (regions : region list) : | RFVar _ -> raise (Failure "Unexpected") | RBVar (bdid, id) -> (* Only substitute the bound regions with DeBruijn index equal to 0 *) - if bdid = 0 then RegionVarId.Map.find id mp else r + if bdid = 0 then BoundRegionId.Map.find id mp else r let make_region_subst_from_vars (vars : region_var list) (regions : region list) : region -> region = diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index b3b8c5318..6e573aed8 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -21,7 +21,7 @@ module TraitDeclId = IdGen () module TraitImplId = IdGen () module TraitClauseId = IdGen () module UnsolvedTraitId = IdGen () -module RegionVarId = IdGen () +module BoundRegionId = IdGen () module FreeRegionId = IdGen () module RegionGroupId = IdGen () module Disambiguator = IdGen () @@ -38,7 +38,7 @@ type region_db_id = int [@@deriving show, ord] (** We define these types to control the name of the visitor functions (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) -type region_var_id = RegionVarId.id [@@deriving show, ord] +type bound_region_id = BoundRegionId.id [@@deriving show, ord] type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] @@ -83,7 +83,9 @@ class ['self] iter_const_generic_base = method visit_global_decl_id : 'env -> global_decl_id -> unit = fun _ _ -> () method visit_region_db_id : 'env -> region_db_id -> unit = fun _ _ -> () method visit_free_region_id : 'env -> free_region_id -> unit = fun _ _ -> () - method visit_region_var_id : 'env -> region_var_id -> unit = fun _ _ -> () + + method visit_bound_region_id : 'env -> bound_region_id -> unit = + fun _ _ -> () method visit_trait_clause_id : 'env -> trait_clause_id -> unit = fun _ _ -> () @@ -113,7 +115,7 @@ class ['self] map_const_generic_base = method visit_free_region_id : 'env -> free_region_id -> free_region_id = fun _ x -> x - method visit_region_var_id : 'env -> region_var_id -> region_var_id = + method visit_bound_region_id : 'env -> bound_region_id -> bound_region_id = fun _ x -> x method visit_trait_clause_id : 'env -> trait_clause_id -> trait_clause_id = @@ -149,7 +151,7 @@ class virtual ['self] reduce_const_generic_base = method visit_free_region_id : 'env -> free_region_id -> 'a = fun _ _ -> self#zero - method visit_region_var_id : 'env -> region_var_id -> 'a = + method visit_bound_region_id : 'env -> bound_region_id -> 'a = fun _ _ -> self#zero method visit_trait_clause_id : 'env -> trait_clause_id -> 'a = @@ -189,7 +191,8 @@ class virtual ['self] mapreduce_const_generic_base = = fun _ x -> (x, self#zero) - method visit_region_var_id : 'env -> region_var_id -> region_var_id * 'a = + method visit_bound_region_id + : 'env -> bound_region_id -> bound_region_id * 'a = fun _ x -> (x, self#zero) method visit_trait_clause_id @@ -247,7 +250,7 @@ type const_generic = }] (** Region variable. *) -type region_var = (region_var_id, string option) indexed_var +type region_var = (bound_region_id, string option) indexed_var [@@deriving show, ord] (** A value of type `'a` bound by generic parameters. *) @@ -284,7 +287,7 @@ class ['self] iter_ty_base_base = visit_right env right method visit_region_var env (x : region_var) = - self#visit_indexed_var self#visit_region_var_id + self#visit_indexed_var self#visit_bound_region_id (self#visit_option self#visit_string) env x @@ -328,7 +331,7 @@ class virtual ['self] map_ty_base_base = (left, right) method visit_region_var env (x : region_var) = - self#visit_indexed_var self#visit_region_var_id + self#visit_indexed_var self#visit_bound_region_id (self#visit_option self#visit_string) env x @@ -354,7 +357,7 @@ and trait_item_name = string and region = | RStatic (** Static region *) - | RBVar of region_db_id * region_var_id + | RBVar of region_db_id * bound_region_id (** Bound region. We use those in function signatures, type definitions, etc. *) | RFVar of free_region_id (** Free region. We use those during the symbolic execution. *) @@ -543,13 +546,13 @@ class ['self] iter_ty = object (self : 'self) inherit [_] iter_ty_inner - method! visit_RBVar env (db_id : region_db_id) (var_id : region_var_id) = + method! visit_RBVar env (db_id : region_db_id) (var_id : bound_region_id) = self#visit_bound_region env db_id var_id method visit_bound_region env (db_id : region_db_id) - (var_id : region_var_id) = + (var_id : bound_region_id) = self#visit_region_db_id env db_id; - self#visit_region_var_id env var_id + self#visit_bound_region_id env var_id method! visit_RFVar env (var_id : free_region_id) = self#visit_free_region env var_id @@ -563,14 +566,14 @@ class virtual ['self] map_ty = object (self : 'self) inherit [_] map_ty_inner - method! visit_RBVar env (db_id : region_db_id) (var_id : region_var_id) = + method! visit_RBVar env (db_id : region_db_id) (var_id : bound_region_id) = let db_id, var_id = self#visit_bound_region env db_id var_id in RBVar (db_id, var_id) method visit_bound_region env (db_id : region_db_id) - (var_id : region_var_id) = + (var_id : bound_region_id) = let db_id = self#visit_region_db_id env db_id in - let var_id = self#visit_region_var_id env var_id in + let var_id = self#visit_bound_region_id env var_id in (db_id, var_id) method! visit_RFVar env (var_id : free_region_id) = @@ -847,7 +850,7 @@ type ('rid, 'id) g_region_group = { } [@@deriving show] -type region_var_group = (RegionVarId.id, RegionGroupId.id) g_region_group +type region_var_group = (BoundRegionId.id, RegionGroupId.id) g_region_group [@@deriving show] type region_var_groups = region_var_group list [@@deriving show] diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 6c70969eb..834b07b64 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -14,7 +14,7 @@ pub type FieldName = String; generate_index_type!(TypeVarId, "T"); generate_index_type!(VariantId, "Variant"); generate_index_type!(FieldId, "Field"); -generate_index_type!(RegionId, "Region"); +generate_index_type!(BoundRegionId, "BoundRegion"); generate_index_type!(FreeRegionId, "FreeRegion"); generate_index_type!(ConstGenericVarId, "Const"); @@ -35,7 +35,7 @@ pub struct TypeVar { )] pub struct RegionVar { /// Unique index identifying the variable - pub index: RegionId, + pub index: BoundRegionId, /// Region name pub name: Option, } @@ -112,7 +112,7 @@ pub enum Region { /// De Bruijn: 1 /// Var id: 1 /// ``` - BVar(DeBruijnId, RegionId), + BVar(DeBruijnId, BoundRegionId), /// Erased region Erased, /// For error reporting. @@ -301,7 +301,7 @@ pub struct TraitTypeConstraint { #[derive(Default, Clone, Eq, PartialEq, Serialize, Deserialize, Hash, Drive, DriveMut)] pub struct GenericArgs { - pub regions: Vector, + pub regions: Vector, pub types: Vector, pub const_generics: Vector, // TODO: rename to match [GenericParams]? @@ -314,7 +314,7 @@ pub struct GenericArgs { #[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash)] pub struct RegionBinder { #[charon::rename("binder_regions")] - pub regions: Vector, + pub regions: Vector, /// Named this way to highlight accesses to the inner value that might be handling parameters /// incorrectly. Prefer using helper methods. #[charon::rename("binder_value")] @@ -330,7 +330,7 @@ pub struct RegionBinder { /// be filled with witnesses/instances. #[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] pub struct GenericParams { - pub regions: Vector, + pub regions: Vector, pub types: Vector, pub const_generics: Vector, // TODO: rename to match [GenericArgs]? diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index adfe76ebd..20018dbbb 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -130,7 +130,7 @@ impl GenericArgs { } pub fn new( - regions: Vector, + regions: Vector, types: Vector, const_generics: Vector, trait_refs: Vector, diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index d3726759e..9c44ab015 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -219,7 +219,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx> { /// The regions. /// We use DeBruijn indices, so we have a stack of regions. /// See the comments for [Region::BVar]. - pub region_vars: VecDeque>, + pub region_vars: VecDeque>, /// The map from rust (free) regions to translated region indices. /// This contains the early bound regions. /// @@ -234,7 +234,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx> { /// /// The [bound_region_vars] field below takes care of the regions which /// are bound in the Rustc representation. - pub free_region_vars: std::collections::BTreeMap, + pub free_region_vars: std::collections::BTreeMap, /// /// The stack of late-bound parameters (can only be lifetimes for now), which /// use DeBruijn indices (the other parameters use free variables). @@ -245,7 +245,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx> { /// **Important**: /// ============== /// We use DeBruijn indices. See the comments for [Region::Var]. - pub bound_region_vars: VecDeque>, + pub bound_region_vars: VecDeque>, /// The generic parameters for the item. `regions` must be empty, as regions are handled /// separately. pub generic_params: GenericParams, @@ -995,7 +995,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { /// /// Important: we must push *all* the free regions (which are early-bound /// regions) before pushing any (late-)bound region. - pub(crate) fn push_free_region(&mut self, r: hax::Region) -> RegionId { + pub(crate) fn push_free_region(&mut self, r: hax::Region) -> BoundRegionId { let name = super::translate_types::translate_region_name(&r); // Check that there are no late-bound regions assert!(self.bound_region_vars.is_empty()); @@ -1009,8 +1009,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { &mut self, span: Span, binder: hax::Binder<()>, - region_vars: &mut Vector, - ) -> Result, Error> { + region_vars: &mut Vector, + ) -> Result, Error> { use hax::BoundVariableKind::*; binder .bound_vars diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 16083d58d..84bbd4ef7 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1016,7 +1016,7 @@ fn generate_ml( indoc!( " | RStatic (** Static region *) - | RBVar of region_db_id * region_var_id + | RBVar of region_db_id * bound_region_id (** Bound region. We use those in function signatures, type definitions, etc. *) | RFVar of free_region_id (** Free region. We use those during the symbolic execution. *) @@ -1026,7 +1026,7 @@ fn generate_ml( ), // Handwritten because we use `indexed_var` as a hack to be able to reuse field names. // TODO: remove the need for this hack. - ("RegionVar", "(region_var_id, string option) indexed_var"), + ("RegionVar", "(bound_region_id, string option) indexed_var"), ("TypeVar", "(type_var_id, string) indexed_var"), ]; let manual_json_impls = &[ @@ -1155,7 +1155,6 @@ fn generate_ml( let manually_implemented: HashSet<_> = [ "ItemOpacity", "DeBruijnId", - "RegionId", "PredicateOrigin", "Ty", // We exclude it since `TyKind` is renamed to `ty` "Opaque", @@ -1338,7 +1337,7 @@ fn generate_ml( "global_decl_id", "region_db_id", "free_region_id", - "region_var_id", + "bound_region_id", "trait_clause_id", "trait_decl_id", "trait_impl_id", diff --git a/charon/src/bin/generate-ml/templates/GAstOfJson.ml b/charon/src/bin/generate-ml/templates/GAstOfJson.ml index 65755f1b8..5615cb91e 100644 --- a/charon/src/bin/generate-ml/templates/GAstOfJson.ml +++ b/charon/src/bin/generate-ml/templates/GAstOfJson.ml @@ -39,7 +39,7 @@ type of_json_ctx = id_to_file_map let de_bruijn_id_of_json = int_of_json let path_buf_of_json = string_of_json -let region_id_of_json = RegionVarId.id_of_json +let region_id_of_json = BoundRegionId.id_of_json (* __REPLACE0__ *) diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index 4b2d679de..435df25a1 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -22,7 +22,7 @@ module TraitDeclId = IdGen () module TraitImplId = IdGen () module TraitClauseId = IdGen () module UnsolvedTraitId = IdGen () -module RegionVarId = IdGen () +module BoundRegionId = IdGen () module FreeRegionId = IdGen () module RegionGroupId = IdGen () module Disambiguator = IdGen () @@ -40,7 +40,7 @@ type region_db_id = int [@@deriving show, ord] (** We define these types to control the name of the visitor functions (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) -type region_var_id = RegionVarId.id [@@deriving show, ord] +type bound_region_id = BoundRegionId.id [@@deriving show, ord] type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] @@ -66,7 +66,7 @@ let option_some_id = VariantId.of_int 1 (* __REPLACE1__ *) (** Region variable. *) -type region_var = (region_var_id, string option) indexed_var +type region_var = (bound_region_id, string option) indexed_var [@@deriving show, ord] (** A value of type `'a` bound by generic parameters. *) @@ -103,7 +103,7 @@ class ['self] iter_ty_base_base = visit_right env right method visit_region_var env (x : region_var) = - self#visit_indexed_var self#visit_region_var_id + self#visit_indexed_var self#visit_bound_region_id (self#visit_option self#visit_string) env x @@ -147,7 +147,7 @@ class virtual ['self] map_ty_base_base = (left, right) method visit_region_var env (x : region_var) = - self#visit_indexed_var self#visit_region_var_id + self#visit_indexed_var self#visit_bound_region_id (self#visit_option self#visit_string) env x @@ -168,12 +168,12 @@ class ['self] iter_ty = object (self : 'self) inherit [_] iter_ty_inner - method! visit_RBVar env (db_id: region_db_id) (var_id: region_var_id) = + method! visit_RBVar env (db_id: region_db_id) (var_id: bound_region_id) = self#visit_bound_region env db_id var_id - method visit_bound_region env (db_id: region_db_id) (var_id: region_var_id) = + method visit_bound_region env (db_id: region_db_id) (var_id: bound_region_id) = self#visit_region_db_id env db_id; - self#visit_region_var_id env var_id + self#visit_bound_region_id env var_id method! visit_RFVar env (var_id: free_region_id) = self#visit_free_region env var_id @@ -187,13 +187,13 @@ class virtual ['self] map_ty = object (self : 'self) inherit [_] map_ty_inner - method! visit_RBVar env (db_id: region_db_id) (var_id: region_var_id) = + method! visit_RBVar env (db_id: region_db_id) (var_id: bound_region_id) = let (db_id, var_id) = self#visit_bound_region env db_id var_id in RBVar (db_id, var_id) - method visit_bound_region env (db_id: region_db_id) (var_id: region_var_id) = + method visit_bound_region env (db_id: region_db_id) (var_id: bound_region_id) = let db_id = self#visit_region_db_id env db_id in - let var_id = self#visit_region_var_id env var_id in + let var_id = self#visit_bound_region_id env var_id in (db_id, var_id) method! visit_RFVar env (var_id: free_region_id) = @@ -227,7 +227,7 @@ type ('rid, 'id) g_region_group = { } [@@deriving show] -type region_var_group = (RegionVarId.id, RegionGroupId.id) g_region_group +type region_var_group = (BoundRegionId.id, RegionGroupId.id) g_region_group [@@deriving show] type region_var_groups = region_var_group list [@@deriving show] diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 47425a2fb..e11f462ce 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -110,13 +110,13 @@ impl<'a, 'b> SetLocals<'a> for FmtCtx<'b> { pub trait PushBoundRegions<'a> { type C: 'a + AstFormatter; - fn push_bound_regions(&'a self, regions: &'a Vector) -> Self::C; + fn push_bound_regions(&'a self, regions: &'a Vector) -> Self::C; } impl<'a, 'b> PushBoundRegions<'a> for FmtCtx<'b> { type C = FmtCtx<'a>; - fn push_bound_regions(&'a self, regions: &'a Vector) -> Self::C { + fn push_bound_regions(&'a self, regions: &'a Vector) -> Self::C { let mut generics = self.generics.clone(); generics.push_front(Cow::Owned(GenericParams { regions: regions.clone(), @@ -140,7 +140,7 @@ pub trait AstFormatter = Formatter + Formatter + Formatter + Formatter - + Formatter<(DeBruijnId, RegionId)> + + Formatter<(DeBruijnId, BoundRegionId)> + Formatter + Formatter<(TypeDeclId, VariantId)> + Formatter<(TypeDeclId, Option, FieldId)> @@ -263,8 +263,8 @@ impl<'a> Formatter for FmtCtx<'a> { } } -impl<'a> Formatter<(DeBruijnId, RegionId)> for FmtCtx<'a> { - fn format_object(&self, (grid, id): (DeBruijnId, RegionId)) -> String { +impl<'a> Formatter<(DeBruijnId, BoundRegionId)> for FmtCtx<'a> { + fn format_object(&self, (grid, id): (DeBruijnId, BoundRegionId)) -> String { match self.generics.get(grid.index) { None => Region::BVar(grid, id).to_string(), Some(generics) => match generics.regions.get(id) { diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index e76efe3f0..fd09e43ad 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -12,7 +12,7 @@ use super::ctx::UllbcPass; #[derive(VisitorMut)] #[visitor(Region(exit), Ty(enter, exit))] struct InsertRegions<'a> { - regions: &'a mut Vector, + regions: &'a mut Vector, // The number of region groups we dived into (we don't count the regions // at the declaration level). We use this for the DeBruijn indices. depth: usize, From 1cb970bf555688704070c0085b4ef26ac8dc43c7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 5 Dec 2024 11:50:56 +0100 Subject: [PATCH 5/9] Add free region vars to the rust side --- charon-ml/src/GAstOfJson.ml | 21 ++++++-- charon-ml/src/Types.ml | 48 ++++++++++++------- charon/src/ast/types.rs | 7 +-- charon/src/bin/generate-ml/main.rs | 21 ++------ .../bin/generate-ml/templates/GAstOfJson.ml | 2 - charon/src/bin/generate-ml/templates/Types.ml | 3 -- charon/src/pretty/fmt_with_ctx.rs | 4 +- 7 files changed, 58 insertions(+), 48 deletions(-) diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 2bccdee62..6d824d793 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -36,9 +36,7 @@ type file_id = FileId.id [@@deriving show, ord] type id_to_file_map = file FileId.Map.t type of_json_ctx = id_to_file_map -let de_bruijn_id_of_json = int_of_json let path_buf_of_json = string_of_json -let region_id_of_json = BoundRegionId.id_of_json let rec ___ = () @@ -880,6 +878,13 @@ and bound_region_id_of_json (ctx : of_json_ctx) (js : json) : | x -> BoundRegionId.id_of_json ctx x | _ -> Error "") +and free_region_id_of_json (ctx : of_json_ctx) (js : json) : + (free_region_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | x -> FreeRegionId.id_of_json ctx x + | _ -> Error "") + and const_generic_var_id_of_json (ctx : of_json_ctx) (js : json) : (const_generic_var_id, string) result = combine_error_msgs js __FUNCTION__ @@ -918,14 +923,24 @@ and const_generic_var_of_json (ctx : of_json_ctx) (js : json) : Ok ({ index; name; ty } : const_generic_var) | _ -> Error "") +and region_db_id_of_json (ctx : of_json_ctx) (js : json) : + (region_db_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | x -> int_of_json ctx x + | _ -> Error "") + and region_of_json (ctx : of_json_ctx) (js : json) : (region, string) result = combine_error_msgs js __FUNCTION__ (match js with | `String "Static" -> Ok RStatic | `Assoc [ ("BVar", `List [ x_0; x_1 ]) ] -> - let* x_0 = de_bruijn_id_of_json ctx x_0 in + let* x_0 = region_db_id_of_json ctx x_0 in let* x_1 = bound_region_id_of_json ctx x_1 in Ok (RBVar (x_0, x_1)) + | `Assoc [ ("FVar", f_var) ] -> + let* f_var = free_region_id_of_json ctx f_var in + Ok (RFVar f_var) | `String "Erased" -> Ok RErased | _ -> Error "") diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 6e573aed8..4c4820c47 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -33,14 +33,10 @@ type ('id, 'x) vector = 'x list [@@deriving show, ord] type integer_type = Values.integer_type [@@deriving show, ord] type float_type = Values.float_type [@@deriving show, ord] type literal_type = Values.literal_type [@@deriving show, ord] -type region_db_id = int [@@deriving show, ord] (** We define these types to control the name of the visitor functions (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) -type bound_region_id = BoundRegionId.id [@@deriving show, ord] - -type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] type ('id, 'name) indexed_var = { @@ -58,6 +54,8 @@ and disambiguator = Disambiguator.id and type_var_id = TypeVarId.id and variant_id = VariantId.id and field_id = FieldId.id +and bound_region_id = BoundRegionId.id +and free_region_id = FreeRegionId.id and const_generic_var_id = ConstGenericVarId.id and trait_clause_id = TraitClauseId.id [@@deriving show, ord] @@ -81,7 +79,6 @@ class ['self] iter_const_generic_base = method visit_fun_decl_id : 'env -> fun_decl_id -> unit = fun _ _ -> () method visit_global_decl_id : 'env -> global_decl_id -> unit = fun _ _ -> () - method visit_region_db_id : 'env -> region_db_id -> unit = fun _ _ -> () method visit_free_region_id : 'env -> free_region_id -> unit = fun _ _ -> () method visit_bound_region_id : 'env -> bound_region_id -> unit = @@ -109,9 +106,6 @@ class ['self] map_const_generic_base = method visit_global_decl_id : 'env -> global_decl_id -> global_decl_id = fun _ x -> x - method visit_region_db_id : 'env -> region_db_id -> region_db_id = - fun _ x -> x - method visit_free_region_id : 'env -> free_region_id -> free_region_id = fun _ x -> x @@ -145,9 +139,6 @@ class virtual ['self] reduce_const_generic_base = method visit_global_decl_id : 'env -> global_decl_id -> 'a = fun _ _ -> self#zero - method visit_region_db_id : 'env -> region_db_id -> 'a = - fun _ _ -> self#zero - method visit_free_region_id : 'env -> free_region_id -> 'a = fun _ _ -> self#zero @@ -184,9 +175,6 @@ class virtual ['self] mapreduce_const_generic_base = = fun _ x -> (x, self#zero) - method visit_region_db_id : 'env -> region_db_id -> region_db_id * 'a = - fun _ x -> (x, self#zero) - method visit_free_region_id : 'env -> free_region_id -> free_region_id * 'a = fun _ x -> (x, self#zero) @@ -212,8 +200,10 @@ class virtual ['self] mapreduce_const_generic_base = fun _ x -> (x, self#zero) end +type region_db_id = int + (** Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value *) -type const_generic = +and const_generic = | CgGlobal of global_decl_id (** A global constant *) | CgVar of const_generic_var_id (** A const generic variable *) | CgValue of literal (** A concrete value *) @@ -358,9 +348,33 @@ and trait_item_name = string and region = | RStatic (** Static region *) | RBVar of region_db_id * bound_region_id - (** Bound region. We use those in function signatures, type definitions, etc. *) + (** Bound region variable. + + **Important**: + ============== + Similarly to what the Rust compiler does, we use De Bruijn indices to + identify *groups* of bound variables, and variable identifiers to + identity the variables inside the groups. + + For instance, we have the following: + ```text + we compute the De Bruijn indices from here + VVVVVVVVVVVVVVVVVVVVVVV + fn f<'a, 'b>(x: for<'c> fn(&'a u8, &'b u16, &'c u32) -> u64) {} + ^^^^^^ ^^ ^ ^ ^ + | De Bruijn: 0 | | | + De Bruijn: 1 | | | + De Bruijn: 1 | De Bruijn: 0 + Var id: 0 | Var id: 0 + | + De Bruijn: 1 + Var id: 1 + ``` + *) | RFVar of free_region_id - (** Free region. We use those during the symbolic execution. *) + (** A variable not attached to specific. This is not present in translated code, and only + provided as a convenience for variable manipulation. + *) | RErased (** Erased region *) (** Identifier of a trait instance. diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 834b07b64..3047f60e8 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -66,6 +66,7 @@ pub struct ConstGenericVar { DriveMut, )] #[serde(transparent)] +#[charon::rename("RegionDbId")] pub struct DeBruijnId { pub index: usize, } @@ -113,11 +114,11 @@ pub enum Region { /// Var id: 1 /// ``` BVar(DeBruijnId, BoundRegionId), + /// A variable not attached to specific. This is not present in translated code, and only + /// provided as a convenience for variable manipulation. + FVar(FreeRegionId), /// Erased region Erased, - /// For error reporting. - #[charon::opaque] - Unknown, } /// Identifier of a trait instance. diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 84bbd4ef7..2f92398c9 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1008,22 +1008,6 @@ fn generate_ml( " ), ), - // Hand-written because we add an extra variant not present on the rust side. - // TODO: either add this variant to the rust side or duplicate this code on the aeneas - // side. - ( - "Region", - indoc!( - " - | RStatic (** Static region *) - | RBVar of region_db_id * bound_region_id - (** Bound region. We use those in function signatures, type definitions, etc. *) - | RFVar of free_region_id - (** Free region. We use those during the symbolic execution. *) - | RErased (** Erased region *) - " - ), - ), // Handwritten because we use `indexed_var` as a hack to be able to reuse field names. // TODO: remove the need for this hack. ("RegionVar", "(bound_region_id, string option) indexed_var"), @@ -1154,7 +1138,6 @@ fn generate_ml( // Compute the sets of types to be put in each module. let manually_implemented: HashSet<_> = [ "ItemOpacity", - "DeBruijnId", "PredicateOrigin", "Ty", // We exclude it since `TyKind` is renamed to `ty` "Opaque", @@ -1315,9 +1298,11 @@ fn generate_ml( target: output_dir.join("Types.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(None), &[ + "BoundRegionId", "ConstGenericVarId", "Disambiguator", "FieldId", + "FreeRegionId", "FunDeclId", "GlobalDeclId", "TraitClauseId", @@ -1335,7 +1320,6 @@ fn generate_ml( "const_generic_var_id", "fun_decl_id", "global_decl_id", - "region_db_id", "free_region_id", "bound_region_id", "trait_clause_id", @@ -1345,6 +1329,7 @@ fn generate_ml( "type_var_id", ], })), &[ + "DeBruijnId", "ConstGeneric", ]), // Can't merge into above because aeneas uses the above alongside their own partial diff --git a/charon/src/bin/generate-ml/templates/GAstOfJson.ml b/charon/src/bin/generate-ml/templates/GAstOfJson.ml index 5615cb91e..e1a727321 100644 --- a/charon/src/bin/generate-ml/templates/GAstOfJson.ml +++ b/charon/src/bin/generate-ml/templates/GAstOfJson.ml @@ -37,9 +37,7 @@ type file_id = FileId.id type id_to_file_map = file FileId.Map.t type of_json_ctx = id_to_file_map -let de_bruijn_id_of_json = int_of_json let path_buf_of_json = string_of_json -let region_id_of_json = BoundRegionId.id_of_json (* __REPLACE0__ *) diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index 435df25a1..4c8bcf79f 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -35,13 +35,10 @@ type ('id, 'x) vector = 'x list [@@deriving show, ord] type integer_type = Values.integer_type [@@deriving show, ord] type float_type = Values.float_type [@@deriving show, ord] type literal_type = Values.literal_type [@@deriving show, ord] -type region_db_id = int [@@deriving show, ord] (** We define these types to control the name of the visitor functions (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) -type bound_region_id = BoundRegionId.id [@@deriving show, ord] -type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] type ('id, 'name) indexed_var = { diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index a770d405f..cec3f92ef 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -810,8 +810,8 @@ impl FmtWithCtx for Region { match self { Region::Static => "'static".to_string(), Region::BVar(grid, id) => ctx.format_object((*grid, *id)), + Region::FVar(id) => format!("'free_{id}"), Region::Erased => "'_".to_string(), - Region::Unknown => "'_UNKNOWN_".to_string(), } } } @@ -1661,8 +1661,8 @@ impl std::fmt::Display for Region { match self { Region::Static => write!(f, "'static"), Region::BVar(grid, id) => write!(f, "'_{}_{id}", grid.index), + Region::FVar(id) => write!(f, "'free_{id}"), Region::Erased => write!(f, "'_"), - Region::Unknown => write!(f, "'_UNKNOWN_"), } } } From 15f9b92d3091e5b943de3e3ee3746772b3bfb6c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 5 Dec 2024 12:02:46 +0100 Subject: [PATCH 6/9] Rename `region_db_id` to `de_bruijn_id` --- charon-ml/src/GAstOfJson.ml | 6 +++--- charon-ml/src/PrintTypes.ml | 6 +++--- charon-ml/src/Types.ml | 21 ++++++++++--------- charon/src/ast/types.rs | 1 - charon/src/bin/generate-ml/main.rs | 2 -- charon/src/bin/generate-ml/templates/Types.ml | 14 +++++++------ 6 files changed, 25 insertions(+), 25 deletions(-) diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 6d824d793..f405e5c23 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -923,8 +923,8 @@ and const_generic_var_of_json (ctx : of_json_ctx) (js : json) : Ok ({ index; name; ty } : const_generic_var) | _ -> Error "") -and region_db_id_of_json (ctx : of_json_ctx) (js : json) : - (region_db_id, string) result = +and de_bruijn_id_of_json (ctx : of_json_ctx) (js : json) : + (de_bruijn_id, string) result = combine_error_msgs js __FUNCTION__ (match js with | x -> int_of_json ctx x @@ -935,7 +935,7 @@ and region_of_json (ctx : of_json_ctx) (js : json) : (region, string) result = (match js with | `String "Static" -> Ok RStatic | `Assoc [ ("BVar", `List [ x_0; x_1 ]) ] -> - let* x_0 = region_db_id_of_json ctx x_0 in + let* x_0 = de_bruijn_id_of_json ctx x_0 in let* x_1 = bound_region_id_of_json ctx x_1 in Ok (RBVar (x_0, x_1)) | `Assoc [ ("FVar", f_var) ] -> diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 13687cfdd..fc170fd54 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -25,9 +25,9 @@ let builtin_ty_to_string (_ : builtin_ty) : string = "Box" let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = "TraitClause@" ^ TraitClauseId.to_string id -let bound_region_id_to_pretty_string (db_id : region_db_id) +let bound_region_id_to_pretty_string (db_id : de_bruijn_id) (id : bound_region_id) : string = - "'" ^ show_region_db_id db_id ^ "_" ^ BoundRegionId.to_string id + "'" ^ show_de_bruijn_id db_id ^ "_" ^ BoundRegionId.to_string id let free_region_id_to_pretty_string (id : free_region_id) : string = "'" ^ FreeRegionId.to_string id @@ -59,7 +59,7 @@ let variant_id_to_pretty_string (id : variant_id) : string = let field_id_to_pretty_string (id : field_id) : string = "Field@" ^ FieldId.to_string id -let bound_region_id_to_string (env : 'a fmt_env) (db_id : region_db_id) +let bound_region_id_to_string (env : 'a fmt_env) (db_id : de_bruijn_id) (id : bound_region_id) : string = match List.nth_opt env.regions db_id with | None -> bound_region_id_to_pretty_string db_id id diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 4c4820c47..14fce0157 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -37,6 +37,9 @@ type literal_type = Values.literal_type [@@deriving show, ord] (** We define these types to control the name of the visitor functions (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) +type bound_region_id = BoundRegionId.id [@@deriving show, ord] + +type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] type ('id, 'name) indexed_var = { @@ -54,8 +57,6 @@ and disambiguator = Disambiguator.id and type_var_id = TypeVarId.id and variant_id = VariantId.id and field_id = FieldId.id -and bound_region_id = BoundRegionId.id -and free_region_id = FreeRegionId.id and const_generic_var_id = ConstGenericVarId.id and trait_clause_id = TraitClauseId.id [@@deriving show, ord] @@ -200,7 +201,7 @@ class virtual ['self] mapreduce_const_generic_base = fun _ x -> (x, self#zero) end -type region_db_id = int +type de_bruijn_id = int (** Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value *) and const_generic = @@ -347,7 +348,7 @@ and trait_item_name = string and region = | RStatic (** Static region *) - | RBVar of region_db_id * bound_region_id + | RBVar of de_bruijn_id * bound_region_id (** Bound region variable. **Important**: @@ -560,12 +561,12 @@ class ['self] iter_ty = object (self : 'self) inherit [_] iter_ty_inner - method! visit_RBVar env (db_id : region_db_id) (var_id : bound_region_id) = + method! visit_RBVar env (db_id : de_bruijn_id) (var_id : bound_region_id) = self#visit_bound_region env db_id var_id - method visit_bound_region env (db_id : region_db_id) + method visit_bound_region env (db_id : de_bruijn_id) (var_id : bound_region_id) = - self#visit_region_db_id env db_id; + self#visit_de_bruijn_id env db_id; self#visit_bound_region_id env var_id method! visit_RFVar env (var_id : free_region_id) = @@ -580,13 +581,13 @@ class virtual ['self] map_ty = object (self : 'self) inherit [_] map_ty_inner - method! visit_RBVar env (db_id : region_db_id) (var_id : bound_region_id) = + method! visit_RBVar env (db_id : de_bruijn_id) (var_id : bound_region_id) = let db_id, var_id = self#visit_bound_region env db_id var_id in RBVar (db_id, var_id) - method visit_bound_region env (db_id : region_db_id) + method visit_bound_region env (db_id : de_bruijn_id) (var_id : bound_region_id) = - let db_id = self#visit_region_db_id env db_id in + let db_id = self#visit_de_bruijn_id env db_id in let var_id = self#visit_bound_region_id env var_id in (db_id, var_id) diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 3047f60e8..c9e7be6eb 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -66,7 +66,6 @@ pub struct ConstGenericVar { DriveMut, )] #[serde(transparent)] -#[charon::rename("RegionDbId")] pub struct DeBruijnId { pub index: usize, } diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 2f92398c9..5aaadabcf 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1298,11 +1298,9 @@ fn generate_ml( target: output_dir.join("Types.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(None), &[ - "BoundRegionId", "ConstGenericVarId", "Disambiguator", "FieldId", - "FreeRegionId", "FunDeclId", "GlobalDeclId", "TraitClauseId", diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index 4c8bcf79f..d5fb9132b 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -39,6 +39,8 @@ type literal_type = Values.literal_type [@@deriving show, ord] (** We define these types to control the name of the visitor functions (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}). *) +type bound_region_id = BoundRegionId.id [@@deriving show, ord] +type free_region_id = FreeRegionId.id [@@deriving show, ord] type region_group_id = RegionGroupId.id [@@deriving show, ord] type ('id, 'name) indexed_var = { @@ -165,11 +167,11 @@ class ['self] iter_ty = object (self : 'self) inherit [_] iter_ty_inner - method! visit_RBVar env (db_id: region_db_id) (var_id: bound_region_id) = + method! visit_RBVar env (db_id: de_bruijn_id) (var_id: bound_region_id) = self#visit_bound_region env db_id var_id - method visit_bound_region env (db_id: region_db_id) (var_id: bound_region_id) = - self#visit_region_db_id env db_id; + method visit_bound_region env (db_id: de_bruijn_id) (var_id: bound_region_id) = + self#visit_de_bruijn_id env db_id; self#visit_bound_region_id env var_id method! visit_RFVar env (var_id: free_region_id) = @@ -184,12 +186,12 @@ class virtual ['self] map_ty = object (self : 'self) inherit [_] map_ty_inner - method! visit_RBVar env (db_id: region_db_id) (var_id: bound_region_id) = + method! visit_RBVar env (db_id: de_bruijn_id) (var_id: bound_region_id) = let (db_id, var_id) = self#visit_bound_region env db_id var_id in RBVar (db_id, var_id) - method visit_bound_region env (db_id: region_db_id) (var_id: bound_region_id) = - let db_id = self#visit_region_db_id env db_id in + method visit_bound_region env (db_id: de_bruijn_id) (var_id: bound_region_id) = + let db_id = self#visit_de_bruijn_id env db_id in let var_id = self#visit_bound_region_id env var_id in (db_id, var_id) From f00143a9eac116bf7529398243fb6a24727138f1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 5 Dec 2024 13:57:28 +0100 Subject: [PATCH 7/9] Factor out the representation of free/bound region vars --- charon-ml/src/GAstOfJson.ml | 23 +++-- charon-ml/src/NameMatcher.ml | 21 ++--- charon-ml/src/PrintTypes.ml | 39 +++++---- charon-ml/src/Substitute.ml | 8 +- charon-ml/src/Types.ml | 83 ++++++++++--------- charon-ml/src/TypesUtils.ml | 18 ++-- charon/src/ast/types.rs | 72 ++++++++++------ charon/src/ast/types_utils.rs | 28 ++++++- .../translate/translate_types.rs | 7 +- charon/src/bin/generate-ml/main.rs | 1 + charon/src/bin/generate-ml/templates/Types.ml | 24 +++--- charon/src/pretty/fmt_with_ctx.rs | 22 ++++- charon/src/pretty/formatter.rs | 31 +++---- .../transform/update_closure_signatures.rs | 2 +- 14 files changed, 233 insertions(+), 146 deletions(-) diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index f405e5c23..738ce71cc 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -930,17 +930,26 @@ and de_bruijn_id_of_json (ctx : of_json_ctx) (js : json) : | x -> int_of_json ctx x | _ -> Error "") -and region_of_json (ctx : of_json_ctx) (js : json) : (region, string) result = +and de_bruijn_var_of_json (ctx : of_json_ctx) (js : json) : + (de_bruijn_var, string) result = combine_error_msgs js __FUNCTION__ (match js with - | `String "Static" -> Ok RStatic - | `Assoc [ ("BVar", `List [ x_0; x_1 ]) ] -> + | `Assoc [ ("Bound", `List [ x_0; x_1 ]) ] -> let* x_0 = de_bruijn_id_of_json ctx x_0 in let* x_1 = bound_region_id_of_json ctx x_1 in - Ok (RBVar (x_0, x_1)) - | `Assoc [ ("FVar", f_var) ] -> - let* f_var = free_region_id_of_json ctx f_var in - Ok (RFVar f_var) + Ok (Bound (x_0, x_1)) + | `Assoc [ ("Free", free) ] -> + let* free = free_region_id_of_json ctx free in + Ok (Free free) + | _ -> Error "") + +and region_of_json (ctx : of_json_ctx) (js : json) : (region, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc [ ("Var", var) ] -> + let* var = de_bruijn_var_of_json ctx var in + Ok (RVar var) + | `String "Static" -> Ok RStatic | `String "Erased" -> Ok RErased | _ -> Error "") diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 136ef7956..e02f9aa20 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -345,19 +345,20 @@ let update_rmap (c : match_config) (m : maps) (id : var) (v : T.region) : bool = (* When it comes to matching, we treat erased regions like variables. *) let is_var = match v with - | RBVar _ | RErased | RFVar _ -> true - | _ -> false + | RVar _ | RErased -> true + | RStatic -> false in if c.map_vars_to_vars && not is_var then false else match v with - | RBVar (db_id, rid) -> ( + | RVar (Bound (dbid, varid)) -> begin (* Special treatment for the bound regions *) - match List.nth_opt m.rmap.bound_regions db_id with + match List.nth_opt m.rmap.bound_regions dbid with | None -> raise (Failure "Unexpected bound variable") | Some brmap -> update_map T.BoundRegionId.Map.find_opt T.BoundRegionId.Map.add - brmap rid v) + brmap varid v + end | _ -> update_map VarMap.find_opt VarMap.add m.rmap.regions id v let update_tmap (c : match_config) (m : maps) (id : var) (v : T.ty) : bool = @@ -436,7 +437,7 @@ let match_region (c : match_config) (m : maps) (id : region) (v : T.region) : bool = match (id, v) with | RStatic, RStatic -> true - | RVar id, (RBVar _ | RFVar _ | RErased) -> + | RVar id, (RVar _ | RErased) -> (* When it comes to matching, we treat erased regions like variables *) opt_update_rmap c m id v | RVar id, _ -> if c.map_vars_to_vars then false else opt_update_rmap c m id v @@ -797,15 +798,15 @@ let ref_kind_to_pattern (rk : T.ref_kind) : ref_kind = let region_to_pattern (m : constraints) (r : T.region) : region = match r with - | RBVar (bdid, r) -> + | RVar (Bound (dbid, varid)) -> RVar - (match List.nth_opt m.rmap bdid with + (match List.nth_opt m.rmap dbid with | None -> None | Some rmap -> ( - match T.BoundRegionId.Map.find_opt r rmap with + match T.BoundRegionId.Map.find_opt varid rmap with | Some r -> r | None -> None)) - | RFVar _ -> + | RVar (Free _) -> (* For now we don't have a precise treatment of the free region variables in the patterns. Note that they should be used only in the symbolic execution *) diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index fc170fd54..c4759d17b 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -25,12 +25,11 @@ let builtin_ty_to_string (_ : builtin_ty) : string = "Box" let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = "TraitClause@" ^ TraitClauseId.to_string id -let bound_region_id_to_pretty_string (db_id : de_bruijn_id) - (id : bound_region_id) : string = - "'" ^ show_de_bruijn_id db_id ^ "_" ^ BoundRegionId.to_string id - -let free_region_id_to_pretty_string (id : free_region_id) : string = - "'" ^ FreeRegionId.to_string id +let bound_region_var_to_pretty_string (var : de_bruijn_var) : string = + match var with + | Bound (dbid, varid) -> + "'" ^ show_de_bruijn_id dbid ^ "_" ^ BoundRegionId.to_string varid + | Free id -> "'" ^ FreeRegionId.to_string id let type_var_id_to_pretty_string (id : type_var_id) : string = "T@" ^ TypeVarId.to_string id @@ -59,15 +58,22 @@ let variant_id_to_pretty_string (id : variant_id) : string = let field_id_to_pretty_string (id : field_id) : string = "Field@" ^ FieldId.to_string id -let bound_region_id_to_string (env : 'a fmt_env) (db_id : de_bruijn_id) - (id : bound_region_id) : string = - match List.nth_opt env.regions db_id with - | None -> bound_region_id_to_pretty_string db_id id - | Some regions -> ( - (* Note that the regions are not necessarily ordered following their indices *) - match List.find_opt (fun (r : region_var) -> r.index = id) regions with - | None -> bound_region_id_to_pretty_string db_id id - | Some r -> region_var_to_string r) +let bound_region_var_to_string (env : 'a fmt_env) (var : de_bruijn_var) : string + = + match var with + | Bound (dbid, varid) -> begin + match List.nth_opt env.regions dbid with + | None -> bound_region_var_to_pretty_string var + | Some regions -> begin + (* Note that the regions are not necessarily ordered following their indices *) + match + List.find_opt (fun (r : region_var) -> r.index = varid) regions + with + | None -> bound_region_var_to_pretty_string var + | Some r -> region_var_to_string r + end + end + | Free _ -> bound_region_var_to_pretty_string var let type_var_id_to_string (env : 'a fmt_env) (id : type_var_id) : string = (* Note that the types are not necessarily ordered following their indices *) @@ -92,8 +98,7 @@ let region_to_string (env : 'a fmt_env) (r : region) : string = match r with | RStatic -> "'static" | RErased -> "'_" - | RBVar (db, rid) -> bound_region_id_to_string env db rid - | RFVar rid -> free_region_id_to_pretty_string rid + | RVar var -> bound_region_var_to_string env var let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index 684518a30..a72b953ab 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -39,7 +39,7 @@ let st_substitute_visitor = (* Decrement the DeBruijn indices before calling the substitution *) let r_subst r = match r with - | RBVar (db, rid) -> subst.r_subst (RBVar (db - 1, rid)) + | RVar var -> subst.r_subst (RVar (decr_db_var var)) | _ -> subst.r_subst r in let subst = { subst with r_subst } in @@ -169,10 +169,10 @@ let make_region_subst (var_ids : BoundRegionId.id list) (regions : region list) fun r -> match r with | RStatic | RErased -> r - | RFVar _ -> raise (Failure "Unexpected") - | RBVar (bdid, id) -> + | RVar (Free _) -> raise (Failure "Unexpected") + | RVar (Bound (dbid, varid)) -> (* Only substitute the bound regions with DeBruijn index equal to 0 *) - if bdid = 0 then BoundRegionId.Map.find id mp else r + if dbid = 0 then BoundRegionId.Map.find varid mp else r let make_region_subst_from_vars (vars : region_var list) (regions : region list) : region -> region = diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 14fce0157..c560a60ec 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -346,36 +346,41 @@ type global_decl_ref = { and trait_item_name = string -and region = - | RStatic (** Static region *) - | RBVar of de_bruijn_id * bound_region_id - (** Bound region variable. +(** Bound region variable. - **Important**: - ============== - Similarly to what the Rust compiler does, we use De Bruijn indices to - identify *groups* of bound variables, and variable identifiers to - identity the variables inside the groups. + **Important**: + ============== + Similarly to what the Rust compiler does, we use De Bruijn indices to + identify *groups* of bound variables, and variable identifiers to + identity the variables inside the groups. - For instance, we have the following: - ```text - we compute the De Bruijn indices from here - VVVVVVVVVVVVVVVVVVVVVVV - fn f<'a, 'b>(x: for<'c> fn(&'a u8, &'b u16, &'c u32) -> u64) {} - ^^^^^^ ^^ ^ ^ ^ - | De Bruijn: 0 | | | - De Bruijn: 1 | | | - De Bruijn: 1 | De Bruijn: 0 - Var id: 0 | Var id: 0 - | - De Bruijn: 1 - Var id: 1 - ``` - *) - | RFVar of free_region_id - (** A variable not attached to specific. This is not present in translated code, and only - provided as a convenience for variable manipulation. + For instance, we have the following: + ```text + we compute the De Bruijn indices from here + VVVVVVVVVVVVVVVVVVVVVVV + fn f<'a, 'b>(x: for<'c> fn(&'a u8, &'b u16, &'c u32) -> u64) {} + ^^^^^^ ^^ ^ ^ ^ + | De Bruijn: 0 | | | + De Bruijn: 1 | | | + De Bruijn: 1 | De Bruijn: 0 + Var id: 0 | Var id: 0 + | + De Bruijn: 1 + Var id: 1 + ``` + *) +and de_bruijn_var = + | Bound of de_bruijn_id * bound_region_id + (** A variable attached to the nth binder, counting from the inside. *) + | Free of free_region_id + (** A variable attached to an implicit binder outside all other binders. This is not present in + translated code, and only provided as a convenience for convenient variable manipulation. *) + +and region = + | RVar of de_bruijn_var + (** Region variable. See `DeBruijnVar` for details. *) + | RStatic (** Static region *) | RErased (** Erased region *) (** Identifier of a trait instance. @@ -561,17 +566,16 @@ class ['self] iter_ty = object (self : 'self) inherit [_] iter_ty_inner - method! visit_RBVar env (db_id : de_bruijn_id) (var_id : bound_region_id) = - self#visit_bound_region env db_id var_id + method! visit_RVar env (var : de_bruijn_var) = + match var with + | Free var_id -> self#visit_free_region env var_id + | Bound (db_id, var_id) -> self#visit_bound_region env db_id var_id method visit_bound_region env (db_id : de_bruijn_id) (var_id : bound_region_id) = self#visit_de_bruijn_id env db_id; self#visit_bound_region_id env var_id - method! visit_RFVar env (var_id : free_region_id) = - self#visit_free_region env var_id - method visit_free_region env (var_id : free_region_id) = self#visit_free_region_id env var_id end @@ -581,9 +585,14 @@ class virtual ['self] map_ty = object (self : 'self) inherit [_] map_ty_inner - method! visit_RBVar env (db_id : de_bruijn_id) (var_id : bound_region_id) = - let db_id, var_id = self#visit_bound_region env db_id var_id in - RBVar (db_id, var_id) + method! visit_RVar env (var : de_bruijn_var) = + match var with + | Free var_id -> + let var_id = self#visit_free_region env var_id in + RVar (Free var_id) + | Bound (db_id, var_id) -> + let db_id, var_id = self#visit_bound_region env db_id var_id in + RVar (Bound (db_id, var_id)) method visit_bound_region env (db_id : de_bruijn_id) (var_id : bound_region_id) = @@ -591,10 +600,6 @@ class virtual ['self] map_ty = let var_id = self#visit_bound_region_id env var_id in (db_id, var_id) - method! visit_RFVar env (var_id : free_region_id) = - let var_id = self#visit_free_region env var_id in - RFVar var_id - method visit_free_region env (var_id : free_region_id) = self#visit_free_region_id env var_id end diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml index bc7492f8e..a9d7fdeef 100644 --- a/charon-ml/src/TypesUtils.ml +++ b/charon-ml/src/TypesUtils.ml @@ -108,6 +108,12 @@ let trait_instance_id_as_trait_impl (id : trait_instance_id) : | TraitImpl (impl_id, args) -> (impl_id, args) | _ -> raise (Failure "Unreachable") +let zero_db_var (varid : bound_region_id) : de_bruijn_var = Bound (0, varid) + +let decr_db_var : de_bruijn_var -> de_bruijn_var = function + | Free id -> Free id + | Bound (dbid, id) -> Bound (dbid - 1, id) + let empty_generic_args : generic_args = { regions = []; types = []; const_generics = []; trait_refs = [] } @@ -146,7 +152,9 @@ let merge_generic_args (g1 : generic_args) (g2 : generic_args) : generic_args = let generic_args_of_params span (generics : generic_params) : generic_args = let regions = - List.map (fun (v : region_var) -> RBVar (0, v.index)) generics.regions + List.map + (fun (v : region_var) -> RVar (zero_db_var v.index)) + generics.regions in let types = List.map (fun (v : type_var) -> TVar v.index) generics.types in let const_generics = @@ -199,9 +207,9 @@ let region_in_set (r : region) (rset : FreeRegionId.Set.t) : bool = | RStatic -> false | RErased -> raise (Failure "region_in_set shouldn't be called on erased regions") - | RBVar _ -> + | RVar (Bound _) -> raise (Failure "region_in_set shouldn't be called on bound regions") - | RFVar id -> FreeRegionId.Set.mem id rset + | RVar (Free id) -> FreeRegionId.Set.mem id rset (** Return the set of regions in an type - TODO: add static? @@ -215,9 +223,9 @@ let ty_regions (ty : ty) : FreeRegionId.Set.t = | RStatic -> () (* TODO: static? *) | RErased -> raise (Failure "ty_regions shouldn't be called on erased regions") - | RBVar _ -> + | RVar (Bound _) -> raise (Failure "region_in_set shouldn't be called on bound regions") - | RFVar rid -> s := FreeRegionId.Set.add rid !s + | RVar (Free id) -> s := FreeRegionId.Set.add id !s in let obj = object diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index c9e7be6eb..2d58527a5 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -70,6 +70,50 @@ pub struct DeBruijnId { pub index: usize, } +/// Bound region variable. +/// +/// **Important**: +/// ============== +/// Similarly to what the Rust compiler does, we use De Bruijn indices to +/// identify *groups* of bound variables, and variable identifiers to +/// identity the variables inside the groups. +/// +/// For instance, we have the following: +/// ```text +/// we compute the De Bruijn indices from here +/// VVVVVVVVVVVVVVVVVVVVVVV +/// fn f<'a, 'b>(x: for<'c> fn(&'a u8, &'b u16, &'c u32) -> u64) {} +/// ^^^^^^ ^^ ^ ^ ^ +/// | De Bruijn: 0 | | | +/// De Bruijn: 1 | | | +/// De Bruijn: 1 | De Bruijn: 0 +/// Var id: 0 | Var id: 0 +/// | +/// De Bruijn: 1 +/// Var id: 1 +/// ``` +#[derive( + Debug, + PartialEq, + Eq, + Copy, + Clone, + Hash, + PartialOrd, + Ord, + Serialize, + Deserialize, + Drive, + DriveMut, +)] +pub enum DeBruijnVar { + /// A variable attached to the nth binder, counting from the inside. + Bound(DeBruijnId, BoundRegionId), + /// A variable attached to an implicit binder outside all other binders. This is not present in + /// translated code, and only provided as a convenience for convenient variable manipulation. + Free(FreeRegionId), +} + #[derive( Debug, PartialEq, @@ -88,34 +132,10 @@ pub struct DeBruijnId { )] #[charon::variants_prefix("R")] pub enum Region { + /// Region variable. See `DeBruijnVar` for details. + Var(DeBruijnVar), /// Static region Static, - /// Bound region variable. - /// - /// **Important**: - /// ============== - /// Similarly to what the Rust compiler does, we use De Bruijn indices to - /// identify *groups* of bound variables, and variable identifiers to - /// identity the variables inside the groups. - /// - /// For instance, we have the following: - /// ```text - /// we compute the De Bruijn indices from here - /// VVVVVVVVVVVVVVVVVVVVVVV - /// fn f<'a, 'b>(x: for<'c> fn(&'a u8, &'b u16, &'c u32) -> u64) {} - /// ^^^^^^ ^^ ^ ^ ^ - /// | De Bruijn: 0 | | | - /// De Bruijn: 1 | | | - /// De Bruijn: 1 | De Bruijn: 0 - /// Var id: 0 | Var id: 0 - /// | - /// De Bruijn: 1 - /// Var id: 1 - /// ``` - BVar(DeBruijnId, BoundRegionId), - /// A variable not attached to specific. This is not present in translated code, and only - /// provided as a convenience for variable manipulation. - FVar(FreeRegionId), /// Erased region Erased, } diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 20018dbbb..bc1dd976a 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -30,6 +30,26 @@ impl DeBruijnId { } } +impl DeBruijnVar { + pub fn bound(index: DeBruijnId, var: BoundRegionId) -> Self { + DeBruijnVar::Bound(index, var) + } + + pub fn decr(&self) -> Self { + match *self { + DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid), + DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid), + } + } + + pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option { + match *self { + DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid), + _ => None, + } + } +} + impl TypeVar { pub fn new(index: TypeVarId, name: String) -> TypeVar { TypeVar { index, name } @@ -79,7 +99,7 @@ impl GenericParams { regions: self .regions .iter_indexed() - .map(|(id, _)| Region::BVar(DeBruijnId::new(0), id)) + .map(|(id, _)| Region::Var(DeBruijnVar::bound(DeBruijnId::new(0), id))) .collect(), types: self .types @@ -583,9 +603,9 @@ impl<'a> SubstVisitor<'a> { fn exit_region(&mut self, r: &mut Region) { match r { - Region::BVar(db, id) => { - if *db == self.binder_depth { - *r = self.generics.regions.get(*id).unwrap().clone() + Region::Var(var) => { + if let Some(varid) = var.bound_at_depth(self.binder_depth) { + *r = self.generics.regions.get(varid).unwrap().clone() } } _ => (), diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 1dadcd6ed..5bf879f50 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -72,8 +72,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { .expect("Error: missing binder when translating lifetime") .get(br.var) .expect("Error: lifetime not found, binders were handled incorrectly"); - let br_id = DeBruijnId::new(*id); - Ok(Region::BVar(br_id, *rid)) + let var = DeBruijnVar::bound(DeBruijnId::new(*id), *rid); + Ok(Region::Var(var)) } hax::RegionKind::ReVar(_) => { // Shouldn't exist outside of type inference. @@ -88,7 +88,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // Note that the DeBruijn index depends // on the current stack of bound region groups. let db_id = self.region_vars.len() - 1; - Ok(Region::BVar(DeBruijnId::new(db_id), *rid)) + let var = DeBruijnVar::bound(DeBruijnId::new(db_id), *rid); + Ok(Region::Var(var)) } None => { let err = format!( diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 5aaadabcf..b498520bd 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1344,6 +1344,7 @@ fn generate_ml( "ExistentialPredicate", "RefKind", "TyKind", + "DeBruijnVar", "Region", "TraitRef", "TraitRefKind", diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index d5fb9132b..40b3b3cc8 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -167,16 +167,15 @@ class ['self] iter_ty = object (self : 'self) inherit [_] iter_ty_inner - method! visit_RBVar env (db_id: de_bruijn_id) (var_id: bound_region_id) = - self#visit_bound_region env db_id var_id + method! visit_RVar env (var: de_bruijn_var) = + match var with + | Free var_id -> self#visit_free_region env var_id + | Bound (db_id, var_id) -> self#visit_bound_region env db_id var_id method visit_bound_region env (db_id: de_bruijn_id) (var_id: bound_region_id) = self#visit_de_bruijn_id env db_id; self#visit_bound_region_id env var_id - method! visit_RFVar env (var_id: free_region_id) = - self#visit_free_region env var_id - method visit_free_region env (var_id: free_region_id) = self#visit_free_region_id env var_id end @@ -186,19 +185,20 @@ class virtual ['self] map_ty = object (self : 'self) inherit [_] map_ty_inner - method! visit_RBVar env (db_id: de_bruijn_id) (var_id: bound_region_id) = - let (db_id, var_id) = self#visit_bound_region env db_id var_id in - RBVar (db_id, var_id) + method! visit_RVar env (var: de_bruijn_var) = + match var with + | Free var_id -> + let var_id = self#visit_free_region env var_id in + RVar (Free var_id) + | Bound (db_id, var_id) -> + let (db_id, var_id) = self#visit_bound_region env db_id var_id in + RVar (Bound (db_id, var_id)) method visit_bound_region env (db_id: de_bruijn_id) (var_id: bound_region_id) = let db_id = self#visit_de_bruijn_id env db_id in let var_id = self#visit_bound_region_id env var_id in (db_id, var_id) - method! visit_RFVar env (var_id: free_region_id) = - let var_id = self#visit_free_region env var_id in - RFVar var_id - method visit_free_region env (var_id: free_region_id) = self#visit_free_region_id env var_id end diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index cec3f92ef..756993aa9 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -809,8 +809,7 @@ impl FmtWithCtx for Region { fn fmt_with_ctx(&self, ctx: &C) -> String { match self { Region::Static => "'static".to_string(), - Region::BVar(grid, id) => ctx.format_object((*grid, *id)), - Region::FVar(id) => format!("'free_{id}"), + Region::Var(var) => ctx.format_object(*var), Region::Erased => "'_".to_string(), } } @@ -1545,6 +1544,22 @@ impl std::fmt::Display for BuiltinFunId { } } +impl std::fmt::Display for DeBruijnId { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { + write!(f, "{}", self.index) + } +} + +impl std::fmt::Display for DeBruijnVar { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { + match *self { + Self::Bound(dbid, varid) if dbid.is_zero() => write!(f, "{varid}"), + Self::Bound(dbid, varid) => write!(f, "{dbid}_{varid}"), + Self::Free(varid) => write!(f, "free_{varid}"), + } + } +} + impl std::fmt::Display for ConstantExpr { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new())) @@ -1660,8 +1675,7 @@ impl std::fmt::Display for Region { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { match self { Region::Static => write!(f, "'static"), - Region::BVar(grid, id) => write!(f, "'_{}_{id}", grid.index), - Region::FVar(id) => write!(f, "'free_{id}"), + Region::Var(var) => write!(f, "'_{var}"), Region::Erased => write!(f, "'_"), } } diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index e11f462ce..2e9309b33 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -140,7 +140,7 @@ pub trait AstFormatter = Formatter + Formatter + Formatter + Formatter - + Formatter<(DeBruijnId, BoundRegionId)> + + Formatter + Formatter + Formatter<(TypeDeclId, VariantId)> + Formatter<(TypeDeclId, Option, FieldId)> @@ -263,21 +263,24 @@ impl<'a> Formatter for FmtCtx<'a> { } } -impl<'a> Formatter<(DeBruijnId, BoundRegionId)> for FmtCtx<'a> { - fn format_object(&self, (grid, id): (DeBruijnId, BoundRegionId)) -> String { - match self.generics.get(grid.index) { - None => Region::BVar(grid, id).to_string(), - Some(generics) => match generics.regions.get(id) { - None => { - let region = Region::BVar(grid, id); - tracing::warn!( - "Found incorrect region `{region}` while pretty-printing. Look for \ +impl<'a> Formatter for FmtCtx<'a> { + fn format_object(&self, var: DeBruijnVar) -> String { + match var { + DeBruijnVar::Bound(dbid, varid) => match self.generics.get(dbid.index) { + None => Region::Var(var).to_string(), + Some(generics) => match generics.regions.get(varid) { + None => { + let region = Region::Var(var); + tracing::warn!( + "Found incorrect region `{region}` while pretty-printing. Look for \ \"wrong_region\" in the pretty output" - ); - format!("wrong_region({region})") - } - Some(v) => self.format_object(v), + ); + format!("wrong_region({region})") + } + Some(v) => self.format_object(v), + }, }, + DeBruijnVar::Free(_) => Region::Var(var).to_string(), } } } diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index fd09e43ad..161dbba7c 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -25,7 +25,7 @@ impl<'a> InsertRegions<'a> { let index = self .regions .push_with(|index| RegionVar { index, name: None }); - *r = Region::BVar(DeBruijnId::new(self.depth), index); + *r = Region::Var(DeBruijnVar::bound(DeBruijnId::new(self.depth), index)); } } From c61d978039e0a7e7423705c4936f49b1292c9059 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 5 Dec 2024 14:29:20 +0100 Subject: [PATCH 8/9] Substitutions take a region var not a full region --- charon-ml/src/Substitute.ml | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index a72b953ab..0d4899c17 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -8,7 +8,7 @@ open Expressions open LlbcAst type subst = { - r_subst : region -> region; + r_subst : de_bruijn_var -> region; (** Remark: this might be called with bound regions with a negative DeBruijn index. A negative DeBruijn index means that the region is locally bound. *) @@ -22,7 +22,7 @@ type subst = { let empty_subst : subst = { - r_subst = (fun x -> x); + r_subst = (fun x -> RVar x); ty_subst = (fun id -> TVar id); cg_subst = (fun id -> CgVar id); tr_subst = (fun id -> Clause id); @@ -32,22 +32,18 @@ let empty_subst : subst = let st_substitute_visitor = object (self) inherit [_] map_statement - method! visit_region (subst : subst) r = subst.r_subst r (** We need to properly handle the DeBruijn indices *) method! visit_region_binder visit_value (subst : subst) x = (* Decrement the DeBruijn indices before calling the substitution *) - let r_subst r = - match r with - | RVar var -> subst.r_subst (RVar (decr_db_var var)) - | _ -> subst.r_subst r - in + let r_subst var = subst.r_subst (decr_db_var var) in let subst = { subst with r_subst } in (* Note that we ignore the bound regions variables *) let { binder_regions; binder_value } = x in let binder_value = visit_value subst binder_value in { binder_regions; binder_value } + method! visit_RVar (subst : subst) var = subst.r_subst var method! visit_TVar (subst : subst) id = subst.ty_subst id method! visit_CgVar (subst : subst) id = subst.cg_subst id method! visit_Clause (subst : subst) id = subst.tr_subst id @@ -152,30 +148,28 @@ let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) (tr_subst : TraitClauseId.id -> trait_instance_id) (tr_self : trait_instance_id) (ty : ty) : ty = - let r_subst (_ : region) : region = RErased in + let r_subst _ : region = RErased in let subst = { r_subst; ty_subst; cg_subst; tr_subst; tr_self } in ty_substitute subst ty (** Create a region substitution from a list of region variable ids and a list of regions (with which to substitute the region variable ids *) let make_region_subst (var_ids : BoundRegionId.id list) (regions : region list) - : region -> region = + : de_bruijn_var -> region = let ls = List.combine var_ids regions in let mp = List.fold_left (fun mp (k, v) -> BoundRegionId.Map.add k v mp) BoundRegionId.Map.empty ls in - fun r -> - match r with - | RStatic | RErased -> r - | RVar (Free _) -> raise (Failure "Unexpected") - | RVar (Bound (dbid, varid)) -> - (* Only substitute the bound regions with DeBruijn index equal to 0 *) - if dbid = 0 then BoundRegionId.Map.find varid mp else r + function + | Free _ -> raise (Failure "Unexpected") + | Bound (dbid, varid) as var -> + (* Only substitute the bound regions with DeBruijn index equal to 0 *) + if dbid = 0 then BoundRegionId.Map.find varid mp else RVar var let make_region_subst_from_vars (vars : region_var list) (regions : region list) - : region -> region = + : de_bruijn_var -> region = make_region_subst (List.map (fun (x : region_var) -> x.index) vars) regions (** Create a type substitution from a list of type variable ids and a list of From 4f5cb493fd5e02976f51eb6aa636f615d7b96fcf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 6 Dec 2024 13:11:52 +0100 Subject: [PATCH 9/9] Custom region id visitors are no longer needed --- charon-ml/src/Types.ml | 47 +------------------ charon/src/bin/generate-ml/main.rs | 2 +- charon/src/bin/generate-ml/templates/Types.ml | 42 ----------------- 3 files changed, 3 insertions(+), 88 deletions(-) diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index c560a60ec..2448e167e 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -548,62 +548,19 @@ and builtin_ty = ord, visitors { - name = "iter_ty_inner"; + name = "iter_ty"; variety = "iter"; ancestors = [ "iter_ty_base_base" ]; nude = true (* Don't inherit VisitorsRuntime *); }, visitors { - name = "map_ty_inner"; + name = "map_ty"; variety = "map"; ancestors = [ "map_ty_base_base" ]; nude = true (* Don't inherit VisitorsRuntime *); }] -(** Ancestor for iter visitor for {!type: Types.ty} *) -class ['self] iter_ty = - object (self : 'self) - inherit [_] iter_ty_inner - - method! visit_RVar env (var : de_bruijn_var) = - match var with - | Free var_id -> self#visit_free_region env var_id - | Bound (db_id, var_id) -> self#visit_bound_region env db_id var_id - - method visit_bound_region env (db_id : de_bruijn_id) - (var_id : bound_region_id) = - self#visit_de_bruijn_id env db_id; - self#visit_bound_region_id env var_id - - method visit_free_region env (var_id : free_region_id) = - self#visit_free_region_id env var_id - end - -(** Ancestor for map visitor for {!type: Types.ty} *) -class virtual ['self] map_ty = - object (self : 'self) - inherit [_] map_ty_inner - - method! visit_RVar env (var : de_bruijn_var) = - match var with - | Free var_id -> - let var_id = self#visit_free_region env var_id in - RVar (Free var_id) - | Bound (db_id, var_id) -> - let db_id, var_id = self#visit_bound_region env db_id var_id in - RVar (Bound (db_id, var_id)) - - method visit_bound_region env (db_id : de_bruijn_id) - (var_id : bound_region_id) = - let db_id = self#visit_de_bruijn_id env db_id in - let var_id = self#visit_bound_region_id env var_id in - (db_id, var_id) - - method visit_free_region env (var_id : free_region_id) = - self#visit_free_region_id env var_id - end - (* Ancestors for the generic_params visitors *) class ['self] iter_generic_params_base = object (self : 'self) diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index b498520bd..cb7e0d72b 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1333,7 +1333,7 @@ fn generate_ml( // Can't merge into above because aeneas uses the above alongside their own partial // copy of `ty`, which causes method type clashes. (GenerationKind::TypeDecl(Some(DeriveVisitors { - name: "ty_inner", + name: "ty", ancestor: Some("ty_base_base"), reduce: false, extra_types: &[], diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index 40b3b3cc8..a303ad374 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -162,48 +162,6 @@ class virtual ['self] map_ty_base_base = (* __REPLACE2__ *) -(** Ancestor for iter visitor for {!type: Types.ty} *) -class ['self] iter_ty = - object (self : 'self) - inherit [_] iter_ty_inner - - method! visit_RVar env (var: de_bruijn_var) = - match var with - | Free var_id -> self#visit_free_region env var_id - | Bound (db_id, var_id) -> self#visit_bound_region env db_id var_id - - method visit_bound_region env (db_id: de_bruijn_id) (var_id: bound_region_id) = - self#visit_de_bruijn_id env db_id; - self#visit_bound_region_id env var_id - - method visit_free_region env (var_id: free_region_id) = - self#visit_free_region_id env var_id - end - -(** Ancestor for map visitor for {!type: Types.ty} *) -class virtual ['self] map_ty = - object (self : 'self) - inherit [_] map_ty_inner - - method! visit_RVar env (var: de_bruijn_var) = - match var with - | Free var_id -> - let var_id = self#visit_free_region env var_id in - RVar (Free var_id) - | Bound (db_id, var_id) -> - let (db_id, var_id) = self#visit_bound_region env db_id var_id in - RVar (Bound (db_id, var_id)) - - method visit_bound_region env (db_id: de_bruijn_id) (var_id: bound_region_id) = - let db_id = self#visit_de_bruijn_id env db_id in - let var_id = self#visit_bound_region_id env var_id in - (db_id, var_id) - - method visit_free_region env (var_id: free_region_id) = - self#visit_free_region_id env var_id - end - - (* __REPLACE3__ *) (* __REPLACE4__ *)