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..738ce71cc 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 = RegionVarId.id_of_json let rec ___ = () @@ -873,6 +871,20 @@ 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 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__ @@ -895,7 +907,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 "") @@ -911,14 +923,33 @@ and const_generic_var_of_json (ctx : of_json_ctx) (js : json) : Ok ({ index; name; ty } : const_generic_var) | _ -> Error "") +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 + | _ -> Error "") + +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 + | `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 (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 - | `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 - Ok (RBVar (x_0, x_1)) | `String "Erased" -> Ok RErased | _ -> Error "") @@ -1024,7 +1055,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 +1080,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 +1101,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 @@ -1329,13 +1360,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..e02f9aa20 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 } @@ -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.RegionVarId.Map.find_opt T.RegionVarId.Map.add brmap - rid v) + update_map T.BoundRegionId.Map.find_opt T.BoundRegionId.Map.add + 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 @@ -551,15 +552,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 @@ -773,7 +778,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; @@ -781,7 +786,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; } @@ -793,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.RegionVarId.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 *) @@ -828,14 +833,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 = @@ -969,15 +974,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..c4759d17b 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,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 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 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 region_var_id_to_string (env : 'a fmt_env) (db_id : region_db_id) - (id : region_var_id) : string = - match List.nth_opt env.regions db_id with - | None -> region_var_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 - | 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) -> region_var_id_to_string env db rid - | RFVar rid -> 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 @@ -183,8 +188,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..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,36 +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_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 *) - let r_subst r = - match r with - | RBVar (db, rid) -> subst.r_subst (RBVar (db - 1, rid)) - | _ -> 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 @@ -166,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 : RegionVarId.id list) (regions : region list) : - region -> region = +let make_region_subst (var_ids : BoundRegionId.id list) (regions : region list) + : de_bruijn_var -> 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 - | RStatic | RErased -> r - | 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 + 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 diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index baba5f4ae..2448e167e 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -21,8 +21,8 @@ module TraitDeclId = IdGen () module TraitImplId = IdGen () module TraitClauseId = IdGen () module UnsolvedTraitId = IdGen () -module RegionVarId = IdGen () -module RegionId = IdGen () +module BoundRegionId = IdGen () +module FreeRegionId = IdGen () module RegionGroupId = IdGen () module Disambiguator = IdGen () module FunDeclId = IdGen () @@ -33,13 +33,13 @@ 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 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] type ('id, 'name) indexed_var = { @@ -57,7 +57,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] @@ -81,9 +80,10 @@ 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_region_var_id : 'env -> region_var_id -> unit = fun _ _ -> () + method visit_free_region_id : 'env -> free_region_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 _ _ -> () @@ -107,12 +107,10 @@ 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 = + method visit_free_region_id : 'env -> free_region_id -> free_region_id = fun _ x -> x - method visit_region_id : 'env -> region_id -> 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 = @@ -142,12 +140,10 @@ 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 = + method visit_free_region_id : 'env -> free_region_id -> 'a = fun _ _ -> self#zero - method visit_region_id : 'env -> 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 = @@ -180,13 +176,12 @@ 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_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 = + method visit_bound_region_id + : 'env -> bound_region_id -> bound_region_id * 'a = fun _ x -> (x, self#zero) method visit_trait_clause_id @@ -206,8 +201,10 @@ class virtual ['self] mapreduce_const_generic_base = fun _ x -> (x, self#zero) end +type de_bruijn_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 *) @@ -244,7 +241,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. *) @@ -281,7 +278,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 @@ -325,7 +322,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 @@ -349,12 +346,41 @@ type global_decl_ref = { and trait_item_name = string +(** 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 + ``` + *) +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 *) - | RBVar of region_db_id * region_var_id - (** Bound region. We use those in function signatures, type definitions, etc. *) - | RFVar of region_id - (** Free region. We use those during the symbolic execution. *) | RErased (** Erased region *) (** Identifier of a trait instance. @@ -494,7 +520,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 @@ -801,7 +827,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-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml index d20113b9d..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 = @@ -194,30 +202,30 @@ 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 _ -> + | RVar (Bound _) -> raise (Failure "region_in_set shouldn't be called on bound regions") - | RFVar id -> RegionId.Set.mem id rset + | RVar (Free 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? *) | 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 := RegionId.Set.add rid !s + | RVar (Free id) -> s := FreeRegionId.Set.add id !s in let obj = object @@ -231,9 +239,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 +257,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/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..2d58527a5 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -14,7 +14,8 @@ 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"); /// Type variable. @@ -34,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, } @@ -69,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, @@ -87,36 +132,12 @@ 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, RegionId), /// Erased region Erased, - /// For error reporting. - #[charon::opaque] - Unknown, } /// Identifier of a trait instance. @@ -300,7 +321,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]? @@ -313,7 +334,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")] @@ -329,7 +350,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]? @@ -755,7 +776,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..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 @@ -130,7 +150,7 @@ impl GenericArgs { } pub fn new( - regions: Vector, + regions: Vector, types: Vector, const_generics: Vector, trait_refs: Vector, @@ -535,12 +555,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 +571,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,27 +593,28 @@ 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) => { - 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() } } _ => (), } } - 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_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/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 2ecb52919..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!( @@ -323,7 +324,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/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 4a12a8515..cb7e0d72b 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1008,25 +1008,9 @@ 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 * region_var_id - (** Bound region. We use those in function signatures, type definitions, etc. *) - | RFVar of 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", "(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 = &[ @@ -1154,8 +1138,6 @@ fn generate_ml( // Compute the sets of types to be put in each module. let manually_implemented: HashSet<_> = [ "ItemOpacity", - "DeBruijnId", - "RegionId", "PredicateOrigin", "Ty", // We exclude it since `TyKind` is renamed to `ty` "Opaque", @@ -1321,7 +1303,6 @@ fn generate_ml( "FieldId", "FunDeclId", "GlobalDeclId", - "RegionId", "TraitClauseId", "TraitDeclId", "TraitImplId", @@ -1337,9 +1318,8 @@ fn generate_ml( "const_generic_var_id", "fun_decl_id", "global_decl_id", - "region_db_id", - "region_id", - "region_var_id", + "free_region_id", + "bound_region_id", "trait_clause_id", "trait_decl_id", "trait_impl_id", @@ -1347,6 +1327,7 @@ fn generate_ml( "type_var_id", ], })), &[ + "DeBruijnId", "ConstGeneric", ]), // Can't merge into above because aeneas uses the above alongside their own partial @@ -1363,6 +1344,7 @@ fn generate_ml( "ExistentialPredicate", "RefKind", "TyKind", + "DeBruijnVar", "Region", "TraitRef", "TraitRefKind", diff --git a/charon/src/bin/generate-ml/templates/GAstOfJson.ml b/charon/src/bin/generate-ml/templates/GAstOfJson.ml index 65755f1b8..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 = RegionVarId.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 a75df0c4e..a303ad374 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -22,8 +22,8 @@ module TraitDeclId = IdGen () module TraitImplId = IdGen () module TraitClauseId = IdGen () module UnsolvedTraitId = IdGen () -module RegionVarId = IdGen () -module RegionId = IdGen () +module BoundRegionId = IdGen () +module FreeRegionId = IdGen () module RegionGroupId = IdGen () module Disambiguator = IdGen () module FunDeclId = IdGen () @@ -35,12 +35,12 @@ 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 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] type ('id, 'name) indexed_var = { @@ -65,7 +65,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. *) @@ -102,7 +102,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 @@ -146,7 +146,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 @@ -184,7 +184,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/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..756993aa9 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -809,9 +809,8 @@ 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::Var(var) => ctx.format_object(*var), Region::Erased => "'_".to_string(), - Region::Unknown => "'_UNKNOWN_".to_string(), } } } @@ -1346,22 +1345,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)) @@ -1548,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())) @@ -1663,9 +1675,8 @@ 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::Var(var) => write!(f, "'_{var}"), Region::Erased => write!(f, "'_"), - Region::Unknown => write!(f, "'_UNKNOWN_"), } } } diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 47425a2fb..2e9309b33 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 + Formatter + Formatter<(TypeDeclId, VariantId)> + Formatter<(TypeDeclId, Option, FieldId)> @@ -263,21 +263,24 @@ impl<'a> Formatter for FmtCtx<'a> { } } -impl<'a> Formatter<(DeBruijnId, RegionId)> for FmtCtx<'a> { - fn format_object(&self, (grid, id): (DeBruijnId, RegionId)) -> 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 e76efe3f0..161dbba7c 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, @@ -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)); } }