nonTerminalDefinitionInlining.ml 11.4 KB
Newer Older
1
open Keyword
2 3 4 5 6 7 8 9 10 11 12
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

13 14
(* [index2id] converts a 0-based index (into a list of producers) to
   an identifier (the name of the producer). *)
15 16 17 18 19 20 21 22 23

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

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

27
let rename_sw_outer (x, startpx, endpx) (subject, where) : (subject * where) option =
28
  match subject, where with
29
  | Before, _ ->
30
      None
31
  | RightNamed x', _ ->
32
      if x' = x then
33
        match where with
34 35
        | WhereStart -> Some startpx
        | WhereEnd   -> Some endpx
POTTIER Francois's avatar
POTTIER Francois committed
36
        | WhereSymbolStart -> assert false (* has been expanded away *)
37 38
      else
        None
39
  | Left, _ ->
POTTIER Francois's avatar
POTTIER Francois committed
40 41
      (* [$startpos], [$endpos], and [$symbolstartpos] have been expanded away
         earlier; see [KeywordExpansion]. *)
42
      assert false
43 44

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

47
let rename_sw_inner beforeendp (subject, where) : (subject * where) option =
48
  match subject, where with
49 50
  | Before, _ ->
      assert (where = WhereEnd);
51
      Some beforeendp
52 53
  | RightNamed _, _ ->
      None
54 55 56 57
  | Left, _ ->
      (* [$startpos] and [$endpos] have been expanded away earlier; see
         [KeywordExpansion]. *)
      assert false
58

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

  let names producers = 
64
    List.fold_left (fun s (_, x) -> StringSet.add x s) 
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 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
      StringSet.empty producers 
  in

  (* This function returns a fresh name beginning with [prefix] and 
     that is not in the set of names [names]. *)
  let rec fresh ?(c=0) names prefix =
    let name = prefix^string_of_int c in
      if StringSet.mem name names then
	fresh ~c:(c+1) names prefix
      else 
	name
  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

  (* This function traverses the producers of the branch [b] and find
     the first non terminal that can be inlined. If it finds one, it
     inlines its branches into [b], that's why this function can return
     several branches. If it does not find one non terminal to be 
     inlined, it raises [NoInlining]. *)
  let rec find_inline_producer b = 
    let prefix, nt, p, psym, suffix = 
      let rec chop_inline i (prefix, suffix) =
	match suffix with
	  | [] -> 
	      raise NoInlining

	  | ((nt, id) as x) :: xs ->
	      try
		let r = StringMap.find nt grammar.rules in
113
		if r.inline_flag then 
114 115
		    (* We have to inline the rule [r] into [b] between
		       [prefix] and [xs]. *)
116 117 118
		  List.rev prefix, nt, r, id, xs
		else 
		  chop_inline (i + 1) (x :: prefix, xs) 
119 120 121 122 123 124 125 126
	      with Not_found -> 
		chop_inline (i + 1) (x :: prefix, xs) 
      in
	chop_inline 1 ([], b.producers)
    in
      prefix, expand_rule nt p, nt, psym, suffix

  (* We have to rename producers' names of the inlined production 
127
     if they clash with the producers' names of the branch into 
128 129 130 131 132 133 134 135
     which we do the inlining. *)
  and rename_if_necessary b producers =

    (* First we compute the set of names already in use. *)
    let producers_names = names (b.producers @ producers) in

    (* Compute a renaming and the new inlined producers' names. *)
    let phi, producers' =
136 137 138 139 140 141 142
      List.fold_left (fun (phi, producers) (p, x) -> 
	if StringSet.mem x producers_names then
	  let x' = fresh producers_names x in
	  ((x, x') :: phi, (p, x') :: producers)
	else 
	  (phi, (p, x) :: producers)
      ) ([], []) producers
143 144 145 146 147 148
    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 =
149
    try
150
      (* [c] is the identifier under which the callee is known. *)
151
      let prefix, p, nt, c, suffix = find_inline_producer b in
152 153 154 155
      use_inline := true;
      (* Inline a branch of [nt] at position [prefix] ... [suffix] in
	 the branch [b]. *)
      let inline_branch pb =
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181

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

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

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

190 191 192
        let prefix = List.length prefix
        and inlined_producers = List.length inlined_producers in

193 194 195 196 197 198 199 200 201 202
        (* 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 =
203
          if inlined_producers > 0 then
204 205 206
            (* 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. *)
207 208
            RightNamed (index2id prefix), WhereStart
          else if prefix > 0 then
209 210 211 212
            (* 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. *)
213
            RightNamed (index2id (prefix - 1)), WhereEnd
214 215
          else
            (* If the inner production is epsilon and the prefix is empty, then
216
               we need to look up the end position stored in the top stack cell.
217
               This is the reason why we need the keyword [$endpos($0)]. It is
218 219 220
               required in this case to preserve the semantics of $startpos and
               $endpos. *)
            Before, WhereEnd
221 222 223 224 225

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

227 228 229 230 231 232 233 234 235 236 237 238 239 240
	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

241
        (* We must also transform [$endpos($0)] if it used by the inner
242 243 244
           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
245
           element of the prefix. Otherwise, it translates to [$endpos($0)]. *)
246

247
        let beforeendp =
248 249 250 251 252 253
          if prefix > 0 then
            RightNamed (index2id (prefix - 1)), WhereEnd
          else
            Before, WhereEnd
        in

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

261 262 263 264 265 266 267 268 269 270 271 272 273
        (* 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

274
	{ b with
275 276 277
	  producers;
	  action = Action.compose c action' outer_action;
          branch_prec_annotation;
278 279 280 281 282
	}
      in
      List.map inline_branch p.branches >>= expand_branch

    with NoInlining ->
283
      return b
284

285 286 287 288 289 290 291
  (* Expand a rule if necessary. *)
  and expand_rule k r = 
    try 
      (match expanded_state k with
	 | BeingExpanded ->
    	     Error.error
	       r.positions
292
	       "there is a cycle in the definition of %s." k
293 294 295 296 297 298 299
	 | Expanded r ->
	     r)
    with Not_found ->
      mark_as_being_expanded k;
      mark_as_expanded k { r with branches = r.branches >>= expand_branch }
  in

300
  (* If we are in Coq mode, %inline is forbidden. *)
301 302 303 304 305 306
  let _ =
    if Settings.coq then
      StringMap.iter 
        (fun _ r -> 
	   if r.inline_flag then
             Error.error r.positions
307
               "%%inline is not supported by the Coq back-end.")
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
        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
  and useful_types = 
      StringMap.filter 
	(fun k _ -> try not (StringMap.find k grammar.rules).inline_flag
	 with Not_found -> true)
	grammar.types
  in

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