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
module W : sig

  type word
  val epsilon: word
  val singleton: Terminal.t -> word
  val append: word -> word -> word
  val length: word -> int
126
  val first: word -> Terminal.t -> Terminal.t
127
  val elements: word -> Terminal.t list
128
  val print: word -> string
129 130 131

end = struct

132 133 134 135 136 137 138
  type word = Terminal.t list
  let epsilon = []
  let singleton t = [t]
  let append = (@)
  let length = List.length
  let first w z = match w with a :: _ -> a | [] -> z
  let elements w = w
139
  let print w =
140
    string_of_int (length w) ^ " " ^
141
    String.concat " " (List.map Terminal.print (elements w))
142

143 144 145 146
end

module Q = LowIntegerPriorityQueue

147 148 149 150
module Trie = struct

  let c = ref 0

151 152
  type trie = {
    identity: int;
153 154
    source: Lr1.node;
    target: Lr1.node;
155
    productions: Production.index list;
156
    transitions: trie SymbolMap.t;
157
  }
158

159
  let mktrie source target productions transitions =
160
    let identity = Misc.postincrement c in
161
    { identity; source; target; productions; transitions }
162

163 164
  let empty source =
    mktrie source source [] SymbolMap.empty
165

166 167
  let is_empty t =
    t.productions = [] && SymbolMap.is_empty t.transitions
168

169 170
  let accepts prod t =
    List.mem prod t.productions
171

172
  let rec insert target w prod t =
173 174
    match w with
    | [] ->
175
        mktrie t.source target (prod :: t.productions) t.transitions
176
    | a :: w ->
177 178 179 180 181 182 183 184 185 186
        match SymbolMap.find a (Lr1.transitions target) with
        | successor ->
            let child = mktrie t.source successor [] SymbolMap.empty in
            mktrie t.source target t.productions
              (update SymbolMap.add SymbolMap.find child id a t.transitions (insert successor w prod))
        | exception Not_found ->
            t

  let insert w prod t =
    insert t.source w prod t
187

188
  let derivative a t =
189
    try
190
      SymbolMap.find a t.transitions
191
    with Not_found ->
192 193 194 195
      assert false

  let has_derivative a t =
    SymbolMap.mem a t.transitions
196

197 198
  let compare t1 t2 =
    Pervasives.compare (t1.identity : int) t2.identity
199

200 201
  let rec size t =
    SymbolMap.fold (fun _ child accu -> size child + accu) t.transitions 1
202

203 204
end

205
type fact = {
206
  future: Trie.trie;
207
  word: W.word;
208
  lookahead: Terminal.t
209 210
}

211 212 213 214 215 216
let source fact =
  fact.future.Trie.source

let target fact =
  fact.future.Trie.target

217 218
let print_fact fact =
  Printf.fprintf stderr
219
    "from state %d to state %d via %s . %s\n%!"
220 221
    (Lr1.number (source fact))
    (Lr1.number (target fact))
222 223 224
    (W.print fact.word)
    (Terminal.print fact.lookahead)

225
let extensible fact sym =
226
  Trie.has_derivative sym fact.future
227

228 229 230 231 232 233
let foreach_terminal f =
  Terminal.iter (fun t ->
    if not (Terminal.equal t Terminal.error) then
      f t
  )

234 235 236 237 238 239 240 241
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
242
          (* could insert this branch only if viable -- leads to 12600 instead of 12900 in ocaml.mly --lalr *)
243
          Trie.insert w prod accu
244
        )
245
  ) (Lr1.transitions s) (Trie.empty s)
246

247 248 249 250 251 252
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)
POTTIER Francois's avatar
POTTIER Francois committed
253 254
    (* In principle, there is no need to insert the fact into the queue
       if [T] already stores a comparable fact. *)
255

256 257
let stars = ref 0

258
let init s =
259
  let trie = star s in
260 261 262 263
  let size = (Trie.size trie) in
  stars := !stars + size;
  Printf.fprintf stderr "State %d has a star of size %d\n.%!"
    (Lr1.number s) size;
