Removed some uses of [lazy] in favor of a more explicit module [Seq].

src/BooleanWitness.ml

 type 'a t =
-| Reachable of 'a list Lazy.t
+| Reachable of 'a Seq.seq
 | Unreachable
 
 let equal p1 p2 =
@@ -14,10 +14,10 @@ let bottom =
   Unreachable
 
 let epsilon =
-  Reachable (lazy [])
+  Reachable Seq.empty
 
 let singleton x =
-  Reachable (lazy [x])
+  Reachable (Seq.singleton x)
 
 let is_maximal p =
   match p with
@@ -43,10 +43,7 @@ let min_lazy p1 p2 =
 let add p1 p2 =
   match p1, p2 with
   | Reachable xs1, Reachable xs2 ->
-      Reachable (
-        (* The only list operation in the code! *)
-        lazy (Lazy.force xs1 @ Lazy.force xs2)
-      )
+      Reachable (Seq.append xs1 xs2)
   | _, _ ->
       Unreachable
 
@@ -60,6 +57,6 @@ let add_lazy p1 p2 =
 let print conv p =
   match p with
   | Reachable xs ->
-      String.concat " " (List.map conv (Lazy.force xs))
+      String.concat " " (List.map conv (Seq.elements xs))
   | Unreachable ->
       "unreachable"

src/BooleanWitness.mli

 (* This is an enriched version of [Boolean], where we compute not just a
    Boolean property, [Unreachable] or [Reachable], but also (in the latter
-   case) a path (a list). During the fixed point computation, instead of
-   manipulating actual lists, we manipulate only recipes for constructing
-   lists. These recipes can be evaluated by the user after the fixed point has
-   been reached. *)
+   case) a path (a sequence). *)
 
-(* A property is either [Reachable xs], where [xs] is a (recipe for
-   constructing a) path; or [Unreachable]. *)
+(* A property is either [Reachable xs], where [xs] is a path; or [Unreachable]. *)
 
 type 'a t =
-| Reachable of 'a list Lazy.t
+| Reachable of 'a Seq.seq
 | Unreachable
 
 val bottom: 'a t

src/CompletedNatWitness.ml

 (* This is an enriched version of [CompletedNat], where we compute not just
-   numbers, but also lists of matching length. During the fixed point
-   computation, instead of manipulating actual lists, we manipulate only
-   recipes for constructing lists. These recipes can be evaluated by the user
-   after the fixed point has been reached. *)
+   numbers, but also sequences of matching length. *)
 
 (* A property is either [Finite (n, xs)], where [n] is a natural number and
-   [xs] is a (recipe for constructing a) list of length [n]; or [Infinity]. *)
+   [xs] is a sequence of length [n]; or [Infinity]. *)
 
 type 'a t =
-| Finite of int * 'a list Lazy.t
+| Finite of int * 'a Seq.seq
 | Infinity
 
 let equal p1 p2 =
@@ -24,10 +21,10 @@ let bottom =
   Infinity
 
 let epsilon =
-  Finite (0, lazy [])
+  Finite (0, Seq.empty)
 
 let singleton x =
-  Finite (1, lazy [x])
+  Finite (1, Seq.singleton x)
 
 let is_maximal p =
   match p with
@@ -65,11 +62,7 @@ let until_finite p1 p2 =
 let add p1 p2 =
   match p1, p2 with
   | Finite (i1, xs1), Finite (i2, xs2) ->
-      Finite (
-        i1 + i2,
-        (* The only list operation in the code! *)
-        lazy (Lazy.force xs1 @ Lazy.force xs2)
-      )
+      Finite (i1 + i2, Seq.append xs1 xs2)
   | _, _ ->
       Infinity
 
@@ -84,6 +77,6 @@ let print conv p =
   match p with
   | Finite (i, xs) ->
       string_of_int i ^ " " ^
-      String.concat " " (List.map conv (Lazy.force xs))
+      String.concat " " (List.map conv (Seq.elements xs))
   | Infinity ->
       "infinity"

src/CompletedNatWitness.mli

 (* This is an enriched version of [CompletedNat], where we compute not just
-   numbers, but also lists of matching length. During the fixed point
-   computation, instead of manipulating actual lists, we manipulate only
-   recipes for constructing lists. These recipes can be evaluated by the user
-   after the fixed point has been reached. *)
+   numbers, but also sequences of matching length. *)
 
 (* A property is either [Finite (n, xs)], where [n] is a natural number and
-   [xs] is a (recipe for constructing a) list of length [n]; or [Infinity]. *)
+   [xs] is a sequence of length [n]; or [Infinity]. *)
 
 type 'a t =
-| Finite of int * 'a list Lazy.t
+| Finite of int * 'a Seq.seq
 | Infinity
 
 val bottom: 'a t

src/Seq.ml

+(* Sequences with constant time concatenation and linear-time conversion
+   to an ordinary list. *)
+
+type 'a seq =
+| SZero
+| SOne of 'a
+| SConcat of 'a seq * 'a seq
+
+let empty =
+  SZero
+
+let singleton x =
+  SOne x
+
+let append xs ys =
+  SConcat (xs, ys)
+
+let rec elements xs accu =
+  match xs with
+  | SZero ->
+      accu
+  | SOne x ->
+      x :: accu
+  | SConcat (xs1, xs2) ->
+      elements xs1 (elements xs2 accu)
+
+let elements xs =
+  elements xs []

src/Seq.mli

+(* Sequences with constant time concatenation and linear-time conversion
+   to an ordinary list. *)
+
+type 'a seq
+
+val empty: 'a seq
+val singleton: 'a -> 'a seq
+val append: 'a seq -> 'a seq -> 'a seq
+val elements: 'a seq -> 'a list

src/grammar.ml

@@ -1036,13 +1036,13 @@ module MINIMAL =
     (struct
       open CompletedNatWitness
       (* A terminal symbol has length 1. *)
-      let terminal t = Finite (1, lazy [t])
+      let terminal = singleton
       (* The length of an alternative is the minimum length of any branch. *)
       let disjunction = min_lazy
       (* The length of a sequence is the sum of the lengths of the members. *)
       let conjunction _ = add_lazy
       (* The epsilon sequence has length 0. *)
-      let epsilon = Finite (0, lazy [])
+      let epsilon = epsilon
      end)
 
 (* ------------------------------------------------------------------------ *)