Finaly clean up formula representation.

diff --git a/src/ata.ml b/src/ata.ml
index 0ae811d..f0882d5 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -183,7 +183,7 @@ let top_down_approx auto states tree =
            else TagSet.positive ts
          in
          let _, _, m, f = Transition.node tr in
-         let (_, _, ls), (_, _, rs) = Formula.st f in
+         let ls, rs = Formula.st f in
          if Ptset.Int.is_empty pos then acc_tr
          else
            (TagSet.inj_positive pos, (ls, rs, m))::acc_tr

diff --git a/src/compile.ml b/src/compile.ml
index 04fa7f1..e60ede6 100644 (file)
--- a/src/compile.ml
+++ b/src/compile.ml
@@ -196,7 +196,7 @@ and compile_path toplevel p conf =
 
 let compile path =
   let cont, conf = compile_path true path empty_info in
-  let (_, _, init), _ = Formula.st cont in
+  let init, _ = Formula.st cont in
   let get t s =
     try Hashtbl.find t s with Not_found -> []
   in

diff --git a/src/formula.ml b/src/formula.ml
index 3b344e7..4690ee0 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -12,7 +12,7 @@ type 'hcons expr =
 type 'hcons node = {
   pos : 'hcons expr;
   mutable neg : 'hcons;
-  st : (StateSet.t*StateSet.t*StateSet.t)*(StateSet.t*StateSet.t*StateSet.t);
+  st : StateSet.t * StateSet.t;
   size: int; (* Todo check if this is needed *)
 }
 
@@ -102,32 +102,33 @@ let cons pos neg s1 s2 size1 size2 =
                                      account for hashing ! *)
     pnode,nnode
 
-let empty_triple = StateSet.empty,StateSet.empty,StateSet.empty
-let empty_hex = empty_triple,empty_triple
-let true_,false_ = cons True False empty_hex empty_hex 0 0
+
+let empty_pair = StateSet.empty, StateSet.empty
+let true_,false_ = cons True False empty_pair empty_pair 0 0
 let atom_ d p s =
   let si = StateSet.singleton s in
   let ss = match d with
-    | `Left -> (si,StateSet.empty,si),empty_triple
-    | `Right -> empty_triple,(si,StateSet.empty,si)
-    | `Epsilon -> empty_triple, empty_triple
+    | `Left -> si, StateSet.empty
+    | `Right -> StateSet.empty, si
+    | `Epsilon -> empty_pair (* TODO CHECK *)
   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 
 let pred_ p =
   let fneg = !(p.Tree.Predicate.node) in
   let pneg = Tree.Predicate.make (ref (fun t n -> not (fneg t n))) in
-  fst (cons (Pred p) (Pred pneg) empty_hex empty_hex 1 1)
+  fst (cons (Pred p) (Pred pneg) empty_pair empty_pair 1 1)
 
 let not_ f = f.Node.node.neg
-let union_hex  ((l1,ll1,lll1),(r1,rr1,rrr1))  ((l2,ll2,lll2),(r2,rr2,rrr2)) =
-  (StateSet.mem_union l1 l2 ,StateSet.mem_union ll1 ll2,StateSet.mem_union lll1 lll2),
-  (StateSet.mem_union r1 r2 ,StateSet.mem_union rr1 rr2,StateSet.mem_union rrr1 rrr2)
+
+let union_pair (l1,r1) (l2, r2) =
+  StateSet.mem_union l1 l2,
+  StateSet.mem_union r1 r2
 
 let merge_states f1 f2 =
   let sp =
-    union_hex (st f1) (st f2)
+    union_pair (st f1) (st f2)
   and sn =
-    union_hex (st (not_ f1)) (st (not_ f2))
+    union_pair (st (not_ f1)) (st (not_ f2))
   in
     sp,sn
 
@@ -143,7 +144,7 @@ let or_ f1 f2 =
   else if is_true f1 || is_true f2 then true_
   else if is_false f1 && is_false f2 then false_
   else if is_false f1 then f2
-  else if is_false f2 then f1 
+  else if is_false f2 then f1
 
              (* commutativity of | *)
   else

