+ ;;
+
+
+
+
+
+ module Code3Cache =
+ struct
+ let get = Array.unsafe_get
+ let set = Array.set
+
+ type fun_tree = [`Tree] Tree.node -> [`Tree] Tree.node -> StateSet.t -> Tag.t -> StateSet.t*RS.t
+ type t = fun_tree array array
+
+ let dummy = fun _ _ _ _ -> failwith "Uninitializd Code3Cache"
+ let default_line = Array.create 1024 dummy (* 256 = max_tag *)
+ let create n = Array.create n default_line
+ let init f =
+ for i = 0 to (Array.length default_line) - 1
+ do
+ default_line.(i) <- f
+ done
+
+ let get_fun h slist tag =
+ get (get h (Uid.to_int slist.StateSet.Node.id)) tag
+
+ let set_fun (h : t) slist tag (data : fun_tree) =
+ let tab = get h (Uid.to_int slist.StateSet.Node.id) in
+ let line = if tab == default_line then
+ let x = Array.copy tab in
+ (set h (Uid.to_int slist.StateSet.Node.id) x;x)
+ else tab
+ in
+ set line tag data
+
+ end
+
+
+
+ module Fold3Res = struct
+ let get = Array.unsafe_get
+ let set = Array.set
+ external field1 : Obj.t -> int = "%field1"
+ type t = Obj.t array array array array
+ let dummy_val = Obj.repr ((),2,())
+
+ let default_line3 = Array.create 1024 dummy_val
+ let default_line2 = Array.create BIG_A_SIZE default_line3
+ let default_line1 = Array.create BIG_A_SIZE default_line2
+
+ let create n = Array.create n default_line1
+
+ let find h tag fl s1 s2 : StateSet.t*bool*merge_conf =
+ let l1 = get h (Uid.to_int fl.Formlist.Node.id) in
+ let l2 = get l1 (Uid.to_int s1.StateSet.Node.id) in
+ let l3 = get l2 (Uid.to_int s2.StateSet.Node.id) in
+ Obj.magic (get l3 tag)
+
+ let is_valid b = b != (Obj.magic dummy_val)
+ let get_replace tab idx default =
+ let e = get tab idx in
+ if e == default then
+ let ne = Array.copy e in (set tab idx ne;ne)
+ else e
+
+ let add h tag fl s1 s2 (data: StateSet.t*bool*merge_conf) =
+ let l1 = get_replace h (Uid.to_int fl.Formlist.Node.id) default_line1 in
+ let l2 = get_replace l1 (Uid.to_int s1.StateSet.Node.id) default_line2 in
+ let l3 = get_replace l2 (Uid.to_int s2.StateSet.Node.id) default_line3 in
+ set l3 tag (Obj.repr data)
+ end
+
+
+ let empty_res = StateSet.empty,RS.empty
+
+ let top_down1 a tree t slist ctx td_trans h_fold2 =
+ (* evaluation starts from the right so we put sl1,res1 at the end *)
+ let eval_fold2_slist fll t tag (sl2,res2) (sl1,res1) =
+ let data = Fold3Res.find h_fold2 tag fll sl1 sl2 in
+ if Fold3Res.is_valid data then
+ let r,b,conf = data in
+ (r,if b then RS.merge conf t res1 res2 else RS.empty)
+ else
+ let r,conf = eval_formlist tag sl1 sl2 fll in
+ let b = conf <> NO in
+ (Fold3Res.add h_fold2 tag fll sl1 sl2 (r,b,conf);
+ (r, if b then RS.merge conf t res1 res2 else RS.empty))
+
+ in
+ let rec loop t ctx slist _ =
+ if t == Tree.nil then empty_res else
+ let tag = Tree.tag tree t in
+ (Code3Cache.get_fun td_trans slist tag) t ctx slist tag
+
+ and loop_tag t ctx slist tag =
+ if t == Tree.nil then empty_res else
+ (Code3Cache.get_fun td_trans slist tag) t ctx slist tag
+
+ and mk_trans t ctx slist tag =
+ let fl_list,llist,rlist,ca,da,sa,fa =
+ StateSet.fold
+ (fun q acc ->
+ List.fold_left
+ (fun ((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc) as acc)
+ (ts,t) ->
+ if (TagSet.mem tag ts)
+ then
+ let _,_,_,f,_ = t.Transition.node in
+ let (child,desc,below),(sibl,foll,after) = Formula.st f in
+ (Formlist.cons t fl_acc,
+ StateSet.union ll_acc below,
+ StateSet.union rl_acc after,
+ StateSet.union child c_acc,
+ StateSet.union desc d_acc,
+ StateSet.union sibl s_acc,
+ StateSet.union foll f_acc)
+ else acc ) acc (
+ try Hashtbl.find a.trans q
+ with
+ Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
+ q;[]
+ )
+
+ ) slist (Formlist.nil,StateSet.empty,StateSet.empty,
+ StateSet.empty,StateSet.empty,StateSet.empty,StateSet.empty)
+
+ in
+ (* Logic to chose the first and next function *)
+ let tags_child,tags_below,tags_siblings,tags_after = Tree.tags tree tag in
+ let d_f = Algebra.decide a tags_child tags_below (StateSet.union ca da) true in
+ let d_n = Algebra.decide a tags_siblings tags_after (StateSet.union sa fa) false in
+ let f_kind,first = choose_jump_down tree d_f
+ and n_kind,next = choose_jump_next tree d_n in
+
+ let cont =
+ match f_kind,n_kind with
+ | `NIL,`NIL ->
+ fun t _ _ tag -> eval_fold2_slist fl_list t tag empty_res empty_res
+
+ | _,`NIL -> (
+ match f_kind with
+ |`TAG(tag1) ->
+ (fun t _ _ tag -> eval_fold2_slist fl_list t tag empty_res
+ (loop_tag (first t) t llist tag1))
+ | _ ->
+ fun t _ _ tag -> eval_fold2_slist fl_list t tag empty_res
+ (loop (first t) t llist tag)
+ )
+ | `NIL,_ -> (
+ match n_kind with
+ |`TAG(tag2) ->
+ fun t ctx _ tag ->
+ eval_fold2_slist fl_list t tag
+ (loop_tag (next t ctx) ctx rlist tag2)
+ empty_res
+
+ | _ ->
+ fun t ctx _ tag ->
+ eval_fold2_slist fl_list t tag
+ (loop (next t ctx) ctx rlist tag)
+ empty_res
+
+ )
+
+ | `TAG(tag1),`TAG(tag2) ->
+ fun t ctx _ tag ->
+ eval_fold2_slist fl_list t tag
+ (loop_tag (next t ctx) ctx rlist tag2)
+ (loop_tag (first t) t llist tag1)
+
+ | `TAG(tag1),`ANY ->
+ fun t ctx _ tag ->
+ eval_fold2_slist fl_list t tag
+ (loop (next t ctx) ctx rlist tag)
+ (loop_tag (first t) t llist tag1)
+
+ | `ANY,`TAG(tag2) ->
+ fun t ctx _ tag ->
+ eval_fold2_slist fl_list t tag
+ (loop_tag (next t ctx) ctx rlist tag2)
+ (loop (first t) t llist tag)
+
+
+ | _,_ ->
+ fun t ctx _ tag ->
+ eval_fold2_slist fl_list t tag
+ (loop (next t ctx) ctx rlist tag)
+ (loop (first t) t llist tag)
+
+
+
+ in
+ Code3Cache.set_fun td_trans slist tag cont;
+ cont t ctx slist tag
+ in
+ let _ = Code3Cache.init mk_trans in
+ loop t ctx slist Tag.dummy
+
+
+ let run_top_down1 a tree =
+ let _,res = top_down1 a tree Tree.root a.init Tree.root (Code3Cache.create BIG_A_SIZE) (Fold3Res.create BIG_A_SIZE)
+ in
+ res