POTTIER Francois's avatar
POTTIER Francois committed
264
  if not (Trie.is_empty trie) then
265 266
    foreach_terminal (fun z ->
      add {
267
        future = trie;
268 269 270 271
        word = W.epsilon;
        lookahead = z
      }
    )
272 273

module T : sig
274 275

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

284 285
  val stats: unit -> unit

286
end = struct
287

288 289
  (* We use a map of [target, z] to a map of [future, a] to facts. *)

290 291 292 293
  module M1 =
    MyMap(struct
      type t = Lr1.node * Terminal.t
      let compare (target1, z1) (target2, z2) =
294 295 296 297 298
        let c = Lr1.Node.compare target1 target2 in
        if c <> 0 then c else
        Terminal.compare z1 z2
    end)

299
  module M2 =
300
    MySet.Make(struct
301 302 303
      type t = fact
      let compare fact1 fact2 =
        let c = Trie.compare fact1.future fact2.future in
304
        if c <> 0 then c else
305 306
        let a1 = W.first fact1.word fact1.lookahead
        and a2 = W.first fact2.word fact2.lookahead in
307 308
        Terminal.compare a1 a2
    end)
309

310
  let m : M2.t M1.t ref =
311
    ref M1.empty
312

313 314
  let count = ref 0

315 316
  let register fact =
    let z = fact.lookahead in
317
    update_ref m (fun m1 ->
318
      M1.update M2.empty id (target fact, z) m1 (fun m2 ->
319 320 321 322
        let m2' = M2.add fact m2 in
        if m2 != m2' then
          incr count;
        m2'
323 324
      )
    )
325

326 327 328
  let query target z f =
    match M1.find (target, z) !m with
    | m2 ->
329
        M2.iter f m2
330 331
    | exception Not_found ->
        ()
332

333 334 335
  let stats () =
    Printf.fprintf stderr "T stores %d facts.\n%!" !count