diff --git a/src/formula.mli b/src/formula.mli
index 1dd05e2..12d13de 100644 (file)
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -11,10 +11,7 @@ val hash : t -> int
 val uid : t -> Uid.t
 val equal : t -> t -> bool
 val expr : t -> t expr
-val st :
-  t ->
-  (StateSet.t * StateSet.t * StateSet.t) *
-    (StateSet.t * StateSet.t * StateSet.t)
+val st : t -> StateSet.t * StateSet.t
 val compare : t -> t -> int
 val size : t -> int
 val print : Format.formatter -> t -> unit

diff --git a/src/l2JIT.ml b/src/l2JIT.ml
index ab8b570..b1fd4da 100644 (file)
--- a/src/l2JIT.ml
+++ b/src/l2JIT.ml
@@ -118,7 +118,7 @@ let collect_trans tag ((a_t, a_s1, a_s2) as acc) (labels, tr) =
   if TagSet.mem tag labels
   then
     let _, _, _, f = Transition.node tr in
-    let (_, _, s1), (_, _, s2) = Formula.st f in
+    let  s1,  s2 = Formula.st f in
       (Translist.cons tr a_t,
        StateSet.union s1 a_s1,
        StateSet.union s2 a_s2)

diff --git a/src/resJIT.ml b/src/resJIT.ml
index df08d9c..64c9624 100644 (file)
--- a/src/resJIT.ml
+++ b/src/resJIT.ml
@@ -197,6 +197,12 @@ let () = at_exit (fun () -> Printf.eprintf "Dummy affectations %i/%i\n%!" !_empt
 
 DEFINE SET(a, b) = (a) <- (b)
 
+DEFINE PRINT_TEMPLATE(ns) =
+      let pr fmt (state, count) =
+       fprintf fmt "%a: %i" State.print state (ns.length count)
+      in
+      Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s)
+
 DEFINE EXEC_INSTR_TEMPLATE(ns) = fun slot1 slot2 t inst acc ->
    match inst with
     | SELF _ ->  ns.snoc acc t
@@ -265,6 +271,34 @@ DEFINE EXEC_CODE_TEMPLATE(ns) = fun slot slot1 slot2 t dst code ->
       slot.(dst) <- !acc
 
 
+DEFINE EXEC_REC_TEMPLATE =
+         (match code with
+         | Nil -> ()
+         | Cons(dst, opcode, code1) ->
+           TRACE("res-jit", 3, __ "  %a := %a\n%!"
+             State.print dst print_opcode opcode;
+           );
+           exec_code slot slot1 slot2 t dst opcode;
+           begin
+             match code1 with
+           | Nil -> ()
+           | Cons(dst, opcode, code1) ->
+             TRACE("res-jit", 3, __ "  %a := %a\n%!"
+               State.print dst print_opcode opcode;
+             );
+             exec_code slot slot1 slot2 t dst opcode;
+             exec slot slot1 slot2 t code1
+
+           end)
+
+DEFINE EXEC_TEMPLATE =
+         (TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t));
+          TRACE("res-jit", 3, __ " LEFT  : %a\n" pr_slot slot1);
+          TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2);
+          exec slot slot1 slot2 t code;
+          TRACE("res-jit", 3, __ " RES   : %a\n\n%!" pr_slot slot))
+
+
 module type S =
   sig
     module NS : NodeSet.S
@@ -276,51 +310,17 @@ module type S =
     val is_open : t -> bool
   end
 
-
-
 module Count =
   struct
     module NS = NodeSet.Count
     type t = NodeSet.Count.t array
-    let print fmt s =
-      let pr fmt (state, count) =
-       fprintf fmt "%a: %i" State.print state (NS.length count)
-      in
-      Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s)
-
+    let print fmt s = PRINT_TEMPLATE(NS)
     let exec_instr = EXEC_INSTR_TEMPLATE(NodeSet.Count)
     let exec_code = EXEC_CODE_TEMPLATE(NodeSet.Count)
