Cosmetic changes (truncate long lines, remove trailing spaces…)

diff --git a/include/debug.ml b/include/debug.ml
index 5a51787..1fd4f8b 100644 (file)
--- a/include/debug.ml
+++ b/include/debug.ml
@@ -4,9 +4,11 @@ DEFINE DEBUG__ML__
 
 IFDEF DEBUG
 THEN
 
 IFDEF DEBUG
 THEN

-  DEFINE DBG(e) = (e)
+  let msg x = Logger.msg `DEBUG x
+  DEFINE DEBUG(e) = (e)

 ELSE
 ELSE

-  DEFINE DBG(e) = ()
+  let msg x = ()
+  DEFINE DEBUG(e) = ()

 END
 
 
 END
 
 

diff --git a/src/ata.ml b/src/ata.ml
index 80843e6..f55452e 100644 (file)
--- 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
     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
 
 
   end
 
 


@@ -258,18 +261,19 @@ let print fmt a =
       []
   in
   let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
       []
   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
     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
   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;
     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
     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
   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) ->
     | Boolean.Atom(a, b') -> begin
       match a.Atom.node with
       | Move (m,  q) ->

diff --git a/src/ata.mli b/src/ata.mli
index 2aa27b3..e1fdc4a 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -39,19 +39,24 @@ module Move :
 (** Type of moves an automaton can perform *)
 
 type predicate =
 (** Type of moves an automaton can perform *)
 
 type predicate =

-    Move of move * State.t  (** In the [move] direction, the automaton must be in the given state *)
-  | Is_first_child          (** True iff the node is the first child of its parent *)
-  | Is_next_sibling         (** True iff the node is the next sibling of its parent *)
+    Move of move * State.t  (** In the [move] direction,
+                                the automaton must be in the given state *)
+  | Is_first_child          (** True iff
+                                the node is the first child of its parent *)
+  | Is_next_sibling         (** True iff
+                                the node is the next sibling of its parent *)

   | Is of Tree.NodeKind.t   (** True iff the node is of the given kind *)
   | Has_first_child         (** True iff the node has a first child *)
   | Has_next_sibling        (** True iff the node has a next sibling *)
   | Is of Tree.NodeKind.t   (** True iff the node is of the given kind *)
   | Has_first_child         (** True iff the node has a first child *)
   | Has_next_sibling        (** True iff the node has a next sibling *)

-(** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
+(** Type of the predicates that can occur in the Boolean formulae that
+    are in the transitions of the automaton *)

 
 module Atom : sig
   include Hcons.S with type data = predicate
   include Common_sig.Printable with type t := t
 end
 
 module Atom : sig
   include Hcons.S with type data = predicate
   include Common_sig.Printable with type t := t
 end

-(** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
+(** Module representing atoms of Boolean formulae, which are simply
+    hashconsed [predicate]s *)

 
 module Formula :
   sig
 
 module Formula :
   sig


@@ -61,25 +66,28 @@ module Formula :
     val parent : State.t -> t
     val previous_sibling : State.t -> t
     val stay : State.t -> t
     val parent : State.t -> t
     val previous_sibling : State.t -> t
     val stay : State.t -> t

-      (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
-          of the corresponding [move] atom. *)
+    (** [first_child], [next_sibling], [parent], [previous_sibling],
+        [stay] create a formula which consists only of the
+        corresponding [move] atom. *)

     val is_first_child : t
     val is_next_sibling : t
     val has_first_child : t
     val has_next_sibling : t
     val is_first_child : t
     val is_next_sibling : t
     val has_first_child : t
     val has_next_sibling : t

-      (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
-          only of the corresponding atom
-      *)
+    (** [is_first_child], [is_next_sibling], [has_first_child],
+        [has_next_sibling] are constant formulae which consist only
+        of the corresponding atom *)

     val is : Tree.NodeKind.t -> t
       (** [is k] creates a formula that tests the kind of the current node *)
     val is_attribute : t
     val is_element : t
     val is_processing_instruction : t
     val is_comment : t
     val is : Tree.NodeKind.t -> t
       (** [is k] creates a formula that tests the kind of the current node *)
     val is_attribute : t
     val is_element : t
     val is_processing_instruction : t
     val is_comment : t

-      (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
-          particular kind *)
+    (** [is_attribute], [is_element], [is_processing_instruction],
+        [is_comment] are constant formulae that tests a particular
+        kind *)

     val get_states : t -> StateSet.t
     val get_states : t -> StateSet.t

-      (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
+    (** [get_state f] retrieves all the states occuring in [move]
+        predicates in [f] *)

     val get_states_by_move : t -> StateSet.t Move.table
   end
 (** Modules representing the Boolean formulae used in transitions *)
     val get_states_by_move : t -> StateSet.t Move.table
   end
 (** Modules representing the Boolean formulae used in transitions *)


@@ -88,7 +96,8 @@ module Transition : sig
   include Hcons.S with type data = State.t * QNameSet.t * Formula.t
   val print : Format.formatter -> t -> unit
 end
   include Hcons.S with type data = State.t * QNameSet.t * Formula.t
   val print : Format.formatter -> t -> unit
 end

-(** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
+(** A [Transition.t] is a hashconsed triple of the state, the set of
+    labels and the formula *)

 
 
 module TransList : sig
 
 
 module TransList : sig


@@ -192,9 +201,9 @@ sig
     (** Add a transition to the automaton *)
 
   val finalize : t  -> auto
     (** Add a transition to the automaton *)
 
   val finalize : t  -> auto

-    (** Finalize the automaton and return it. Clean-up unused states (states that
-        do not occur in any transitions and remove instantes of negative [move] atoms
-        by creating fresh states that accept the complement of the negated state.
-    *)
+(** Finalize the automaton and return it. Clean-up unused states
+    (states that do not occur in any transitions and remove
+    instantes of negative [move] atoms by creating fresh states
+    that accept the complement of the negated state.  *)

 end
   (** Builder facility for the automaton *)
 end
   (** Builder facility for the automaton *)

diff --git a/src/boolean.ml b/src/boolean.ml
index 09b62b6..882f30f 100644 (file)
--- a/src/boolean.ml
+++ b/src/boolean.ml
@@ -96,10 +96,11 @@ struct
           fprintf ppf " %s "  Pretty.wedge;
           print ~parent:(prio f > prio f2) ppf f2;
       | Or(f1,f2) ->
           fprintf ppf " %s "  Pretty.wedge;
           print ~parent:(prio f > prio f2) ppf f2;
       | Or(f1,f2) ->

-          (print ppf f1);
+          print ppf f1;

           fprintf ppf " %s " Pretty.vee;
           fprintf ppf " %s " Pretty.vee;

-          (print ppf f2);
-      | Atom(p,b) -> fprintf ppf "%s%a" (if b then "" else Pretty.lnot) A.print p
+          print ppf f2
+      | Atom(p,b) ->
+        fprintf ppf "%s%a" (if b then "" else Pretty.lnot) A.print p

   in
     if parent then fprintf ppf ")"
 
   in
     if parent then fprintf ppf ")"
 


@@ -111,9 +112,9 @@ let is_false f = (expr f) == False
 let cons pos neg =
   let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
   let pnode = Node.make { pos = pos; neg = nnode } in
 let cons pos neg =
   let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
   let pnode = Node.make { pos = pos; neg = nnode } in

-    (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
-                                       account for hashing ! *)
-    pnode,nnode
+  (Node.node nnode).neg <- pnode; (* works because the neg field isn't
+                                    taken into account for hashing ! *)
+  pnode, nnode

 
 
 let true_,false_ = cons True False
 
 
 let true_,false_ = cons True False

diff --git a/src/cache.mli b/src/cache.mli
index 6ebfded..e5f837c 100644 (file)
--- a/src/cache.mli
+++ b/src/cache.mli
@@ -67,7 +67,8 @@ module N5 :
     val find : 'a t -> int -> int -> int -> int -> int -> 'a
     val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit
     val dummy : 'a t -> 'a
     val find : 'a t -> int -> int -> int -> int -> int -> 'a
     val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit
     val dummy : 'a t -> 'a

-    val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+    val iteri :
+      (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit

     val stats : 'a t -> int*int
   end
 
     val stats : 'a t -> int*int
   end
 


@@ -78,6 +79,8 @@ module N6 :
     val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a
     val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit
     val dummy : 'a t -> 'a
     val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a
     val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit
     val dummy : 'a t -> 'a

-    val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+    val iteri :
+      (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit)
+      -> 'a t -> unit

     val stats : 'a t -> int*int
   end
     val stats : 'a t -> int*int
   end

diff --git a/src/hlist.ml b/src/hlist.ml
index 3ffb8fc..f3dd254 100644 (file)
--- a/src/hlist.ml
+++ b/src/hlist.ml
@@ -11,7 +11,9 @@ struct
   type elt = H.t
 
   module rec Node : Hcons.S with type data = Data.t = HCB(Data)
   type elt = H.t
 
   module rec Node : Hcons.S with type data = Data.t = HCB(Data)

-                            and Data : Common_sig.HashedType with type t = (elt, Node.t) node =
+                            and Data : Common_sig.HashedType
+                                       with type t = (elt, Node.t) node
+    =

   struct
     type t = (elt, Node.t) node
     let equal x y =
   struct
     type t = (elt, Node.t) node
     let equal x y =


@@ -22,7 +24,8 @@ struct
 
     let hash = function
     | Nil -> 0
 
     let hash = function
     | Nil -> 0

-    | Cons(e, l) -> HASHINT3 (PRIME1, Uid.to_int (H.uid e), Uid.to_int (Node.uid l))
+    | Cons(e, l) ->
+      HASHINT3 (PRIME1, Uid.to_int (H.uid e), Uid.to_int (Node.uid l))

   end
 
   include Node
   end
 
   include Node


@@ -79,4 +82,3 @@ end
 
 module Make = Builder(Hcons.Make)
 module Weak = Builder(Hcons.Weak)
 
 module Make = Builder(Hcons.Make)
 module Weak = Builder(Hcons.Weak)

-

diff --git a/src/html.ml b/src/html.ml
index 21b33e6..b35f17d 100644 (file)
--- a/src/html.ml
+++ b/src/html.ml
@@ -37,7 +37,7 @@ let finalize_node n r b =
 module K =
 struct
   type t = int * StateSet.t * StateSet.t
 module K =
 struct
   type t = int * StateSet.t * StateSet.t

-  let hash (a,b,c) = HASHINT3(a, (b.StateSet.id :> int), (c.StateSet.id :> int) )
+  let hash (a,b,c) = HASHINT3(a, (b.StateSet.id :> int), (c.StateSet.id :> int))

   let equal ((a1,b1,c1) as x) ((a2,b2,c2) as y) =
     x == y || (a1 == a2 && b1 == b2 && c1 == c2)
 end
   let equal ((a1,b1,c1) as x) ((a2,b2,c2) as y) =
     x == y || (a1 == a2 && b1 == b2 && c1 == c2)
 end


@@ -92,14 +92,28 @@ let gen_trace (type s) = fun auto t tree ->
           | [ e ] -> e
           | l -> List.hd (List.tl (List.rev l))
         in
           | [ e ] -> e
           | l -> List.hd (List.tl (List.rev l))
         in

-        let c = (last_round, StateSet.union sat todo, StateSet.empty) in color c, text_color c
+        let c = (last_round, StateSet.union sat todo, StateSet.empty) in
+        color c, text_color c

       in
       let tag = QName.to_string (T.tag tree node) in
       let lbox = (String.length tag + 2) * 10 in
       let s_node = "node" ^ (string_of_int node_id) in
       in
       let tag = QName.to_string (T.tag tree node) in
       let lbox = (String.length tag + 2) * 10 in
       let s_node = "node" ^ (string_of_int node_id) in

-      fprintf osvg "<rect id=\"%s\" onclick=\"activate(\'%s\');\" x=\"%i\" y=\"%i\" width=\"%i\" height=\"20\" style=\"fill:%s;stroke:rgb(0,0,0)%s\"/>\n%!"
-        s_node s_node x y lbox scolor (if marked then ";stroke-width:4" else ";stroke-width:2;stroke-dasharray:2,2");
-      fprintf osvg "<text x=\"%i\" y=\"%i\" style=\"fill:%s;font-size:17;font-family:typewriter;\" onclick=\"activate(\'%s\');\" >%s</text>\n" (x+10) (y+15) tcolor s_node tag;
+      fprintf osvg
+        "<rect id=\"%s\" onclick=\"activate(\'%s\');\" x=\"%i\" y=\"%i\"\
+ width=\"%i\" height=\"20\" style=\"fill:%s;stroke:rgb(0,0,0)%s\"/>\n%!"
+        s_node
+        s_node
+        x y
+        lbox
+        scolor
+        (if marked
+         then ";stroke-width:4"
+         else ";stroke-width:2;stroke-dasharray:2,2");
+      fprintf osvg "<text x=\"%i\" y=\"%i\" style=\"fill:%s;font-size:17;\
+font-family:typewriter;\" onclick=\"activate(\'%s\');\" >%s</text>\n"
+        (x+10)
+        (y+15)
+        tcolor s_node tag;

       fprintf ohtml "data['%s'] = new Array();\n" s_node;
       M.iter
         (fun i l ->
       fprintf ohtml "data['%s'] = new Array();\n" s_node;
       M.iter
         (fun i l ->


@@ -112,10 +126,12 @@ let gen_trace (type s) = fun auto t tree ->
       let x_next = max (x+lbox) (maxw1+10) in
       if node != root then begin
         if node == T.first_child tree parent then
       let x_next = max (x+lbox) (maxw1+10) in
       if node != root then begin
         if node == T.first_child tree parent then

-          fprintf osvg  "<line x1=\"%i\" y1=\"%i\" x2=\"%i\" y2=\"%i\" style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"
+          fprintf osvg  "<line x1=\"%i\" y1=\"%i\" x2=\"%i\" y2=\"%i\"\
+style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"

             (x + lbox / 2) (y-20) (x + lbox / 2) (y);
         if next != T.nil then
             (x + lbox / 2) (y-20) (x + lbox / 2) (y);
         if next != T.nil then

-          fprintf osvg "<line x1=\"%i\" y1=\"%i\" x2=\"%i\" y2=\"%i\" style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"
+          fprintf osvg "<line x1=\"%i\" y1=\"%i\" x2=\"%i\" y2=\"%i\"\
+style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"

             (x + lbox) (y+10) x_next (y+10);
       end;
       let maxw2, maxy2 = loop osvg ohtml next node x_next y in
             (x + lbox) (y+10) x_next (y+10);
       end;
       let maxw2, maxy2 = loop osvg ohtml next node x_next y in


@@ -150,7 +166,8 @@ Ata.print auto;
   d.innerHTML = msg;
   return;
   };\n";
   d.innerHTML = msg;
   return;
   };\n";

-  fprintf ohtml "</script>\n<div id='svg'><svg width=\"%i\" height=\"%i\" xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n"
+  fprintf ohtml "</script>\n<div id='svg'><svg width=\"%i\"\
+height=\"%i\" xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n"

     maxw maxh;
   let fi = open_in "tests/trace/trace.svg" in
   try
     maxw maxh;
   let fi = open_in "tests/trace/trace.svg" in
   try

diff --git a/src/html.mli b/src/html.mli
index 48551f7..a6cd212 100644 (file)
--- a/src/html.mli
+++ b/src/html.mli
@@ -1,5 +1,6 @@
 val trace : ?msg:string -> int -> int -> StateSet.t -> StateSet.t  -> unit
 val trace : ?msg:string -> int -> int -> StateSet.t -> StateSet.t  -> unit

-(** [trace nid round d t msg] records a the message [msg] together with the a node preorder
-    [nid], the [round], the [d]one set and the [t]odo set *)
+(** [trace nid round d t msg] records the message [msg] together
+    with the a node preorder [nid], the [round], the [d]one set and
+    the [t]odo set *)

 val finalize_node : int -> int -> bool -> unit
 val gen_trace : Ata.t -> (module Tree.S with type t = 'a) -> 'a -> unit
 val finalize_node : int -> int -> bool -> unit
 val gen_trace : Ata.t -> (module Tree.S with type t = 'a) -> 'a -> unit

diff --git a/src/naive_tree.ml b/src/naive_tree.ml
index 33c953d..38421e0 100644 (file)
--- a/src/naive_tree.ml
+++ b/src/naive_tree.ml
@@ -72,7 +72,9 @@ struct
           "NODE " ^  string_of_int n.preorder)
 
   let debug_node fmt node =
           "NODE " ^  string_of_int n.preorder)
 
   let debug_node fmt node =

-    Format.fprintf fmt "{ tag=%s; preorder=%i; data=%S; first_child=%a; next_sibling=%a; parent=%a }"
+    Format.fprintf fmt
+      "{ tag=%s; preorder=%i; data=%S;\
+first_child=%a; next_sibling=%a; parent=%a }"

       (QName.to_string node.tag)
       node.preorder
       node.data
       (QName.to_string node.tag)
       node.preorder
       node.data


@@ -82,7 +84,8 @@ struct
 
 
   let debug_ctx fmt ctx =
 
 
   let debug_ctx fmt ctx =

-    Format.fprintf fmt "Current context: { preorder = %i\n; stack = \n%a\n }\n-------------\n"
+    Format.fprintf fmt "Current context: { preorder = %i\n; stack = \n%a\n }\
+\n-------------\n"

       ctx.current_preorder
       (Pretty.print_list ~sep:";\n" debug_node) ctx.stack
 
       ctx.current_preorder
       (Pretty.print_list ~sep:";\n" debug_node) ctx.stack
 

diff --git a/src/options.ml b/src/options.ml
index 3c2239a..b8c5730 100644 (file)
--- a/src/options.ml
+++ b/src/options.ml
@@ -11,22 +11,30 @@ let parallel = ref false
 let set_string_option r s = r := Some s
 
 let specs = align [
 let set_string_option r s = r := Some s
 
 let specs = align [

-  "-c", Set count, " write the number of results only";
+  "-c", Set count,
+        " write the number of results only";

   "--count", Set count, " ";
   "--count", Set count, " ";

-  "-s", Set stats, " display timing and various statistics";
+  "-s", Set stats,
+        " display timing and various statistics";

   "--stats", Set stats, " ";
   "--stats", Set stats, " ";

-  "-d", String (set_string_option input_file), " specify the input document file [default stdin]";
+  "-d", String (set_string_option input_file),
+        " specify the input document file [default stdin]";

   "--doc", String (set_string_option input_file), " ";
   "--doc", String (set_string_option input_file), " ";

-  "-o", String (set_string_option output_file), " specify the output file [default stdout]";
+  "-o", String (set_string_option output_file),
+        " specify the output file [default stdout]";

   "--out", String (set_string_option output_file), " ";
   "--out", String (set_string_option output_file), " ";

-  "-C", Set compose, " compose queries: each query is applied to the results of the previous one [default run all queries
-from the root node]";
+  "-C", Set compose,
+        " compose queries: each query is applied to the results of the \
+previous one [default run all queries from the root node]";

   "--compose", Set compose, " ";
   "--compose", Set compose, " ";

-  "-p", Set parallel, " run all queries in parallel [default run all queries sequentially]";
+  "-p", Set parallel,
+        " run all queries in parallel [default run all queries \
+sequentially]";

   "--parallel", Set parallel, " ";
 ]
 
   "--parallel", Set parallel, " ";
 ]
 

-let usage_msg = Printf.sprintf "usage: %s [options] query [query ... query]" Sys.argv.(0)
+let usage_msg =
+  Printf.sprintf "usage: %s [options] query [query ... query]" Sys.argv.(0)

 
 let usage () = usage specs usage_msg
 
 
 let usage () = usage specs usage_msg
 


@@ -35,4 +43,3 @@ let parse () =
   match !queries with
     [] -> raise (Arg.Bad "missing query")
   | l -> queries := List.rev l
   match !queries with
     [] -> raise (Arg.Bad "missing query")
   | l -> queries := List.rev l

-

diff --git a/src/pretty.mli b/src/pretty.mli
index 96fb773..36fd430 100644 (file)
--- a/src/pretty.mli
+++ b/src/pretty.mli
@@ -47,8 +47,12 @@ val pp_subscript : Format.formatter -> int -> unit
 val pp_superscript : Format.formatter -> int -> unit
 
 val pp_print_list :
 val pp_superscript : Format.formatter -> int -> unit
 
 val pp_print_list :

-  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit)
+  -> Format.formatter -> 'a list -> unit

 val pp_print_array :
 val pp_print_array :

-  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
-val print_list : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-val print_array : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
+  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit)
+  -> Format.formatter -> 'a array -> unit
+val print_list : ?sep:string -> (Format.formatter -> 'a -> unit)
+  -> Format.formatter -> 'a list -> unit
+val print_array : ?sep:string -> (Format.formatter -> 'a -> unit)
+  -> Format.formatter -> 'a array -> unit

diff --git a/src/ptset.ml b/src/ptset.ml
index 08332b3..779d24f 100644 (file)
--- a/src/ptset.ml
+++ b/src/ptset.ml
@@ -38,7 +38,9 @@ struct
     | Branch of int * int * 'a * 'a
 
   module rec Node : Hcons.S with type data = Data.t = HCB(Data)
     | Branch of int * int * 'a * 'a
 
   module rec Node : Hcons.S with type data = Data.t = HCB(Data)

-                            and Data : Common_sig.HashedType with type t = Node.t set =
+                            and Data : Common_sig.HashedType
+                                with type t = Node.t set
+    =

   struct
     type t =  Node.t set
     let equal x y =
   struct
     type t =  Node.t set
     let equal x y =


@@ -67,13 +69,12 @@ struct
 
   let leaf k = Node.make (Leaf k)
 
 
   let leaf k = Node.make (Leaf k)
 

-                            (* To enforce the invariant that a branch contains two non empty
-                               sub-trees *)
+  (* To enforce the invariant that a branch contains two non empty sub-trees *)

   let branch_ne p m t0 t1 =
     if (is_empty t0) then t1
     else if is_empty t1 then t0 else branch p m t0 t1
 
   let branch_ne p m t0 t1 =
     if (is_empty t0) then t1
     else if is_empty t1 then t0 else branch p m t0 t1
 

-                            (******** from here on, only use the smart constructors ************)
+  (******** from here on, only use the smart constructors ************)

 
   let singleton k = leaf k
 
 
   let singleton k = leaf k
 


@@ -149,7 +150,7 @@ struct
     let kid = Uid.to_int (H.uid k) in
     let rec ins n = match n.Node.node with
     | Empty -> leaf k
     let kid = Uid.to_int (H.uid k) in
     let rec ins n = match n.Node.node with
     | Empty -> leaf k

-    | Leaf j ->  if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
+    | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n

     | Branch (p,m,t0,t1)  ->
         if match_prefix kid p m then
           if zero_bit kid m then
     | Branch (p,m,t0,t1)  ->
         if match_prefix kid p m then
           if zero_bit kid m then


@@ -177,7 +178,7 @@ struct
     in
     rmv t
 
     in
     rmv t
 

-  (* should run in O(1) thanks to hash consing *)
+  (* runs in O(1) thanks to hash consing *)

 
   let equal a b = a == b
 
 
   let equal a b = a == b
 


@@ -231,7 +232,7 @@ struct
 
 
   let union s1 s2 = merge s1 s2
 
 
   let union s1 s2 = merge s1 s2

-                            (* Todo replace with e Memo Module *)
+  (* Todo replace with e Memo Module *)

 
   let rec inter s1 s2 =
     if equal s1 s2
 
   let rec inter s1 s2 =
     if equal s1 s2

diff --git a/src/qNameSet.ml b/src/qNameSet.ml
index 91309e0..95228bd 100644 (file)
--- a/src/qNameSet.ml
+++ b/src/qNameSet.ml
@@ -24,7 +24,10 @@ let printer fmt e test conv inv is_any =
   if test e then print_finite fmt e conv
   else
     let () = Format.fprintf fmt "%s" Pretty.big_sigma in
   if test e then print_finite fmt e conv
   else
     let () = Format.fprintf fmt "%s" Pretty.big_sigma in

-    if not (is_any e) then begin Format.fprintf fmt "-";print_finite fmt (inv e) conv end
+    if not (is_any e) then begin
+      Format.fprintf fmt "-";
+      print_finite fmt (inv e) conv
+    end

 
 let print fmt e = printer fmt e is_finite elements complement is_any
 
 
 let print fmt e = printer fmt e is_finite elements complement is_any
 

diff --git a/src/run.ml b/src/run.ml
index 2dd5ad5..b51daf9 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -14,6 +14,8 @@
 (***********************************************************************)
 
 INCLUDE "utils.ml"
 (***********************************************************************)
 
 INCLUDE "utils.ml"

+INCLUDE "debug.ml"
+

 open Format
 open Misc
 
 open Format
 open Misc
 


@@ -289,23 +291,12 @@ DEFINE AND_(t1,t2) =
          in
 
          let v = eval_form phi fcs nss ps old_status old_summary in
          in
 
          let v = eval_form phi fcs nss ps old_status old_summary in

-(*
-         Logger.msg `STATS "Evaluating for tag %a, state %a@\ncontext: %a@\nleft: %a@\nright: %a@\n\t formula %a yields %s"
-           QName.print tag
-           State.print q
-           NodeStatus.print old_status
-           NodeStatus.print fcs
-           NodeStatus.print nss
-           Ata.Formula.print phi
-           (match v with True -> "True" | False -> "False" | _ -> "Unknown");
-*)

          match v with
            True -> StateSet.add q a_sat, a_todo
          | False -> acc
          | Unknown -> a_sat, StateSet.add q a_todo
        ) old_todo (old_sat, StateSet.empty)
      in
          match v with
            True -> StateSet.add q a_sat, a_todo
          | False -> acc
          | Unknown -> a_sat, StateSet.add q a_todo
        ) old_todo (old_sat, StateSet.empty)
      in

