From 1f36c9e02bd0d96a97ec091d072df745054bcc1b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 12 May 2014 15:30:13 +0200
Subject: [PATCH] qtest

---
 .gitignore  |  2 +-
 circList.ml | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 20f09d16..d44b4ce6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,4 +8,4 @@ TAGS
 *.docdir
 setup.log
 setup.data
-qtest
+qtest*
diff --git a/circList.ml b/circList.ml
index 06d69e72..0b0670be 100644
--- a/circList.ml
+++ b/circList.ml
@@ -51,6 +51,14 @@ let of_list l =
 
 let length l = l.f_len + l.r_len
 
+(*$Q
+  (Q.list Q.small_int) (fun l -> \
+    l = [] || \
+    let q = of_list l in \
+    let _, q = next q in \
+    length q = List.length l)
+*)
+
 let cons x l = make (x::l.front) (l.f_len+1) l.rear l.r_len
 
 let snoc l x = make l.front l.f_len (x::l.rear) (l.r_len+1)
@@ -113,6 +121,12 @@ let gen l =
     l := l';
     Some x
 
+(*$Q
+  (Q.list Q.small_int) (fun l -> \
+    l = [] || let q = of_list l in \
+    gen q |> Gen.take (List.length l) |> Gen.to_list = l)
+  *)
+
 let seq l k =
   let r' = lazy (List.rev l.rear) in
   while true do