Enriched the analysis [MINIMAL] to compute a word of minimal length

for every nonterminal symbol.

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. *)
+
+(* 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]. *)
+
+type 'a t =
+| Finite of int * 'a list Lazy.t
+| Infinity
+
+let equal p1 p2 =
+  match p1, p2 with
+  | Finite (i1, _), Finite (i2, _) ->
+      i1 = i2
+  | Infinity, Infinity ->
+      true
+  | _, _ ->
+      false
+
+let bottom =
+  Infinity
+
+let is_maximal p =
+  match p with
+  | Finite (0, _) ->
+      true
+  | _ ->
+      false
+
+let min p1 p2 =
+  match p1, p2 with
+  | Finite (i1, _), Finite (i2, _) ->
+      if i1 <= i2 then p1 else p2
+  | p, Infinity
+  | Infinity, p ->
+      p
+
+let min_lazy p1 p2 =
+  match p1 with
+  | Finite (0, _) ->
+      p1
+  | _ ->
+      min p1 (Lazy.force 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)
+      )
+  | _, _ ->
+      Infinity
+
+let add_lazy p1 p2 =
+  match p1 with
+  | Infinity ->
+      Infinity
+  | _ ->
+      add p1 (Lazy.force p2)
+
+let print conv p =
+  match p with
+  | Finite (i, xs) ->
+      string_of_int i ^ " " ^
+      String.concat " " (List.map conv (Lazy.force 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. *)
+
+(* 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]. *)
+
+type 'a t =
+| Finite of int * 'a list Lazy.t
+| Infinity
+
+val bottom: 'a t
+val equal: 'a t -> 'b t -> bool
+val is_maximal: 'a t -> bool
+
+val min: 'a t -> 'a t -> 'a t
+val add: 'a t -> 'a t -> 'a t
+
+val min_lazy: 'a t -> 'a t Lazy.t -> 'a t
+val add_lazy: 'a t -> 'a t Lazy.t -> 'a t
+
+val print: ('a -> string) -> 'a t -> string

src/grammar.ml

@@ -1014,27 +1014,32 @@ let () =
   done
 
 (* ------------------------------------------------------------------------ *)
-(* For every nonterminal symbol [nt], compute the minimal length of any word
-   generated by [nt]. This analysis subsumes [NONEMPTY] and [NULLABLE]. Indeed,
-   [nt] produces a nonempty language if only if the minimal length is finite;
-   [nt] is nullable if only if the minimal length is zero. *)
+(* For every nonterminal symbol [nt], compute a word of minimal length
+   generated by [nt]. This analysis subsumes [NONEMPTY] and [NULLABLE].
+   Indeed, [nt] produces a nonempty language if only if the minimal length is
+   finite; [nt] is nullable if only if the minimal length is zero. *)
 
-(* This analysis is more costly than the [NONEMPTY] and [NULLABLE], so it is
-   performed only on demand. *)
+(* This analysis is in principle more costly than the [NONEMPTY] and
+   [NULLABLE], so it is performed only on demand. In practice, it seems
+   to be very cheap: its cost is not measurable for any of the grammars
+   in our benchmark suite. *)
 
 module MINIMAL =
   GenericAnalysis
-    (CompletedNat)
     (struct
-      open CompletedNat
+      include CompletedNatWitness
+      type property = Terminal.t t
+     end)
+    (struct
+      open CompletedNatWitness
       (* A terminal symbol has length 1. *)
-      let terminal _ = Finite 1
+      let terminal t = Finite (1, lazy [t])
       (* 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
+      let epsilon = Finite (0, lazy [])
      end)
 
 (* ------------------------------------------------------------------------ *)
@@ -1055,7 +1060,7 @@ let () =
     for nt = Nonterminal.start to Nonterminal.n - 1 do
       Printf.fprintf f "minimal(%s) = %s\n"
 	(Nonterminal.print false nt)
-	(CompletedNat.print (MINIMAL.nonterminal nt))
+	(CompletedNatWitness.print Terminal.print (MINIMAL.nonterminal nt))
     done
   )