-  (*   Logger.msg `STATS ""; *)

      if old_sat != sat || old_todo != todo then
        NodeStatus.make { os_node with sat; todo }
      else old_status
      if old_sat != sat || old_todo != todo then
        NodeStatus.make { os_node with sat; todo }
      else old_status


@@ -344,7 +335,8 @@ DEFINE AND_(t1,t2) =
     let init_todo = states_by_rank.(i) in
     let rec loop node =
       let node_id = T.preorder tree node in
     let init_todo = states_by_rank.(i) in
     let rec loop node =
       let node_id = T.preorder tree node in

-      if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false else begin
+      if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false
+      else begin

         let parent = T.parent tree node in
         let fc = T.first_child tree node in
         let fc_id = T.preorder tree fc in
         let parent = T.parent tree node in
         let fc = T.first_child tree node in
         let fc_id = T.preorder tree fc in


@@ -375,19 +367,20 @@ DEFINE AND_(t1,t2) =
           else c
         in
         IFTRACE(html tree node _i status0 "Entering node");
           else c
         in
         IFTRACE(html tree node _i status0 "Entering node");

-

         (* get the node_statuses for the first child, next sibling and parent *)
         let ps = unsafe_get_status status (T.preorder tree parent) in
         let fcs = unsafe_get_status status fc_id in
         let nss = unsafe_get_status status ns_id in
         (* evaluate the transitions with all this statuses *)
         (* get the node_statuses for the first child, next sibling and parent *)
         let ps = unsafe_get_status status (T.preorder tree parent) in
         let fcs = unsafe_get_status status fc_id in
         let nss = unsafe_get_status status ns_id in
         (* evaluate the transitions with all this statuses *)

-        let status1 = if status0.NodeStatus.node.todo == StateSet.empty then status0 else begin
-          let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
-          IFTRACE(html tree node _i status1 "Updating transitions");
+        let status1 =
+          if status0.NodeStatus.node.todo == StateSet.empty then status0
+          else begin
+            let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
+            IFTRACE(html tree node _i status1 "Updating transitions");

           (* update the cache if the status of the node changed *)
           (* update the cache if the status of the node changed *)

-          if status1 != status0 then status.(node_id) <- status1;
-          status1
-        end
+            if status1 != status0 then status.(node_id) <- status1;
+            status1
+          end

         in
         (* recursively traverse the first child *)
         let unstable_left = loop fc in
         in
         (* recursively traverse the first child *)
         let unstable_left = loop fc in


@@ -395,25 +388,32 @@ DEFINE AND_(t1,t2) =
            get the new status of the first child *)
         let fcs1 = unsafe_get_status status fc_id in
         (* update the status *)
            get the new status of the first child *)
         let fcs1 = unsafe_get_status status fc_id in
         (* update the status *)

-        let status2 = if status1.NodeStatus.node.todo == StateSet.empty then status1 else begin
-          let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in
-          IFTRACE(html tree node _i status2 "Updating transitions (after first-child)");
-          if status2 != status1 then status.(node_id) <- status2;
-          status2
-        end
+        let status2 =
+          if status1.NodeStatus.node.todo == StateSet.empty then status1
+          else begin
+            let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in
+            IFTRACE(html tree node _i status2
+                      "Updating transitions (after first-child)");
+            if status2 != status1 then status.(node_id) <- status2;
+            status2
+          end

         in
         let unstable_right = loop ns in
         let nss1 = unsafe_get_status status ns_id in
         in
         let unstable_right = loop ns in
         let nss1 = unsafe_get_status status ns_id in

-        let status3 = if status2.NodeStatus.node.todo == StateSet.empty then status2 else begin
-          let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
-          IFTRACE(html tree node _i status3 "Updating transitions (after next-sibling)");
+        let status3 =
+          if status2.NodeStatus.node.todo == StateSet.empty then status2
+          else begin
+            let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
+            IFTRACE(html tree node _i status3
+                      "Updating transitions (after next-sibling)");

           if status3 != status2 then status.(node_id) <- status3;
           status3
         end
         in
         let unstable_self =
           if status3 != status2 then status.(node_id) <- status3;
           status3
         end
         in
         let unstable_self =

-          (* if either our left or right child is unstable or if we still have transitions
-             pending, the current node is unstable *)
+          (* if either our left or right child is unstable or if we
+             still have transitions pending, the current node is
+             unstable *)

           unstable_left
           || unstable_right
           || StateSet.empty != status3.NodeStatus.node.todo
           unstable_left
           || unstable_right
           || StateSet.empty != status3.NodeStatus.node.todo


@@ -423,7 +423,8 @@ DEFINE AND_(t1,t2) =
             Html.finalize_node
               node_id
               _i
             Html.finalize_node
               node_id
               _i

-              Ata.(StateSet.intersect status3.NodeStatus.node.sat (get_selecting_states auto))));
+              Ata.(StateSet.intersect status3.NodeStatus.node.sat
+                     (get_selecting_states auto))));

         unstable_self
       end
     in
         unstable_self
       end
     in

diff --git a/src/tatoo.ml b/src/tatoo.ml
index ca16227..485d8e1 100644 (file)
--- a/src/tatoo.ml
+++ b/src/tatoo.ml
@@ -122,7 +122,8 @@ let main () =
   in
   let s = Naive.stats () in
   Run.(
   in
   let s = Naive.stats () in
   Run.(

-  Logger.msg `STATS "@[tree size: %d@\ntraversals: %d@\ncache2 hit ratio: %f@\ncache5 hit ratio: %f@]"
+  Logger.msg `STATS
+    "@[tree size: %d@\ntraversals: %d@\ncache2 hit ratio: %f@\ncache5 hit ratio: %f@]"

     s.tree_size s.run
     (float s.cache2_hit /. float s.cache2_access)
     (float s.cache5_hit /. float s.cache5_access));
     s.tree_size s.run
     (float s.cache2_hit /. float s.cache2_access)
     (float s.cache5_hit /. float s.cache5_access));

diff --git a/src/tree.ml b/src/tree.ml
index 97711dd..525f8c7 100644 (file)
--- a/src/tree.ml
+++ b/src/tree.ml
@@ -18,7 +18,8 @@
 module NodeKind =
   struct
     type t =
 module NodeKind =
   struct
     type t =

-        Document | Element | Text | Comment | Attribute | ProcessingInstruction | Node
+      Document | Element | Text | Comment | Attribute
+    | ProcessingInstruction | Node

 
     let to_string =
       function
 
     let to_string =
       function