Use the new collections

11 files changed, 65 insertions, 138 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index 8a9c4857..1a9dcfc8 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -137,7 +137,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
   }
 
 type type_context = {
-  type_defs_groups : M.types_decl_group TypeDefId.map_t;
+  type_defs_groups : M.types_decl_group TypeDefId.Map.t;
   type_defs : type_def list;
 }
 [@@deriving show]
@@ -147,7 +147,7 @@ type eval_ctx = {
   fun_context : fun_def list;
   type_vars : type_var list;
   env : env;
-  ended_regions : RegionId.set_t;
+  ended_regions : RegionId.Set.t;
 }
 [@@deriving show]
 (** Evaluation context *)
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 4ec5aab7..fd07b7b6 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,4 +1,4 @@
-open Collections
+module C = Collections
 
 (** Signature for a module describing an identifier.
     
@@ -12,19 +12,18 @@ module type Id = sig
   type generator
   (** Id generator - simply a counter *)
 
-  type set_t
-
-  type +!'a map_t
-
   val zero : id
 
   val generator_zero : generator
 
   val fresh_stateful_generator : unit -> generator ref * (unit -> id)
 
-  (* TODO: this is stateful! - but we may want to be able to duplicate contexts... *)
+  (* TODO: this should be stateful! - but we may want to be able to duplicate
+     contexts...
+     Maybe we could have a `fresh` and a `global_fresh`
+     TODO: change the order of the returned types
+  *)
   val fresh : generator -> id * generator
-  (* TODO: change the order of the returned types *)
 
   val to_string : id -> string
 
@@ -32,6 +31,8 @@ module type Id = sig
 
   val show_id : id -> string
 
+  val id_of_json : Yojson.Basic.t -> (id, string) result
+
   val pp_generator : Format.formatter -> generator -> unit
 
   val show_generator : generator -> string
@@ -53,38 +54,16 @@ module type Id = sig
   val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list
 
   val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
-  (** Same as [mapi], but where the indices start with 1 *)
-
-  val pp_set_t : Format.formatter -> set_t -> unit
-
-  val show_set_t : set_t -> string
-
-  val pp_map_t :
-    (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a map_t -> unit
-
-  val show_map_t : ('a -> string) -> 'a map_t -> string
-
-  module Ord : Map.OrderedType with type t = id
-
-  module Set : Set.S with type elt = id with type t = set_t
-
-  val set_to_string : string option -> Set.t -> string
-  (** Convert a set to a string.
-      
-      Takes an indentation as parameter, in case you want to insert a breakline
-      for every binding.
+  (** Same as [mapi], but where the indices start with 1.
+       
+      TODO: generalize to `map_from_i`
    *)
 
-  module Map : Map.S with type key = id with type 'a t = 'a map_t
+  module Ord : C.OrderedType with type t = id
 
-  val map_to_string : string option -> ('a -> string) -> 'a map_t -> string
-  (** Convert a map to a string.
-      
-      Takes an indentation as parameter, in case you want to insert a breakline
-      for every binding.
-   *)
+  module Set : C.Set with type elt = id
 
-  val id_of_json : Yojson.Basic.t -> (id, string) result
+  module Map : C.Map with type key = id
 end
 
 (** Generative functor for identifiers.
@@ -124,6 +103,12 @@ module IdGen () : Id = struct
 
   let of_int x = x
 
+  let id_of_json js =
+    (* TODO: check boundaries ? *)
+    match js with
+    | `Int i -> Ok i
+    | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
+
   let nth v id = List.nth v id
 
   let nth_opt v id = List.nth_opt v id
@@ -146,73 +131,16 @@ module IdGen () : Id = struct
     type t = id
 
     let compare = compare
-  end
-
-  module Set = Set.Make (Ord)
-  module Map = Map.Make (Ord)
 
-  type set_t = Set.t
+    let to_string = to_string
 
-  type +!'a map_t = 'a Map.t
+    let pp_t = pp_id
 
-  let show_set_t s =
-    let ids = Set.fold (fun id s -> to_string id :: s) s [] in
-    let ids = List.rev ids in
-    "{" ^ String.concat "," ids ^ "}"
-
-  let pp_set_t fmt s =
-    let pp_string = Format.pp_print_string fmt in
-    pp_string "{";
-    Set.iter (fun id -> pp_string (to_string id ^ ",")) s;
-    pp_string "}"
-
-  let show_map_t show_a s =
-    let ids =
-      Map.fold (fun id x s -> (to_string id ^ " -> " ^ show_a x) :: s) s []
-    in
-    let ids = List.rev ids in
-    "{" ^ String.concat "," ids ^ "}"
-
-  let pp_map_t (pp_a : Format.formatter -> 'a -> unit) (fmt : Format.formatter)
-      (m : 'a map_t) : unit =
-    let pp_string = Format.pp_print_string fmt in
-    pp_string "{";
-    Map.iter
-      (fun id x ->
-        pp_string (to_string id ^ " -> ");
-        pp_a fmt x;
-        pp_string ",")
-      m;
-    pp_string "}"
-
-  let set_to_string indent_opt ids =
-    let indent, sep =
-      match indent_opt with Some indent -> (indent, ",\n") | None -> ("", ",")
-    in
-    let ids = Set.fold (fun id ids -> (indent ^ to_string id) :: ids) ids [] in
-    match ids with
-    | [] -> "{}"
-    | _ -> "{\n" ^ String.concat sep (List.rev ids) ^ "\n}"
-
-  let map_to_string indent_opt a_to_string ids =
-    let indent, sep =
-      match indent_opt with Some indent -> (indent, ",\n") | None -> ("", ",")
-    in
-    let ids =
-      Map.fold
-        (fun id v ids ->
-          (indent ^ to_string id ^ " -> " ^ a_to_string v) :: ids)
-        ids []
-    in
-    match ids with
-    | [] -> "{}"
-    | _ -> "{\n" ^ String.concat sep (List.rev ids) ^ "\n}"
+    let show_t = show_id
+  end
 
-  let id_of_json js =
-    (* TODO: check boundaries ? *)
-    match js with
-    | `Int i -> Ok i
-    | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
+  module Set = C.MakeSet (Ord)
+  module Map = C.MakeMap (Ord)
 end
 
 type name = string list [@@deriving show]
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index cde799d8..faa63c0a 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -430,7 +430,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     it was left unchanged.
   *)
 let give_back_symbolic_value (_config : C.config)
-    (proj_regions : T.RegionId.set_t) (proj_ty : T.rty) (sv : V.symbolic_value)
+    (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value)
     (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
   let subst local_regions local_ty =
     let child_proj =
@@ -971,7 +971,7 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
   ctx
 
 and end_abstractions (config : C.config) (chain : borrow_or_abs_ids)
-    (abs_ids : V.AbstractionId.set_t) (ctx : C.eval_ctx) : C.eval_ctx =
+    (abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
   V.AbstractionId.Set.fold
     (fun id ctx -> end_abstraction config chain id ctx)
     abs_ids ctx
@@ -1185,7 +1185,7 @@ and end_abstraction_remove_from_context (_config : C.config)
         abstraction
 *)
 and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
-    (abs_id : V.AbstractionId.id) (regions : T.RegionId.set_t)
+    (abs_id : V.AbstractionId.id) (regions : T.RegionId.Set.t)
     (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
   (* Find the first proj_borrows which intersects the proj_loans *)
   let explore_shared = true in
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 6bc31d63..455d62c3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -31,7 +31,7 @@ type exploration_kind = {
 let ek_all : exploration_kind =
   { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
 
-type borrow_ids = Borrows of V.BorrowId.set_t | Borrow of V.BorrowId.id
+type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id
 [@@deriving show]
 
 exception FoundBorrowIds of borrow_ids
@@ -84,8 +84,8 @@ let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id)
     Note that the two abstractions have different views (in terms of regions)
     of the symbolic value (hence the two region types).
 *)
-let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
-    (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool =
+let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.Set.t)
+    (ty2 : T.rty) (rset2 : T.RegionId.Set.t) : bool =
   match (ty1, ty2) with
   | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
   | T.Integer int_ty1, T.Integer int_ty2 ->
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index d2d10670..7c648563 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -13,7 +13,7 @@ type symbolic_expansion =
   | SeConcrete of V.constant_value
   | SeAdt of (T.VariantId.id option * V.symbolic_value list)
   | SeMutRef of V.BorrowId.id * V.symbolic_value
-  | SeSharedRef of V.BorrowId.set_t * V.symbolic_value
+  | SeSharedRef of V.BorrowId.Set.t * V.symbolic_value
 
 (** Auxiliary function.
 
@@ -23,7 +23,7 @@ type symbolic_expansion =
 *)
 let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
     (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
-    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
+    (regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) :
     V.abstract_shared_borrows =
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
@@ -132,7 +132,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
 *)
 let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
     (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
-    (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t)
+    (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t)
     (v : V.typed_value) (ty : T.rty) : V.typed_avalue =
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
@@ -235,9 +235,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
               (lazy
                 ("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1
                ^ "\n- rset1: "
-                ^ T.RegionId.set_to_string None rset1
+                ^ T.RegionId.Set.to_string None rset1
                 ^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: "
-                ^ T.RegionId.set_to_string None rset2
+                ^ T.RegionId.Set.to_string None rset2
                 ^ "\n"));
             assert (not (projections_intersect ty1 rset1 ty2 rset2)));
           V.ASymbolic (V.AProjBorrows (s, ty))
@@ -290,7 +290,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
 
     TODO: detailed comments. See [apply_proj_borrows]
 *)
-let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
+let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
     (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
@@ -528,7 +528,7 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
   (fresh_reborrow, apply_registered_reborrows)
 
 let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
-    (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t)
+    (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t)
     (v : V.typed_value) (ty : T.rty) : C.eval_ctx * V.typed_avalue =
   let check_symbolic_no_ended = true in
   let allow_reborrows = true in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 1b06dd7f..8b29bac9 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -554,7 +554,7 @@ let create_empty_abstractions_from_abs_region_groups
    * - the regions of the ancestors of abs_id
    * - the regions of abs_id
    *)
-  let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+  let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref =
     ref V.AbstractionId.Map.empty
   in
   (* Auxiliary function to create one abstraction *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index fc86f1f5..971dc801 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -192,7 +192,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     check that the set of ended regions doesn't intersect the set of
     regions used in the type (this is more general).
 *)
-let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t)
+let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t)
     (s : V.symbolic_value) : bool =
   let regions = rty_regions s.V.sv_ty in
   not (T.RegionId.Set.disjoint regions ended_regions)
@@ -202,7 +202,7 @@ let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t)
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
  *)
-let bottom_in_value (ended_regions : T.RegionId.set_t) (v : V.typed_value) :
+let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
     bool =
   let obj =
     object
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 66a5e5ac..77b11136 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -19,8 +19,8 @@ type borrow_info = {
   loan_kind : T.ref_kind;
   loan_in_abs : bool;
   (* true if the loan was found in an abstraction *)
-  loan_ids : V.BorrowId.set_t;
-  borrow_ids : V.BorrowId.set_t;
+  loan_ids : V.BorrowId.Set.t;
+  borrow_ids : V.BorrowId.Set.t;
 }
 [@@deriving show]
 
@@ -36,14 +36,13 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info =
 let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
   { outer_borrow = true; outer_shared = true }
 
-(* TODO: we need to factorize print functions for sets *)
 let ids_reprs_to_string (indent : string)
     (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
-  V.BorrowId.map_to_string (Some indent) V.BorrowId.to_string reprs
+  V.BorrowId.Map.to_string (Some indent) V.BorrowId.to_string reprs
 
 let borrows_infos_to_string (indent : string)
     (infos : borrow_info V.BorrowId.Map.t) : string =
-  V.BorrowId.map_to_string (Some indent) show_borrow_info infos
+  V.BorrowId.Map.to_string (Some indent) show_borrow_info infos
 
 type borrow_kind = Mut | Shared | Inactivated
 
@@ -79,7 +78,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     ignored_loans := (rkind, bid) :: !ignored_loans
   in
 
-  let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit
+  let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.Set.t) : unit
       =
     let reprs = !ids_reprs in
     let infos = !borrows_infos in
@@ -612,7 +611,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
 
 type proj_borrows_info = {
   abs_id : V.AbstractionId.id;
-  regions : T.RegionId.set_t;
+  regions : T.RegionId.Set.t;
   proj_ty : T.rty;
   as_shared_value : bool;  (** True if the value is below a shared borrow *)
 }
@@ -620,7 +619,7 @@ type proj_borrows_info = {
 
 type proj_loans_info = {
   abs_id : V.AbstractionId.id;
-  regions : T.RegionId.set_t;
+  regions : T.RegionId.Set.t;
 }
 [@@deriving show]
 
@@ -704,7 +703,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
   log#ldebug
     (lazy
       ("check_symbolic_values: collected information:\n"
-      ^ V.SymbolicValueId.map_to_string (Some "  ") show_sv_info !infos));
+      ^ V.SymbolicValueId.Map.to_string (Some "  ") show_sv_info !infos));
   (* Check *)
   let check_info _id info =
     assert (info.env_count = 0 || info.aproj_borrows = []);
diff --git a/src/Print.ml b/src/Print.ml
index 000874fe..282b2860 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -290,7 +290,7 @@ module Values = struct
       string =
     match lc with
     | SharedLoan (loans, v) ->
-        let loans = V.BorrowId.set_to_string None loans in
+        let loans = V.BorrowId.Set.to_string None loans in
         "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
     | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
 
@@ -375,7 +375,7 @@ module Values = struct
         ^ typed_avalue_to_string fmt av
         ^ "⌋"
     | ASharedLoan (loans, v, av) ->
-        let loans = V.BorrowId.set_to_string None loans in
+        let loans = V.BorrowId.Set.to_string None loans in
         "@shared_loan(" ^ loans ^ ", "
         ^ typed_value_to_string fmt v
         ^ ", "
@@ -441,9 +441,9 @@ module Values = struct
     indent ^ "abs@"
     ^ V.AbstractionId.to_string abs.abs_id
     ^ "{parents="
-    ^ V.AbstractionId.set_to_string None abs.parents
+    ^ V.AbstractionId.Set.to_string None abs.parents
     ^ "}" ^ "{regions="
-    ^ T.RegionId.set_to_string None abs.regions
+    ^ T.RegionId.Set.to_string None abs.regions
     ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
 end
 
@@ -552,7 +552,7 @@ module Contexts = struct
 
   let eval_ctx_to_string (ctx : C.eval_ctx) : string =
     let fmt = eval_ctx_to_ctx_formatter ctx in
-    let ended_regions = T.RegionId.set_to_string None ctx.ended_regions in
+    let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in
     let frames = split_env_according_to_frames ctx.env in
     let num_frames = List.length frames in
     let frames =
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 38560894..3accb9c5 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -44,11 +44,11 @@ let mk_ref_ty (r : 'r) (ty : 'r ty) (ref_kind : ref_kind) : 'r ty =
 let mk_box_ty (ty : 'r ty) : 'r ty = Adt (Assumed Box, [], [ ty ])
 
 (** Check if a region is in a set of regions *)
-let region_in_set (r : RegionId.id region) (rset : RegionId.set_t) : bool =
+let region_in_set (r : RegionId.id region) (rset : RegionId.Set.t) : bool =
   match r with Static -> false | Var id -> RegionId.Set.mem id rset
 
 (** Return the set of regions in an rty *)
-let rty_regions (ty : rty) : RegionId.set_t =
+let rty_regions (ty : rty) : RegionId.Set.t =
   let s = ref RegionId.Set.empty in
   let add_region (r : RegionId.id region) =
     match r with Static -> () | Var rid -> s := RegionId.Set.add rid !s
@@ -65,7 +65,7 @@ let rty_regions (ty : rty) : RegionId.set_t =
   (* Return the set of accumulated regions *)
   !s
 
-let rty_regions_intersect (ty : rty) (regions : RegionId.set_t) : bool =
+let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool =
   let ty_regions = rty_regions ty in
   not (RegionId.Set.disjoint ty_regions regions)
 
diff --git a/src/Values.ml b/src/Values.ml
index 31f47709..59cfbdca 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -132,7 +132,7 @@ and borrow_content =
        *)
 
 and loan_content =
-  | SharedLoan of (BorrowId.set_t[@opaque]) * typed_value
+  | SharedLoan of (BorrowId.Set.t[@opaque]) * typed_value
   | MutLoan of (BorrowId.id[@opaque])
       (** TODO: we might want to add a set of borrow ids (useful for inactivated
           borrows, and extremely useful when giving shared values to abstractions).
@@ -322,7 +322,7 @@ and aloan_content =
           px -> mut_borrow l0 (mut_borrow @s1)
           ```
        *)
-  | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue
+  | ASharedLoan of (BorrowId.Set.t[@opaque]) * typed_value * typed_avalue
       (** A shared loan owned by an abstraction.
 
           Example:
@@ -599,9 +599,9 @@ and typed_avalue = { value : avalue; ty : rty }
 
 type abs = {
   abs_id : (AbstractionId.id[@opaque]);
-  parents : (AbstractionId.set_t[@opaque]);  (** The parent abstractions *)
-  regions : (RegionId.set_t[@opaque]);  (** Regions owned by this abstraction *)
-  ancestors_regions : (RegionId.set_t[@opaque]);
+  parents : (AbstractionId.Set.t[@opaque]);  (** The parent abstractions *)
+  regions : (RegionId.Set.t[@opaque]);  (** Regions owned by this abstraction *)
+  ancestors_regions : (RegionId.Set.t[@opaque]);
       (** Union of the regions owned by this abstraction's ancestors (not
           including the regions of this abstraction itself) *)
   avalues : typed_avalue list;  (** The values in this abstraction *)