15 | OP_LEFT2 of State.t * State.t
16 | OP_RIGHT1 of State.t
17 | OP_RIGHT2 of State.t * State.t
18 | OP_LEFT1_RIGHT1 of State.t * State.t
19 | OP_LEFT2_RIGHT1 of State.t * State.t * State.t
20 | OP_LEFT1_RIGHT2 of State.t * State.t * State.t
21 | OP_LEFT2_RIGHT2 of State.t * State.t * State.t * State.t
23 | OP_SELF_LEFT1 of State.t
24 | OP_SELF_LEFT2 of State.t * State.t
25 | OP_SELF_RIGHT1 of State.t
26 | OP_SELF_RIGHT2 of State.t * State.t
27 | OP_SELF_LEFT1_RIGHT1 of State.t * State.t
28 | OP_SELF_LEFT2_RIGHT1 of State.t * State.t * State.t
29 | OP_SELF_LEFT1_RIGHT2 of State.t * State.t * State.t
30 | OP_SELF_LEFT2_RIGHT2 of State.t * State.t * State.t * State.t
31 | OP_OTHER of instr array
33 type code = Nil | Cons of State.t * opcode * code
38 | Cons(_, _, t) -> 1 + length t
40 fprintf fmt "length of code is %i\n%!" (length l)
43 let print_instr fmt i =
45 | SELF _ -> fprintf fmt "SELF"
46 | LEFT q -> fprintf fmt "LEFT{%a}" State.print q
47 | RIGHT q -> fprintf fmt "RIGHT{%a}" State.print q
49 let print_opcode fmt code =
51 | OP_NOP _ -> fprintf fmt "OP_NOP"
54 fprintf fmt "OP_LEFT1{%a}" State.print src
56 | OP_LEFT2 (src1, src2) ->
57 fprintf fmt "OP_LEFT2{%a, %a}" State.print src1 State.print src2
60 fprintf fmt "OP_RIGHT1{%a}" State.print src
62 | OP_RIGHT2 (src1, src2) ->
63 fprintf fmt "OP_RIGHT2{%a, %a}" State.print src1 State.print src2
65 | OP_LEFT1_RIGHT1 (src1, src2) ->
66 fprintf fmt "OP_LEFT1_RIGHT1{%a}{%a}" State.print src1 State.print src2
68 | OP_LEFT2_RIGHT1 (src1, src2, src3) ->
69 fprintf fmt "OP_LEFT2_RIGHT1{%a, %a}{%a}"
70 State.print src1 State.print src2 State.print src3
72 | OP_LEFT1_RIGHT2 (src1, src2, src3) ->
73 fprintf fmt "OP_LEFT1_RIGHT2{%a}{%a, %a}"
74 State.print src1 State.print src2 State.print src3
76 | OP_LEFT2_RIGHT2 (src1, src2, src3, src4) ->
77 fprintf fmt "OP_LEFT2_RIGHT2{%a, %a}{%a, %a}"
78 State.print src1 State.print src2 State.print src3 State.print src4
83 | OP_SELF_LEFT1 src ->
84 fprintf fmt "OP_SELF_LEFT1{%a}" State.print src
86 | OP_SELF_LEFT2 (src1, src2) ->
87 fprintf fmt "OP_SELF_LEFT2{%a, %a}" State.print src1 State.print src2
89 | OP_SELF_RIGHT1 src ->
90 fprintf fmt "OP_SELF_RIGHT1{%a}" State.print src
92 | OP_SELF_RIGHT2 (src1, src2) ->
93 fprintf fmt "OP_SELF_RIGHT2{%a, %a}" State.print src1 State.print src2
95 | OP_SELF_LEFT1_RIGHT1 (src1, src2) ->
96 fprintf fmt "OP_SELF_LEFT1_RIGHT1{%a}{%a}" State.print src1 State.print src2
98 | OP_SELF_LEFT2_RIGHT1 (src1, src2, src3) ->
99 fprintf fmt "OP_SELF_LEFT2_RIGHT1{%a, %a}{%a}"
100 State.print src1 State.print src2 State.print src3
102 | OP_SELF_LEFT1_RIGHT2 (src1, src2, src3) ->
103 fprintf fmt "OP_SELF_LEFT1_RIGHT2{%a}{%a, %a}"
104 State.print src1 State.print src2 State.print src3
106 | OP_SELF_LEFT2_RIGHT2 (src1, src2, src3, src4) ->
107 fprintf fmt "OP_SELF_LEFT2_RIGHT2{%a, %a}{%a, %a}"
108 State.print src1 State.print src2 State.print src3 State.print src4
110 fprintf fmt "OP_OTHER: ";
111 Array.iter (fun i -> print_instr fmt i; fprintf fmt " ") line
113 let merge_rev equal choose l =
119 let j = List.hd acc in
120 if equal i j then (choose i j)::(List.tl acc)
123 let compile_instr_list l =
124 let linstr = merge_rev (=) (fun i _ -> i) (List.sort (fun x y -> compare y x) l) in
127 | [ LEFT q ] -> OP_LEFT1 q
128 | [ LEFT q1; LEFT q2 ] -> OP_LEFT2(q2, q1)
129 | [ RIGHT q ] -> OP_RIGHT1 q
130 | [ RIGHT q1; RIGHT q2 ] -> OP_RIGHT2(q2, q1)
131 | [ LEFT q1; RIGHT q2 ] -> OP_LEFT1_RIGHT1(q1, q2)
132 | [ LEFT q1; LEFT q2; RIGHT q3 ] -> OP_LEFT2_RIGHT1 (q2, q1, q3)
133 | [ LEFT q1; RIGHT q2; RIGHT q3 ] -> OP_LEFT1_RIGHT2 (q1, q3, q2)
134 | [ LEFT q1; LEFT q2; RIGHT q3; RIGHT q4 ] -> OP_LEFT2_RIGHT2 (q2, q1, q4, q3)
135 | [ SELF () ] -> OP_SELF()
137 | [ SELF _; LEFT q ] -> OP_SELF_LEFT1 q
138 | [ SELF _; LEFT q1; LEFT q2 ] -> OP_SELF_LEFT2(q2, q1)
139 | [ SELF _; RIGHT q ] -> OP_SELF_RIGHT1 q
140 | [ SELF _; RIGHT q1; RIGHT q2 ] -> OP_SELF_RIGHT2(q2, q1)
141 | [ SELF _; LEFT q1; RIGHT q2 ] -> OP_SELF_LEFT1_RIGHT1(q1, q2)
142 | [ SELF _; LEFT q1; LEFT q2; RIGHT q3 ] -> OP_SELF_LEFT2_RIGHT1 (q2, q1, q3)
143 | [ SELF _; LEFT q1; RIGHT q2; RIGHT q3 ] -> OP_SELF_LEFT1_RIGHT2 (q1, q3, q2)
144 | [ SELF _; LEFT q1; LEFT q2; RIGHT q3; RIGHT q4 ] ->
145 OP_SELF_LEFT2_RIGHT2 (q2, q1, q4, q3)
146 | i -> OP_OTHER (Array.of_list i)
153 | (a, b)::ll -> loop ll (Cons(a,b, acc))
157 let rec filter_uniq statel stater l =
163 (fun ((a_il, al, ar)as acc) i ->
166 if List.mem q al then acc
167 else (i :: a_il, q::al, ar)
169 if List.mem q ar then acc
170 else (i :: a_il, al, q :: ar)
171 | _ -> (i :: a_il, al, ar)) ([], statel, stater) il
173 (s, nil) :: (filter_uniq nsl nsr ll)
176 let l = List.sort (fun (s1, _) (s2, _) -> compare s1 s2) l in
177 let l = filter_uniq [] [] l in
179 (fun (s1, _) (s2, _) -> s1 = s2)
180 (fun (s1, i1) (_, i2) -> (s1, i1@i2)) l
184 (fun (_, l) -> List.exists (function SELF _ -> true | _ -> false) l)
187 let l = List.map (fun (s, il) -> (s, compile_instr_list il)) l in
188 let l = List.filter (fun (_, instr) -> instr <> OP_NOP ()) l in
189 to_list l, not marking
192 type 'a update = 'a -> 'a -> 'a -> Tree.t -> Tree.node -> StateSet.t * 'a
193 type 'a cache = 'a update Cache.Lvl3.t
195 let dummy_update = fun _ _ _ _ _ -> failwith "Uninitialized L3JIT"
196 let show_stats (a : 'a cache) =
198 Cache.Lvl3.iteri (fun _ _ _ _ b -> if not b then incr count) a;
199 eprintf "%!L3JIT: %i used entries\n%!" !count
202 let v = Cache.Lvl3.create 1024 dummy_update in
203 if !Options.verbose then at_exit (fun () -> show_stats v);
206 let find (t : 'a cache) tlist s1 s2 =
208 (Uid.to_int s2.StateSet.Node.id)
209 (Uid.to_int s1.StateSet.Node.id)
210 (Uid.to_int tlist.Translist.Node.id)
212 let add (t : 'a cache) tlist s1 s2 v =
214 (Uid.to_int s2.StateSet.Node.id)
215 (Uid.to_int s1.StateSet.Node.id)
216 (Uid.to_int tlist.Translist.Node.id)
219 let eval_form auto s1 s2 f =
221 match Formula.expr f with
222 | Formula.False | Formula.True | Formula.Pred _ -> f, []
223 | Formula.Atom(`Left, b, q) ->
224 Formula.of_bool (b == (StateSet.mem q s1)),
225 if b && StateSet.mem q auto.Ata.topdown_marking_states then [LEFT q] else []
226 | Formula.Atom (`Right, b, q) ->
227 Formula.of_bool(b == (StateSet.mem q s2)),
228 if b && StateSet.mem q auto.Ata.topdown_marking_states then [RIGHT q] else []
229 | Formula.Atom (`Epsilon, _, _) -> assert false
231 | Formula.Or(f1, f2) ->
232 let b1, i1 = loop f1 in
233 let b2, i2 = loop f2 in
234 Formula.or_pred b1 b2, i1 @ i2
235 | Formula.And(f1, f2) ->
236 let b1, i1 = loop f1 in
237 let b2, i2 = loop f2 in
238 Formula.and_pred b1 b2, i1 @ i2
242 let eval_trans auto s1 s2 trans =
244 (fun t ((a_st, a_op, a_todo) as acc)->
245 let q, _, m, f = Transition.node t in
246 let form, ops = eval_form auto s1 s2 f in
247 match Formula.expr form with
250 (q, (if m then (SELF() :: ops) else ops)):: a_op,
252 | Formula.False -> acc
253 | Formula.Pred p -> a_st, a_op,
254 (p.Tree.Predicate.node, q, [(q,(if m then (SELF() :: ops) else ops))]) :: a_todo
256 ) trans (StateSet.empty, [], [])
258 let compile_update auto trl s1 s2 =
259 let orig_s1, orig_s2 =
260 Translist.fold (fun t (a1, a2) ->
261 let _, _, _, f = Transition.node t in
262 let fs1, fs2 = Formula.st f in
263 (StateSet.union a1 fs1, StateSet.union a2 fs2)
264 ) trl (StateSet.empty, StateSet.empty)
266 let ns1 = StateSet.inter s1 orig_s1
267 and ns2 = StateSet.inter s2 orig_s2 in
268 let res, ops, todo = eval_trans auto ns1 ns2 trl in
269 let code, not_marking = compile ops in
270 let todo_code, todo_notmarking =
271 List.fold_left (fun (l, b) (p, q, o) -> let c, b' = compile o in
272 (p, q, c)::l, b && b')
273 ([], not_marking) todo
275 let opcode = res, code, todo_notmarking, todo_code in
278 let gen_code exec auto tlist s1 s2 =
279 let res, code, not_marking, todo_code = compile_update auto tlist s1 s2 in
281 if todo_code == [] then
282 if not_marking then begin fun empty_slot sl1 sl2 _ node ->
283 let slot1_empty = sl1 == empty_slot
284 and slot2_empty = sl2 == empty_slot in
285 if slot1_empty && slot2_empty then res,sl2
290 Array.copy empty_slot
294 exec sl sl1 sl2 node code;
297 else (* marking *) begin fun empty_slot sl1 sl2 _ node ->
299 if sl2 == empty_slot then
300 if sl1 == empty_slot then
301 Array.copy empty_slot
305 exec sl sl1 sl2 node code;
308 else (* todo != [] *)
309 begin fun empty_slot sl1 sl2 tree node ->
311 if sl2 == empty_slot then
312 if sl1 == empty_slot then
313 Array.copy empty_slot
317 exec sl sl1 sl2 node code;
319 (fun ares (p, q, code) ->
320 if !p tree node then begin
321 if code != Nil then exec sl sl1 sl2 node code;
324 else ares) res todo_code, sl
334 DEFINE SET(a, b) = (a) <- (b)
336 DEFINE PRINT_TEMPLATE(ns) =
337 let pr fmt (state, count) =
338 fprintf fmt "%a: %i" State.print state (ns.length count)
340 Pretty.print_array ~sep:", " pr fmt (Array.mapi (fun x y -> (x,y)) s)
342 DEFINE EXEC_INSTR_TEMPLATE(ns) = fun slot1 slot2 t inst acc ->
344 | SELF _ -> ns.snoc acc t
345 | LEFT src -> ns.concat acc slot1.(src)
346 | RIGHT src -> ns.concat acc slot2.(src)
349 DEFINE EXEC_CODE_BODY_TEMPLATE(ns) =
354 SET(slot.(dst), slot1.(src))
356 | OP_LEFT2 (src1, src2) ->
357 SET(slot.(dst) , ns.concat slot1.(src1) slot1.(src2))
359 | OP_RIGHT1 src -> SET(slot.(dst) , slot2.(src))
361 | OP_RIGHT2 (src1, src2) ->
362 SET (slot.(dst) , ns.concat slot2.(src1) slot2.(src2) )
364 | OP_LEFT1_RIGHT1 (src1, src2) ->
365 SET (slot.(dst) , ns.concat slot1.(src1) slot2.(src2))
367 | OP_LEFT2_RIGHT1 (src1, src2, src3) ->
368 SET (slot.(dst) , ns.concat3 slot1.(src1) slot1.(src2) slot2.(src3))
370 | OP_LEFT1_RIGHT2 (src1, src2, src3) ->
371 SET (slot.(dst) , ns.concat3 slot1.(src1) slot2.(src2) slot2.(src3));
373 | OP_LEFT2_RIGHT2 (src1, src2, src3, src4) ->
374 SET (slot.(dst) , ns.concat4 slot1.(src1) slot1.(src2) slot2.(src3) slot2.(src4))
377 slot.(dst) <- ns.singleton t
379 | OP_SELF_LEFT1 src -> slot.(dst) <- ns.cons t slot1.(src)
381 | OP_SELF_LEFT2 (src1, src2) ->
382 slot.(dst) <- ns.conscat t slot1.(src1) slot1.(src2)
384 | OP_SELF_RIGHT1 src -> slot.(dst) <- ns.cons t slot2.(src)
386 | OP_SELF_RIGHT2 (src1, src2) ->
387 slot.(dst) <- ns.conscat t slot2.(src1) slot2.(src2)
389 | OP_SELF_LEFT1_RIGHT1 (src1, src2) ->
390 slot.(dst) <- ns.conscat t slot1.(src1) slot2.(src2)
392 | OP_SELF_LEFT2_RIGHT1 (src1, src2, src3) ->
393 slot.(dst) <- ns.conscat3 t slot1.(src1) slot1.(src2) slot2.(src3)
395 | OP_SELF_LEFT1_RIGHT2 (src1, src2, src3) ->
396 slot.(dst) <- ns.conscat3 t slot1.(src1) slot2.(src2) slot2.(src3)
398 | OP_SELF_LEFT2_RIGHT2 (src1, src2, src3, src4) ->
400 ns.conscat4 t slot1.(src1) slot1.(src2) slot2.(src3) slot2.(src4)
401 | OP_OTHER line -> assert false (*
402 let acc = ref ns.empty in
403 let len = Array.length line - 1 in
405 acc := exec_instr slot1 slot2 t line.(j) !acc
407 slot.(dst) <- !acc *) )
409 DEFINE EXEC_CODE_TEMPLATE(ns) = fun slot slot1 slot2 t dst code ->
410 EXEC_CODE_BODY_TEMPLATE(ns)
413 DEFINE EXEC_REC_TEMPLATE(exec_code) =
416 | Cons(dst, opcode, code1) ->
417 TRACE("res-jit", 3, __ " %a := %a\n%!"
418 State.print dst print_opcode opcode;
420 exec_code slot slot1 slot2 t dst opcode;
424 | Cons(dst, opcode, code1) ->
425 TRACE("res-jit", 3, __ " %a := %a\n%!"
426 State.print dst print_opcode opcode;
428 exec_code slot slot1 slot2 t dst opcode;
429 exec slot slot1 slot2 t code1
432 let count_exec_code slot slot1 slot2 t dst code =
433 EXEC_CODE_BODY_TEMPLATE(NodeSet.Count)
436 let count_exec slot slot1 slot2 t code =
437 let rec exec slot slot1 slot2 t code =
438 EXEC_REC_TEMPLATE(count_exec_code)
440 exec slot slot1 slot2 t code
442 let mat_exec_code slot slot1 slot2 t dst code =
443 EXEC_CODE_BODY_TEMPLATE(NodeSet.Mat)
446 let mat_exec slot slot1 slot2 t code =
447 let rec exec slot slot1 slot2 t code =
448 EXEC_REC_TEMPLATE(mat_exec_code)
450 exec slot slot1 slot2 t code
453 DEFINE EXEC_TEMPLATE =
454 (TRACE("res-jit", 3, __ "Node %i:\n" (Node.to_int t));
455 TRACE("res-jit", 3, __ " LEFT : %a\n" pr_slot slot1);
456 TRACE("res-jit", 3, __ " RIGHT : %a\n" pr_slot slot2);
457 exec slot slot1 slot2 t code;
458 TRACE("res-jit", 3, __ " RES : %a\n\n%!" pr_slot slot))
461 DEFINE UPDATE_TEMPLATE =
462 let f = find cache tlist s1 s2 in
463 if f == dummy_update then
464 let f = gen_code exec auto tlist s1 s2 in
465 add cache tlist s1 s2 f;
466 f empty_res sl1 sl2 tree node
468 f empty_res sl1 sl2 tree node
471 let update exec cache auto tlist s1 s2 empty_res sl1 sl2 tree node =
472 let f = find cache tlist s1 s2 in
473 if f == dummy_update then
474 let f = gen_code exec auto tlist s1 s2 in
475 add cache tlist s1 s2 f;
476 f empty_res sl1 sl2 tree node
478 f empty_res sl1 sl2 tree node
483 module NS : NodeSet.S
485 val exec : t -> t -> t -> Tree.node -> code -> unit
486 val update : t cache -> Ata.t -> Translist.t -> StateSet.t -> StateSet.t ->
487 t -> t -> t -> Tree.t -> Tree.node -> StateSet.t * t
488 val print : Format.formatter -> t -> unit
489 val var : int -> t -> t
490 val close : ((int*State.t, NS.t) Hashtbl.t) -> t -> t
491 val is_open : t -> bool
496 module NS = NodeSet.Count
497 type t = NodeSet.Count.t array
498 let print fmt s = PRINT_TEMPLATE(NS)
499 let exec_instr = EXEC_INSTR_TEMPLATE(NodeSet.Count)
500 let exec_code = EXEC_CODE_TEMPLATE(NodeSet.Count)
501 let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE(exec_code)
502 let exec slot slot1 slot2 t code = EXEC_TEMPLATE
503 let update cache auto tlist s1 s2 empty_res sl1 sl2 tree node = UPDATE_TEMPLATE
506 let is_open _ = false
511 module NS = NodeSet.Mat
512 type t = NodeSet.Mat.t array
513 let print fmt s = PRINT_TEMPLATE(NS)
514 let exec_instr = EXEC_INSTR_TEMPLATE(NodeSet.Mat)
515 let exec_code = EXEC_CODE_TEMPLATE(NodeSet.Mat)
516 let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE(exec_code)
517 let exec slot slot1 slot2 t code = EXEC_TEMPLATE
518 let update cache auto tlist s1 s2 empty_res sl1 sl2 tree node = UPDATE_TEMPLATE
521 let is_open _ = false
526 module Make(U : NodeSet.S) =
530 let print fmt s = PRINT_TEMPLATE(NS)
531 let exec_instr = EXEC_INSTR_TEMPLATE(U)
532 let exec_code = EXEC_CODE_TEMPLATE(U)
533 let rec exec slot slot1 slot2 t code = EXEC_REC_TEMPLATE(exec_code)
534 let exec slot slot1 slot2 t code = EXEC_TEMPLATE
535 let update cache auto tlist s1 s2 empty_res sl1 sl2 tree node = UPDATE_TEMPLATE
537 Array.mapi (fun j _ -> NS.var (i,j)) t
539 Array.map (NS.close h) t
542 List.exists NS.is_open (Array.to_list t)