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 *)
}
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
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
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
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
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
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
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 =