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: Format.formatter) (t : t) : unit =
  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 string_of f x =
  ignore (flush_str_formatter());
  fprintf str_formatter "%a" f x;
  flush_str_formatter ()

let print ppf f =
  let s1 = string_of print_lhs f in
  let s2 = string_of print_arrow f in
  let s3 = string_of print_rhs f in
  fprintf ppf "%s %s %s%!" s1 s2 s3
(*
  fprintf ppf "%!%a%a%a%!" print_lhs f print_arrow f print_rhs f
*)
let format_list =
  let b = Buffer.create 10 in
  fun l ->
  let make_str f x =
    Buffer.clear b;
    let fmt = formatter_of_buffer b in
    pp_print_flush fmt ();
    fprintf fmt "%a" f x;
    pp_print_flush fmt ();
    Buffer.contents b
  in
  let str_trans t =
    let lhs = make_str print_lhs t in
    let arrow = make_str print_arrow t in
    let 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