336 337 338 339 340 341 342 343 344
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
345 346 347
     [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
348 349 350 351

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

355 356
  val stats: unit -> unit

357 358 359 360 361
end = struct

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

  module M =
362
    MyMap(struct
363 364 365 366 367 368 369 370 371 372 373 374 375 376
      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

377 378
  let count = ref 0

379
  let register s nt w z =
380
    let a = W.first w z in
381 382 383
    update_ref m (fun m ->
      M.update None some (s, nt, a, z) m (function
      | None ->
384
          incr count;
385 386
          w
      | Some earlier_w ->
387
          (* assert (W.length earlier_w <= W.length w); *)
388 389 390
          earlier_w
      )
    )
391

392 393 394 395
  let query s nt a z f =
    match M.find (s, nt, a, z) !m with
    | w -> f w
    | exception Not_found -> ()
396

397 398 399
  let stats () =
    Printf.fprintf stderr "E stores %d facts.\n%!" !count

400 401
end

402 403
let extend fact sym w z =
  assert (Terminal.equal fact.lookahead (W.first w z));
404
  {
405
    future = Trie.derivative sym fact.future;
406
    word = W.append fact.word w;
407
    lookahead = z
408 409
  }

410
let new_edge s nt w z =
POTTIER Francois's avatar
POTTIER Francois committed
411 412 413 414
  (*
  Printf.fprintf stderr "Considering reduction on %s in state %d\n"
    (Terminal.print z) (Lr1.number s);
  *)
415
  if E.register s nt w z then
416
    let sym = (Symbol.N nt) in
417
    T.query s (W.first w z) (fun fact ->
418
      if extensible fact sym then
419
        add (extend fact sym w z)
420
    )
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442

(* [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]. *)
  
443
  SymbolMap.iter (fun sym _ ->
444
    if extensible fact sym then
445 446 447
      match sym with
      | Symbol.T t ->

448 449 450 451
          (* 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. *)
452 453 454 455
          (**)

          if Terminal.equal fact.lookahead t then
            foreach_terminal (fun z ->
456
              add (extend fact sym (W.singleton t) z)
457 458 459 460 461 462 463 464 465 466 467 468
            )

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

470
          foreach_terminal (fun z ->
471 472
            E.query (target fact) nt fact.lookahead z (fun w ->
              add (extend fact sym w z)
473
            )
474
          )
475

476
  ) (Lr1.transitions (target fact));
477 478 479 480

  (* 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
481 482 483 484 485
     [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. *)
486 487
  (**)

488
  match has_reduction (target fact) fact.lookahead with
489
  | Some prod when Trie.accepts prod fact.future ->
490
      new_edge (source fact) (Production.nt prod) fact.word fact.lookahead
491 492 493
  | _ ->
      ()

494
let level = ref 0
495 496

let discover fact =
497
  if T.register fact then begin
498 499 500 501 502

    if W.length fact.word > ! level then begin
      Printf.fprintf stderr "Done with level %d.\n" !level;
      level := W.length fact.word;
      T.stats();
503 504
      E.stats();
      Printf.fprintf stderr "Q stores %d facts.\n%!" (Q.cardinal q)
505
    end;
506
(*
507
    incr facts;
508
    Printf.fprintf stderr "Facts = %d, current length = %d\n%!"
509
      !facts ();
510
    Printf.fprintf stderr "New fact:\n";
511
    print_fact fact;
512
*)
513
    consequences fact
514
  end
515

516
let main =
517
  Lr1.iter init;
518
  Printf.fprintf stderr "Cumulated star size: %d\n%!" !stars;
519
  Q.repeat q discover;
520 521
  Time.tick "Running LRijkstra";
  T.stats();
522
  E.stats()
523

524 525
(* ------------------------------------------------------------------------ *)

526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
(* 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')
      )

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

556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 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
(* 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. *)

636
  let _, _ = A.search (fun ((s, _), path) ->
637 638 639 640 641
    (* Debugging. TEMPORARY *)
    incr es;
    if !es mod 10000 = 0 then
      Printf.fprintf stderr "es = %d\n%!" !es;
    (* If [s] is a start state... *)
642
    let _, ws = A.reverse path in
POTTIER Francois's avatar
POTTIER Francois committed
643
    let ws = List.rev ws in
644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
    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
  ()

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

660
(* Forward search. *)
661

662
let forward () =
663

664
  let module A = Astar.Make(struct
665

666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686
    (* 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
687 688
      )

689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713
    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. *)

714
  Printf.fprintf stderr "Forward search:\n%!";
715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732
  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);
733
      (*
734 735 736 737 738
      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;
739
      *)
740 741 742
      assert (validate s s' w)
    end
  ) in
743 744 745
  Printf.fprintf stderr "Reachable (forward): %d states\n%!"
    (Lr1.NodeSet.cardinal !seen);
  !seen
746

747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
(* ------------------------------------------------------------------------ *)

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

779 780
let backward () =
  let reachable = ref Lr1.NodeSet.empty in
781 782 783
  Lr1.iter (fun s' ->
    begin match backward s' with
    | None ->
784
        Printf.fprintf stderr "infinity\n%!"
785
    | Some w ->
786 787
        Printf.fprintf stderr "%s\n%!" (W.print w);
        reachable := Lr1.NodeSet.add s' !reachable
788
    end;
789 790 791 792 793 794
    Printf.fprintf stderr "Edges so far: %d\n" !es
  );
  Printf.fprintf stderr "Reachable (backward): %d states\n%!"
    (Lr1.NodeSet.cardinal !reachable);
  !reachable

795 796
(* TEMPORARY what about the pseudo-token [#]? *)
(* TEMPORARY the code in this module should run only if --coverage is set *)
797 798

let () =
799
(*
800 801
  let b = backward() in
  Time.tick "Backward search";
802
*)
803 804
  let f = forward() in
  Time.tick "Forward search";
805 806
  ignore f
(*
807
  assert (Lr1.NodeSet.equal b f)
808
*)