Commit bbca9449 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Cleanup. Introduce [Analysis.first_prod_lookahead].

parent 00b1e9df
......@@ -22,34 +22,75 @@
- If the grammar has conflicts, conflict resolution removes some
(shift or reduce) actions, hence may suppress the shortest path. *)
(* TEMPORARY explain how we approach the problem *)
open Grammar
(* Using [CompletedNatWitness] means that we wish to compute shortest paths.
An alternative would be to use [BooleanWitness], which offers the same
interface. That would mean we wish to compute an arbitrary path. That
would be faster, but the paths thus obtained are (according to a quick
experiment) really far from optimal. *)
module P =
CompletedNatWitness
(* TEMPORARY avoid [error] token unless forced to use it *)
(* TEMPORARY implement and exploit [Lr1.ImperativeNodeMap] using an array *)
(* ------------------------------------------------------------------------ *)
type property =
Terminal.t P.t
(* First, we implement the computation of forward shortest paths in the
automaton. We view the automaton as a graph whose vertices are states. We
label each edge with the minimum length of a word that it generates. This
yields a lower bound on the actual distance to every state from any entry
state. *)
module ForwardAutomaton = struct
type vertex =
Lr1.node
let equal s1 s2 =
Lr1.Node.compare s1 s2 = 0
let hash s =
Hashtbl.hash (Lr1.number s)
type label =
int
let weight w = w
let sources f =
(* The sources are the entry states. *)
ProductionMap.iter (fun _ s -> f s) Lr1.entry
let successors edge s =
SymbolMap.iter (fun sym s' ->
(* The weight of the edge from [s] to [s'] is given by the function
[Grammar.Analysis.minimal_symbol]. *)
edge (CompletedNatWitness.to_int (Analysis.minimal_symbol sym)) s'
) (Lr1.transitions s)
end
let approximate : Lr1.node -> int =
let module D = Dijkstra.Make(ForwardAutomaton) in
D.search (fun (_, _, _) -> ())
(* Test. TEMPORARY *)
let () =
Lr1.iter (fun s ->
Printf.fprintf stderr
"State %d is at least %d steps away from an initial state.\n%!"
(Lr1.number s) (approximate s)
)
(* ------------------------------------------------------------------------ *)
(* Auxiliary functions. *)
(* This tests whether state [s] has a default reduction on [prod]. *)
let has_default_reduction s prod =
let has_default_reduction_on s prod =
match Invariant.has_default_reduction s with
| Some (prod', _) ->
prod = prod'
| None ->
false
(* This tests whether state [s] is willing to reduce production [prod]
when the lookahead symbol is [z]. This test takes a possible default
reduction into account. *)
(* This returns the list of reductions of [state] on token [z]. This
should be a list of zero or one elements. *)
let reductions s z =
try
......@@ -57,21 +98,14 @@ let reductions s z =
with Not_found ->
[]
(* This tests whether state [s] is willing to reduce production [prod]
when the lookahead symbol is [z]. This test takes a possible default
reduction into account. *)
let has_reduction s prod z : bool =
has_default_reduction s prod ||
has_default_reduction_on s prod ||
List.mem prod (reductions s z)
(* This tests whether state [s] has an outgoing transition labeled [sym].
If so, [s'] is passed to the continuation [k]. Otherwise, [P.bottom] is
returned. *)
let has_transition s sym k : property =
try
let s' = SymbolMap.find sym (Lr1.transitions s) in
k s'
with Not_found ->
P.bottom
(* This tests whether state [s] will initiate an error on the lookahead
symbol [z]. *)
......@@ -84,15 +118,27 @@ let causes_an_error s z =
reductions s z = [] &&
not (SymbolMap.mem (Symbol.T z) (Lr1.transitions s))
(* This computes [FIRST(alpha.z)], where [alpha] is the suffix determined
by [prod] and [i]. *)
(* Using [CompletedNatWitness] means that we wish to compute shortest paths.
An alternative would be to use [BooleanWitness], which offers the same
interface. That would mean we wish to compute an arbitrary path. That
would be faster, but the paths thus obtained are (according to a quick
experiment) really far from optimal. *)
module P =
CompletedNatWitness
type property =
Terminal.t P.t
let first prod i z =
let nullable, first = Analysis.nullable_first_prod prod i in
if nullable then
TerminalSet.add z first
else
first
(* This tests whether state [s] has an outgoing transition labeled [sym].
If so, [s'] is passed to the continuation [k]. Otherwise, [P.bottom] is
returned. *)
let has_transition s sym k : property =
try
let s' = SymbolMap.find sym (Lr1.transitions s) in
k s'
with Not_found ->
P.bottom
(* This computes a minimum over a set of terminal symbols. *)
......@@ -114,49 +160,6 @@ let foreach_production nt (f : Production.index -> property) : property =
P.min_lazy accu (fun () -> f prod)
)
(* The automaton, viewed as a graph, whose vertices are states.
We label each edge with the minimum length of a word that it
generates. This allows us to compute a lower bound on the
distance to every state from any entry state. *)
module ForwardAutomaton = struct
type vertex =
Lr1.node
let equal s1 s2 =
Lr1.Node.compare s1 s2 = 0
let hash s =
Hashtbl.hash (Lr1.number s)
type label =
int
let weight w = w
let sources f =
(* The sources are the entry states. *)
ProductionMap.iter (fun _ s -> f s) Lr1.entry
let successors edge s =
SymbolMap.iter (fun sym s' ->
edge (P.to_int (Analysis.minimal_symbol sym)) s'
) (Lr1.transitions s)
end
let approximate : Lr1.node -> int =
let module D = Dijkstra.Make(ForwardAutomaton) in
D.search (fun (_, _, _) -> ())
let () =
Lr1.iter (fun s ->
Printf.fprintf stderr
"State %d is at least %d steps away from an initial state.\n%!"
(Lr1.number s) (approximate s)
)
(* A question takes the form [s, a, prod, i, z], as defined below.
Such a question means: what is the set of terminal words [w]
......@@ -212,6 +215,9 @@ end
module QuestionMap =
Map.Make(Question)
let first =
Analysis.first_prod_lookahead
(* The following function answers a question. This requires a fixed point
computation. We have a certain amount of flexibility in how much
information we memoize; if we use a recursive call to [answer], we
......@@ -397,3 +403,6 @@ let () =
also: first compute an optimistic path using the simple algorithm
and check if this path is feasible in the real automaton
*)
(* TEMPORARY avoid [error] token unless forced to use it *)
(* TEMPORARY implement and exploit [Lr1.ImperativeNodeMap] using an array *)
(* TEMPORARY the code in this module should run only if --coverage is set *)
......@@ -1249,6 +1249,13 @@ module Analysis = struct
NULLABLE.production prod i,
FIRST.production prod i
let first_prod_lookahead prod i z =
let first = FIRST.production prod i in
if NULLABLE.production prod i then
TerminalSet.add z first
else
first
let explain_first_rhs (tok : Terminal.t) (rhs : Symbol.t array) (i : int) =
convert (explain tok rhs i)
......
......@@ -389,6 +389,13 @@ module Analysis : sig
val nullable_first_prod: Production.index -> int -> bool * TerminalSet.t
(* [first_prod_lookahead prod i t] computes [FIRST(alpha.t)], where [alpha]
is the suffix of the production defined by offset [i], and [t] is a
terminal symbol. The offset [i] must be contained between [0] and [n],
inclusive, where [n] is the length of production [prod]. *)
val first_prod_lookahead: Production.index -> int -> Terminal.t -> TerminalSet.t
(* [explain_first_rhs tok rhs i] explains why the token [tok] appears
in the FIRST set for the string of symbols found at offset [i] in
the array [rhs]. *)
......
Supports Markdown
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