Correctly handle binders in ml printing

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 = [];
   }
 

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
@@ -22,23 +19,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
 
@@ -60,57 +73,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
@@ -205,7 +225,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;
+  }