bundles/menhirLib/menhir-20120123/src/nonTerminalDefinitionInlining.ml

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (*  Menhir                                                                *)
   4 (*                                                                        *)
   5 (*  François Pottier, INRIA Rocquencourt                                  *)
   6 (*  Yann Régis-Gianas, PPS, Université Paris Diderot                      *)
   7 (*                                                                        *)
   8 (*  Copyright 2005-2008 Institut National de Recherche en Informatique    *)
   9 (*  et en Automatique. All rights reserved. This file is distributed      *)
  10 (*  under the terms of the Q Public License version 1.0, with the change  *)
  11 (*  described in file LICENSE.                                            *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* $Id: nonTerminalDefinitionInlining.ml,v 1.17 2006/06/26 09:41:33 regisgia Exp $ *)
  16 open UnparameterizedSyntax
  17 open ListMonad
  18
  19 (* This exception will be raised when a branch does not need inlining. *)
  20 exception NoInlining
  21
  22 (* Color are used to detect cycles. *)
  23 type 'a color =
  24   | BeingExpanded
  25   | Expanded of 'a
  26
  27 (* Inline a grammar. The resulting grammar does not contain any definitions
  28    that can be inlined. *)
  29 let inline grammar =
  30
  31   let names producers =
  32     List.fold_left (fun s -> function (_, Some x) -> StringSet.add x s | _ -> s)
  33       StringSet.empty producers
  34   in
  35
  36   (* This function returns a fresh name beginning with [prefix] and
  37      that is not in the set of names [names]. *)
  38   let rec fresh ?(c=0) names prefix =
  39     let name = prefix^string_of_int c in
  40       if StringSet.mem name names then
  41         fresh ~c:(c+1) names prefix
  42       else
  43         name
  44   in
  45
  46   let use_inline = ref false in
  47
  48   (* This table associates a color to each non terminal that can be expanded. *)
  49   let expanded_non_terminals =
  50     Hashtbl.create 13
  51   in
  52
  53   let expanded_state k =
  54     Hashtbl.find expanded_non_terminals k
  55   in
  56
  57   let mark_as_being_expanded k =
  58     Hashtbl.add expanded_non_terminals k BeingExpanded
  59   in
  60
  61   let mark_as_expanded k r =
  62     Hashtbl.replace expanded_non_terminals  k (Expanded r);
  63     r
  64   in
  65
  66   (* This function traverses the producers of the branch [b] and find
  67      the first non terminal that can be inlined. If it finds one, it
  68      inlines its branches into [b], that's why this function can return
  69      several branches. If it does not find one non terminal to be
  70      inlined, it raises [NoInlining]. *)
  71   let rec find_inline_producer b =
  72     let prefix, nt, p, psym, suffix =
  73       let rec chop_inline i (prefix, suffix) =
  74         match suffix with
  75           | [] ->
  76               raise NoInlining
  77
  78           | ((nt, id) as x) :: xs ->
  79               try
  80                 let r = StringMap.find nt grammar.rules in
  81                 let id = match id with
  82                   | None -> "_"^string_of_int i
  83                   | Some id -> id
  84                 in
  85                   if r.inline_flag then
  86                     (* We have to inline the rule [r] into [b] between
  87                        [prefix] and [xs]. *)
  88                     List.rev prefix, nt, r, id, xs
  89                   else
  90                     chop_inline (i + 1) (x :: prefix, xs)
  91               with Not_found ->
  92                 chop_inline (i + 1) (x :: prefix, xs)
  93       in
  94         chop_inline 1 ([], b.producers)
  95     in
  96       prefix, expand_rule nt p, nt, psym, suffix
  97
  98   (* We have to rename producers' names of the inlined production
  99      if they clashes with the producers' names of the branch into
 100      which we do the inlining. *)
 101   and rename_if_necessary b producers =
 102
 103     (* First we compute the set of names already in use. *)
 104     let producers_names = names (b.producers @ producers) in
 105
 106     (* Compute a renaming and the new inlined producers' names. *)
 107     let phi, producers' =
 108       List.fold_left (fun (phi, producers) -> function (p, Some x) ->
 109                 if StringSet.mem x producers_names then
 110                   let x' = fresh producers_names x in
 111                     ((x, x') :: phi, (p, Some x') :: producers)
 112                 else
 113                   (phi, (p, Some x) :: producers)
 114                 | p -> phi, p :: producers) ([], []) producers
 115     in
 116       phi, List.rev producers'
 117
 118   (* Inline the non terminals that can be inlined in [b]. We use the
 119      ListMonad to combine the results. *)
 120   and expand_branch (b : branch) : branch ListMonad.m =
 121     try
 122       let prefix, p, nt, psym, suffix = find_inline_producer b in
 123         use_inline := true;
 124         if Action.use_dollar b.action then
 125           Error.error [ b.branch_position ]
 126             (Printf.sprintf
 127                "You cannot use %s and the $i syntax in this branch since the \
 128                definition of %s has to be inlined."
 129                nt nt)
 130         else
 131           (* Inline a branch of [nt] at position [prefix] ... [suffix] in
 132              the branch [b]. *)
 133           let inline_branch pb =
 134             (* Rename the producers of this branch is they conflict with
 135                the name of the host's producers. *)
 136             let phi, inlined_producers = rename_if_necessary b pb.producers in
 137
 138             (* Define the renaming environment given the shape of the branch. *)
 139             let renaming_env, prefix', suffix' =
 140
 141               let start_position, prefix' =
 142                 match List.rev prefix with
 143
 144                   (* If the prefix is empty, the start position is the rule
 145                      start position. *)
 146                   | [] -> (Keyword.Left, Keyword.WhereStart), prefix
 147
 148                   (* If the last producer of prefix is unnamed, we cannot refer to
 149                      its position. We give it a name. *)
 150                   | (p, None) :: ps ->
 151                       let x = fresh (names (inlined_producers @ prefix @ suffix)) (CodeBits.prefix "p") in
 152                         (Keyword.RightNamed x, Keyword.WhereEnd), List.rev ((p, Some x) :: ps)
 153
 154                  (* The last producer of prefix is named [x],
 155                     $startpos in the inlined rule will be changed to $endpos(x). *)
 156                  | (_, Some x) :: _ -> (Keyword.RightNamed x, Keyword.WhereEnd), prefix
 157
 158               in
 159               (* Same thing for the suffix. *)
 160               let end_position, suffix' =
 161                 match suffix with
 162                   | [] -> (Keyword.Left, Keyword.WhereEnd), suffix
 163                   | (p, None) :: ps ->
 164                       let x = fresh (names (inlined_producers @ prefix' @ suffix)) (CodeBits.prefix "p") in
 165                         ((Keyword.RightNamed x, Keyword.WhereStart), (p, Some x) :: ps)
 166                  | (_, Some x) :: _ -> (Keyword.RightNamed x, Keyword.WhereStart), suffix
 167               in
 168                 (psym, start_position, end_position), prefix', suffix'
 169             in
 170             (* Rename the host semantic action.
 171                Each reference of the inlined non terminal [psym] must be taken into
 172                account. $startpos(psym) is changed to $startpos(x) where [x] is
 173                the first producer of the inlined branch if it is not empty or
 174                the preceding producer found in the prefix. *)
 175             let outer_action, (used1, used2) =
 176               Action.rename_inlined_psym renaming_env [] b.action
 177             in
 178             let action', (used1', used2') =
 179               Action.rename renaming_env phi pb.action
 180             in
 181             let prefix = if used1 || used1' then prefix' else prefix in
 182             let suffix = if used2 || used2' then suffix' else suffix in
 183
 184               { b with
 185                   producers = prefix @ inlined_producers @ suffix;
 186                   action = Action.compose psym action' outer_action
 187               }
 188           in
 189             List.map inline_branch p.branches >>= expand_branch
 190
 191     with NoInlining ->
 192       return b
 193
 194   (* Expand a rule if necessary. *)
 195   and expand_rule k r =
 196     try
 197       (match expanded_state k with
 198          | BeingExpanded ->
 199              Error.error
 200                r.positions
 201                (Printf.sprintf "there is a cycle in the definition of %s." k)
 202          | Expanded r ->
 203              r)
 204     with Not_found ->
 205       mark_as_being_expanded k;
 206       mark_as_expanded k { r with branches = r.branches >>= expand_branch }
 207   in
 208
 209     (* We check that the %inline rules do not use $i syntax since
 210        expansion of $i is impossible. *)
 211   let _ =
 212     StringMap.iter
 213       (fun _ r ->
 214          if r.inline_flag
 215            && List.exists (fun b -> Action.use_dollar b.action) r.branches then
 216              Error.error r.positions
 217                (Printf.sprintf
 218                   "You cannot use $i syntax in this branch since its \
 219                    definition will be inlined."))
 220       grammar.rules
 221   in
 222
 223     (* If we are in Coq mode, %inline is forbidden. *)
 224   let _ =
 225     if Settings.coq then
 226       StringMap.iter
 227         (fun _ r ->
 228            if r.inline_flag then
 229              Error.error r.positions
 230                (Printf.sprintf "%%inline is not supported by the coq back-end"))
 231         grammar.rules
 232   in
 233
 234     (* To expand a grammar, we expand all its rules and remove
 235        the %inline rules. *)
 236   let expanded_rules =
 237     StringMap.mapi expand_rule grammar.rules
 238   and useful_types =
 239       StringMap.filter
 240         (fun k _ -> try not (StringMap.find k grammar.rules).inline_flag
 241          with Not_found -> true)
 242         grammar.types
 243   in
 244
 245     { grammar with
 246         rules = StringMap.filter (fun _ r -> not r.inline_flag) expanded_rules;
 247         types = useful_types
 248     }, !use_inline
 249