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 in
  19   let r = compare s1 s2 in
  20   if r != 0 then r else
  21     let r = TagSet.compare l1 l2 in
  22     if r != 0 then r else
  23       let r = compare m1 m2 in
  24       if r != 0 then r else
  25         Formula.compare f1 f2
  26
  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
  31
  32 let print_arrow ppf t =
  33   let _, _, mark, _ = node t in
  34   fprintf ppf "%s%!"
  35     (if mark then Pretty.double_right_arrow else Pretty.right_arrow)
  36
  37 let print_rhs ppf t =
  38   let _, _, _, f = node t in
  39   Formula.print ppf f
  40
  41 let string_of f x =
  42   ignore (flush_str_formatter());
  43   fprintf str_formatter "%a" f x;
  44   flush_str_formatter ()
  45
  46 let print ppf f =
  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
  51 (*
  52   fprintf ppf "%!%a%a%a%!" print_lhs f print_arrow f print_rhs f
  53 *)
  54 let format_list =
  55   let b = Buffer.create 10 in
  56   fun l ->
  57   let make_str f x =
  58     Buffer.clear b;
  59     let fmt = formatter_of_buffer b in
  60     pp_print_flush fmt ();
  61     fprintf fmt "%a" f x;
  62     pp_print_flush fmt ();
  63     Buffer.contents b
  64   in
  65   let str_trans t =
  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
  69     (lhs, arrow, rhs)
  70   in
  71   let size, strings =
  72     List.fold_left
  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
  78   in
  79   List.map (fun (lhs, arrow, rhs) ->
  80     sprintf "%s%s%s %s@?"
  81       lhs
  82       (Pretty.padding (size - Pretty.length lhs))
  83       arrow
  84       rhs) (List.rev strings)
  85
  86 module Infix = struct
  87   let ( ?< ) x = x
  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)))
  91 end