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

Make the safe-expansion check more liberal,

as suggested by Yann in merge request !9.
When a parameterized symbol does not use its parameter,
fewer graph edges are created.
Add two tests that were rejected but can be accepted
(expansion_ok, expansion_unused)
and another test which was accepted already
(self_ground).
The effect of this change is marginal: in practice,
very few graphs are affected by this change.
Nevertheless, with this change, the safe-expansion check
might be correct and complete (who knows?).
parent 962e6823
Pipeline #125387 passed with stages
in 25 seconds
......@@ -52,6 +52,43 @@ let formals : formal array =
|> List.concat
|> Array.of_list
(* If [nt/i] is a formal parameter, we may need to find the rule that defines
the symbol [nt] as well as the name of the [i]-th formal parameter in this
rule. *)
let info ((nt, i) : formal) : parameterized_rule * symbol =
let rule = try StringMap.find nt g.p_rules with Not_found -> assert false in
let x = try List.nth rule.pr_parameters i with Failure _ -> assert false in
rule, x
(* -------------------------------------------------------------------------- *)
(* For each formal parameter [nt/i], we want to know whether this parameter is
actually used, that is, whether it occurs in the right-hand side. *)
(* Note that we look for syntactic occurrences *anywhere* in the right-hand
side. We do *not* ignore occurrences that appear as the actual argument
of a parameterized symbol that happens to ignore its argument... That
would probably require a fixed point computation, and might be unsound:
expansion might diverge as soon as there is a syntactic occurrence
in the right-hand side. *)
let used_in_producer x ((_, param, _) : producer) =
Parameters.occurs x param
let used_in_branch x (branch : parameterized_branch) =
List.exists (used_in_producer x) branch.pr_producers
let used (formal : formal) : bool =
let rule, x = info formal in
List.exists (used_in_branch x) rule.pr_branches
(* Memoize this function. *)
let used : formal -> bool =
let module M = Fix.Memoize.ForType(struct type t = formal end) in
M.memoize used
(* -------------------------------------------------------------------------- *)
(* The graph edges are as follows. First, for every rule of the following form:
......@@ -97,6 +134,10 @@ let formals : formal array =
then we must create an edge of F/i to G/j, and this edge is safe if and
only if the context K is empty, i.e., X occurs at depth 0 in K[x]. *)
(* As an exception to the previous rule, if it is known that the parameterized
symbol G does not use its [j]-th parameter, then the edge of F/i to G/j
should not be created, nor should the applications inside K be inspected. *)
(* The code below has quadratic complexity because [Parameters.occurs_deep]
is expensive. In principle, we could achieve linear complexity by first
annotating subterm (bottom-up) with a Boolean flag that indicates whether
......@@ -116,15 +157,19 @@ let rec successors_parameter (f : edge -> formal -> unit) x (param : parameter)
| ParameterApp (sym, params) ->
let nt = value sym in
List.iteri (fun i param ->
(* Check, recursively, the applications that appear inside [param]. *)
successors_parameter f x param;
(* If [x] occurs in the [i]-th actual parameter of this application,
then there is an edge to the formal [nt, i]. Whether it is a safe
or dangerous edge depends on whether [x] occurs shallow or deep. *)
if Parameters.occurs_shallow x param then
f Safe (nt, i)
else if Parameters.occurs_deep x param then
f Dangerous (nt, i)
(* If it is known that [nt] does not use its [i]-th parameter, then
there is nothing to do here. *)
if used (nt, i) then begin
(* Check, recursively, the applications that appear inside [param]. *)
successors_parameter f x param;
(* If [x] occurs in the [i]-th actual parameter of this application,
then there is an edge to the formal [nt, i]. Whether it is a safe
or dangerous edge depends on whether [x] occurs shallow or deep. *)
if Parameters.occurs_shallow x param then
f Safe (nt, i)
else if Parameters.occurs_deep x param then
f Dangerous (nt, i)
end
) params
| ParameterAnonymous _ ->
assert false
......@@ -135,9 +180,8 @@ let successors_producer f x ((_, param, _) : producer) =
let successors_branch f x (branch : parameterized_branch) =
List.iter (successors_producer f x) branch.pr_producers
let successors f ((nt, i) : formal) =
let rule = try StringMap.find nt g.p_rules with Not_found -> assert false in
let x = try List.nth rule.pr_parameters i with Failure _ -> assert false in
let successors f (formal : formal) =
let rule, x = info formal in
List.iter (successors_branch f x) rule.pr_branches
(* -------------------------------------------------------------------------- *)
......
Grammar has 3 nonterminal symbols, among which 1 start symbols.
Grammar has 1 terminal symbols.
Grammar has 3 productions.
nullable(wrap(seq(wrap(A)))) = false
nullable(start) = false
nullable(seq(A)) = false
first(wrap(seq(wrap(A)))) = A
first(start) = A
first(seq(A)) = A
minimal(wrap(seq(wrap(A)))) = (* 1 *) A
minimal(start) = (* 1 *) A
minimal(seq(A)) = (* 1 *) A
follow(wrap(seq(wrap(A)))) = #
follow(start) = #
follow(seq(A)) = #
Built an LR(0) automaton with 5 states.
The grammar is SLR(1).
The construction mode is pager.
Built an LR(1) automaton with 5 states.
4 out of 5 states have a default reduction.
0 out of 5 states are represented.
0 out of 7 symbols keep track of their start position.
0 out of 7 symbols keep track of their end position.
4 out of 4 productions exploit shiftreduce optimization.
0 out of 5 states can peek at an error.
23 functions before inlining, 1 functions after inlining.
(* This grammar looks very much like ../bad/expansion_diverges.mly
except [wrap] does not use its argument, so expansion actually
terminates. This grammar can (and should) be accepted. *)
%token A
%start<unit> start
%%
start:
seq(A) {}
wrap(t):
A {}
seq(t):
| wrap(seq(wrap(t))) {}
%start start
%token A
%type <unit> start
%%
start:
_1 = seq_A_
{ ()}
wrap_seq_wrap_A___:
_1 = A
{ ()}
seq_A_:
_1 = wrap_seq_wrap_A___
{ ()}
%%
Grammar has 3 nonterminal symbols, among which 1 start symbols.
Grammar has 3 terminal symbols.
Grammar has 3 productions.
nullable(start) = false
nullable(ignore(foo(bar(A)))) = false
nullable(foo(A)) = false
first(start) = C
first(ignore(foo(bar(A)))) = C
first(foo(A)) = C
minimal(start) = (* 1 *) C
minimal(ignore(foo(bar(A)))) = (* 1 *) C
minimal(foo(A)) = (* 1 *) C
follow(start) = #
follow(ignore(foo(bar(A)))) = #
follow(foo(A)) = #
Built an LR(0) automaton with 5 states.
The grammar is SLR(1).
The construction mode is pager.
Built an LR(1) automaton with 5 states.
4 out of 5 states have a default reduction.
0 out of 5 states are represented.
0 out of 9 symbols keep track of their start position.
0 out of 9 symbols keep track of their end position.
4 out of 4 productions exploit shiftreduce optimization.
0 out of 5 states can peek at an error.
23 functions before inlining, 1 functions after inlining.
(* Because [ignore] does not use its argument, expansion terminates.
This grammar can (and should) be accepted. *)
%token A B C
%start<unit> start
%%
ignore(X):
C {}
foo(X):
ignore(foo(bar(X))) {}
bar(X):
B {}
start:
foo(A) {}
%start start
%token A
%token B
%token C
%type <unit> start
%%
ignore_foo_bar_A___:
_1 = C
{ ()}
foo_A_:
_1 = ignore_foo_bar_A___
{ ()}
start:
_1 = foo_A_
{ ()}
%%
Grammar has 3 nonterminal symbols, among which 1 start symbols.
Grammar has 3 terminal symbols.
Grammar has 5 productions.
nullable(start) = false
nullable(self(B)) = false
nullable(self(A)) = false
first(start) = C A
first(self(B)) = C A
first(self(A)) = C A
minimal(start) = (* 1 *) C
minimal(self(B)) = (* 1 *) C
minimal(self(A)) = (* 1 *) C
follow(start) = #
follow(self(B)) = #
follow(self(A)) = #
Built an LR(0) automaton with 9 states.
The grammar is SLR(1).
The construction mode is pager.
Built an LR(1) automaton with 9 states.
6 out of 9 states have a default reduction.
2 out of 9 states are represented.
0 out of 9 symbols keep track of their start position.
0 out of 9 symbols keep track of their end position.
6 out of 6 productions exploit shiftreduce optimization.
0 out of 9 states can peek at an error.
33 functions before inlining, 7 functions after inlining.
(* Because [self] ignores its argument (it calls itself recursively
with a ground actual argument), expansion terminates. This grammar
can (and should) be accepted. *)
%token A B C
%start<unit> start
%%
self(X):
A self(B) {}
| C {}
start:
self(A) {}
%start start
%token A
%token B
%token C
%type <unit> start
%%
self_A_:
_1 = A _2 = self_B_
{ ()}
| _1 = C
{ ()}
self_B_:
_1 = A _2 = self_B_
{ ()}
| _1 = C
{ ()}
start:
_1 = self_A_
{ ()}
%%
......@@ -2378,6 +2378,48 @@
(rule (alias execparser)
(action (diff ../good/execparser.exp execparser.out)))
(rule (target expansion_ok.opp.out) (deps ../good/expansion_ok.mly)
(action
(with-outputs-to expansion_ok.opp.out
(chdir ../good
(system
"timeout 60 %{bin:menhir} --only-preprocess %{deps} || echo 'TIMEOUT after 60 seconds.'")))))
(rule (alias expansion_ok)
(action (diff ../good/expansion_ok.opp.exp expansion_ok.opp.out)))
(rule (targets expansion_ok.out expansion_ok.out.timings)
(deps ../good/expansion_ok.mly)
(action
(with-outputs-to expansion_ok.out
(chdir ../good
(system
"timeout 60 %{bin:menhir} --explain -lg 2 -la 2 -lc 2 --timings-to ../src/expansion_ok.out.timings %{deps} || echo 'TIMEOUT after 60 seconds.'")))))
(rule (alias expansion_ok)
(action (diff ../good/expansion_ok.exp expansion_ok.out)))
(rule (target expansion_unused.opp.out) (deps ../good/expansion_unused.mly)
(action
(with-outputs-to expansion_unused.opp.out
(chdir ../good
(system
"timeout 60 %{bin:menhir} --only-preprocess %{deps} || echo 'TIMEOUT after 60 seconds.'")))))
(rule (alias expansion_unused)
(action (diff ../good/expansion_unused.opp.exp expansion_unused.opp.out)))
(rule (targets expansion_unused.out expansion_unused.out.timings)
(deps ../good/expansion_unused.mly)
(action
(with-outputs-to expansion_unused.out
(chdir ../good
(system
"timeout 60 %{bin:menhir} --explain -lg 2 -la 2 -lc 2 --timings-to ../src/expansion_unused.out.timings %{deps} || echo 'TIMEOUT after 60 seconds.'")))))
(rule (alias expansion_unused)
(action (diff ../good/expansion_unused.exp expansion_unused.out)))
(rule (target featherweight.opp.out) (deps ../good/featherweight.mly)
(action
(with-outputs-to featherweight.opp.out
......@@ -6755,6 +6797,27 @@
(rule (alias self) (action (diff ../good/self.exp self.out)))
(rule (target self_ground.opp.out) (deps ../good/self_ground.mly)
(action
(with-outputs-to self_ground.opp.out
(chdir ../good
(system
"timeout 60 %{bin:menhir} --only-preprocess %{deps} || echo 'TIMEOUT after 60 seconds.'")))))
(rule (alias self_ground)
(action (diff ../good/self_ground.opp.exp self_ground.opp.out)))
(rule (targets self_ground.out self_ground.out.timings)
(deps ../good/self_ground.mly)
(action
(with-outputs-to self_ground.out
(chdir ../good
(system
"timeout 60 %{bin:menhir} --explain -lg 2 -la 2 -lc 2 --timings-to ../src/self_ground.out.timings %{deps} || echo 'TIMEOUT after 60 seconds.'")))))
(rule (alias self_ground)
(action (diff ../good/self_ground.exp self_ground.out)))
(rule (target sibylfs-lem.0.4.0-parser.opp.out)
(deps ../good/sibylfs-lem.0.4.0-parser.mly)
(action
......@@ -9430,6 +9493,8 @@
(alias execparser)
(alias expansion-capture)
(alias expansion_diverges)
(alias expansion_ok)
(alias expansion_unused)
(alias expression)
(alias expression-expected)
(alias expressions)
......@@ -9714,6 +9779,7 @@
(alias sage)
(alias scilabParser)
(alias self)
(alias self_ground)
(alias semantic)
(alias semibar)
(alias semibarcomma)
......
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