4 type node = State.t*TagSet.t*bool*Formula.t
5 include Hcons.Make(struct
7 let hash (s,ts,m,f) = HASHINT4(s,
8 Uid.to_int (TagSet.uid ts),
10 Uid.to_int (Formula.uid f)
12 let equal ((s,ts,m,f) as t) ((s',ts',m',f')as t') =
14 (s == s' && ts == ts' && m == m' && f == f')
17 let s1, l1, m1, f1 = node t1
18 and s2, l2, m2, f2 = node t2 in
19 let r = compare s1 s2 in
21 let r = TagSet.compare l1 l2 in
23 let r = compare m1 m2 in
27 let print_lhs (ppf: Format.formatter) (t : t) : unit =
28 let state, tagset , _, _ = node t in
29 fprintf ppf "(%a, %a)%!"
30 State.print state TagSet.print tagset
32 let print_arrow ppf t =
33 let _, _, mark, _ = node t in
35 (if mark then Pretty.double_right_arrow else Pretty.right_arrow)
38 let _, _, _, f = node t in
42 ignore (flush_str_formatter());
43 fprintf str_formatter "%a" f x;
44 flush_str_formatter ()
47 let s1 = string_of print_lhs f in
48 let s2 = string_of print_arrow f in
49 let s3 = string_of print_rhs f in
50 fprintf ppf "%s %s %s%!" s1 s2 s3
52 fprintf ppf "%!%a%a%a%!" print_lhs f print_arrow f print_rhs f
55 let b = Buffer.create 10 in
59 let fmt = formatter_of_buffer b in
60 pp_print_flush fmt ();
62 pp_print_flush fmt ();
66 let lhs = make_str print_lhs t in
67 let arrow = make_str print_arrow t in
68 let rhs = make_str print_rhs t in
73 (fun (a_size, a_str) tr ->
74 let lhs, _, _ as str = str_trans tr in
75 let len = String.length lhs in
76 ((if len > a_size then len else a_size),
77 str::a_str)) (0, []) l
79 List.map (fun (lhs, arrow, rhs) ->
82 (Pretty.padding (size - Pretty.length lhs))
84 rhs) (List.rev strings)
88 let ( >< ) state (l,mark) = state,(l,mark,false)
89 let ( ><@ ) state (l,mark) = state,(l,mark,true)
90 let ( >=> ) (state,(label,mark,_bur)) form = (state,label,(make (state,label,mark,form)))