LRijkstra.ml 23.2 KB
Newer Older
1
open Grammar
2
module Q = LowIntegerPriorityQueue
3
module W = Terminal.Word(struct end) (* TEMPORARY wrap side effect in functor *)
4

5 6 7 8
(* Throughout, we ignore the [error] pseudo-token completely. We consider that
   it never appears on the input stream. Hence, any state whose incoming
   symbol is [error] is considered unreachable. *)

9 10
(* ------------------------------------------------------------------------ *)

11 12 13 14 15 16 17 18
(* We begin with a number of auxiliary functions that provide information
   about the LR(1) automaton. These functions could perhaps be moved to a
   separate module. We keep them here, for the moment, because they are not
   used anywhere else. *)

(* [reductions s z] is the list of reductions permitted in state [s] when the
   lookahead symbol is [z]. This is a list of zero or one elements. This does
   not take default reductions into account. *)
19

20
let reductions s z : Production.index list =
21 22 23 24 25
  try
    TerminalMap.find z (Lr1.reductions s)
  with Not_found ->
    []

26 27 28
(* [has_reduction s z] tells whether state [s] is willing to reduce some
   production (and if so, which one) when the lookahead symbol is [z]. It
   takes a possible default reduction into account. *)
29 30 31 32 33 34 35 36 37 38 39 40 41

let has_reduction s z : Production.index option =
  match Invariant.has_default_reduction s with
  | Some (prod, _) ->
      Some prod
  | None ->
      match reductions s z with
      | prod :: prods ->
          assert (prods = []);
          Some prod
      | [] ->
          None

42 43 44 45 46 47 48 49 50 51 52 53 54
(* [can_reduce s prod] indicates whether state [s] is able to reduce
   production [prod] (either as a default reduction, or as a normal
   reduction). *)

let can_reduce s prod =
  match Invariant.has_default_reduction s with
  | Some (prod', _) when prod = prod' ->
      true
  | _ ->
      TerminalMap.fold (fun _ prods accu ->
        accu || List.mem prod prods
      ) (Lr1.reductions s) false

55 56
(* [causes_an_error s z] tells whether state [s] will initiate an error on the
   lookahead symbol [z]. *)
57

58
let causes_an_error s z : bool =
59 60 61 62 63 64 65
  match Invariant.has_default_reduction s with
  | Some _ ->
      false
  | None ->
      reductions s z = [] &&
      not (SymbolMap.mem (Symbol.T z) (Lr1.transitions s))

66 67 68
(* [foreach_terminal f] applies the function [f] to every terminal symbol in
   turn, except [error]. *)

69 70 71 72 73 74
let foreach_terminal f =
  Terminal.iter (fun t ->
    if not (Terminal.equal t Terminal.error) then
      f t
  )

75 76 77 78 79
(* [foreach_terminal_not_causing_an_error s f] applies the function [f] to
   every terminal symbol [z] such that [causes_an_error s z] is false. This
   could be implemented in a naive manner using [foreach_terminal] and
   [causes_an_error]. This implementation is slightly more efficient. *)

80 81 82
let foreach_terminal_not_causing_an_error s f =
  match Invariant.has_default_reduction s with
  | Some _ ->
83
      (* There is a default reduction. No symbol causes an error. *)
84 85
      foreach_terminal f
  | None ->
86 87 88 89 90
      (* Enumerate every terminal symbol [z] for which there is a
         reduction. *)
      TerminalMap.iter (fun z _ ->
        if not (Terminal.equal z Terminal.error) then
          f z
91
      ) (Lr1.reductions s);
92 93
      (* Enumerate every terminal symbol [z] for which there is a
         transition. *)
94 95
      SymbolMap.iter (fun sym _ ->
        match sym with
96 97 98
        | Symbol.T z ->
            if not (Terminal.equal z Terminal.error) then
              f z
99 100 101 102
        | Symbol.N _ ->
            ()
      ) (Lr1.transitions s)

103 104
(* ------------------------------------------------------------------------ *)

POTTIER Francois's avatar
POTTIER Francois committed
105 106 107 108 109 110 111 112 113 114 115 116
(* Suppose [s] is a state that carries an outgoing edge labeled with a
   non-terminal symbol [nt]. We are interested in finding out how this edge
   can be taken. In order to do that, we must determine how, by starting in
   [s], one can follow a path that corresponds to (the right-hand side of) a
   production [prod] associated with [nt]. There are in general several such
   productions. The paths that they determine in the automaton form a "star".
   We represent the star rooted at [s] as a trie. For every state [s], the
   star rooted at [s] is constructed in advance, before the algorithm runs.
   While the algorithm runs, a point in the trie (that is, a sub-trie) tells
   us where we come form, where we are, and which production(s) we are hoping
   to reduce in the future. *)

117 118 119
module Trie : sig

  type trie
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135

  (* [star s] creates a (new) trie whose source is [s], populated with its
     branches. (There is one branch for every production [prod] associated
     with every non-terminal symbol [nt] for which [s] carries an outgoing
     edge.) If the star turns out to be trivial (i.e., without any branches)
     then [None] is returned. *)
  val star: Lr1.node -> trie option

  (* Every (sub-)trie has a unique identity. (One can think of it as its
     address.) [compare] compares the identity of two tries. This can be
     used, e.g., to set up a map whose keys are tries. *)
  val compare: trie -> trie -> int

  (* [source t] returns the source state of the (sub-)trie [t]. This is
     the root of the star of which [t] is a sub-trie. In other words, this
     tells us "where we come from". *)
136
  val source: trie -> Lr1.node
137 138 139 140
    
  (* [target t] returns the current state of the (sub-)trie [t]. This is
     the root of the sub-trie [t]. In other words, this tells us "where
     we are". *)
141 142
  val target: trie -> Lr1.node

143 144 145 146 147
  (* [accepts prod t] tells whether the current state of the trie [t] is
     the end of a branch associated with production [prod]. If so, this
     means that we have successfully followed a path that corresponds to
     the right-hand side of production [prod]. *)
  val accepts: Production.index -> trie -> bool
148

149 150 151 152 153 154 155 156
  (* [step sym t] is the immediate sub-trie of [t] along the symbol [sym].
     This function raises [Not_found] if [t] has no child labeled [sym]. *)
  val step: Symbol.t -> trie -> trie

  (* [verbose()] outputs debugging & performance information. *)
  val verbose: unit -> unit

end = struct
157

158 159
  (* A trie has the following structure. *)

160
  type trie = {
161 162 163
    (* A unique identity, used by [compare]. The trie construction code
       ensures that these numbers are indeed unique: see [fresh], [insert],
       [star]. *)
164
    identity: int;
165
    (* The root state of this star: "where we come from". *)
166
    source: Lr1.node;
167
    (* The current state, i.e., the root of this sub-trie: "where we are". *)
168
    target: Lr1.node;
169 170 171
    (* The productions that we can reduce in the current state. In other
       words, if this list is nonempty, then the current state is the end
       of one (or several) branches. It can nonetheless have children. *)
172
    productions: Production.index list;
173 174
    (* The children, or sub-tries. *)
    transitions: trie SymbolMap.t
175
  }
176

177
  (* This counter is used by [mktrie] to produce unique identities. *)
178 179
  let c = ref 0

180
  (* This smart constructor creates a new trie with a unique identity. *)
181
  let mktrie source target productions transitions =
182
    let identity = Misc.postincrement c in
183
    { identity; source; target; productions; transitions }
184

185 186
  exception DeadBranch

187
  let rec insert w prod t =
188 189
    match w with
    | [] ->
190 191 192 193 194 195 196 197 198 199 200 201 202
        (* We check whether the current state [t.target] is able to reduce
           production [prod]. (If [prod] cannot be reduced, the reduction
           action must have been suppressed by conflict resolution.) If not,
           then this branch is dead. This test is superfluous (i.e., it would
           be OK to conservatively assume that [prod] can be reduced) but
           allows us to build a slightly smaller star in some cases. *)
        if can_reduce t.target prod then
          (* We consume (update) the trie [t], so there is no need to allocate
             a new stamp. (Of course we could allocate a new stamp, but I prefer
             to be precise.) *)
          { t with productions = prod :: t.productions }
        else
          raise DeadBranch
203
    | a :: w ->
204
        (* Check if there is a transition labeled [a] out of [t.target]. If
205 206
           there is, we add a child to the trie [t]. If there isn't, then it
           must have been removed by conflict resolution. (Indeed, it must be
207 208 209
           present in a canonical automaton.) We could in this case return an
           unchanged sub-trie. We can do slightly better: we abort the whole
           insertion, so as to return an unchanged toplevel trie. *)
210
        match SymbolMap.find a (Lr1.transitions t.target) with
211
        | successor ->
212 213 214 215 216 217 218 219
            (* Find our child at [a], or create it. *)
            let t' =
              try
                SymbolMap.find a t.transitions
              with Not_found ->
                mktrie t.source successor [] SymbolMap.empty
            in
            (* Update the child [t']. *)
220
            let t' = insert w prod t' in
221 222
            (* Update [t]. Again, no need to allocate a new stamp. *)
            { t with transitions = SymbolMap.add a t' t.transitions }
223
        | exception Not_found ->
224
            raise DeadBranch
225

226 227 228 229 230
  (* [insert prod t] inserts a new branch, corresponding to production
     [prod], into the trie [t]. This function consumes its argument,
     which should no longer be used afterwards. *)
  let insert prod t =
    let w = Array.to_list (Production.rhs prod) in
231 232 233 234 235 236
    let save = !c in
    try
      insert w prod t
    with DeadBranch ->
      c := save;
      t
237

238 239 240 241 242 243 244 245 246 247 248 249 250
  (* [fresh s] creates a new empty trie whose source is [s]. *)
  let fresh source =
    mktrie source source [] SymbolMap.empty

  let star s =
    SymbolMap.fold (fun sym _ accu ->
      match sym with
      | Symbol.T _ ->
          accu
      | Symbol.N nt ->
          Production.foldnt nt accu insert
    ) (Lr1.transitions s) (fresh s)

251 252
  (* [nontrivial t] tests whether the trie [t] has any branches, i.e.,
     contains at least one sub-trie whose [productions] field is nonempty. *)
253 254 255
  let nontrivial t =
    not (t.productions = [] && SymbolMap.is_empty t.transitions)

256
  (* Redefine [star] to include a [nontrivial] test. *)
257 258 259 260 261 262 263
  let star s =
    let t = star s in
    if nontrivial t then
      Some t
    else
      None

264 265
  (* Accessors. *)

266 267 268 269 270 271
  let source t =
    t.source

  let target t =
    t.target

272 273 274
  let accepts prod t =
    List.mem prod t.productions

275
  let step a t =
276
    SymbolMap.find a t.transitions (* careful: may raise [Not_found] *)
277

278 279
  let compare t1 t2 =
    Pervasives.compare (t1.identity : int) t2.identity
280

281
  let verbose () =
282
    Printf.fprintf stderr "Cumulated star size: %d\n%!" !c
283

284 285
end

286
type fact = {
287
  future: Trie.trie;
288
  word: W.word;
289
  lookahead: Terminal.t
290 291
}

292
let source fact =
293
  Trie.source fact.future
294 295

let target fact =
296
  Trie.target fact.future
297

298 299 300 301
let q =
  Q.create()

let add fact =
302 303
  (* assert (not (causes_an_error (target fact) fact.lookahead)); *)

304 305
  (* The length of the word serves as the priority of this fact. *)
  Q.add q fact (W.length fact.word)
POTTIER Francois's avatar
POTTIER Francois committed
306 307
    (* In principle, there is no need to insert the fact into the queue
       if [T] already stores a comparable fact. *)
308 309

let init s =
310 311 312 313 314 315 316 317 318 319 320
  match Trie.star s with
  | Some trie ->
      foreach_terminal_not_causing_an_error s (fun z ->
        add {
          future = trie;
          word = W.epsilon;
          lookahead = z
        }
      )
  | None ->
      ()
321 322

module T : sig
323 324

  (* [register fact] registers the fact [fact]. It returns [true] if this fact
325
     is new, i.e., no fact concerning the same quintuple of [source], [future],
326 327 328 329 330
     [target], [a], and [z] was previously known. *)
  val register: fact -> bool

  (* [query target z f] enumerates all known facts whose target state is [target]
     and whose lookahead assumption is [z]. *)
331
  val query: Lr1.node -> Terminal.t -> (fact -> unit) -> unit
332

333
  val verbose: unit -> unit
334

335
end = struct
336

337 338 339 340 341 342 343 344 345 346 347
  (* This module implements a set of facts. Two facts are considered equal
     (for the purposes of this set) if they have the same [future], [a], and
     [z] fields. The [word] is not considered. Indeed, we are not interested
     in keeping track of several words that produce the same effect. Only the
     shortest such word is of interest. *)

  (* We need to query the set of facts in two ways. In [register], we need to
     test whether a fact is in the set. In [query], we need to find all facts
     that match a pair [target, z]. For this reason, we use a two-level table.
     The first level is a matrix indexed by [target] and [z]. At the second
     level, we find sets of facts. *)
348 349 350
(**)

  module M =
351
    MySet.Make(struct
352 353 354
      type t = fact
      let compare fact1 fact2 =
        let c = Trie.compare fact1.future fact2.future in
355
        if c <> 0 then c else
356 357
        let a1 = W.first fact1.word fact1.lookahead
        and a2 = W.first fact2.word fact2.lookahead in
358 359
        Terminal.compare a1 a2
    end)
360

361 362 363 364 365
  let table = (* a pretty large table... *)
    Array.make (Lr1.n * Terminal.n) M.empty

  let index target z =
    Terminal.n * (Lr1.number target) + Terminal.t2i z
366

367 368
  let count = ref 0

369
  let register fact =
370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388
    let target = target fact in
    let z = fact.lookahead in
    let i = index target z in
    let m = table.(i) in
    (* We crucially rely on the fact that [M.add] guarantees not to
       change the set if an ``equal'' fact already exists. Thus, a
       later, longer path is ignored in favor of an earlier, shorter
       path. *)
    let m' = M.add fact m in
    m != m' && begin
      incr count;
      table.(i) <- m';
      true
    end

  let query target z f =
    let i = index target z in
    let m = table.(i) in
    M.iter f m
389

390
  let verbose () =
391 392
    Printf.fprintf stderr "T stores %d facts.\n%!" !count

393 394 395 396 397 398 399 400 401
end

(* The module [E] is in charge of recording the non-terminal edges that we have
   discovered, or more precisely, the conditions under which these edges can be
   taken. *)

module E : sig

  (* [register s nt w z] records that, in state [s], the outgoing edge labeled
402 403 404
     [nt] can be taken by consuming the word [w], if the next symbol is [z].
     It returns [true] if this information is new. *)
  val register: Lr1.node -> Nonterminal.t -> W.word -> Terminal.t -> bool
405 406 407 408

  (* [query s nt a z] answers whether, in state [s], the outgoing edge labeled
     [nt] can be taken by consuming some word [w], under the assumption that
     the next symbol is [z], and under the constraint that the first symbol of
409 410
     [w.z] is [a]. *)
  val query: Lr1.node -> Nonterminal.t -> Terminal.t -> Terminal.t -> (W.word -> unit) -> unit
411

412
  val verbose: unit -> unit
413

414 415 416 417 418
end = struct

  (* For now, we implement a mapping of [s, nt, a, z] to [w]. *)

  module M =
419 420 421
    MySet.Make(struct
      type t = Nonterminal.t * Terminal.t * Terminal.t * W.word
      let compare (nt1, a1, z1, _w1) (nt2, a2, z2, _w2) =
422 423 424 425 426 427 428
        let c = Nonterminal.compare nt1 nt2 in
        if c <> 0 then c else
        let c = Terminal.compare a1 a2 in
        if c <> 0 then c else
        Terminal.compare z1 z2
    end)

429 430
  let table =
    Array.make Lr1.n M.empty
431

432 433
  let count = ref 0

434
  let register s nt w z =
435 436
    let i = Lr1.number s in
    let m = table.(i) in
437
    let a = W.first w z in
438
    let m' = M.add (nt, a, z, w) m in
439 440 441 442 443
    m != m' && begin
      incr count;
      table.(i) <- m';
      true
    end
444

445
  let query s nt a z f =
446 447
    let i = Lr1.number s in
    let m = table.(i) in
448 449 450
    let dummy = W.epsilon in
    match M.find (nt, a, z, dummy) m with
    | (_, _, _, w) -> f w
451
    | exception Not_found -> ()
452

453
  let verbose () =
454 455
    Printf.fprintf stderr "E stores %d facts.\n%!" !count

456 457
end

458
let new_edge s nt w z =
POTTIER Francois's avatar
POTTIER Francois committed
459 460 461 462
  (*
  Printf.fprintf stderr "Considering reduction on %s in state %d\n"
    (Terminal.print z) (Lr1.number s);
  *)
463
  if E.register s nt w z then
464
    let sym = Symbol.N nt in
465
    T.query s (W.first w z) (fun fact ->
466
      assert (Terminal.equal fact.lookahead (W.first w z));
467
      match Trie.step sym fact.future with
468
      | future ->
469
          if not (causes_an_error (Trie.target future) z) then
470 471 472 473 474 475 476
            add {
              future;
              word = W.append fact.word w;
              lookahead = z
            }
      | exception Not_found ->
          ()
477
    )
478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497

(* [consequences fact] is invoked when we discover a new fact (i.e., one that
   was not previously known). It studies the consequences of this fact. These
   consequences are of two kinds:

   - As in Dijkstra's algorithm, the new fact can be viewed as a newly
   discovered vertex. We study its (currently known) outgoing edges,
   and enqueue new facts in the priority queue.

   - Sometimes, a fact can also be viewed as a newly discovered edge.
   This is the case when the word from [fact.source] to [fact.target]
   represents a production of the grammar and [fact.target] is willing
   to reduce this production. We record the existence of this edge,
   and re-inspect any previously discovered vertices which are
   interested in this outgoing edge.
*)
(**)

let consequences fact =

498 499 500
  let target = target fact in

  (* 1. View [fact] as a vertex. Examine the transitions out of [target]. *)
501
  
502
  SymbolMap.iter (fun sym s' ->
503
    match Trie.step sym fact.future, sym with
504 505 506
    | exception Not_found -> ()
    | future, Symbol.T t ->

507
        (* 1a. There is a transition labeled [t] out of [target]. If
508 509 510 511 512 513 514 515
           the lookahead assumption [fact.lookahead] is compatible with [t],
           then we derive a new fact, where one more edge has been taken. We
           enqueue this new fact for later examination. *)
        (**)

        if Terminal.equal fact.lookahead t then
          let word = W.append fact.word (W.singleton t) in
          (* assert (Lr1.Node.compare future.Trie.target s' = 0); *)
516
          foreach_terminal_not_causing_an_error s' (fun z ->
517
            add { future; word; lookahead = z }
518
          )
519 520 521

    | future, Symbol.N nt ->

522
        (* 1b. There is a transition labeled [nt] out of [target]. We
523 524 525 526 527 528 529 530 531
           need to know how this nonterminal edge can be taken. We query for a
           word [w] that allows us to take this edge. The answer depends on
           the terminal symbol [z] that comes *after* this word: we try all
           such symbols. Furthermore, we need the first symbol of [w.z] to
           satisfy the lookahead assumption [fact.lookahead], so the answer
           also depends on this assumption. *)
        (**)

        foreach_terminal_not_causing_an_error s' (fun z ->
532
          E.query target nt fact.lookahead z (fun w ->
533 534 535 536 537 538 539 540
            assert (Terminal.equal fact.lookahead (W.first w z));
            add {
              future;
              word = W.append fact.word w;
              lookahead = z
            }
          )
        )
541

542
  ) (Lr1.transitions target);
543 544

  (* 2. View [fact] as a possible edge. This is possible if the path from
545 546
     [fact.source] to [target] represents a production [prod] and
     [target] is willing to reduce this production. We check that
547 548 549 550 551
     [fact.future] accepts [epsilon]. This guarantees that reducing [prod]
     takes us all the way back to [fact.source]. Thus, this production gives
     rise to an edge labeled [nt] -- the left-hand side of [prod] -- out of
     [fact.source]. This edge is subject to the lookahead assumption
     [fact.lookahead], so we record that. *)
552 553
  (**)

554
  match has_reduction target fact.lookahead with
555
  | Some prod when Trie.accepts prod fact.future ->
556
      new_edge (source fact) (Production.nt prod) fact.word fact.lookahead
557 558 559
  | _ ->
      ()

560
let level = ref 0
561

POTTIER Francois's avatar
POTTIER Francois committed
562 563
let done_with_level () =
  Printf.fprintf stderr "Done with level %d.\n" !level;
564 565
  T.verbose();
  E.verbose();
POTTIER Francois's avatar
POTTIER Francois committed
566 567
  Printf.fprintf stderr "Q stores %d facts.\n%!" (Q.cardinal q)

568
let discover fact =
569
  if T.register fact then begin
570
    if W.length fact.word > ! level then begin
POTTIER Francois's avatar
POTTIER Francois committed
571
      done_with_level();
572 573
      level := W.length fact.word;
    end;
574
    consequences fact
575
  end
576

POTTIER Francois's avatar
POTTIER Francois committed
577
let () =
578
  Lr1.iter init;
579
  Trie.verbose();
580
  Q.repeat q discover;
581
  Time.tick "Running LRijkstra";
POTTIER Francois's avatar
POTTIER Francois committed
582
  done_with_level()
583

584 585
(* ------------------------------------------------------------------------ *)

586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615
(* The following code validates the fact that an error can be triggered in
   state [s'] by beginning in the initial state [s] and reading the
   sequence of terminal symbols [w]. We use this for debugging purposes. *)

let fail msg =
  Printf.fprintf stderr "coverage: internal error: %s.\n%!" msg;
  false

open ReferenceInterpreter

let validate s s' w : bool =
  match
    ReferenceInterpreter.check_error_path (Lr1.nt_of_entry s) (W.elements w)
  with
  | OInputReadPastEnd ->
      fail "input was read past its end"
  | OInputNotFullyConsumed ->
      fail "input was not fully consumed"
  | OUnexpectedAccept ->
      fail "input was unexpectedly accepted"
  | OK state ->
      Lr1.Node.compare state s' = 0 ||
      fail (
        Printf.sprintf "error occurred in state %d instead of %d"
          (Lr1.number state)
          (Lr1.number s')
      )

(* ------------------------------------------------------------------------ *)

616 617 618 619 620 621 622
(* We now wish to determine, given a state [s'] and a terminal symbol [z], a
   minimal path that takes us from some entry state to state [s'] with [z] as
   the next (unconsumed) symbol. *)

(* This can be formulated as a search for a shortest path in a graph. The
   graph is not just the automaton, though. It is a (much) larger graph whose
   vertices are pairs [s, z] and whose edges are obtained by querying the
623
   module [E] above. *)
624

625
let forward () =
626

627
  let module A = Astar.Make(struct
628

629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649
    (* A vertex is a pair [s, z].
       [z] cannot be the [error] token. *)
    type node =
        Lr1.node * Terminal.t

    let equal (s'1, z1) (s'2, z2) =
      Lr1.Node.compare s'1 s'2 = 0 && Terminal.compare z1 z2 = 0

    let hash (s, z) =
      Hashtbl.hash (Lr1.number s, z)

    (* An edge is labeled with a word. *)
    type label =
      W.word

    (* Forward search from every [s, z], where [s] is an initial state. *)
    let sources f =
      foreach_terminal (fun z ->
        ProductionMap.iter (fun _ s ->
          f (s, z)
        ) Lr1.entry
650 651
      )

652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676
    let successors (s, z) edge =
      assert (not (Terminal.equal z Terminal.error));
      SymbolMap.iter (fun sym s' ->
        match sym with
        | Symbol.T t ->
            if Terminal.equal z t then
              let w = W.singleton t in
              foreach_terminal (fun z ->
                edge w 1 (s', z)
              )
        | Symbol.N nt ->
           foreach_terminal (fun z' ->
             E.query s nt z z' (fun w ->
               edge w (W.length w) (s', z')
             )
           )
      ) (Lr1.transitions s)

    let estimate _ =
      0

  end) in

  (* Search forward. *)

677
  Printf.fprintf stderr "Forward search:\n%!";
678
  let seen = ref Lr1.NodeSet.empty in
679
  let _, _ = A.search (fun ((s', z), path) ->
680 681 682 683 684 685 686 687 688 689 690 691 692 693
    if causes_an_error s' z && not (Lr1.NodeSet.mem s' !seen) then begin
      seen := Lr1.NodeSet.add s' !seen;
      (* An error can be triggered in state [s'] by beginning in the initial
         state [s] and reading the sequence of terminal symbols [w]. *)
      let (s, _), ws = A.reverse path in
      let w = List.fold_right W.append ws (W.singleton z) in
      Printf.fprintf stderr
        "An error can be reached from state %d to state %d:\n%!"
        (Lr1.number s)
        (Lr1.number s');
      Printf.fprintf stderr "%s\n%!" (W.print w);
      assert (validate s s' w)
    end
  ) in
694 695 696
  Printf.fprintf stderr "Reachable (forward): %d states\n%!"
    (Lr1.NodeSet.cardinal !seen);
  !seen
697

698
(* TEMPORARY the code in this module should run only if --coverage is set *)
699 700

let () =
701 702
  let f = forward() in
  Time.tick "Forward search";
703
  ignore f
704 705 706 707 708 709

(* TODO:
  subject to --coverage
  write to .coverage file
  collect performance data, correlated with star size and alphabet size; draw a graph
*)