summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-18 18:10:42 +0100
committerSon Ho2022-01-18 18:10:42 +0100
commite21464bd6fbfd26bc8453995d180a519a10ba867 (patch)
tree5cae70fd34f6c4bf48ba6a76a6ec932aea194ac6
parentbb158d611c9138fe0c49d669807dff84dc5fba21 (diff)
Derive ord for the types
-rw-r--r--TODO.md4
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Types.ml21
3 files changed, 17 insertions, 12 deletions
diff --git a/TODO.md b/TODO.md
index 862f863c..b7f03ee3 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,10 +2,10 @@
0. derive [ord] for types
-0. compute the region constraints for the type definitions
-
1. stateful maps/sets modules (hashtbl?)
+0. compute the region constraints for the type definitions
+
2. set of types with mutable borrows (what to do when type variables appear under
shared borrows?), nested borrows...
necessary to know what to return.
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index fd07b7b6..f2b88fd4 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -33,6 +33,8 @@ module type Id = sig
val id_of_json : Yojson.Basic.t -> (id, string) result
+ val compare_id : id -> id -> int
+
val pp_generator : Format.formatter -> generator -> unit
val show_generator : generator -> string
@@ -109,6 +111,8 @@ module IdGen () : Id = struct
| `Int i -> Ok i
| _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
+ let compare_id = compare
+
let nth v id = List.nth v id
let nth_opt v id = List.nth_opt v id
diff --git a/src/Types.ml b/src/Types.ml
index 44855eb2..286b8163 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -40,13 +40,13 @@ type region_var = (RegionVarId.id, string option) indexed_var [@@deriving show]
type 'rid region =
| Static (** Static region *)
| Var of 'rid (** Non-static region *)
-[@@deriving show]
+[@@deriving show, ord]
(** The type of erased regions.
We could use unit, but having a dedicated type makes things more explicit.
*)
-type erased_region = Erased [@@deriving show]
+type erased_region = Erased [@@deriving show, ord]
type ('id, 'r) g_region_group = {
id : 'id;
@@ -83,11 +83,11 @@ type integer_type =
| U32
| U64
| U128
-[@@deriving show]
+[@@deriving show, ord]
-type ref_kind = Mut | Shared [@@deriving show]
+type ref_kind = Mut | Shared [@@deriving show, ord]
-type assumed_ty = Box [@@deriving show]
+type assumed_ty = Box [@@deriving show, ord]
(** Type identifier for ADTs.
@@ -95,7 +95,7 @@ type assumed_ty = Box [@@deriving show]
tuples and also assumed types.
*)
type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty
-[@@deriving show]
+[@@deriving show, ord]
(** Ancestor for iter visitor for [ty] *)
class ['self] iter_ty_base =
@@ -144,6 +144,7 @@ type 'r ty =
| Ref of 'r * 'r ty * ref_kind
[@@deriving
show,
+ ord,
visitors
{
name = "iter_ty";
@@ -164,22 +165,22 @@ type 'r ty =
}]
(* TODO: group Bool, Char, etc. in Constant *)
-type 'r gr_ty = 'r region ty [@@deriving show]
+type 'r gr_ty = 'r region ty [@@deriving show, ord]
(** Generic type with regions *)
-type sty = RegionVarId.id gr_ty [@@deriving show]
+type sty = RegionVarId.id gr_ty [@@deriving show, ord]
(** *S*ignature types.
Used in function signatures and type definitions.
*)
-type rty = RegionId.id gr_ty [@@deriving show]
+type rty = RegionId.id gr_ty [@@deriving show, ord]
(** Type with *R*egions.
Used during symbolic execution.
*)
-type ety = erased_region ty [@@deriving show]
+type ety = erased_region ty [@@deriving show, ord]
(** Type with *E*rased regions.
Used in function bodies, "general" value types, etc.