X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fstate.ml;fp=src%2Fstate.ml;h=4b02d596c1430153e58185ca069bc9d820e639d3;hp=4fbfc1cdeabcbda8bfb6175921b87d577ada82b9;hb=4f265eb7d78b740292b5543d94f9f0fa40d206d5;hpb=31d45495fda9a110fd348f8b492761c28b434ec9 diff --git a/src/state.ml b/src/state.ml index 4fbfc1c..4b02d59 100644 --- a/src/state.ml +++ b/src/state.ml @@ -14,23 +14,14 @@ (***********************************************************************) open Format +include Hcons.PosInt -type t = int -let make = +let next = 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