projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
* Seal the representation of states
[tatoo.git]
/
src
/
state.ml
diff --git
a/src/state.ml
b/src/state.ml
index
4fbfc1c
..
4b02d59
100644
(file)
--- a/
src/state.ml
+++ b/
src/state.ml
@@
-14,23
+14,14
@@
(***********************************************************************)
open Format
(***********************************************************************)
open Format
+include Hcons.PosInt
-type t = int
-let make =
+let next =
let id = ref ~-1 in
let id = ref ~-1 in
- fun () -> incr id; !id
+ fun () -> incr id;
make
!id
-let compare
= (-
)
+let compare
(a : t) (b : t) = (a :> int) - (b :> int
)
-let
equal = (==
)
+let
print fmt (x : t) = fprintf fmt "q%a" Pretty.pp_subscript (x :> int
)
-external hash : t -> int = "%identity"
-
-let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x
-
-let dump fmt x = print fmt x
-
-let check x =
- if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x)
-
-let dummy = max_int
+let dummy_state = make max_int