LRijkstra.ml 23.2 KB
Newer Older
1 2
open Grammar

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
(* ------------------------------------------------------------------------ *)

(* 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. *)

let approximate : Lr1.node -> int =

  let module A = Astar.Make(struct

    type node =
      Lr1.node

    let equal s1 s2 =
      Lr1.Node.compare s1 s2 = 0

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

    type label =
      unit

    let sources f =
      (* The sources are the entry states. *)
      ProductionMap.iter (fun _ s -> f s) Lr1.entry

    let successors s edge =
      SymbolMap.iter (fun sym s' ->
        (* The weight of the edge from [s] to [s'] is given by the function
           [Grammar.Analysis.minimal_symbol]. If [sym] produces the empty
           language, this could be infinite, in which case no edge exists. *)
        match Analysis.minimal_symbol sym with
        | CompletedNatWitness.Finite (w, _) ->
            edge () w s'
        | CompletedNatWitness.Infinity ->
            ()
      ) (Lr1.transitions s)

    let estimate _ =
      (* A* with a zero [estimate] behaves like Dijkstra's algorithm. *)
      0

  end) in
        
  let distance, _ = A.search (fun (_, _) -> ()) in
  distance

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

(* This returns the list of reductions of [state] on token [z]. This
   is a list of zero or one elements. *)

let reductions s z =
  assert (not (Terminal.equal z Terminal.error));
  try
    TerminalMap.find z (Lr1.reductions s)
  with Not_found ->
    []

(* This tests whether state [s] is willing to reduce some production
   when the lookahead symbol is [z]. This test takes a possible default
   reduction into account. *)

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

(* This tests whether state [s] will initiate an error on the lookahead
   symbol [z]. *)

let causes_an_error s z =
  assert (not (Terminal.equal z Terminal.error));
  match Invariant.has_default_reduction s with
  | Some _ ->
      false
  | None ->
      reductions s z = [] &&
      not (SymbolMap.mem (Symbol.T z) (Lr1.transitions s))

93 94 95 96 97 98 99 100
  let id x = x
  let some x = Some x

let update_ref r f : bool =
  let v = !r in
  let v' = f v in
  v != v' && (r := v'; true)

101 102 103 104 105 106 107 108 109 110 111 112
let update add find none some key m f =
  match find key m with
  | data ->
      let data' = f (some data) in
      if data' == data then
        m
      else
        add key data' m
  | exception Not_found ->
      let data' = f none in
      add key data' m

113 114 115
module MyMap (X : Map.OrderedType) = struct
  include Map.Make(X)
  let update none some key m f =
116
    update add find none some key m f
117 118
end

119 120 121 122 123 124 125 126
module W : sig

  type word
  val epsilon: word
  val singleton: Terminal.t -> word
  val append: word -> word -> word
  val length: word -> int
  val first: word -> Terminal.t (* word must be nonempty *)
127
  val elements: word -> Terminal.t list
128
  val print: word -> string
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163

end = struct

  type word = {
    data: Terminal.t Seq.seq;
    length: int;
  }

  let epsilon = {
    data = Seq.empty;
    length = 0;
  }

  (* TEMPORARY tabulate? *)
  let singleton t = {
    data = Seq.singleton t;
    length = 1;
  }

  let append w1 w2 =
    if w1.length = 0 then
      w2
    else if w2.length = 0 then
      w1
    else {
      data = Seq.append w1.data w2.data;
      length = w1.length + w2.length;
    }

  let length w =
    w.length

  let first w =
    Seq.first w.data

164 165 166
  let elements w =
    Seq.elements w.data

167 168
  let print w =
    string_of_int w.length ^ " " ^
169
    String.concat " " (List.map Terminal.print (elements w))
170

171 172 173 174
end

module Q = LowIntegerPriorityQueue

175 176 177 178 179
module Trie = struct

  let c = ref 0

  type trie =
180
    | Trie of int * Production.index list * trie SymbolMap.t
181

182
  let mktrie prods children =
183
    let stamp = Misc.postincrement c in
184
    Trie (stamp, prods, children)
185 186

  let empty =
187
    mktrie [] SymbolMap.empty
188

189 190
  let is_empty (Trie (_, prods, children)) =
    prods = [] && SymbolMap.is_empty children
191

192 193
  let accepts prod (Trie (_, prods, _)) =
    List.mem prod prods
194 195 196 197

  let update : Symbol.t -> trie SymbolMap.t -> (trie -> trie) -> trie SymbolMap.t =
    update SymbolMap.add SymbolMap.find empty id

198
  let rec insert w prod (Trie (_, prods, children)) =
199 200
    match w with
    | [] ->
201
        mktrie (prod :: prods) children
202
    | a :: w ->
203
        mktrie prods (update a children (insert w prod))
204 205 206 207 208 209 210 211

  let derivative a (Trie (_, _, children)) =
    try
      SymbolMap.find a children
    with Not_found ->
      empty

  let compare (Trie (stamp1, _, _)) (Trie (stamp2, _, _)) =
212
    Pervasives.compare (stamp1 : int) stamp2
213 214 215

end

216 217 218
type fact = {
  source: Lr1.node;
  target: Lr1.node;
219
  future: Trie.trie;
220
  word: W.word;
221
  lookahead: Terminal.t
222 223
}

224 225
let print_fact fact =
  Printf.fprintf stderr
226
    "from state %d to state %d via %s . %s\n%!"
227 228 229 230 231
    (Lr1.number fact.source)
    (Lr1.number fact.target)
    (W.print fact.word)
    (Terminal.print fact.lookahead)

232 233
let extensible fact sym =
  not (Trie.is_empty (Trie.derivative sym fact.future))
234

235 236 237 238 239 240
let foreach_terminal f =
  Terminal.iter (fun t ->
    if not (Terminal.equal t Terminal.error) then
      f t
  )

241 242 243 244 245 246 247 248
let star s : Trie.trie =
  SymbolMap.fold (fun sym _ accu ->
    match sym with
    | Symbol.T _ ->
        accu
    | Symbol.N nt ->
        Production.foldnt nt accu (fun prod accu ->
          let w = Array.to_list (Production.rhs prod) in
249
          Trie.insert w prod accu
250 251 252
        )
  ) (Lr1.transitions s) Trie.empty

253 254 255 256 257 258 259 260
let q =
  Q.create()

let add fact =
  (* The length of the word serves as the priority of this fact. *)
  Q.add q fact (W.length fact.word)

let init s =
261
  let trie = star s in
POTTIER Francois's avatar
POTTIER Francois committed
262
  if not (Trie.is_empty trie) then
263 264 265 266
    foreach_terminal (fun z ->
      add {
        source = s;
        target = s;
267
        future = trie;
268 269 270 271
        word = W.epsilon;
        lookahead = z
      }
    )
272

273 274 275
let first w z =
  if W.length w > 0 then W.first w else z

276
module T : sig
277 278

  (* [register fact] registers the fact [fact]. It returns [true] if this fact
279
     is new, i.e., no fact concerning the same quintuple of [source], [future],
280 281 282 283 284
     [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]. *)
285
  val query: Lr1.node -> Terminal.t -> (fact -> unit) -> unit
286

287 288
  val stats: unit -> unit

289
end = struct
290

291 292 293 294 295 296
  (* We use a map of [target, z] to a map of [future, a] to facts. *)

  (* A minor and subtle optimization: we need not use [source] as part
     of the key in [M2], because [future] determines [source]. Indeed,
     [future] is (a sub-trie of) the trie generated by [init source],
     and every trie contains unique stamps. *)
297

298 299 300 301
  module M1 =
    MyMap(struct
      type t = Lr1.node * Terminal.t
      let compare (target1, z1) (target2, z2) =
302 303 304 305 306
        let c = Lr1.Node.compare target1 target2 in
        if c <> 0 then c else
        Terminal.compare z1 z2
    end)

307 308
  module M2 =
    MyMap(struct
309 310
      type t = Trie.trie * Terminal.t
      let compare (future1, a1) (future2, a2) =
311
        let c = Trie.compare future1 future2 in
312 313 314
        if c <> 0 then c else
        Terminal.compare a1 a2
    end)
315

316 317
  let m : fact M2.t M1.t ref =
    ref M1.empty
318

319 320
  let count = ref 0

321 322 323
  let register fact =
    let z = fact.lookahead in
    let a = first fact.word z in
324 325
    update_ref m (fun m1 ->
      M1.update M2.empty id (fact.target, z) m1 (fun m2 ->
326
        M2.update None some (fact.future, a) m2 (function
327
          | None ->
328
              incr count;
329 330 331 332 333 334 335
              fact
          | Some earlier_fact ->
              assert (W.length earlier_fact.word <= W.length fact.word);
              earlier_fact
        )
      )
    )
336

337 338 339 340 341 342 343 344
  let query target z f =
    match M1.find (target, z) !m with
    | m2 ->
        M2.iter (fun _ fact ->
          f fact
        ) m2
    | exception Not_found ->
        ()
345

346 347 348
  let stats () =
    Printf.fprintf stderr "T stores %d facts.\n%!" !count

349 350 351 352 353 354 355 356 357
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
358 359 360
     [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
361 362 363 364

  (* [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
365 366
     [w.z] is [a]. *)
  val query: Lr1.node -> Nonterminal.t -> Terminal.t -> Terminal.t -> (W.word -> unit) -> unit
367

368 369
  val stats: unit -> unit

370 371 372 373 374
end = struct

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

  module M =
375
    MyMap(struct
376 377 378 379 380 381 382 383 384 385 386 387 388 389
      type t = Lr1.node * Nonterminal.t * Terminal.t * Terminal.t
      let compare (s1, nt1, a1, z1) (s2, nt2, a2, z2) =
        let c = Lr1.Node.compare s1 s2 in
        if c <> 0 then c else
        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)

  let m =
    ref M.empty

390 391
  let count = ref 0

392 393
  let register s nt w z =
    let a = first w z in
394 395 396
    update_ref m (fun m ->
      M.update None some (s, nt, a, z) m (function
      | None ->
397
          incr count;
398 399 400 401 402 403
          w
      | Some earlier_w ->
          assert (W.length earlier_w <= W.length w);
          earlier_w
      )
    )
404

405 406 407 408
  let query s nt a z f =
    match M.find (s, nt, a, z) !m with
    | w -> f w
    | exception Not_found -> ()
409

410 411 412
  let stats () =
    Printf.fprintf stderr "E stores %d facts.\n%!" !count

413 414
end

415
let extend fact target sym w z =
416
  assert (Terminal.equal fact.lookahead (first w z));
417 418
  let future = Trie.derivative sym fact.future in
  assert (not (Trie.is_empty future));
419 420 421
  {
    source = fact.source;
    target = target;
422
    future = future;
423
    word = W.append fact.word w;
424
    lookahead = z
425 426
  }

427
let new_edge s nt w z =
POTTIER Francois's avatar
POTTIER Francois committed
428 429 430 431
  (*
  Printf.fprintf stderr "Considering reduction on %s in state %d\n"
    (Terminal.print z) (Lr1.number s);
  *)
432
  if E.register s nt w z then
433
    let sym = (Symbol.N nt) in
434
    let s' = try SymbolMap.find sym (Lr1.transitions s) with Not_found -> assert false in
435
    T.query s (first w z) (fun fact ->
436
      if extensible fact sym then
437
        add (extend fact s' sym w z)
438
    )
439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460

(* [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 =

  (* 1. View [fact] as a vertex. Examine the transitions out of [fact.target]. *)
  
461 462
  SymbolMap.iter (fun sym s ->
    if extensible fact sym then
463 464 465
      match sym with
      | Symbol.T t ->

466 467 468 469
          (* 1a. There is a transition labeled [t] out of [fact.target]. If
             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. *)
470 471 472 473
          (**)

          if Terminal.equal fact.lookahead t then
            foreach_terminal (fun z ->
474
              add (extend fact s sym (W.singleton t) z)
475 476 477 478 479 480 481 482 483 484 485 486
            )

      | Symbol.N nt ->

          (* 1b. There is a transition labeled [nt] out of [fact.target]. We
             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. *)
          (**)
487

488
          foreach_terminal (fun z ->
489
            E.query fact.target nt fact.lookahead z (fun w ->
490
              add (extend fact s sym w z)
491
            )
492
          )
493

494
  ) (Lr1.transitions fact.target);
495 496 497 498

  (* 2. View [fact] as a possible edge. This is possible if the path from
     [fact.source] to [fact.target] represents a production [prod] and
     [fact.target] is willing to reduce this production. We check that
499 500 501 502 503
     [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. *)
504 505
  (**)

506
  match has_reduction fact.target fact.lookahead with
507
  | Some prod when Trie.accepts prod fact.future ->
508 509 510 511
      new_edge fact.source (Production.nt prod) fact.word fact.lookahead
  | _ ->
      ()

512
let level = ref 0
513 514

let discover fact =
515
  if T.register fact then begin
516 517 518 519 520 521 522

    if W.length fact.word > ! level then begin
      Printf.fprintf stderr "Done with level %d.\n" !level;
      level := W.length fact.word;
      T.stats();
      E.stats()
    end;
523
(*
524
    incr facts;
525
    Printf.fprintf stderr "Facts = %d, current length = %d\n%!"
526
      !facts ();
527
    Printf.fprintf stderr "New fact:\n";
528
    print_fact fact;
529
*)
530
    consequences fact
531
  end
532

533
let main =
534
  Lr1.iter init;
535
  Q.repeat q discover;
536 537 538
  Time.tick "Running LRijkstra";
  T.stats();
  E.stats()
539

540 541
(* ------------------------------------------------------------------------ *)

542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571
(* 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')
      )

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

572 573 574 575 576 577 578 579 580 581 582 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 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
(* 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
   module [E] above. Because we perform a backward search, from [s', z] to any
   entry state, we use reverse edges, from a state to its predecessors in the
   automaton. *)

(* Debugging. TEMPORARY *)
let es = ref 0

exception Success of Lr1.node * W.word

let backward (s', z) : unit =

  let module A = Astar.Make(struct

    (* 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

    (* Backward search from the single source [s', z]. *)
    let sources f = f (s', z)

    let successors (s', z) edge =
      assert (not (Terminal.equal z Terminal.error));
      match Lr1.incoming_symbol s' with
      | None ->
          (* An entry state has no predecessor states. *)
          ()

      | Some (Symbol.T t) ->
          if not (Terminal.equal t Terminal.error) then
            (* There is an edge from [s] to [s'] labeled [t] in the automaton.
               Thus, our graph has an edge from [s', z] to [s, t], labeled [t]. *)
            let w = W.singleton t in
            List.iter (fun s ->
              edge w 1 (s, t)
            ) (Lr1.predecessors s')

      | Some (Symbol.N nt) ->
          (* There is an edge from [s] to [s'] labeled [nt] in the automaton.
             For every letter [a], we query [E] for a word [w] that begins in
             [s] and allows us to take the edge labeled [nt] when the
             lookahead symbol is [z]. Such a path [w] takes us from [s, a] to
             [s', z]. Thus, our graph has an edge, labeled [w], in the reverse
             direction. *)
          (**)
          List.iter (fun s ->
            foreach_terminal (fun a ->
              assert (not (Terminal.equal a Terminal.error));
              E.query s nt a z (fun w ->
                edge w (W.length w) (s, a)
              )
            )
          ) (Lr1.predecessors s')

    let estimate (s', _z) =
      approximate s'

  end) in

  (* Search backwards from [s', z], stopping as soon as an entry state [s] is
     reached. In that case, return the state [s] and the path that has been
     found. *)

652
  let _, _ = A.search (fun ((s, _), path) ->
653 654 655 656 657
    (* Debugging. TEMPORARY *)
    incr es;
    if !es mod 10000 = 0 then
      Printf.fprintf stderr "es = %d\n%!" !es;
    (* If [s] is a start state... *)
658
    let _, ws = A.reverse path in
POTTIER Francois's avatar
POTTIER Francois committed
659
    let ws = List.rev ws in
660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675
    if Lr1.incoming_symbol s = None then
      (* [labels] is a list of properties. Projecting onto the second
         component yields a list of paths (sequences of terminal symbols),
         which we concatenate to obtain a path. Because the edges that were
         followed last are in front of the list, and because this is a
         reverse graph, we obtain a path that makes direct sense: it is a
         sequence of terminal symbols that will take the automaton into
         state [s'] if the next (unconsumed) symbol is [z]. We append [z]
         at the end of this path. *)
      let w = List.fold_right W.append ws (W.singleton z) in
      raise (Success (s, w))
  ) in
  ()

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

676
(* Forward search. *)
677

678
let forward () =
679

680
  let module A = Astar.Make(struct
681

682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702
    (* 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
703 704
      )

705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729
    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. *)

730
  Printf.fprintf stderr "Forward search:\n%!";
731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748
  let es = ref 0 in
  let seen = ref Lr1.NodeSet.empty in
  let _, _ = A.search (fun ((s', z), (path : A.path)) ->
    (* Debugging. TEMPORARY *)
    incr es;
    if !es mod 10000 = 0 then
      Printf.fprintf stderr "es = %d\n%!" !es;
    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);
749
      (*
750 751 752 753 754
      let approx = approximate s'
      and real = W.length w - 1 in
      assert (approx <= real);
      if approx < real then
        Printf.fprintf stderr "Approx = %d, real = %d\n" approx real;
755
      *)
756 757 758
      assert (validate s s' w)
    end
  ) in
759 760 761
  Printf.fprintf stderr "Reachable (forward): %d states\n%!"
    (Lr1.NodeSet.cardinal !seen);
  !seen
762

763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794
(* ------------------------------------------------------------------------ *)

(* For each state [s'] and for each terminal symbol [z] such that [z] triggers
   an error in [s'], backward search is performed. For each state [s'], we
   stop as soon as one [z] is found, i.e., as soon as one way of causing an
   error in state [s'] is found. *)

let backward s' : W.word option =
  
  (* Debugging. TEMPORARY *)
  Printf.fprintf stderr
    "Attempting to reach an error in state %d:\n%!"
    (Lr1.number s');

  try

    (* This loop stops as soon as we are able to reach one error at [s']. *)
    Terminal.iter (fun z ->
      if not (Terminal.equal z Terminal.error) && causes_an_error s' z then
        backward (s', z)
    );
    (* No error can be triggered in state [s']. *)
    None

  with Success (s, w) ->
    (* An error can be triggered in state [s'] by beginning in the initial
       state [s] and reading the sequence of terminal symbols [w]. *)
    assert (validate s s' w);
    Some w

(* Test. TEMPORARY *)

795 796
let backward () =
  let reachable = ref Lr1.NodeSet.empty in
797 798 799
  Lr1.iter (fun s' ->
    begin match backward s' with
    | None ->
800
        Printf.fprintf stderr "infinity\n%!"
801
    | Some w ->
802 803
        Printf.fprintf stderr "%s\n%!" (W.print w);
        reachable := Lr1.NodeSet.add s' !reachable
804
    end;
805 806 807 808 809 810
    Printf.fprintf stderr "Edges so far: %d\n" !es
  );
  Printf.fprintf stderr "Reachable (backward): %d states\n%!"
    (Lr1.NodeSet.cardinal !reachable);
  !reachable

811 812
(* TEMPORARY what about the pseudo-token [#]? *)
(* TEMPORARY the code in this module should run only if --coverage is set *)
813 814

let () =
815
(*
816 817
  let b = backward() in
  Time.tick "Backward search";
818
*)
819 820
  let f = forward() in
  Time.tick "Forward search";
821 822
  ignore f
(*
823
  assert (Lr1.NodeSet.equal b f)
824
*)