projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Change the interface of node_list (fully imperative now)
[tatoo.git]
/
src
/
run.ml
diff --git
a/src/run.ml
b/src/run.ml
index
8eb58f9
..
f125346
100644
(file)
--- a/
src/run.ml
+++ b/
src/run.ml
@@
-295,17
+295,17
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
let auto = run.auto in
let tree = run.tree in
let sel_states = Ata.get_selecting_states auto in
let auto = run.auto in
let tree = run.tree in
let sel_states = Ata.get_selecting_states auto in
- let res =
ref (L.create ()
) in
+ let res =
L.create (
) in
let rec loop node =
if node != T.nil then begin
if StateSet.intersect sel_states cache.(T.preorder tree node) then
let rec loop node =
if node != T.nil then begin
if StateSet.intersect sel_states cache.(T.preorder tree node) then
-
res := L.add node !
res;
+
L.push_back node
res;
loop (T.first_child tree node);
loop (T.next_sibling tree node)
end
in
loop (T.root tree);
loop (T.first_child tree node);
loop (T.next_sibling tree node)
end
in
loop (T.root tree);
-
!
res
+ res
let get_full_results run =
let get_full_results run =
@@
-331,8
+331,7
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
StateSet.iter
(fun q ->
let res = Cache.N1.find res_mapper (q :> int) in
StateSet.iter
(fun q ->
let res = Cache.N1.find res_mapper (q :> int) in
- if res != dummy then
- Cache.N1.add res_mapper (q :> int) (L.add node res)
+ if res != dummy then L.add node res
)
cache.(T.preorder tree node);
loop (T.first_child tree node);
)
cache.(T.preorder tree node);
loop (T.first_child tree node);