Commit c98db5fe authored by POTTIER Francois's avatar POTTIER Francois

For every goal state [s'], stop as soon as we find one way of

triggering an error in this state.
This is about 10x faster for alphaCaml.mly. Still, alphaprolog.mly
does not go through.
parent 32c3f181
......@@ -51,6 +51,17 @@ let min_lazy p1 p2 =
| _ ->
min p1 (Lazy.force p2)
(* [until_finite] can be viewed as a variant of [min_lazy] where
we are happy as soon as we find a finite value. It can be viewed
as a minimum operation for the partial ordering where [Infinity]
is above everyone and everyone else is incomparable. *)
let until_finite p1 p2 =
match p1 with
| Finite _ ->
p1
| Infinity ->
Lazy.force p2
let add p1 p2 =
match p1, p2 with
| Finite (i1, xs1), Finite (i2, xs2) ->
......
......@@ -24,4 +24,6 @@ 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 until_finite: 'a t -> 'a t Lazy.t -> 'a t
val print: ('a -> string) -> 'a t -> string
......@@ -87,6 +87,13 @@ let foreach_terminal_in toks (f : Terminal.t -> property) : property =
P.min_lazy accu (lazy (f t))
) toks P.bottom
let foreach_terminal_until_finite (f : Terminal.t -> property) : property =
Terminal.fold (fun t accu ->
(* Here, laziness is important. We stop as soon as we obtain a
finite result. *)
P.until_finite accu (lazy (f t))
) P.bottom
(* This computes a minimum over the productions associated with [nt]. *)
let foreach_production nt (f : Production.index -> property) : property =
......@@ -323,7 +330,7 @@ let backward s s' : property =
P.bottom
else
foreach_terminal (fun z ->
foreach_terminal_until_finite (fun z ->
if causes_an_error s z then
P.add (backward s (s', z)) (P.singleton z)
else
......
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