Use de Bruijn indices for all type-level variables

charon-ml/src/Expressions.ml

@@ -278,7 +278,7 @@ and raw_constant_expr =
           Remark: trait constants can not be used in types, they are necessarily
           values.
        *)
-  | CVar of const_generic_var_id  (** A const generic var *)
+  | CVar of const_generic_var_id de_bruijn_var  (** A const generic var *)
   | CFnPtr of fn_ptr  (** Function pointer *)
 
 and constant_expr = { value : raw_constant_expr; ty : ty }

charon-ml/src/GAstOfJson.ml

@@ -261,7 +261,7 @@ and raw_constant_expr_of_json (ctx : of_json_ctx) (js : json) :
         let* x_1 = trait_item_name_of_json ctx x_1 in
         Ok (CTraitConst (x_0, x_1))
     | `Assoc [ ("Var", var) ] ->
-        let* var = const_generic_var_id_of_json ctx var in
+        let* var = de_bruijn_var_of_json const_generic_var_id_of_json ctx var in
         Ok (CVar var)
     | `Assoc [ ("FnPtr", fn_ptr) ] ->
         let* fn_ptr = fn_ptr_of_json ctx fn_ptr in
@@ -911,14 +911,28 @@ and const_generic_var_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ index; name; ty } : const_generic_var)
     | _ -> Error "")
 