-      (* inline by hand for efficiency reason *)
-    let rec exec slot slot1 slot2 t code =
-      match code with
-       | Nil -> ()
-       | Cons(dst, opcode, code1) ->
-         TRACE("res-jit", 3, __ "  %a := %a\n%!"
-           State.print dst print_opcode opcode;
-         );
-         exec_code slot slot1 slot2 t dst opcode;
-         begin
-           match code1 with
-           | Nil -> ()
-           | Cons(dst, opcode, code1) ->
-             TRACE("res-jit", 3, __ "  %a := %a\n%!"
-               State.print dst print_opcode opcode;
-             );
-             exec_code slot slot1 slot2 t dst opcode;
-             exec slot slot1 slot2 t code1
-         end
-
-    let exec slot slot1 slot2 t code =
-      TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t));
-      TRACE("res-jit", 3, __ " LEFT  : %a\n" pr_slot slot1);
-      TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2);
-      exec slot slot1 slot2 t code;
-      TRACE("res-jit", 3, __ " RES   : %a\n\n%!" pr_slot slot)
-
-
+    let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE
+    let exec slot slot1 slot2 t code = EXEC_TEMPLATE
     let var _ x = x
     let close _ x = x
-
     let is_open _ = false
   end
 
@@ -328,28 +328,11 @@ module Mat =
   struct
     module NS = NodeSet.Mat
     type t = NodeSet.Mat.t array
-    let print fmt s =
-      let pr fmt (state, count) =
-       fprintf fmt "%a: %i" State.print state (NS.length count)
-      in
-      Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s)
-
+    let print fmt s = PRINT_TEMPLATE(NS)
     let exec_instr = EXEC_INSTR_TEMPLATE(NodeSet.Mat)
     let exec_code = EXEC_CODE_TEMPLATE(NodeSet.Mat)
-      (* inline by hand for efficiency reason *)
-    let rec exec slot slot1 slot2 t code =
-      match code with
-       | Nil -> ()
-       | Cons(dst, code, code1) ->
-           exec_code slot slot1 slot2 t dst code;
-           begin
-             match code1 with
-             | Nil -> ()
-             | Cons(dst', code', code1') ->
-               exec_code slot slot1 slot2 t dst' code';
-               exec slot slot1 slot2 t code1'
-           end
-
+    let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE
+    let exec slot slot1 slot2 t code = EXEC_TEMPLATE
     let var _ x = x
     let close _ x = x
     let is_open _ = false
@@ -361,42 +344,11 @@ module Make(U : NodeSet.S) =
   struct
     module NS = U
     type t = U.t array
-    let print fmt s =
-      let pr fmt (state, count) =
-       fprintf fmt "%a: %i" State.print state (NS.length count)
-      in
-      Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s)
-
+    let print fmt s = PRINT_TEMPLATE(NS)
     let exec_instr = EXEC_INSTR_TEMPLATE(U)
     let exec_code = EXEC_CODE_TEMPLATE(U)
-      (* inline by hand for efficiency reason *)
-    let rec exec slot slot1 slot2 t code =
-      match code with
-       | Nil -> ()
-       | Cons(dst, opcode, code1) ->
-         TRACE("res-jit", 3, __ "  %a := %a\n%!"
-           State.print dst print_opcode opcode;
-         );
-         exec_code slot slot1 slot2 t dst opcode;
-         begin
-           match code1 with
-           | Nil -> ()
-           | Cons(dst, opcode, code1) ->
-             TRACE("res-jit", 3, __ "  %a := %a\n%!"
-               State.print dst print_opcode opcode;
-             );
-             exec_code slot slot1 slot2 t dst opcode;
-             exec slot slot1 slot2 t code1
-         end
-
-    let exec slot slot1 slot2 t code =
-      TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t));
-      TRACE("res-jit", 3, __ " LEFT  : %a\n" pr_slot slot1);
-      TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2);
-      exec slot slot1 slot2 t code;
-      TRACE("res-jit", 3, __ " RES   : %a\n\n%!" pr_slot slot)
-
-
+    let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE
+    let exec slot slot1 slot2 t code = EXEC_TEMPLATE
     let var i t =
       Array.mapi (fun j _ -> NS.var (i,j)) t
     let close h t =