X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fstate.ml;fp=src%2Fstate.ml;h=bb7a06393cc75e880211b9e01c0b571386ed3483;hp=0000000000000000000000000000000000000000;hb=b00bff88c7902e828804c06b7f9dc55222fdc84e;hpb=03b6a364e7240ca827585e7baff225a0aaa33bc6 diff --git a/src/state.ml b/src/state.ml new file mode 100644 index 0000000..bb7a063 --- /dev/null +++ b/src/state.ml @@ -0,0 +1,40 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + +(* + Time-stamp: +*) + +open Format + +type t = int +let make = + let id = ref ~-1 in + fun () -> incr id; !id + +let compare = (-) + +let equal = (==) + +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