Derive more debugging facilities

2 files changed, 47 insertions, 13 deletions

diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index e1684f2c..931ec97b 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -12,6 +12,8 @@ module type Id = sig
 
   type 'a vector
 
+  type set_t
+
   val zero : id
 
   val generator_zero : generator
@@ -68,9 +70,13 @@ module type Id = sig
 
   val exists : ('a -> bool) -> 'a vector -> bool
 
+  val pp_set_t : Format.formatter -> set_t -> unit
+
+  val show_set_t : set_t -> string
+
   module Ord : Map.OrderedType with type t = id
 
-  module Set : Set.S with type elt = id
+  module Set : Set.S with type elt = id with type t = set_t
 
   val set_to_string : Set.t -> string
 
@@ -157,6 +163,15 @@ module IdGen () : Id = struct
   module Set = Set.Make (Ord)
   module Map = Map.Make (Ord)
 
+  type set_t = Set.t
+
+  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 = Format.pp_print_string fmt (show_set_t s)
+
   let set_to_string ids =
     let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in
     "{" ^ String.concat ", " (List.rev ids) ^ "}"
diff --git a/src/Values.ml b/src/Values.ml
index e549846d..07dfb618 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -35,7 +35,12 @@ let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
 
 let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
 
-type scalar_value = { value : big_int; int_ty : integer_type }
+let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
+  Format.pp_print_string fmt (Z.to_string bi)
+
+let show_big_int (bi : big_int) : string = Z.to_string bi
+
+type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
 (** A scalar value
 
     Note that we use unbounded integers everywhere.
@@ -48,15 +53,18 @@ type constant_value =
   | Bool of bool
   | Char of char
   | String of string
+[@@deriving show]
 
 type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
+[@@deriving show]
 (** Symbolic value *)
 
 type symbolic_proj_comp = {
   svalue : symbolic_value;  (** The symbolic value itself *)
-  rset_ended : RegionId.Set.t;
+  rset_ended : RegionId.set_t;
       (** The regions used in the symbolic value which have already ended *)
 }
+[@@deriving show]
 (** A complementary projector over a symbolic value.
     
     "Complementary" stands for the fact that it is a projector over all the
@@ -74,6 +82,7 @@ type value =
   | Borrow of borrow_content  (** A borrowed value *)
   | Loan of loan_content  (** A loaned value *)
   | Symbolic of symbolic_proj_comp  (** Unknown value *)
+[@@deriving show]
 
 and adt_value = {
   def_id : TypeDefId.id;
@@ -82,6 +91,7 @@ and adt_value = {
   types : ety list;
   field_values : typed_value FieldId.vector;
 }
+[@@deriving show]
 
 and borrow_content =
   | SharedBorrow of BorrowId.id  (** A shared value *)
@@ -97,20 +107,23 @@ and borrow_content =
           is well typed) of this value and replace the inactivated borrow with a
           mutable borrow.
        *)
+[@@deriving show]
 
 and loan_content =
-  | SharedLoan of BorrowId.Set.t * typed_value
+  | SharedLoan of BorrowId.set_t * typed_value
   | MutLoan of BorrowId.id
+[@@deriving show]
 
-and assumed_value = Box of typed_value
+and assumed_value = Box of typed_value [@@deriving show]
 
-and typed_value = { value : value; ty : ety }
+and typed_value = { value : value; ty : ety } [@@deriving show]
 
 type abstract_shared_borrows =
-  | AsbSet of BorrowId.Set.t
+  | AsbSet of BorrowId.set_t
   | AsbProjReborrows of symbolic_value * rty
   | AsbUnion of abstract_shared_borrows * abstract_shared_borrows
       (** TODO: explanations *)
+[@@deriving show]
 
 (** Abstraction values are used inside of abstractions to properly model
     borrowing relations introduced by function calls.
@@ -127,6 +140,7 @@ type avalue =
   | ABorrow of aborrow_content
   | AAssumed of aassumed_value
   | AProj of aproj
+[@@deriving show]
 
 and aadt_value = {
   adef_id : TypeDefId.id;
@@ -135,14 +149,16 @@ and aadt_value = {
   atypes : rty list;
   afield_values : typed_avalue FieldId.vector;
 }
+[@@deriving show]
 
 and aloan_content =
   | AMutLoan of BorrowId.id * typed_avalue
-  | ASharedLoan of BorrowId.Set.t * typed_value * typed_avalue
+  | ASharedLoan of BorrowId.set_t * typed_value * typed_avalue
   | AEndedMutLoan of { given_back : typed_value; child : typed_avalue }
   | AEndedSharedLoan of typed_value * typed_avalue
   | AIgnoredMutLoan of BorrowId.id * typed_avalue
   | AIgnoredSharedLoan of abstract_shared_borrows
+[@@deriving show]
 
 (** Note that when a borrow content is ended, it is replaced by Bottom (while
     we need to track ended loans more precisely, especially because of their
@@ -153,24 +169,27 @@ and aborrow_content =
   | AIgnoredMutBorrow of typed_avalue
   | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
   | AIgnoredSharedBorrow of abstract_shared_borrows
+[@@deriving show]
 
-and aassumed_value = ABox of typed_avalue
+and aassumed_value = ABox of typed_avalue [@@deriving show]
 
 and aproj =
   | AProjLoans of symbolic_value
   | AProjBorrows of symbolic_value * rty
+[@@deriving show]
 
-and typed_avalue = { avalue : avalue; aty : rty }
+and typed_avalue = { avalue : avalue; aty : rty } [@@deriving show]
 
 type abs = {
   abs_id : AbstractionId.id;
-  parents : AbstractionId.Set.t;  (** The parent abstractions *)
-  acc_regions : RegionId.Set.t;
+  parents : AbstractionId.set_t;  (** The parent abstractions *)
+  acc_regions : RegionId.set_t;
       (** Union of the regions owned by the (transitive) parent abstractions and
           by the current abstraction *)
-  regions : RegionId.Set.t;  (** Regions owned by this abstraction *)
+  regions : RegionId.set_t;  (** Regions owned by this abstraction *)
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }
+[@@deriving show]
 (** Abstractions model the parts in the borrow graph where the borrowing relations
     have been abstracted because of a function call.