From 172af8a5311dd53ad6df9e330d6917200441dd39 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sat, 11 Jan 2014 13:13:59 +0100 Subject: [PATCH] Change the interface of node_list (fully imperative now) --- src/naive_node_list.ml | 50 +++++++++++++++++++++++++++++++++--------- src/node_list.ml | 12 +++++++++- src/run.ml | 9 ++++---- src/tatoo.ml | 4 ++-- 4 files changed, 57 insertions(+), 18 deletions(-) diff --git a/src/naive_node_list.ml b/src/naive_node_list.ml index c148732..b6f0ae4 100644 --- a/src/naive_node_list.ml +++ b/src/naive_node_list.ml @@ -18,6 +18,7 @@ type node = Naive_tree.node type cell = { node : node; mutable next : cell } +type iterator = cell type t = { mutable length : int; mutable head : cell; @@ -41,18 +42,47 @@ let iter f l = let length l = l.length - +let is_empty l = l.head == nil let add n l = let ncell = { node = n; next = nil } in - if l.last == nil then - { length = 1; - head = ncell; - last = ncell } - else - let () = l.last.next <- ncell in - { length = l.length + 1; - head = l.head; - last = ncell } + if l.head == nil then begin + l.head <- ncell; + l.last <- ncell; + l.length <- 1 + end else begin + l.last.next <- ncell; + l.last <- ncell; + l.length <- l.length + 1 + end + +let push_back n l = add n l +let push_front n l = + let ncell = { node = n; + next = l.head } + in + if l.head == nil then begin + l.head <- ncell; + l.last <- ncell; + l.length <- 1; + end else begin + l.head <- ncell; + l.length <- l.length + 1; + end + +let head l = l.head +let last l = l.last +let next i = i.next +let value i = i.node +let finished i = i == nil + +let copy l = + let rec loop l2 i = + if finished i then l2 else begin + add (value i) l2; + loop l2 (next i) + end + in + loop (create ()) (head l) diff --git a/src/node_list.ml b/src/node_list.ml index 2219d5b..e9bb58a 100644 --- a/src/node_list.ml +++ b/src/node_list.ml @@ -17,9 +17,19 @@ module type S = sig type node type t + type iterator val create : unit -> t - val add : node -> t -> t + val add : node -> t -> unit + val push_front : node -> t -> unit + val push_back : node -> t -> unit val iter : (node -> unit) -> t -> unit val length : t -> int + val is_empty : t -> bool + val head : t -> iterator + val last : t -> iterator + val next : iterator -> iterator + val value : iterator -> node + val finished : iterator -> bool + val copy : t -> t end diff --git a/src/run.ml b/src/run.ml index 8eb58f9..f125346 100644 --- 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 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 - 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); - !res + res 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 - 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); diff --git a/src/tatoo.ml b/src/tatoo.ml index 24e212f..0987b6d 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -106,8 +106,8 @@ let main () = let module Naive = Run.Make(Naive_tree)(Naive_node_list) in let result_list = - - let root = Naive_node_list.(add (Naive_tree.root doc) (create())) in + let root = Naive_node_list.create () in + let () = Naive_node_list.add (Naive_tree.root doc) root in let f, msg = match !Options.parallel, !Options.compose with true, true -> -- 2.17.1