Remove the vector type for the Id module

10 files changed, 136 insertions, 289 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 7be1a4bc..36977aad 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -14,10 +14,10 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
 type assertion = { cond : operand; expected : bool } [@@deriving show]
 
 type fun_sig = {
-  region_params : region_var RegionVarId.vector;
+  region_params : region_var list;
   num_early_bound_regions : int;
-  type_params : type_var TypeVarId.vector;
-  inputs : rty VarId.vector;
+  type_params : type_var list;
+  inputs : rty list;
   output : rty;
 }
 [@@deriving show]
@@ -75,7 +75,7 @@ type fun_def = {
   signature : fun_sig;
   divergent : bool;
   arg_count : int;
-  locals : var VarId.vector;
+  locals : var list;
   body : expression;
 }
 [@@deriving show]
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index bb0e9b69..4f6c2e73 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -138,7 +138,7 @@ let variant_of_json (js : json) : (T.variant, string) result =
     (match js with
     | `Assoc [ ("name", name); ("fields", fields) ] ->
         let* name = string_of_json name in
-        let* fields = T.FieldId.vector_of_json field_of_json fields in
+        let* fields = list_of_json field_of_json fields in
         Ok { T.variant_name = name; fields }
     | _ -> Error "")
 
@@ -146,10 +146,10 @@ let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result =
   combine_error_msgs js "type_def_kind_of_json"
     (match js with
     | `Assoc [ ("Struct", fields) ] ->
-        let* fields = T.FieldId.vector_of_json field_of_json fields in
+        let* fields = list_of_json field_of_json fields in
         Ok (T.Struct fields)
     | `Assoc [ ("Enum", variants) ] ->
-        let* variants = T.VariantId.vector_of_json variant_of_json variants in
+        let* variants = list_of_json variant_of_json variants in
         Ok (T.Enum variants)
     | _ -> Error "")
 
@@ -166,12 +166,8 @@ let type_def_of_json (js : json) : (T.type_def, string) result =
         ] ->
         let* def_id = T.TypeDefId.id_of_json def_id in
         let* name = name_of_json name in
-        let* region_params =
-          T.RegionVarId.vector_of_json region_var_of_json region_params
-        in
-        let* type_params =
-          T.TypeVarId.vector_of_json type_var_of_json type_params
-        in
+        let* region_params = list_of_json region_var_of_json region_params in
+        let* type_params = list_of_json type_var_of_json type_params in
         let* kind = type_def_kind_of_json kind in
         Ok { T.def_id; name; region_params; type_params; kind }
     | _ -> Error "")
@@ -445,14 +441,10 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
           ("inputs", inputs);
           ("output", output);
         ] ->
-        let* region_params =
-          T.RegionVarId.vector_of_json region_var_of_json region_params
-        in
+        let* region_params = list_of_json region_var_of_json region_params in
         let* num_early_bound_regions = int_of_json num_early_bound_regions in
-        let* type_params =
-          T.TypeVarId.vector_of_json type_var_of_json type_params
-        in
-        let* inputs = V.VarId.vector_of_json rty_of_json inputs in
+        let* type_params = list_of_json type_var_of_json type_params in
+        let* inputs = list_of_json rty_of_json inputs in
         let* output = rty_of_json output in
         Ok
           {
@@ -572,7 +564,7 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result =
         let* signature = fun_sig_of_json signature in
         let* divergent = bool_of_json divergent in
         let* arg_count = int_of_json arg_count in
-        let* locals = V.VarId.vector_of_json var_of_json locals in
+        let* locals = list_of_json var_of_json locals in
         let* body = expression_of_json body in
         Ok { A.def_id; name; signature; divergent; arg_count; locals; body }
     | _ -> Error "")
@@ -604,7 +596,7 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result =
           ("functions", functions);
         ] ->
         let* declarations = list_of_json declaration_of_json declarations in
-        let* types = T.TypeDefId.vector_of_json type_def_of_json types in
-        let* functions = A.FunDefId.vector_of_json fun_def_of_json functions in
+        let* types = list_of_json type_def_of_json types in
+        let* functions = list_of_json fun_def_of_json functions in
         Ok { M.declarations; types; functions }
     | _ -> Error "")
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 8a498e2e..84c88e1c 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -18,9 +18,9 @@ type config = { mode : interpreter_mode; check_invariants : bool }
 [@@deriving show]
 
 type eval_ctx = {
-  type_context : type_def TypeDefId.vector;
-  fun_context : fun_def FunDefId.vector;
-  type_vars : type_var TypeVarId.vector;
+  type_context : type_def list;
+  fun_context : fun_def list;
+  type_vars : type_var list;
   env : env;
   symbolic_counter : SymbolicValueId.generator;
   borrow_counter : BorrowId.generator;
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index ebe0d898..3c07b511 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -10,16 +10,13 @@ module type Id = sig
   type generator
   (** Id generator - simply a counter *)
 
-  (* TODO: use list instead *)
-  type 'a vector
-
   type set_t
 
   val zero : id
 
   val generator_zero : generator
 
-  (* TODO: this is stateful! *)
+  (* TODO: this is stateful! - but we may want to be able to duplicated contexts... *)
   val fresh : generator -> id * generator
 
   val to_string : id -> string
@@ -36,42 +33,21 @@ module type Id = sig
 
   val of_int : id -> int
 
-  val pp_vector :
-    (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a vector -> unit
-
-  val show_vector : (Format.formatter -> 'a -> unit) -> 'a vector -> string
-
-  val empty_vector : 'a vector
-
-  val vector_to_list : 'a vector -> 'a list
-
-  val vector_of_list : 'a list -> 'a vector
-
-  val length : 'a vector -> int
+  val nth : 'a list -> id -> 'a
 
-  val nth : 'a vector -> id -> 'a
+  val nth_opt : 'a list -> id -> 'a option
 
-  val nth_opt : 'a vector -> id -> 'a option
-
-  val update_nth : 'a vector -> id -> 'a -> 'a vector
-  (** Update the nth element of the vector.
+  val update_nth : 'a list -> id -> 'a -> 'a list
+  (** Update the nth element of the list.
 
       Raises [Invalid_argument] if the identifier is out of range.
    *)
 
-  val iter : ('a -> unit) -> 'a vector -> unit
-
-  val map : ('a -> 'b) -> 'a vector -> 'b vector
-
-  val mapi : (id -> 'a -> 'b) -> 'a vector -> 'b vector
+  val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list
 
-  val mapi_from1 : (id -> 'a -> 'b) -> 'a vector -> 'b vector
+  val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
   (** Same as [mapi], but where the indices start with 1 *)
 
-  val for_all : ('a -> bool) -> 'a vector -> bool
-
-  val exists : ('a -> bool) -> 'a vector -> bool
-
   val pp_set_t : Format.formatter -> set_t -> unit
 
   val show_set_t : set_t -> string
@@ -85,11 +61,6 @@ module type Id = sig
   module Map : Map.S with type key = id
 
   val id_of_json : Yojson.Basic.t -> (id, string) result
-
-  val vector_of_json :
-    (Yojson.Basic.t -> ('a, string) result) ->
-    Yojson.Basic.t ->
-    ('a vector, string) result
 end
 
 (** Generative functor for identifiers.
@@ -102,8 +73,6 @@ module IdGen () : Id = struct
 
   type generator = id [@@deriving show]
 
-  type 'a vector = 'a list [@@deriving show]
-
   let zero = 0
 
   let generator_zero = 0
@@ -122,14 +91,6 @@ module IdGen () : Id = struct
 
   let of_int x = x
 
-  let empty_vector = []
-
-  let vector_to_list v = v
-
-  let vector_of_list v = v
-
-  let length v = List.length v
-
   let nth v id = List.nth v id
 
   let nth_opt v id = List.nth_opt v id
@@ -140,10 +101,6 @@ module IdGen () : Id = struct
     | _ :: vec', 0 -> v :: vec'
     | x :: vec', _ -> x :: update_nth vec' (id - 1) v
 
-  let iter = List.iter
-
-  let map = List.map
-
   let mapi = List.mapi
 
   let mapi_from1 f ls =
@@ -152,10 +109,6 @@ module IdGen () : Id = struct
     in
     aux 1 ls
 
-  let for_all = List.for_all
-
-  let exists = List.exists
-
   module Ord = struct
     type t = id
 
@@ -183,10 +136,6 @@ module IdGen () : Id = struct
     match js with
     | `Int i -> Ok i
     | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
-
-  let vector_of_json a_of_json js =
-    OfJsonBasic.combine_error_msgs js "vector_of_json"
-      (OfJsonBasic.list_of_json a_of_json js)
 end
 
 type name = string list [@@deriving show]
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 05dc3f5a..003f5411 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -47,8 +47,7 @@ let expression_to_string ctx =
 let mk_unit_ty : T.ety = T.Tuple []
 
 (* TODO: move *)
-let mk_unit_value : V.typed_value =
-  { V.value = V.Tuple (T.FieldId.vector_of_list []); V.ty = mk_unit_ty }
+let mk_unit_value : V.typed_value = { V.value = V.Tuple []; V.ty = mk_unit_ty }
 
 let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value =
   { V.value; ty }
@@ -81,8 +80,8 @@ let rec check_borrows_in_value (check : V.borrow_content -> bool)
     (v : V.typed_value) : bool =
   match v.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> true
-  | V.Adt av -> T.FieldId.for_all (check_borrows_in_value check) av.field_values
-  | V.Tuple values -> T.FieldId.for_all (check_borrows_in_value check) values
+  | V.Adt av -> List.for_all (check_borrows_in_value check) av.field_values
+  | V.Tuple values -> List.for_all (check_borrows_in_value check) values
   | V.Assumed (Box bv) -> check_borrows_in_value check bv
   | V.Borrow bc -> (
       check bc
@@ -100,8 +99,8 @@ let rec check_loans_in_value (check : V.loan_content -> bool)
     (v : V.typed_value) : bool =
   match v.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> true
-  | V.Adt av -> T.FieldId.for_all (check_loans_in_value check) av.field_values
-  | V.Tuple values -> T.FieldId.for_all (check_loans_in_value check) values
+  | V.Adt av -> List.for_all (check_loans_in_value check) av.field_values
+  | V.Tuple values -> List.for_all (check_loans_in_value check) values
   | V.Assumed (Box bv) -> check_loans_in_value check bv
   | V.Borrow bc -> (
       match bc with
@@ -119,12 +118,8 @@ let rec lookup_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
     (v : V.typed_value) : V.loan_content option =
   match v.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> None
-  | V.Adt av ->
-      let values = T.FieldId.vector_to_list av.field_values in
-      List.find_map (lookup_loan_in_value ek l) values
-  | V.Tuple values ->
-      let values = T.FieldId.vector_to_list values in
-      List.find_map (lookup_loan_in_value ek l) values
+  | V.Adt av -> List.find_map (lookup_loan_in_value ek l) av.field_values
+  | V.Tuple values -> List.find_map (lookup_loan_in_value ek l) values
   | V.Assumed (Box bv) -> lookup_loan_in_value ek l bv
   | V.Borrow bc -> (
       match bc with
@@ -175,13 +170,11 @@ let rec update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
   match v.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> v
   | V.Adt av ->
-      let values =
-        T.FieldId.map (update_loan_in_value ek l nlc) av.field_values
-      in
+      let values = List.map (update_loan_in_value ek l nlc) av.field_values in
       let av = { av with field_values = values } in
       { v with value = Adt av }
   | V.Tuple values ->
-      let values = T.FieldId.map (update_loan_in_value ek l nlc) values in
+      let values = List.map (update_loan_in_value ek l nlc) values in
       { v with value = Tuple values }
   | V.Assumed (Box bv) ->
       { v with value = Assumed (Box (update_loan_in_value ek l nlc bv)) }
@@ -228,12 +221,8 @@ let rec lookup_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id)
     (v : V.typed_value) : V.borrow_content option =
   match v.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> None
-  | V.Adt av ->
-      let values = T.FieldId.vector_to_list av.field_values in
-      List.find_map (lookup_borrow_in_value ek l) values
-  | V.Tuple values ->
-      let values = T.FieldId.vector_to_list values in
-      List.find_map (lookup_borrow_in_value ek l) values
+  | V.Adt av -> List.find_map (lookup_borrow_in_value ek l) av.field_values
+  | V.Tuple values -> List.find_map (lookup_borrow_in_value ek l) values
   | V.Assumed (Box bv) -> lookup_borrow_in_value ek l bv
   | V.Borrow bc -> (
       match bc with
@@ -281,13 +270,11 @@ let rec update_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id)
   match v.V.value with
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> v
   | V.Adt av ->
-      let values =
-        T.FieldId.map (update_borrow_in_value ek l nbc) av.field_values
-      in
+      let values = List.map (update_borrow_in_value ek l nbc) av.field_values in
       let av = { av with field_values = values } in
       { v with value = Adt av }
   | V.Tuple values ->
-      let values = T.FieldId.map (update_borrow_in_value ek l nbc) values in
+      let values = List.map (update_borrow_in_value ek l nbc) values in
       { v with value = Tuple values }
   | V.Assumed (Box bv) ->
       { v with value = Assumed (Box (update_borrow_in_value ek l nbc bv)) }
@@ -369,12 +356,8 @@ let borrows_in_value (v : V.typed_value) : bool =
 let rec loans_in_value (v : V.typed_value) : bool =
   match v.V.value with
   | V.Concrete _ -> false
-  | V.Adt av ->
-      let fields = T.FieldId.vector_to_list av.field_values in
-      List.exists loans_in_value fields
-  | V.Tuple fields ->
-      let fields = T.FieldId.vector_to_list fields in
-      List.exists loans_in_value fields
+  | V.Adt av -> List.exists loans_in_value av.field_values
+  | V.Tuple fields -> List.exists loans_in_value fields
   | V.Assumed (Box bv) -> loans_in_value bv
   | V.Borrow bc -> (
       match bc with
@@ -387,12 +370,8 @@ let rec loans_in_value (v : V.typed_value) : bool =
 let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
   match v.V.value with
   | V.Concrete _ -> None
-  | V.Adt av ->
-      let fields = T.FieldId.vector_to_list av.field_values in
-      get_first_loan_in_values fields
-  | V.Tuple fields ->
-      let fields = T.FieldId.vector_to_list fields in
-      get_first_loan_in_values fields
+  | V.Adt av -> get_first_loan_in_values av.field_values
+  | V.Tuple fields -> get_first_loan_in_values fields
   | V.Assumed (Box bv) -> get_first_loan_in_value bv
   | V.Borrow bc -> (
       match bc with
@@ -413,12 +392,8 @@ and get_first_loan_in_values (vl : V.typed_value list) : V.loan_content option =
 let rec bottom_in_value (v : V.typed_value) : bool =
   match v.V.value with
   | V.Concrete _ -> false
-  | V.Adt av ->
-      let fields = T.FieldId.vector_to_list av.field_values in
-      List.exists bottom_in_value fields
-  | V.Tuple fields ->
-      let fields = T.FieldId.vector_to_list fields in
-      List.exists bottom_in_value fields
+  | V.Adt av -> List.exists bottom_in_value av.field_values
+  | V.Tuple fields -> List.exists bottom_in_value fields
   | V.Assumed (Box bv) -> bottom_in_value bv
   | V.Borrow bc -> (
       match bc with
@@ -450,19 +425,16 @@ let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer)
        * boxes upon ending inner borrows *)
       ({ v0 with value = Assumed (Box bv') }, res)
   | V.Adt adt ->
-      let values = T.FieldId.vector_to_list adt.field_values in
-      let values', res =
-        end_borrow_get_borrow_in_values config io l outer_borrows values
+      let values, res =
+        end_borrow_get_borrow_in_values config io l outer_borrows
+          adt.field_values
       in
-      let values' = T.FieldId.vector_of_list values' in
-      ({ v0 with value = Adt { adt with field_values = values' } }, res)
+      ({ v0 with value = Adt { adt with field_values = values } }, res)
   | V.Tuple values ->
-      let values = T.FieldId.vector_to_list values in
-      let values', res =
+      let values, res =
         end_borrow_get_borrow_in_values config io l outer_borrows values
       in
-      let values' = T.FieldId.vector_of_list values' in
-      ({ v0 with value = Tuple values' }, res)
+      ({ v0 with value = Tuple values }, res)
   | V.Loan (V.MutLoan _) -> (v0, NotFound)
   | V.Loan (V.SharedLoan (borrows, v)) ->
       (* Update the outer borrows, if necessary *)
@@ -543,19 +515,11 @@ let rec give_back_value_to_value config bid (v : V.typed_value)
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> destv
   | V.Adt av ->
       let field_values =
-        List.map
-          (give_back_value_to_value config bid v)
-          (T.FieldId.vector_to_list av.field_values)
+        List.map (give_back_value_to_value config bid v) av.field_values
       in
-      let field_values = T.FieldId.vector_of_list field_values in
       { destv with value = Adt { av with field_values } }
   | V.Tuple values ->
-      let values =
-        List.map
-          (give_back_value_to_value config bid v)
-          (T.FieldId.vector_to_list values)
-      in
-      let values = T.FieldId.vector_of_list values in
+      let values = List.map (give_back_value_to_value config bid v) values in
       { destv with value = Tuple values }
   | V.Assumed (Box destv') ->
       {
@@ -590,19 +554,11 @@ let rec give_back_shared_to_value (config : C.config) bid
   | V.Concrete _ | V.Bottom | V.Symbolic _ -> destv
   | V.Adt av ->
       let field_values =
-        List.map
-          (give_back_shared_to_value config bid)
-          (T.FieldId.vector_to_list av.field_values)
+        List.map (give_back_shared_to_value config bid) av.field_values
       in
-      let field_values = T.FieldId.vector_of_list field_values in
       { destv with value = Adt { av with field_values } }
   | V.Tuple values ->
-      let values =
-        List.map
-          (give_back_shared_to_value config bid)
-          (T.FieldId.vector_to_list values)
-      in
-      let values = T.FieldId.vector_of_list values in
+      let values = List.map (give_back_shared_to_value config bid) values in
       { destv with value = Tuple values }
   | V.Assumed (Box destv') ->
       {
@@ -699,14 +655,10 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id)
     match v.V.value with
     | V.Concrete _ | V.Bottom | V.Symbolic _ -> v
     | V.Adt av ->
-        let fields = T.FieldId.vector_to_list av.field_values in
-        let fields = List.map reborrow_in_value fields in
-        let fields = T.FieldId.vector_of_list fields in
+        let fields = List.map reborrow_in_value av.field_values in
         { v with value = Adt { av with field_values = fields } }
     | V.Tuple fields ->
-        let fields = T.FieldId.vector_to_list fields in
         let fields = List.map reborrow_in_value fields in
-        let fields = T.FieldId.vector_of_list fields in
         { v with value = Tuple fields }
     | V.Assumed (Box bv) ->
         { v with value = Assumed (Box (reborrow_in_value bv)) }
@@ -1045,7 +997,7 @@ let rec access_projection (access : projection_access) (env : C.env)
               Ok (env1, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), V.Tuple values -> (
-          assert (arity = T.FieldId.length values);
+          assert (arity = List.length values);
           let fv = T.FieldId.nth values field_id in
           (* Project *)
           match access_projection access env update p' fv with
@@ -1238,7 +1190,7 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
   | Ok ctx -> ctx
 
 (** Compute an expanded ADT bottom value *)
-let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.vector)
+let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
     (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
     (regions : T.erased_region list) (types : T.ety list) : V.typed_value =
   (* Lookup the definition and check if it is an enumeration - it
@@ -1246,15 +1198,13 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.vector)
      is a field projection with *some* variant id. Retrieve the list
      of fields at the same time. *)
   let def = T.TypeDefId.nth tyctx def_id in
-  assert (List.length regions = T.RegionVarId.length def.T.region_params);
+  assert (List.length regions = List.length def.T.region_params);
   (* Compute the field types *)
   let field_types =
     Subst.type_def_get_instantiated_field_type def opt_variant_id types
   in
   (* Initialize the expanded value *)
-  let field_types = T.FieldId.vector_to_list field_types in
   let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in
-  let fields = T.FieldId.vector_of_list fields in
   let av =
     V.Adt
       {
@@ -1273,7 +1223,6 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
     V.typed_value =
   (* Generate the field values *)
   let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in
-  let fields = T.FieldId.vector_of_list fields in
   let v = V.Tuple fields in
   let ty = T.Tuple field_types in
   { V.value = v; V.ty }
@@ -1434,8 +1383,8 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind)
             (* Nothing to do for symbolic values - note that if the value needs
                to be copied, etc. we perform additional checks later *)
             ()
-        | V.Adt adt -> T.FieldId.iter inspect_update adt.field_values
-        | V.Tuple values -> T.FieldId.iter inspect_update values
+        | V.Adt adt -> List.iter inspect_update adt.field_values
+        | V.Tuple values -> List.iter inspect_update values
         | V.Assumed (Box v) -> inspect_update v
         | V.Borrow bc -> (
             match bc with
@@ -1534,9 +1483,8 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
         | V.Symbolic _ ->
             (* Nothing to do for symbolic values - TODO: not sure *)
             raise Unimplemented
-        | V.Adt adt ->
-            T.FieldId.iter (inspect_update end_loans) adt.field_values
-        | V.Tuple values -> T.FieldId.iter (inspect_update end_loans) values
+        | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values
+        | V.Tuple values -> List.iter (inspect_update end_loans) values
         | V.Assumed (Box v) -> inspect_update end_loans v
         | V.Borrow bc -> (
             assert (not end_loans);
@@ -1609,15 +1557,13 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
   match v.V.value with
   | V.Concrete _ -> (ctx, v)
   | V.Adt av ->
-      let fields = T.FieldId.vector_to_list av.field_values in
-      let ctx', fields = List.fold_left_map (copy_value config) ctx fields in
-      let fields = T.FieldId.vector_of_list fields in
-      (ctx', { v with V.value = V.Adt { av with field_values = fields } })
+      let ctx, fields =
+        List.fold_left_map (copy_value config) ctx av.field_values
+      in
+      (ctx, { v with V.value = V.Adt { av with field_values = fields } })
   | V.Tuple fields ->
-      let fields = T.FieldId.vector_to_list fields in
-      let ctx', fields = List.fold_left_map (copy_value config) ctx fields in
-      let fields = T.FieldId.vector_of_list fields in
-      (ctx', { v with V.value = V.Tuple fields })
+      let ctx, fields = List.fold_left_map (copy_value config) ctx fields in
+      (ctx, { v with V.value = V.Tuple fields })
   | V.Bottom -> failwith "Can't copy ⊥"
   | V.Assumed _ -> failwith "Can't copy an assumed value"
   | V.Borrow bc -> (
@@ -1625,6 +1571,7 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
       match bc with
       | SharedBorrow bid ->
           let ctx', bid' = C.fresh_borrow_id ctx in
+          (* TODO: clean indices *)
           let env'' = reborrow_shared config bid bid' ctx'.env in
           let ctx'' = { ctx' with env = env'' } in
           (ctx'', { v with V.value = V.Borrow (SharedBorrow bid') })
@@ -1646,36 +1593,30 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
   (* Check the type while converting *)
   match (ty, cv) with
   (* Unit *)
-  | T.Tuple [], Unit -> { V.value = V.Tuple (T.FieldId.vector_of_list []); ty }
+  | T.Tuple [], Unit -> { V.value = V.Tuple []; ty }
   (* Adt with one variant and no fields *)
   | T.Adt (def_id, [], []), ConstantAdt def_id' ->
       assert (def_id = def_id');
       (* Check that the adt definition only has one variant with no fields,
          compute the variant id at the same time. *)
       let def = T.TypeDefId.nth ctx.type_context def_id in
-      assert (T.RegionVarId.length def.region_params = 0);
-      assert (T.TypeVarId.length def.type_params = 0);
+      assert (List.length def.region_params = 0);
+      assert (List.length def.type_params = 0);
       let variant_id =
         match def.kind with
         | Struct fields ->
-            assert (T.FieldId.length fields = 0);
+            assert (List.length fields = 0);
             None
         | Enum variants ->
-            assert (T.VariantId.length variants = 1);
+            assert (List.length variants = 1);
             let variant_id = T.VariantId.zero in
             let variant = T.VariantId.nth variants variant_id in
-            assert (T.FieldId.length variant.fields = 0);
+            assert (List.length variant.fields = 0);
             Some variant_id
       in
       let value =
         V.Adt
-          {
-            def_id;
-            variant_id;
-            regions = [];
-            types = [];
-            field_values = T.FieldId.vector_of_list [];
-          }
+          { def_id; variant_id; regions = []; types = []; field_values = [] }
       in
       { value; ty }
   (* Scalar, boolean... *)
@@ -1918,24 +1859,20 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
   | E.Aggregate (aggregate_kind, ops) -> (
       (* Evaluate the operands *)
       let ctx, values = eval_operands config ctx ops in
-      let values = T.FieldId.vector_of_list values in
       (* Match on the aggregate kind *)
       match aggregate_kind with
       | E.AggregatedTuple ->
-          let tys =
-            List.map (fun v -> v.V.ty) (T.FieldId.vector_to_list values)
-          in
+          let tys = List.map (fun v -> v.V.ty) values in
           Ok (ctx, { V.value = Tuple values; ty = T.Tuple tys })
       | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
           (* Sanity checks *)
           let type_def = C.ctx_lookup_type_def ctx def_id in
-          assert (
-            T.RegionVarId.length type_def.region_params = List.length regions);
+          assert (List.length type_def.region_params = List.length regions);
           let expected_field_types =
             Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id
               types
           in
-          assert (expected_field_types = T.FieldId.map (fun v -> v.V.ty) values);
+          assert (expected_field_types = List.map (fun v -> v.V.ty) values);
           (* Construct the value *)
           let av =
             {
@@ -2312,10 +2249,7 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
 
       (* Create and push the input variables *)
       let input_vars =
-        V.VarId.vector_to_list
-          (V.VarId.mapi_from1
-             (fun id v -> (mk_var id None v.V.ty, v))
-             (V.VarId.vector_of_list args_vl))
+        V.VarId.mapi_from1 (fun id v -> (mk_var id None v.V.ty, v)) args_vl
       in
       let ctx = C.ctx_push_vars ctx input_vars in
 
@@ -2413,13 +2347,10 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
   | ConcreteMode -> (
       let tsubst =
         Subst.make_type_subst
-          (List.map
-             (fun v -> v.T.tv_index)
-             (T.TypeVarId.vector_to_list def.A.signature.type_params))
+          (List.map (fun v -> v.T.tv_index) def.A.signature.type_params)
           type_params
       in
       let locals, body = Subst.fun_def_substitute_in_body tsubst def in
-      let locals = V.VarId.vector_to_list locals in
 
       (* Evaluate the input operands *)
       let ctx1, args = eval_operands config ctx args in
@@ -2554,9 +2485,8 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) :
 (** Test a unit function (taking no arguments) by evaluating it in an empty
     environment
  *)
-let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
-    (fun_defs : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) :
-    unit eval_result =
+let test_unit_function (type_defs : T.type_def list) (fun_defs : A.fun_def list)
+    (fid : A.FunDefId.id) : unit eval_result =
   (* Retrieve the function declaration *)
   let fdef = A.FunDefId.nth fun_defs fid in
 
@@ -2565,8 +2495,8 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
     (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name));
 
   (* Sanity check - *)
-  assert (T.RegionVarId.length fdef.A.signature.region_params = 0);
-  assert (T.TypeVarId.length fdef.A.signature.type_params = 0);
+  assert (List.length fdef.A.signature.region_params = 0);
+  assert (List.length fdef.A.signature.type_params = 0);
   assert (fdef.A.arg_count = 0);
 
   (* Create the evaluation context *)
@@ -2574,7 +2504,7 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
     {
       C.type_context = type_defs;
       C.fun_context = fun_defs;
-      C.type_vars = T.TypeVarId.empty_vector;
+      C.type_vars = [];
       C.env = [];
       C.symbolic_counter = V.SymbolicValueId.generator_zero;
       C.borrow_counter = V.BorrowId.generator_zero;
@@ -2582,9 +2512,7 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
   in
 
   (* Put the (uninitialized) local variables *)
-  let ctx =
-    C.ctx_push_uninitialized_vars ctx (V.VarId.vector_to_list fdef.A.locals)
-  in
+  let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
 
   (* Evaluate the function *)
   let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in
@@ -2596,13 +2524,13 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
     no arguments) - TODO: move *)
 let fun_def_is_unit (def : A.fun_def) : bool =
   def.A.arg_count = 0
-  && T.RegionVarId.length def.A.signature.region_params = 0
-  && T.TypeVarId.length def.A.signature.type_params = 0
-  && V.VarId.length def.A.signature.inputs = 0
+  && List.length def.A.signature.region_params = 0
+  && List.length def.A.signature.type_params = 0
+  && List.length def.A.signature.inputs = 0
 
 (** Test all the unit functions in a list of function definitions *)
-let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector)
-    (fun_defs : A.fun_def A.FunDefId.vector) : unit =
+let test_all_unit_functions (type_defs : T.type_def list)
+    (fun_defs : A.fun_def list) : unit =
   let test_fun (def : A.fun_def) : unit =
     if fun_def_is_unit def then
       match test_unit_function type_defs fun_defs def.A.def_id with
@@ -2610,4 +2538,4 @@ let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector)
       | Ok _ -> ()
     else ()
   in
-  A.FunDefId.iter test_fun fun_defs
+  List.iter test_fun fun_defs
diff --git a/src/Modules.ml b/src/Modules.ml
index a2b1d3bf..3be1c742 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -15,7 +15,7 @@ type declaration =
 
 type cfim_module = {
   declarations : declaration list;
-  types : type_def TypeDefId.vector;
-  functions : fun_def FunDefId.vector;
+  types : type_def list;
+  functions : fun_def list;
 }
 (** CFIM module *)
diff --git a/src/Print.ml b/src/Print.ml
index 8547d5cb..bb172d5f 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -98,18 +98,15 @@ module Types = struct
 
   let variant_to_string fmt (v : T.variant) : string =
     v.variant_name ^ "("
-    ^ String.concat ", "
-        (List.map (field_to_string fmt) (T.FieldId.vector_to_list v.fields))
+    ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
     ^ ")"
 
   let name_to_string (name : name) : string = String.concat "::" name
 
   let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string)
       (def : T.type_def) : string =
-    let regions : T.region_var list =
-      T.RegionVarId.vector_to_list def.region_params
-    in
-    let types : T.type_var list = T.TypeVarId.vector_to_list def.type_params in
+    let regions = def.region_params in
+    let types = def.type_params in
     let rid_to_string rid =
       match List.find_opt (fun rv -> rv.T.rv_index = rid) regions with
       | Some rv -> region_var_to_string rv
@@ -133,7 +130,6 @@ module Types = struct
     in
     match def.kind with
     | T.Struct fields ->
-        let fields = T.FieldId.vector_to_list fields in
         if List.length fields > 0 then
           let fields =
             String.concat ","
@@ -142,7 +138,6 @@ module Types = struct
           "struct " ^ name ^ params ^ "{" ^ fields ^ "}"
         else "struct " ^ name ^ params ^ "{}"
     | T.Enum variants ->
-        let variants = T.VariantId.vector_to_list variants in
         let variants =
           List.map (fun v -> "|  " ^ variant_to_string fmt v) variants
         in
@@ -222,8 +217,9 @@ module Values = struct
           | Some vid -> fmt.adt_variant_to_string av.def_id vid
           | None -> fmt.type_def_id_to_string av.def_id
         in
-        let field_values = T.FieldId.vector_to_list av.field_values in
-        let field_values = List.map (typed_value_to_string fmt) field_values in
+        let field_values =
+          List.map (typed_value_to_string fmt) av.field_values
+        in
         if List.length field_values > 0 then
           match fmt.adt_field_names av.V.def_id av.V.variant_id with
           | None ->
@@ -240,7 +236,6 @@ module Values = struct
               adt_ident ^ " { " ^ field_values ^ " }"
         else adt_ident
     | Tuple values ->
-        let values = T.FieldId.vector_to_list values in
         let values =
           String.concat ", " (List.map (typed_value_to_string fmt) values)
         in
@@ -302,7 +297,7 @@ module Values = struct
           | Some vid -> fmt.adt_variant_to_string av.adef_id vid
           | None -> fmt.type_def_id_to_string av.adef_id
         in
-        let field_values = T.FieldId.vector_to_list av.afield_values in
+        let field_values = av.afield_values in
         if List.length field_values > 0 then
           let field_values =
             String.concat " "
@@ -311,7 +306,6 @@ module Values = struct
           adt_ident ^ " " ^ field_values
         else adt_ident
     | ATuple values ->
-        let values = T.FieldId.vector_to_list values in
         let values =
           String.concat ", " (List.map (typed_avalue_to_string fmt) values)
         in
@@ -428,8 +422,7 @@ module Contexts = struct
   let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter =
     PV.value_to_rtype_formatter fmt
 
-  let type_ctx_to_adt_variant_to_string_fun
-      (ctx : T.type_def T.TypeDefId.vector) :
+  let type_ctx_to_adt_variant_to_string_fun (ctx : T.type_def list) :
       T.TypeDefId.id -> T.VariantId.id -> string =
    fun def_id variant_id ->
     let def = T.TypeDefId.nth ctx def_id in
@@ -439,14 +432,14 @@ module Contexts = struct
         let variant = T.VariantId.nth variants variant_id in
         PT.name_to_string def.name ^ "::" ^ variant.variant_name
 
-  let type_ctx_to_adt_field_names_fun (ctx : T.type_def T.TypeDefId.vector) :
+  let type_ctx_to_adt_field_names_fun (ctx : T.type_def list) :
       T.TypeDefId.id -> T.VariantId.id option -> string list option =
    fun def_id opt_variant_id ->
     let def = T.TypeDefId.nth ctx def_id in
     let fields = T.type_def_get_fields def opt_variant_id in
     (* TODO: the field name should be optional?? *)
-    let fields = T.FieldId.map (fun f -> f.T.field_name) fields in
-    Some (T.FieldId.vector_to_list fields)
+    let fields = List.map (fun f -> f.T.field_name) fields in
+    Some fields
 
   let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
     (* We shouldn't use r_to_string *)
@@ -547,8 +540,8 @@ module CfimAst = struct
       PT.type_def_id_to_string = fmt.type_def_id_to_string;
     }
 
-  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def T.TypeDefId.vector)
-      : T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
+  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def list) :
+      T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
    fun def_id opt_variant_id field_id ->
     let def = T.TypeDefId.nth ctx def_id in
     let fields = T.type_def_get_fields def opt_variant_id in
@@ -783,8 +776,8 @@ module CfimAst = struct
     let name = PT.name_to_string def.A.name in
 
     (* Region/type parameters *)
-    let regions = T.RegionVarId.vector_to_list sg.region_params in
-    let types = T.TypeVarId.vector_to_list sg.type_params in
+    let regions = sg.region_params in
+    let types = sg.type_params in
     let params =
       if List.length regions + List.length types = 0 then ""
       else
@@ -794,14 +787,14 @@ module CfimAst = struct
     in
 
     (* Arguments *)
-    let inputs = V.VarId.vector_to_list def.locals in
+    let inputs = def.locals in
     let ret_var, inputs =
       match inputs with
       | [] -> failwith "Inconsistent signature"
       | ret_var :: inputs -> (ret_var, inputs)
     in
     let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in
-    let args = List.combine inputs (V.VarId.vector_to_list sg.inputs) in
+    let args = List.combine inputs sg.inputs in
     let args =
       List.map
         (fun (var, rty) -> PV.var_to_string var ^ " : " ^ rty_to_string rty)
@@ -821,7 +814,7 @@ module CfimAst = struct
         (fun var ->
           indent ^ indent_incr ^ PV.var_to_string var ^ " : "
           ^ ety_to_string var.var_ty ^ ";")
-        (V.VarId.vector_to_list def.locals)
+        def.locals
     in
     let locals = String.concat "\n" locals in
 
@@ -841,8 +834,8 @@ module PA = CfimAst (* local module *)
 module Module = struct
   (** This function pretty-prints a type definition by using a definition
       context *)
-  let type_def_to_string (type_context : T.type_def T.TypeDefId.vector)
-      (def : T.type_def) : string =
+  let type_def_to_string (type_context : T.type_def list) (def : T.type_def) :
+      string =
     let type_def_id_to_string (id : T.TypeDefId.id) : string =
       let def = T.TypeDefId.nth type_context id in
       PT.name_to_string def.name
@@ -851,9 +844,8 @@ module Module = struct
 
   (** Generate an [ast_formatter] by using a definition context in combination
       with the variables local to a function's definition *)
-  let def_ctx_to_ast_formatter (type_context : T.type_def T.TypeDefId.vector)
-      (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) :
-      PA.ast_formatter =
+  let def_ctx_to_ast_formatter (type_context : T.type_def list)
+      (fun_context : A.fun_def list) (def : A.fun_def) : PA.ast_formatter =
     let r_to_string vid =
       let var = T.RegionVarId.nth def.signature.region_params vid in
       PT.region_var_to_string var
@@ -894,24 +886,18 @@ module Module = struct
 
   (** This function pretty-prints a function definition by using a definition
       context *)
-  let fun_def_to_string (type_context : T.type_def T.TypeDefId.vector)
-      (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) : string =
+  let fun_def_to_string (type_context : T.type_def list)
+      (fun_context : A.fun_def list) (def : A.fun_def) : string =
     let fmt = def_ctx_to_ast_formatter type_context fun_context def in
     PA.fun_def_to_string fmt "" "  " def
 
   let module_to_string (m : M.cfim_module) : string =
     (* The types *)
-    let type_defs =
-      List.map
-        (type_def_to_string m.M.types)
-        (T.TypeDefId.vector_to_list m.M.types)
-    in
+    let type_defs = List.map (type_def_to_string m.M.types) m.M.types in
 
     (* The functions *)
     let fun_defs =
-      List.map
-        (fun_def_to_string m.M.types m.M.functions)
-        (A.FunDefId.vector_to_list m.M.functions)
+      List.map (fun_def_to_string m.M.types m.M.functions) m.M.functions
     in
 
     (* Put everything together *)
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 452b125f..b8c3edd9 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -54,17 +54,12 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
 (** Instantiate the type variables in an ADT definition, and return the list
     of types of the fields for the chosen variant *)
 let type_def_get_instantiated_field_type (def : T.type_def)
-    (opt_variant_id : T.VariantId.id option) (types : T.ety list) :
-    T.ety T.FieldId.vector =
+    (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list =
   let ty_subst =
-    make_type_subst
-      (List.map
-         (fun x -> x.T.tv_index)
-         (T.TypeVarId.vector_to_list def.T.type_params))
-      types
+    make_type_subst (List.map (fun x -> x.T.tv_index) def.T.type_params) types
   in
   let fields = T.type_def_get_fields def opt_variant_id in
-  T.FieldId.map
+  List.map
     (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty)
     fields
 
@@ -72,7 +67,7 @@ let type_def_get_instantiated_field_type (def : T.type_def)
     context *)
 let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx)
     (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
-    (types : T.ety list) : T.ety T.FieldId.vector =
+    (types : T.ety list) : T.ety list =
   let def = C.ctx_lookup_type_def ctx def_id in
   type_def_get_instantiated_field_type def opt_variant_id types
 
@@ -204,10 +199,10 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety)
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
 let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
-    (def : A.fun_def) : V.var V.VarId.vector * A.expression =
+    (def : A.fun_def) : V.var list * A.expression =
   let rsubst r = r in
   let locals =
-    V.VarId.map
+    List.map
       (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty })
       def.A.locals
   in
diff --git a/src/Types.ml b/src/Types.ml
index 77296ac1..2b57e3f7 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -90,19 +90,16 @@ type ety = erased_region ty [@@deriving show]
 
 type field = { field_name : string; field_ty : rty } [@@deriving show]
 
-type variant = { variant_name : string; fields : field FieldId.vector }
-[@@deriving show]
+type variant = { variant_name : string; fields : field list } [@@deriving show]
 
-type type_def_kind =
-  | Struct of field FieldId.vector
-  | Enum of variant VariantId.vector
+type type_def_kind = Struct of field list | Enum of variant list
 [@@deriving show]
 
 type type_def = {
   def_id : TypeDefId.id;
   name : name;
-  region_params : region_var RegionVarId.vector;
-  type_params : type_var TypeVarId.vector;
+  region_params : region_var list;
+  type_params : type_var list;
   kind : type_def_kind;
 }
 [@@deriving show]
@@ -137,7 +134,7 @@ let rec erase_regions (ty : rty) : ety =
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
 let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
-    : field FieldId.vector =
+    : field list =
   match (def.kind, opt_variant_id) with
   | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
   | Struct fields, None -> fields
diff --git a/src/Values.ml b/src/Values.ml
index 9d1cb819..330f22d3 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -79,7 +79,7 @@ type symbolic_proj_comp = {
 type value =
   | Concrete of constant_value  (** Concrete (non-symbolic) value *)
   | Adt of adt_value  (** Enumerations and structures *)
-  | Tuple of typed_value FieldId.vector
+  | Tuple of typed_value list
       (** Tuple - note that units are encoded as 0-tuples *)
   | Bottom  (** No value (uninitialized or moved value) *)
   | Assumed of assumed_value  (** Assumed types (Box, Vec, Cell...) *)
@@ -93,7 +93,7 @@ and adt_value = {
   variant_id : VariantId.id option;
   regions : erased_region list;
   types : ety list;
-  field_values : typed_value FieldId.vector;
+  field_values : typed_value list;
 }
 [@@deriving show]
 
@@ -138,7 +138,7 @@ type abstract_shared_borrows =
 type avalue =
   | AConcrete of constant_value
   | AAdt of aadt_value
-  | ATuple of typed_avalue FieldId.vector
+  | ATuple of typed_avalue list
   | ABottom
   | ALoan of aloan_content
   | ABorrow of aborrow_content
@@ -151,7 +151,7 @@ and aadt_value = {
   avariant_id : VariantId.id option;
   aregions : erased_region list;
   atypes : rty list;
-  afield_values : typed_avalue FieldId.vector;
+  afield_values : typed_avalue list;
 }
 [@@deriving show]