Commit e3332614 authored by POTTIER Francois's avatar POTTIER Francois

At verbosity level `-lg 2`, for each nonterminal symbol `N`, display

a sentence (composed of terminal symbols) of minimal length generated
by `N`.
parent cd88d673
# Changes
## 2018/09/13
## 2018/09/18
* Install `.cmxs` files for menhirLib and menhirSdk.
......@@ -11,6 +11,10 @@
* Coq back-end: add a few newlines in the generated file for readability.
(Suggested by Bernhard Schommer.)
* At verbosity level `-lg 2`, for each nonterminal symbol `N`, display
a sentence (composed of terminal symbols) of minimal length generated
by `N`.
## 2018/09/05
* When `--explain` is enabled, always create a fresh `.conflicts` file
......
......@@ -11,12 +11,6 @@
(* *)
(******************************************************************************)
(* This is an enriched version of [CompletedNat], where we compute not just
numbers, but also sequences of matching length. *)
(* A property is either [Finite (n, xs)], where [n] is a natural number and
[xs] is a sequence of length [n]; or [Infinity]. *)
type 'a t =
| Finite of int * 'a Seq.seq
| Infinity
......@@ -30,17 +24,6 @@ let equal p1 p2 =
| _, _ ->
false
let compare p1 p2 =
match p1, p2 with
| Finite (i1, _), Finite (i2, _) ->
if i1 < i2 then -1 else if i1 = i2 then 0 else 1
| Infinity, Infinity ->
0
| Finite _, Infinity ->
-1
| Infinity, Finite _ ->
1
let bottom =
Infinity
......@@ -72,17 +55,6 @@ let min_lazy p1 p2 =
| _ ->
min p1 (p2())
let min_cutoff p1 p2 =
match p1 with
| Finite (0, _) ->
p1
| Finite (i1, _) ->
(* Pass [i1] as a cutoff value to [p2]. *)
min p1 (p2 i1)
| Infinity ->
(* Pass [max_int] to indicate no cutoff. *)
p2 max_int
let add p1 p2 =
match p1, p2 with
| Finite (i1, xs1), Finite (i2, xs2) ->
......@@ -97,22 +69,10 @@ let add_lazy p1 p2 =
| _ ->
add p1 (p2())
let add_cutoff cutoff p1 p2 =
match p1 with
| Infinity ->
Infinity
| Finite (i1, _) ->
if cutoff <= i1 then
(* Cut. No need to evaluate [p2]. *)
Infinity
else
(* Evaluate [p2], with an adjusted cutoff value. *)
add p1 (p2 (cutoff - i1))
let print conv p =
match p with
| Finite (i, xs) ->
string_of_int i ^ " " ^
Printf.sprintf "(* %d *) " i ^
String.concat " " (List.map conv (Seq.elements xs))
| Infinity ->
"infinity"
......
......@@ -11,11 +11,15 @@
(* *)
(******************************************************************************)
(* This is an enriched version of [CompletedNat], where we compute not just
numbers, but also sequences of matching length. *)
(* This is the lattice of the natural numbers, completed with [Infinity], and
ordered towards zero (i.e. [Infinity] is [bottom], [Finite 0] is [top]). *)
(* A property is either [Finite (n, xs)], where [n] is a natural number and
[xs] is a sequence of length [n]; or [Infinity]. *)
(* These numbers are further enriched with sequences of matching length. Thus,
a lattice element is either [Finite (n, xs)], where [n] is a natural number
and [xs] is a sequence of length [n]; or [Infinity]. The sequences [xs] are
ignored by the ordering (e.g., [compare] ignores them) but are nevertheless
constructed (e.g., [add] concatenates two sequences). They should be thought
of as witnesses, or proofs, that explain why the number [n] was obtained. *)
type 'a t =
| Finite of int * 'a Seq.seq
......@@ -25,8 +29,6 @@ val bottom: 'a t
val equal: 'a t -> 'b t -> bool
val is_maximal: 'a t -> bool
val compare: 'a t -> 'b t -> int
val epsilon: 'a t
val singleton: 'a -> 'a t
......@@ -36,9 +38,6 @@ val add: 'a t -> 'a t -> 'a t
val min_lazy: 'a t -> (unit -> 'a t) -> 'a t
val add_lazy: 'a t -> (unit -> 'a t) -> 'a t
val min_cutoff: 'a t -> (int -> 'a t) -> 'a t
val add_cutoff: (* cutoff: *) int -> 'a t -> (int -> 'a t) -> 'a t
val print: ('a -> string) -> 'a t -> string
val to_int: 'a t -> int
val extract: 'a t -> 'a list
......@@ -1059,6 +1059,35 @@ module FIRST =
let epsilon = TerminalSet.empty
end)
(* ------------------------------------------------------------------------ *)
(* 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 in principle more costly than [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
(struct
include CompletedNatWitness
type property = Terminal.t t
end)
(struct
open CompletedNatWitness
(* A terminal symbol has length 1. *)
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 = epsilon
end)
(* ------------------------------------------------------------------------ *)
let () =
......@@ -1104,8 +1133,13 @@ let () =
Printf.fprintf f "first(%s) = %s\n"
(Nonterminal.print false nt)
(TerminalSet.print (FIRST.nonterminal nt))
done;
for nt = Nonterminal.start to Nonterminal.n - 1 do
Printf.fprintf f "minimal(%s) = %s\n"
(Nonterminal.print false nt)
(CompletedNatWitness.print Terminal.print (MINIMAL.nonterminal nt))
done
)
)
let () =
if verbose then
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment