X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=f55452ea0932ed469e10c9354b966f6daa92bcb4;hp=80843e6deae7aafb8860db5a3b8bce7125968ed5;hb=35abea737ead2d4fd121d0cb8bdbda38cfcaa8d3;hpb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615 diff --git a/src/ata.ml b/src/ata.ml index 80843e6..f55452e 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -206,7 +206,10 @@ end = let print ppf ?(sep="\n") l = iter (fun t -> let q, lab, f = Transition.node t in - fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab Formula.print f sep) l + fprintf ppf "%a, %a → %a%s" + State.print q + QNameSet.print lab + Formula.print f sep) l end @@ -258,18 +261,19 @@ let print fmt a = [] in let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) -> - let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c)) + let c = State.compare q2 q1 in if c == 0 then QNameSet.compare s2 s1 else c) trs in let _ = _flush_str_fmt () in - let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> - let s1 = State.print _str_fmt q; _flush_str_fmt () in - let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in - let s3 = Formula.print _str_fmt f; _flush_str_fmt () in - let pre = Pretty.length s1 + Pretty.length s2 in - let all = Pretty.length s3 in - ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) - ) ([], 0, 0) sorted_trs + let strs_strings, max_pre, max_all = + List.fold_left (fun (accl, accp, acca) (q, s, f) -> + let s1 = State.print _str_fmt q; _flush_str_fmt () in + let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in + let s3 = Formula.print _str_fmt f; _flush_str_fmt () in + let pre = Pretty.length s1 + Pretty.length s2 in + let all = Pretty.length s3 in + ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) + ) ([], 0, 0) sorted_trs in let line = Pretty.line (max_all + max_pre + 6) in let prev_q = ref State.dummy in @@ -278,7 +282,8 @@ let print fmt a = if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line; prev_q := q; fprintf fmt "%s, %s" s1 s2; - fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); + fprintf fmt "%s" + (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); fprintf fmt " %s %s@\n" Pretty.right_arrow s3; ) strs_strings; fprintf fmt "%s@\n" line @@ -357,8 +362,10 @@ let normalize_negations auto = let rec flip b f = match Formula.expr f with Boolean.True | Boolean.False -> if b then f else Formula.not_ f - | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2) - | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2) + | Boolean.Or(f1, f2) -> + (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2) + | Boolean.And(f1, f2) -> + (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2) | Boolean.Atom(a, b') -> begin match a.Atom.node with | Move (m, q) ->