aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/votour.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-23 10:31:53 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-23 10:31:53 +0100
commite5b128c7d4c2fd28a4ad7c5df8e48d485cd703f3 (patch)
tree645bff029a811018d80e77cb9f6743ff5cea6762 /checker/votour.ml
parentf6f80f68c890813522fabe5787181d0eaab8695e (diff)
Tail-recursive list traversal in votour.
Diffstat (limited to 'checker/votour.ml')
-rw-r--r--checker/votour.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 7fb7aee94..38f1ff9bc 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -195,13 +195,13 @@ let access_children vs os pos =
else raise Exit
let access_list v o pos =
- let rec loop o pos = match Repr.repr o with
- | INT 0 -> []
+ let rec loop o pos accu = match Repr.repr o with
+ | INT 0 -> List.rev accu
| BLOCK (0, [|hd; tl|]) ->
- (v, hd, 0 :: pos) :: loop tl (1 :: pos)
+ loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu)
| _ -> raise Exit
in
- Array.of_list (loop o pos)
+ Array.of_list (loop o pos [])
let access_block o = match Repr.repr o with
| BLOCK (tag, os) -> (tag, os)