--- /dev/null
+INCLUDE "utils.ml"
+open Format
+
+type node = State.t*TagSet.t*bool*Formula.t
+include Hcons.Make(struct
+ type t = node
+ let hash (s,ts,m,f) = HASHINT4(s,
+ Uid.to_int (TagSet.uid ts),
+ vb m,
+ Uid.to_int (Formula.uid f)
+ )
+ let equal ((s,ts,m,f) as t) ((s',ts',m',f')as t') =
+ t == t' ||
+ (s == s' && ts == ts' && m == m' && f == f')
+ end)
+let compare t1 t2 =
+ let s1, l1, m1, f1 = node t1
+ and s2, l2, m2, f2 = node t2
+ in
+ let r = compare s1 s2 in
+ if r != 0 then r else
+ let r = TagSet.compare l1 l2 in
+ if r != 0 then r else
+ let r = compare m1 m2 in
+ if r != 0 then r else
+ Formula.compare f1 f2
+
+let print_lhs ppf t =
+ let state, tagset , _, _ = node t in
+ fprintf ppf "(%a, %a)"
+ State.print state TagSet.print tagset
+
+let print_arrow ppf t =
+ let _, _, mark, _ = node t in
+ fprintf ppf "%s"
+ (if mark then Pretty.double_right_arrow else Pretty.right_arrow)
+
+let print_rhs ppf t =
+ let _, _, _, f = node t in
+ Formula.print ppf f
+
+let print ppf f =
+ print_lhs ppf f;
+ print_arrow ppf f;
+ print_rhs ppf f
+
+let format_list l =
+ let make_str f x =
+ let b = Buffer.create 10 in
+ let fmt = formatter_of_buffer b in
+ fprintf fmt "@[%a@]@?" f x;
+ Buffer.contents b
+ in
+ let str_trans t =
+ let lhs = make_str print_lhs t
+ and arrow = make_str print_arrow t
+ and rhs = make_str print_rhs t in
+ (lhs, arrow, rhs)
+ in
+ let size, strings =
+ List.fold_left
+ (fun (a_size, a_str) tr ->
+ let lhs, _, _ as str = str_trans tr in
+ let len = String.length lhs in
+ ((if len > a_size then len else a_size),
+ str::a_str)) (0, []) l
+ in
+ List.map (fun (lhs, arrow, rhs) ->
+ sprintf "%s%s%s %s"
+ lhs
+ (Pretty.padding (size - Pretty.length lhs))
+ arrow
+ rhs) (List.rev strings)
+
+module Infix = struct
+ let ( ?< ) x = x
+ let ( >< ) state (l,mark) = state,(l,mark,false)
+ let ( ><@ ) state (l,mark) = state,(l,mark,true)
+ let ( >=> ) (state,(label,mark,_bur)) form = (state,label,(make (state,label,mark,form)))
+end