Clean up region variables

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"

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) :

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,15 +778,15 @@ 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;
 }
 
 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")

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