nonTerminalDefinitionInlining.ml

(******************************************************************************)
(*                                                                            *)
(*                                   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 Keyword
open UnparameterizedSyntax
open ListMonad

(* This exception will be raised when a branch does not need inlining. *)
exception NoInlining

(* Color are used to detect cycles. *)
type 'a color =
  | BeingExpanded
  | Expanded of 'a

(* [index2id] converts a 0-based index (into a list of producers) to
   an identifier (the name of the producer). *)

let index2id producers i =
  try
    producer_identifier (List.nth producers i)
  with Failure _ ->
    assert false (* should not happen *)

(* [rename_sw_outer] transforms the keywords in the outer production (the
   caller) during inlining. It replaces [$startpos(x)] and [$endpos(x)], where
   [x] is the name of the callee, with [startpx] and [endpx], respectively. *)

let rename_sw_outer (x, startpx, endpx) (subject, where) : (subject * where) option =
  match subject, where with
  | Before, _ ->
      None
  | RightNamed x', _ ->
      if x' = x then
        match where with
        | WhereStart -> Some startpx
        | WhereEnd   -> Some endpx
        | WhereSymbolStart -> assert false (* has been expanded away *)
      else
        None
  | Left, _ ->
      (* [$startpos], [$endpos], and [$symbolstartpos] have been expanded away
         earlier; see [KeywordExpansion]. *)
      assert false

(* [rename_sw_inner] transforms the keywords in the inner production (the callee)
   during inlining. It replaces [$endpos($0)] with [beforeendp]. *)

let rename_sw_inner beforeendp (subject, where) : (subject * where) option =
  match subject, where with
  | Before, _ ->
      assert (where = WhereEnd);
      Some beforeendp
  | RightNamed _, _ ->
      None
  | Left, _ ->
      (* [$startpos] and [$endpos] have been expanded away earlier; see
         [KeywordExpansion]. *)
      assert false

(* This auxiliary function checks that a use site of an %inline symbol does
   not carry any attributes. *)

let check_no_producer_attributes producer =
  match producer_attributes producer with
  | [] ->
      ()
  | (id, _payload) :: _attributes ->
      Error.error
        [Positions.position id]
        "the nonterminal symbol %s is declared %%inline.\n\
         A use of it cannot carry an attribute."
        (producer_symbol producer)

let names (producers : producers) : StringSet.t =
  List.fold_left (fun s producer ->
    StringSet.add (producer_identifier producer) s
  ) StringSet.empty producers

(* Inline a grammar. The resulting grammar does not contain any definitions
   that can be inlined. *)
let inline grammar =

  (* This function returns a fresh name that begins with [prefix] (although
     this is not essential!) and that is not in the set [names]. *)
  let rec fresh names prefix =
    if StringSet.mem prefix names then
      let prefix = prefix ^ "'" in
      fresh names prefix
    else
      prefix
  in

  let use_inline = ref false in

  (* This table associates a color to each non terminal that can be expanded. *)
  let expanded_non_terminals =
    Hashtbl.create 13
  in

  let expanded_state k =
    Hashtbl.find expanded_non_terminals k
  in

  let mark_as_being_expanded k =
    Hashtbl.add expanded_non_terminals k BeingExpanded
  in

  let mark_as_expanded k r =
    Hashtbl.replace expanded_non_terminals  k (Expanded r);
    r
  in

  (* [find_inline_producer b] traverses the producers of the branch [b] and
     looks for the first nonterminal symbol that can be inlined. If it finds
     one, it inlines its branches into [b], which is why this function can
     return several branches. Otherwise, it raises [NoInlining]. *)
  let rec chop_inline (prefix, suffix) =
    match suffix with
    | [] ->
        raise NoInlining
    | x :: xs ->
        let nt = producer_symbol x
        and id = producer_identifier x in
        try
          let r = StringMap.find nt grammar.rules in
          if r.inline_flag then begin
            (* We have checked earlier than an %inline symbol does not carry
               any attributes. In addition, we now check that the use site of
               this symbol does not carry any attributes either. Thus, we need
               not worry about propagating these attributes through inlining. *)
            check_no_producer_attributes x;
            (* We inline the rule [r] into [b] between [prefix] and [xs]. *)
            List.rev prefix, nt, r, id, xs
          end
          else
            chop_inline (x :: prefix, xs)
        with Not_found ->
          chop_inline (x :: prefix, xs)
  in

  let rec find_inline_producer b =
    let prefix, nt, p, psym, suffix = chop_inline ([], b.producers) in
    prefix, expand_rule nt p, nt, psym, suffix

  (* We have to rename the producers [producers] of the inlined production
     if they clash with the names of the producers of the host branch [b]. *)
  and rename_if_necessary b producers =

    (* Compute the set of the names already in use in the host branch. *)
    let used = names b.producers in

    (* Compute a renaming and the new names of the inlined producers. *)
    let phi, _used, producers' =
      List.fold_left (fun (phi, used, producers) producer ->
        let x = producer_identifier producer in
        if StringSet.mem x used then
          let x' = fresh used x in
          (x, x') :: phi,
          StringSet.add x' used,
          { producer with producer_identifier = x' } :: producers
        else
          (phi, used, producer :: producers)
      ) ([], used, []) producers
    in
    phi, List.rev producers'

  (* Inline the non terminals that can be inlined in [b]. We use the
     ListMonad to combine the results. *)
  and expand_branch (b : branch) : branch ListMonad.m =
    try
      (* [c] is the identifier under which the callee is known. *)
      let prefix, p, nt, c, suffix = find_inline_producer b in
      use_inline := true;
      (* Inline a branch of [nt] at position [prefix] ... [suffix] in
         the branch [b]. *)
      let inline_branch pb =

        (* 2015/11/18. The interaction of %prec and %inline is not documented.
           It used to be the case that we would disallow marking a production
           both %inline and %prec. Now, we allow it, but we check that (1) it
           is inlined at the last position of the host production and (2) the
           host production does not already have a %prec annotation. *)
        pb.branch_prec_annotation |> Option.iter (fun callee_prec ->
          (* The callee has a %prec annotation. *)
          (* Check condition 1. *)
          if List.length suffix > 0 then
            Error.error [ Positions.position callee_prec; b.branch_position ]
              "this production carries a %%prec annotation,\n\
               and the nonterminal symbol %s is marked %%inline.\n\
               For this reason, %s can be used only in tail position."
              nt nt;
          (* Check condition 2. *)
          b.branch_prec_annotation |> Option.iter (fun caller_prec ->
            Error.error [ Positions.position callee_prec; Positions.position caller_prec ]
              "this production carries a %%prec annotation,\n\
               and the nonterminal symbol %s is marked %%inline.\n\
               For this reason, %s cannot be used in a production\n\
               which itself carries a %%prec annotation."
              nt nt
          )
        );

        (* Rename the producers of this branch if they conflict with
           the name of the host's producers. *)
        let phi, inlined_producers = rename_if_necessary b pb.producers in

        (* After inlining, the producers are as follows. *)
        let producers = prefix @ inlined_producers @ suffix in
        let index2id = index2id producers in

        let prefix = List.length prefix
        and inlined_producers = List.length inlined_producers in

        (* Define how the start and end positions of the inner production should
           be computed once it is inlined into the outer production. These
           definitions of [startp] and [endp] are then used to transform
           [$startpos] and [$endpos] in the inner production and to transform
           [$startpos(x)] and [$endpos(x)] in the outer production. *)

        (* 2015/11/04. We ensure that positions are computed in the same manner,
           regardless of whether inlining is performed. *)

        let startp =
          if inlined_producers > 0 then
            (* If the inner production is non-epsilon, things are easy. The start
               position of the inner production is the start position of its first
               element. *)
            RightNamed (index2id prefix), WhereStart
          else if prefix > 0 then
            (* If the inner production is epsilon, we are supposed to compute the
               end position of whatever comes in front of it. If the prefix is
               nonempty, then this is the end position of the last symbol in the
               prefix. *)
            RightNamed (index2id (prefix - 1)), WhereEnd
          else
            (* If the inner production is epsilon and the prefix is empty, then
               we need to look up the end position stored in the top stack cell.
               This is the reason why we need the keyword [$endpos($0)]. It is
               required in this case to preserve the semantics of $startpos and
               $endpos. *)
            Before, WhereEnd

          (* Note that, to contrary to intuition perhaps, we do NOT have that
             if the prefix is empty, then the start position of the inner
             production is the start production of the outer production.
             This is true only if the inner production is non-epsilon. *)

        in

        let endp =
          if inlined_producers > 0 then
            (* If the inner production is non-epsilon, things are easy, then its end
               position is the end position of its last element. *)
            RightNamed (index2id (prefix + inlined_producers - 1)), WhereEnd
          else
            (* If the inner production is epsilon, then its end position is equal
               to its start position. *)
            startp

        in

        (* We must also transform [$endpos($0)] if it used by the inner
           production. It refers to the end position of the stack cell
           that comes before the inner production. So, if the prefix is
           non-empty, then it translates to the end position of the last
           element of the prefix. Otherwise, it translates to [$endpos($0)]. *)

        let beforeendp =
          if prefix > 0 then
            RightNamed (index2id (prefix - 1)), WhereEnd
          else
            Before, WhereEnd
        in

        (* Rename the outer and inner semantic action. *)
        let outer_action =
          Action.rename (rename_sw_outer (c, startp, endp)) [] b.action
        and action' =
          Action.rename (rename_sw_inner beforeendp) phi pb.action
        in

        (* 2015/11/18. If the callee has a %prec annotation (which implies
           the caller does not have one, and the callee appears in tail
           position in the caller) then the annotation is inherited. This
           seems reasonable, but remains undocumented. *)
        let branch_prec_annotation =
          match pb.branch_prec_annotation with
          | (Some _) as annotation ->
              assert (b.branch_prec_annotation = None);
              annotation
          | None ->
              b.branch_prec_annotation
        in

        { b with
          producers;
          action = Action.compose c action' outer_action;
          branch_prec_annotation;
        }
      in
      List.map inline_branch p.branches >>= expand_branch

    with NoInlining ->
      return b

  (* Expand a rule if necessary. *)
  and expand_rule k r =
    try
      (match expanded_state k with
         | BeingExpanded ->
             Error.error
               r.positions
               "there is a cycle in the definition of %s." k
         | Expanded r ->
             r)
    with Not_found ->
      mark_as_being_expanded k;
      mark_as_expanded k { r with branches = r.branches >>= expand_branch }
  in

  (* If we are in Coq mode, %inline is forbidden. *)
  let _ =
    if Settings.coq then
      StringMap.iter
        (fun _ r ->
           if r.inline_flag then
             Error.error r.positions
               "%%inline is not supported by the Coq back-end.")
        grammar.rules
  in

  (* To expand a grammar, we expand all its rules and remove
     the %inline rules. *)
  let expanded_rules =
    StringMap.mapi expand_rule grammar.rules
  in

  let useful (k : string) : bool =
    try
      not (StringMap.find k grammar.rules).inline_flag
    with Not_found ->
      true (* could be: assert false? *)
  in

  (* Remove %on_error_reduce declarations for symbols that are expanded away,
     and warn about them, at the same time. *)
  let useful_warn (k : string) : bool =
    let u = useful k in
    if not u then
      Error.grammar_warning []
        "the declaration %%on_error_reduce %s\n\
          has no effect, since this symbol is marked %%inline and is expanded away." k;
    u
  in

  { grammar with
      rules = StringMap.filter (fun _ r -> not r.inline_flag) expanded_rules;
      types = StringMap.filter (fun k _ -> useful k) grammar.types;
      on_error_reduce = StringMap.filter (fun k _ -> useful_warn k) grammar.on_error_reduce;
  }, !use_inline