+and de_bruijn_var_of_json :
+      'a0.
+      (of_json_ctx -> json -> ('a0, string) result) ->
+      of_json_ctx ->
+      json ->
+      ('a0 de_bruijn_var, string) result =
+ fun arg0_of_json ctx js ->
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("dbid", dbid); ("varid", varid) ] ->
+        let* dbid = de_bruijn_id_of_json ctx dbid in
+        let* varid = arg0_of_json ctx varid in
+        Ok ({ dbid; varid } : _ de_bruijn_var)
+    | _ -> 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_1 = region_id_of_json ctx x_1 in
-        Ok (RBVar (x_0, x_1))
+    | `Assoc [ ("BVar", b_var) ] ->
+        let* b_var = de_bruijn_var_of_json region_id_of_json ctx b_var in
+        Ok (RBVar b_var)
     | `String "Erased" -> Ok RErased
     | _ -> Error "")
 
@@ -931,7 +945,9 @@ and trait_instance_id_of_json (ctx : of_json_ctx) (js : json) :
         let* x_1 = generic_args_of_json ctx x_1 in
         Ok (TraitImpl (x_0, x_1))
     | `Assoc [ ("Clause", clause) ] ->
-        let* clause = trait_clause_id_of_json ctx clause in
+        let* clause =
+          de_bruijn_var_of_json trait_clause_id_of_json ctx clause
+        in
         Ok (Clause clause)
     | `Assoc [ ("ParentClause", `List [ x_0; x_1; x_2 ]) ] ->
         let* x_0 = box_of_json trait_instance_id_of_json ctx x_0 in
@@ -1292,7 +1308,7 @@ and const_generic_of_json (ctx : of_json_ctx) (js : json) :
         let* global = global_decl_id_of_json ctx global in
         Ok (CgGlobal global)
     | `Assoc [ ("Var", var) ] ->
-        let* var = const_generic_var_id_of_json ctx var in
+        let* var = de_bruijn_var_of_json const_generic_var_id_of_json ctx var in
         Ok (CgVar var)
     | `Assoc [ ("Value", value) ] ->
         let* value = literal_of_json ctx value in
@@ -1307,7 +1323,9 @@ and ty_of_json (ctx : of_json_ctx) (js : json) : (ty, string) result =
         let* x_1 = generic_args_of_json ctx x_1 in
         Ok (TAdt (x_0, x_1))
     | `Assoc [ ("TypeVar", type_var) ] ->
-        let* type_var = type_var_id_of_json ctx type_var in
+        let* type_var =
+          de_bruijn_var_of_json type_var_id_of_json ctx type_var
+        in
         Ok (TVar type_var)
     | `Assoc [ ("Literal", literal) ] ->
         let* literal = literal_type_of_json ctx literal in

charon-ml/src/NameMatcher.ml

@@ -235,8 +235,7 @@ let ctx_to_fmt_env (ctx : ctx) : PrintLlbcAst.fmt_env =
     global_decls = ctx.global_decls;
     trait_decls = ctx.trait_decls;
     trait_impls = ctx.trait_impls;
-    regions = [];
-    generics = TypesUtils.empty_generic_params;
+    generics = [];
     locals = [];
   }
 
@@ -351,13 +350,13 @@ let update_rmap (c : match_config) (m : maps) (id : var) (v : T.region) : bool =
   if c.map_vars_to_vars && not is_var then false
   else
     match v with
-    | RBVar (db_id, rid) -> (
+    | RBVar { dbid; varid } -> (
         (* 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)
+              varid 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 =
@@ -770,35 +769,39 @@ let mk_name_matcher (ctx : ctx) (c : match_config) (pat : string) :
  * Helpers to convert names to patterns
  *)
 
-(* 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;
-      (** Note that we have a stack of maps for the regions *)
+(* Maps from variable ids to option pattern variable ids *)
+type vars_map = {
+  rmap : var option T.RegionVarId.Map.t;
   tmap : var option T.TypeVarId.Map.t;
   cmap : var option T.ConstGenericVarId.Map.t;
 }
 
-let empty_constraints =
+let empty_vars_map =
   {
-    rmap = [ T.RegionVarId.Map.empty ];
+    rmap = T.RegionVarId.Map.empty;
     tmap = T.TypeVarId.Map.empty;
     cmap = T.ConstGenericVarId.Map.empty;
   }
 
+(* We use this to store the constraints maps. Not that we have a stack of map,
+   with one level per binder. *)
+type constraints = vars_map list
+
+let empty_constraints = [ empty_vars_map ]
+
 let ref_kind_to_pattern (rk : T.ref_kind) : ref_kind =
   match rk with
   | RMut -> RMut
   | RShared -> RShared
 
 let region_to_pattern (m : constraints) (r : T.region) : region =
   match r with
-  | RBVar (bdid, r) ->
+  | RBVar { dbid; varid } ->
       RVar
-        (match List.nth_opt m.rmap bdid with
+        (match List.nth_opt m dbid with
         | None -> None
-        | Some rmap -> (
-            match T.RegionVarId.Map.find_opt r rmap with
+        | Some map -> (
+            match T.RegionVarId.Map.find_opt varid map.rmap with
             | Some r -> r
             | None -> None))
   | RFVar _ ->
@@ -812,20 +815,29 @@ let region_to_pattern (m : constraints) (r : T.region) : region =
          detect specific function calls) to patterns. *)
       RVar None
 
-let type_var_to_pattern (m : constraints) (v : T.TypeVarId.id) : var option =
-  match T.TypeVarId.Map.find_opt v m.tmap with
-  | Some v -> v
-  | None ->
-      (* Return the empty pattern *)
-      None
-
-let const_generic_var_to_pattern (m : constraints) (v : T.ConstGenericVarId.id)
-    : var option =
-  match T.ConstGenericVarId.Map.find_opt v m.cmap with
-  | Some v -> v
-  | None ->
-      (* Return the empty pattern *)
-      None
+let type_var_to_pattern (m : constraints) (v : T.TypeVarId.id T.de_bruijn_var) :
+    var option =
+  match List.nth_opt m v.dbid with
+  | None -> None
+  | Some map -> begin
+      match T.TypeVarId.Map.find_opt v.varid map.tmap with
+      | Some v -> v
+      | None ->
+          (* Return the empty pattern *)
+          None
+    end
+
+let const_generic_var_to_pattern (m : constraints)
+    (v : T.ConstGenericVarId.id T.de_bruijn_var) : var option =
+  match List.nth_opt m v.dbid with
+  | None -> None
+  | Some map -> begin
+      match T.ConstGenericVarId.Map.find_opt v.varid map.cmap with
+      | Some v -> v
+      | None ->
+          (* Return the empty pattern *)
+          None
+    end
 
 let constraints_map_compute_regions_map (regions : T.region_var list) :
     var option T.RegionVarId.Map.t =
@@ -847,7 +859,7 @@ let constraints_map_compute_regions_map (regions : T.region_var list) :
        regions)
 
 let compute_constraints_map (generics : T.generic_params) : constraints =
-  let rmap = [ constraints_map_compute_regions_map generics.regions ] in
+  let rmap = constraints_map_compute_regions_map generics.regions in
   let tmap =
     T.TypeVarId.Map.of_list
       (List.map
@@ -860,12 +872,12 @@ let compute_constraints_map (generics : T.generic_params) : constraints =
          (fun (x : T.const_generic_var) -> (x.index, Some (VarName x.name)))
          generics.const_generics)
   in
-  { rmap; tmap; cmap }
+  [ { rmap; tmap; cmap } ]
 
 let constraints_map_push_regions_map (m : constraints)
     (regions : T.region_var list) : constraints =
   let rmap = constraints_map_compute_regions_map regions in
-  { m with rmap = rmap :: m.rmap }
+  { empty_vars_map with rmap } :: m
 
 (** Push a regions map to the constraints map, if the group of regions
     is non-empty - TODO: do something more precise *)

charon-ml/src/PrintLlbcAst.ml

@@ -149,8 +149,7 @@ module Crate = struct
       global_decls = m.global_decls;
       trait_decls = m.trait_decls;
       trait_impls = m.trait_impls;
-      regions = [];
-      generics = empty_generic_params;
+      generics = [];
       locals = [];
     }
 

charon-ml/src/PrintTypes.ml

@@ -25,18 +25,25 @@ 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) :
+let trait_clause_var_to_pretty_string (var : trait_clause_id de_bruijn_var) :
     string =
-  "'" ^ show_region_db_id db_id ^ "_" ^ RegionVarId.to_string id
+  "TraitClause@" ^ show_de_bruijn_id var.dbid ^ "_"
+  ^ TraitClauseId.to_string var.varid
+
+let bound_region_var_to_pretty_string (var : region_var_id de_bruijn_var) :
+    string =
+  "'" ^ show_de_bruijn_id var.dbid ^ "_" ^ RegionVarId.to_string var.varid
 
 let region_id_to_pretty_string (id : region_id) : string =
   "'" ^ RegionId.to_string id
 
-let type_var_id_to_pretty_string (id : type_var_id) : string =
-  "T@" ^ TypeVarId.to_string id
+let type_var_id_to_pretty_string (var : type_var_id de_bruijn_var) : string =
+  "T@" ^ show_de_bruijn_id var.dbid ^ "_" ^ TypeVarId.to_string var.varid
 
-let const_generic_var_id_to_pretty_string (id : const_generic_var_id) : string =
-  "C@" ^ ConstGenericVarId.to_string id
+let const_generic_var_id_to_pretty_string
+    (var : const_generic_var_id de_bruijn_var) : string =
+  "C@" ^ show_de_bruijn_id var.dbid ^ "_"
+  ^ ConstGenericVarId.to_string var.varid
 
 let type_decl_id_to_pretty_string (id : type_decl_id) : string =
   "TypeDecl@" ^ TypeDeclId.to_string id
@@ -59,40 +66,53 @@ 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 -> (
+let bound_region_var_to_string (env : 'a fmt_env)
+    (var : region_var_id de_bruijn_var) : string =
+  match List.nth_opt env.generics var.dbid with
+  | None -> bound_region_var_to_pretty_string var
+  | Some generics -> (
       (* 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
+      match
+        List.find_opt
+          (fun (r : region_var) -> r.index = var.varid)
+          generics.regions
+      with
+      | None -> bound_region_var_to_pretty_string var
       | Some r -> region_var_to_string r)
 
-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 *)
-  match
-    List.find_opt (fun (x : type_var) -> x.index = id) env.generics.types
-  with
-  | None -> type_var_id_to_pretty_string id
-  | Some x -> type_var_to_string x
+let type_var_id_to_string (env : 'a fmt_env) (var : type_var_id de_bruijn_var) :
+    string =
+  match List.nth_opt env.generics var.dbid with
+  | None -> type_var_id_to_pretty_string var
+  | Some generics -> begin
+      (* Note that the types are not necessarily ordered following their indices *)
+      match
+        List.find_opt (fun (x : type_var) -> x.index = var.varid) generics.types
+      with
+      | None -> type_var_id_to_pretty_string var
+      | Some x -> type_var_to_string x
+    end
 
 let const_generic_var_id_to_string (env : 'a fmt_env)
-    (id : const_generic_var_id) : string =
-  (* Note that the const generics are not necessarily ordered following their indices *)
-  match
-    List.find_opt
-      (fun (x : const_generic_var) -> x.index = id)
-      env.generics.const_generics
-  with
-  | None -> const_generic_var_id_to_pretty_string id
-  | Some x -> const_generic_var_to_string x
+    (var : const_generic_var_id de_bruijn_var) : string =
+  match List.nth_opt env.generics var.dbid with
+  | None -> const_generic_var_id_to_pretty_string var
+  | Some generics -> begin
+      (* Note that the const generics are not necessarily ordered following their indices *)
+      match
+        List.find_opt
+          (fun (x : const_generic_var) -> x.index = var.varid)
+          generics.const_generics
+      with
+      | None -> const_generic_var_id_to_pretty_string var
+      | Some x -> const_generic_var_to_string x
+    end
 
 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 var -> bound_region_var_to_string env var
   | RFVar rid -> region_id_to_pretty_string rid
 
 let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id
@@ -154,7 +174,7 @@ and trait_impl_id_to_string env id =
 and const_generic_to_string (env : 'a fmt_env) (cg : const_generic) : string =
   match cg with
   | CgGlobal id -> global_decl_id_to_string env id
-  | CgVar id -> const_generic_var_id_to_string env id
+  | CgVar var -> const_generic_var_id_to_string env var
   | CgValue lit -> literal_to_string lit
 
 and ty_to_string (env : 'a fmt_env) (ty : ty) : string =
@@ -184,7 +204,7 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string =
       | 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
+      let env = fmt_env_push_regions env regions in
       let inputs =
         "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> "
       in
@@ -247,7 +267,7 @@ and trait_instance_id_to_string (env : 'a fmt_env) (id : trait_instance_id) :
       impl ^ generics
   | BuiltinOrAuto trait ->
       region_binder_to_string trait_decl_ref_to_string env trait
-  | Clause id -> trait_clause_id_to_string env id
+  | Clause id -> trait_clause_var_to_pretty_string id
   | ParentClause (inst_id, _decl_id, clause_id) ->
       let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in

charon-ml/src/PrintUllbcAst.ml

@@ -119,8 +119,7 @@ module Crate = struct
         global_decls = m.global_decls;
         trait_decls = m.trait_decls;
         trait_impls = m.trait_impls;
-        regions = [];
-        generics = empty_generic_params;
+        generics = [];
         locals = [];
       }
     in