(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

open Grammar

exception Oops

module Run (X : sig

  (* A restricted set of tokens of interest. *)

  val tokens: TerminalSet.t

  (* A state of the (merged) LR(1) automaton that we're trying to
     simulate. *)

  val goal: Lr1.node

end) = struct

  (* First, let's restrict our interest to the nodes of the merged
     LR(1) automaton that can reach the goal node. Some experiments
     show that this can involve one tenth to one half of all nodes.
     This optimization seems minor, but is easy to implement. *)

  let relevant =
    Lr1.reverse_dfs X.goal

  (* Second, all of the states that we shall consider are restricted
     to the set of tokens of interest. This is an important idea: by
     abstracting away some information, we make the construction much
     faster. *)

  let restrict =
    Lr0.restrict X.tokens

  (* Constructing the automaton. The automaton is represented as a
     graph. States are never merged -- this is a canonical LR(1)
     construction!

     As we go, we record the correspondence between nodes in this
     automaton and nodes in the merged LR(1) automaton. This allows
     us to tell when we have reached the desired place.

     This also allows us not to follow transitions that have already
     been eliminated, in the merged automaton, via resolution of
     shift/reduce conflicts. Whenever we follow a transition in the
     canonical LR(1) automaton, we check that the corresponding
     transition is legal in the merged LR(1) automaton.

     The automaton is explored breadth-first and shortest paths from
     every node to one of the start nodes are recorded. *)

  type node = {
      state: Lr0.lr1state;
      ancestor: (Symbol.t * node) option;
      shadow: Lr1.node;
    }

  (* A queue of pending nodes, whose successors should be explored. *)

  let queue : node Queue.t =
    Queue.create()

  (* Mapping of LR(0) state numbers to lists of nodes. *)

  let map : node list array =
    Array.make Lr0.n []

  (* Exploring a state. This creates a new node, if necessary, and
     enqueues it for further exploration. *)

  exception Goal of node * Terminal.t

  let explore ancestor shadow (state : Lr0.lr1state) : unit =

    (* Find all existing nodes that share the same LR(0) core. *)

    let k = Lr0.core state in
    assert (k < Lr0.n);
    let similar = map.(k) in

    (* Check whether one of these nodes coincides with the candidate
       new node. If so, stop. This check requires comparing not only
       the states of the partial, canonical automaton, but also their
       shadows in the full, merged automaton. This is because a single
       state of the canonical automaton may be reached along several
       different paths, leading to distinct shadows in the merged
       automaton, and we must explore all of these paths in order to
       ensure that we eventually find a goal node. *)

    if not (List.exists (fun node ->
      Lr0.equal state node.state && shadow == node.shadow
    ) similar) then begin

      (* Otherwise, create a new node. *)

      let node = {
        state = state;
        ancestor = ancestor;
        shadow = shadow;
      } in

      map.(k) <- node :: similar;
      Queue.add node queue;

      (* Check whether this is a goal node. A node [N] is a goal node
         if (i) [N] has a conflict involving one of the tokens of
         interest and (ii) [N] corresponds to the goal node, that is,
         the path that leads to [N] in the canonical LR(1) automaton
         leads to the goal node in the merged LR(1) automaton. Note
         that these conditions do not uniquely define [N]. *)

      if shadow == X.goal then
        let can_reduce =
          ref TerminalSet.empty in
        let reductions1 : Production.index list TerminalMap.t =
          Lr1.reductions shadow in
        List.iter (fun (toks, prod) ->
          TerminalSet.iter (fun tok ->

            (* We are looking at a [(tok, prod)] pair -- a reduction
               in the canonical automaton state. *)

            (* Check that this reduction, which exists in the canonical
               automaton state, also exists in the merged automaton --
               that is, it wasn't suppressed by conflict resolution. *)

            if List.mem prod (TerminalMap.lookup tok reductions1) then

              try
                let (_ : Lr1.node) =
                  SymbolMap.find (Symbol.T tok) (Lr1.transitions shadow)
                in
                (* Shift/reduce conflict. *)
                raise (Goal (node, tok))
              with Not_found ->
                let toks = !can_reduce in
                (* We rely on the property that [TerminalSet.add tok toks]
                   preserves physical equality when [tok] is a member of
                   [toks]. *)
                let toks' = TerminalSet.add tok toks in
                if toks == toks' then
                  (* Reduce/reduce conflict. *)
                  raise (Goal (node, tok))
                else
                  (* No conflict so far. *)
                  can_reduce := toks'

          ) toks
        ) (Lr0.reductions state)

    end

  (* Populate the queue with the start nodes. Until we find a goal
     node, take a node out the queue, construct the nodes that
     correspond to its successors, and enqueue them. *)

  let goal, token =
    try

      ProductionMap.iter (fun (prod : Production.index) (k : Lr0.node) ->
        let shadow = try
            ProductionMap.find prod Lr1.entry
          with Not_found ->
            assert false
        in
        if relevant shadow then
          explore None shadow (restrict (Lr0.start k))
      ) Lr0.entry;

      Misc.qiter (fun node ->
        SymbolMap.iter (fun symbol state ->
          try
            let shadow =
              SymbolMap.find symbol (Lr1.transitions node.shadow) in
            if relevant shadow then
              explore (Some (symbol, node)) shadow (restrict state)
          with Not_found ->
            (* No shadow. This can happen if a shift/reduce conflict
               was resolved in favor in reduce. Ignore that transition. *)
            ()
        ) (Lr0.transitions node.state)
      ) queue;

      (* We didn't find a goal node. This shouldn't happen! If the
         goal node in the merged LR(1) automaton has a conflict,
         then there should exist a node with a conflict in the
         canonical automaton as well. Otherwise, Pager's construction
         is incorrect. *)

      raise Oops

    with Goal (node, tok) ->
      node, tok

  (* Query the goal node that was found about the shortest path from
     it to one of the entry nodes. *)

  let source, path =

    let rec follow path node =
      match node.ancestor with
      | None ->
          Lr1.start2item node.shadow, Array.of_list path
      | Some (symbol, node) ->
          follow (symbol :: path) node
    in
    follow [] goal

  let goal =
    Lr0.export goal.state

end

