src/transition.ml

   1 INCLUDE "utils.ml"
   2 open Format
   3
   4 type node = State.t*TagSet.t*bool*Formula.t
   5 include Hcons.Make(struct
   6                      type t = node
   7                      let hash (s,ts,m,f) = HASHINT4(s,
   8                                                     Uid.to_int (TagSet.uid ts),
   9                                                     vb m,
  10                                                     Uid.to_int (Formula.uid f)
  11                                                    )
  12                      let equal ((s,ts,m,f) as t) ((s',ts',m',f')as t') =
  13                        t == t' ||
  14                          (s == s' && ts == ts' && m == m' && f == f')
  15                    end)
  16 let compare t1 t2 =
  17   let s1, l1, m1, f1 = node t1
  18   and s2, l2, m2, f2 = node t2
  19   in
  20   let r = compare s1 s2 in
  21     if r != 0 then r else
  22       let r = TagSet.compare l1 l2 in
  23         if r != 0 then r else
  24           let r = compare m1 m2 in
  25             if r != 0 then r else
  26               Formula.compare f1 f2
  27
  28 let print_lhs ppf t =
  29   let state, tagset , _, _ = node t in
  30     fprintf ppf "(%a, %a)"
  31       State.print state TagSet.print tagset
  32
  33 let print_arrow ppf t =
  34   let _, _, mark, _ = node t in
  35     fprintf ppf "%s"
  36       (if mark then Pretty.double_right_arrow else Pretty.right_arrow)
  37
  38 let print_rhs ppf t =
  39   let _, _, _, f = node t in
  40     Formula.print ppf f
  41
  42 let print ppf f =
  43   print_lhs ppf f;
  44   print_arrow ppf f;
  45   print_rhs ppf f
  46
  47 let format_list l =
  48   let make_str f x =
  49     let b = Buffer.create 10 in
  50     let fmt = formatter_of_buffer b in
  51     pp_print_flush fmt ();
  52     fprintf fmt "%a" f x;
  53     pp_print_flush fmt ();
  54     Buffer.contents b
  55   in
  56   let str_trans t =
  57     let lhs = make_str print_lhs t
  58     and arrow = make_str print_arrow t
  59     and rhs = make_str print_rhs t in
  60       (lhs, arrow, rhs)
  61   in
  62   let size, strings =
  63     List.fold_left
  64       (fun (a_size, a_str) tr ->
  65          let lhs, _, _ as str = str_trans tr in
  66          let len = String.length lhs in
  67            ((if len > a_size then len else a_size),
  68             str::a_str)) (0, []) l
  69   in
  70     List.map (fun (lhs, arrow, rhs) ->
  71                 sprintf "%s%s%s %s"
  72                   lhs
  73                   (Pretty.padding (size - Pretty.length lhs))
  74                   arrow
  75                   rhs) (List.rev strings)
  76
  77 module Infix = struct
  78   let ( ?< ) x = x
  79   let ( >< ) state (l,mark) = state,(l,mark,false)
  80   let ( ><@ ) state (l,mark) = state,(l,mark,true)
  81   let ( >=> ) (state,(label,mark,_bur)) form = (state,label,(make (state,label,mark,form)))
  82 end