Use bound vars internally

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 = [];
   }
 
@@ -777,68 +776,69 @@ 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.RegionId.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.RegionId.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.RegionId.Map.empty ];
+    rmap = T.RegionId.Map.empty;
     tmap = T.TypeVarId.Map.empty;
     cmap = T.ConstGenericVarId.Map.empty;
   }
 
+(* We use this to store the constraints maps. Note that we have a stack of
+   maps, 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 lookup_var_in_maps (m : constraints)
+    (lookup : 'id -> vars_map -> 'a option option) (var : 'id T.de_bruijn_var) :
+    'a option =
+  let dbid, varid =
+    match var with
+    | Bound (dbid, varid) -> (dbid, varid)
+    | Free varid -> (List.length m - 1, varid)
+  in
+  match List.nth_opt m dbid with
+  | None -> None
+  | Some map -> (
+      match lookup varid map with
+      | Some r -> r
+      | None -> None)
+
 let region_to_pattern (m : constraints) (r : T.region) : region =
   match r with
   | RVar var ->
-      let dbid, varid =
-        match var with
-        | Bound (dbid, varid) -> (dbid, varid)
-        | Free varid -> (List.length m.rmap - 1, varid)
-      in
       RVar
-        (match List.nth_opt m.rmap dbid with
-        | None -> None
-        | Some rmap -> (
-            match T.RegionId.Map.find_opt varid rmap with
-            | Some r -> r
-            | None -> None))
+        (lookup_var_in_maps m
+           (fun varid map -> T.RegionId.Map.find_opt varid map.rmap)
+           var)
   | RStatic -> RStatic
   | RErased ->
       (* We do get there when converting function pointers (when we try to
          detect specific function calls) to patterns. *)
       RVar None
 
 let type_var_to_pattern (m : constraints) (var : T.type_db_var) : var option =
-  match var with
-  | Bound _ -> failwith "bound type var"
-  | Free id -> begin
-      match T.TypeVarId.Map.find_opt id m.tmap with
-      | Some v -> v
-      | None -> None
-      (* Return the empty pattern *)
-    end
+  lookup_var_in_maps m
+    (fun varid map -> T.TypeVarId.Map.find_opt varid map.tmap)
+    var
 
 let const_generic_var_to_pattern (m : constraints)
     (var : T.const_generic_db_var) : var option =
-  match var with
-  | Bound _ -> failwith "bound const generic var"
-  | Free id -> begin
-      match T.ConstGenericVarId.Map.find_opt id m.cmap with
-      | Some v -> v
-      | None -> None
-      (* Return the empty pattern *)
-    end
+  lookup_var_in_maps m
+    (fun varid map -> T.ConstGenericVarId.Map.find_opt varid map.cmap)
+    var
 
 let constraints_map_compute_regions_map (regions : T.region_var list) :
     var option T.RegionId.Map.t =
@@ -860,7 +860,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
@@ -873,12 +873,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

@@ -150,8 +150,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

@@ -7,9 +7,6 @@ open TypesUtils
 open GAst
 open PrintUtils
 
-let type_var_to_string (tv : type_var) : string = tv.name
-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
@@ -37,23 +34,39 @@ let ref_kind_to_string (rk : ref_kind) : string =
 
 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 de_bruijn_var_to_pretty_string show_bound show_free var : string =
+let de_bruijn_var_to_pretty_string show_varid var : string =
   match var with
-  | Bound (dbid, varid) -> show_de_bruijn_id dbid ^ "_" ^ show_bound varid
-  | Free varid -> "'" ^ show_free varid
+  | Bound (dbid, varid) -> show_de_bruijn_id dbid ^ "_" ^ show_varid varid
+  | Free varid -> show_varid varid
 
 let region_db_var_to_pretty_string (var : region_db_var) : string =
-  "'" ^ de_bruijn_var_to_pretty_string RegionId.to_string RegionId.to_string var
+  "'" ^ de_bruijn_var_to_pretty_string RegionId.to_string var
+
+let type_db_var_to_pretty_string (var : type_db_var) : string =
+  "T@" ^ de_bruijn_var_to_pretty_string TypeVarId.to_string var
 
 let type_var_id_to_pretty_string (id : type_var_id) : string =
   "T@" ^ TypeVarId.to_string id
 
+let type_var_to_string (tv : type_var) : string = tv.name
+
 let const_generic_var_id_to_pretty_string (id : const_generic_var_id) : string =
   "C@" ^ ConstGenericVarId.to_string id
 
+let const_generic_db_var_to_pretty_string (var : const_generic_db_var) : string
+    =
+  "C@" ^ de_bruijn_var_to_pretty_string ConstGenericVarId.to_string var
+
+let const_generic_var_to_string (v : const_generic_var) : string = v.name
+
+let trait_clause_id_to_pretty_string (id : trait_clause_id) : string =
+  "TraitClause@" ^ TraitClauseId.to_string id
+
+let trait_db_var_to_pretty_string (var : trait_db_var) : string =
+  "TraitClause@" ^ de_bruijn_var_to_pretty_string TraitClauseId.to_string var
+
+let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id
+
 let type_decl_id_to_pretty_string (id : type_decl_id) : string =
   "TypeDecl@" ^ TypeDeclId.to_string id
 
@@ -75,57 +88,64 @@ 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 trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id
+let lookup_var_in_env (env : 'a fmt_env)
+    (find_in : generic_params -> 'id -> 'b option) (var : 'id de_bruijn_var) :
+    'b option =
+  if List.length env.generics == 0 then None
+  else
+    let dbid, varid =
+      match var with
+      | Bound (dbid, varid) -> (dbid, varid)
+      | Free varid ->
+          let len = List.length env.generics in
+          let dbid = len - 1 in
+          (dbid, varid)
+    in
+    match List.nth_opt env.generics dbid with
+    | None -> None
+    | Some generics -> begin
+        match find_in generics varid with
+        | None -> None
+        | Some r -> Some r
+      end
 
 let region_db_var_to_string (env : 'a fmt_env) (var : region_db_var) : string =
-  let dbid, varid =
-    match var with
-    | Bound (dbid, varid) -> (dbid, varid)
-    | Free varid ->
-        let len = List.length env.regions in
-        let dbid = if len == 0 then 0 else len - 1 in
-        (dbid, varid)
+  (* Note that the regions are not necessarily ordered following their indices *)
+  let find (generics : generic_params) varid =
+    List.find_opt (fun (v : region_var) -> v.index = varid) generics.regions
   in
-  match List.nth_opt env.regions dbid with
+  match lookup_var_in_env env find var with
   | None -> region_db_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 -> region_db_var_to_pretty_string var
-      | Some r -> region_var_to_string r
-    end
+  | Some r -> region_var_to_string r
 
 let type_db_var_to_string (env : 'a fmt_env) (var : type_db_var) : string =
-  match var with
-  | Bound _ -> failwith "bound type variable"
-  | Free id -> begin
-      (* 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
-    end
+  let find (generics : generic_params) varid =
+    List.find_opt (fun (v : type_var) -> v.index = varid) generics.types
+  in
+  match lookup_var_in_env env find var with
+  | None -> type_db_var_to_pretty_string var
+  | Some r -> type_var_to_string r
 
 let const_generic_db_var_to_string (env : 'a fmt_env)
     (var : const_generic_db_var) : string =
-  match var with
-  | Bound _ -> failwith "bound const generic variable"
-  | Free id -> begin
-      (* Note that the types 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
-    end
+  let find (generics : generic_params) varid =
+    List.find_opt
+      (fun (v : const_generic_var) -> v.index = varid)
+      generics.const_generics
+  in
+  match lookup_var_in_env env find var with
+  | None -> const_generic_db_var_to_pretty_string var
+  | Some r -> const_generic_var_to_string r
 
 let trait_db_var_to_string (env : 'a fmt_env) (var : trait_db_var) : string =
-  match var with
-  | Bound _ -> failwith "bound trait clause variable"
-  | Free id -> trait_clause_id_to_pretty_string id
+  let find (generics : generic_params) varid =
+    List.find_opt
+      (fun (v : trait_clause) -> v.clause_id = varid)
+      generics.trait_clauses
+  in
+  match lookup_var_in_env env find var with
+  | None -> trait_db_var_to_pretty_string var
+  | Some r -> trait_clause_id_to_pretty_string r.clause_id
 
 let region_to_string (env : 'a fmt_env) (r : region) : string =
   match r with
@@ -220,7 +240,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 binder ->
-      let env = { env with regions = binder.binder_regions :: env.regions } in
+      let env = fmt_env_push_regions env binder.binder_regions in
       let inputs, output = binder.binder_value in
       let inputs =
         "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> "

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

charon-ml/src/PrintUtils.ml

@@ -19,26 +19,21 @@ type 'fun_body fmt_env = {
   global_decls : global_decl GlobalDeclId.Map.t;
   trait_decls : trait_decl TraitDeclId.Map.t;
   trait_impls : trait_impl TraitImplId.Map.t;
-  regions : region_var list list;
-      (** We have a stack of regions, because we can dive into groups of
-          universally quantified regions (for instance because of the arrow
-          type).
-
-          Note that the variables in the generics don't need to be ordered following their
-          indices, i.e., the region var of index 0 doesn't have to be at index 0,
-          etc. We lookup the variables by checking their id, not their position.
+  generics : generic_params list;
+      (** We have a stack of generic parameters, because we can dive into
+          binders (for instance because of the arrow type).
       *)
-  generics : generic_params;
-      (* We ignore `generics.regions` as they are tracked in `regions` already *)
   locals : (VarId.id * string option) list;
       (** The local variables don't need to be ordered (same as the generics) *)
 }
 
 let fmt_env_update_generics_and_preds (env : 'a fmt_env)
     (generics : generic_params) : 'a fmt_env =
-  let { regions; _ } : generic_params = generics in
-  { env with regions = regions :: env.regions; generics }
+  { env with generics = generics :: env.generics }
 
 let fmt_env_push_regions (env : 'a fmt_env) (regions : region_var list) :
     'a fmt_env =
-  { env with regions = regions :: env.regions }
+  {
+    env with
+    generics = { TypesUtils.empty_generic_params with regions } :: env.generics;
+  }