CheckSafeParameterizedGrammar.ml 6.92 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   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.                                                             *)
(*                                                                            *)
(******************************************************************************)

14
let value = Positions.value
15
open Syntax
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

(* This test accepts a parameterized grammar, with the restriction that all
   parameters must have sort [*]. This implies that the head of every
   application must be a toplevel nonterminal symbol: it cannot be a formal
   parameter of the current rule. *)

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

(* This flag causes graph edges to be logged on the standard error channel. *)

let debug = false

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

(* For syntactic convenience, the code is wrapped in a functor. *)

module Run (G : sig val g : grammar end) = struct
open G

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

(* We build a graph whose vertices are all formal parameters of all rules. A
   formal parameter is represented as a pair of a nonterminal symbol and a
   0-based integer index (the number of this parameter within this rule).
   We use OCaml's generic equality and hash functions at this type. *)

type formal =
  symbol * int

let formals (nt, rule) : formal list =
  let arity = List.length rule.pr_parameters in
  Misc.mapi arity (fun i -> nt, i)

let formals : formal array =
  StringMap.bindings g.p_rules
  |> List.map formals
  |> List.concat
  |> Array.of_list

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

(* The graph edges are as follows. First, for every rule of the following form:

     F(..., X, ...):           # where X is the i-th formal parameter of F
       ... G(..., X, ...) ...  # where X is the j-th actual parameter of G

   there is a "safe" edge from the formal parameter F/i to the formal G/j. This
   reflects the fact that there is a flow from F/i to G/j. It is "safe" in the
   sense that it is not size-increasing: the same parameter X is passed from F
   to G.

   Second, for every rule of the following form:

     F(..., X, ...):           # where X is the i-th formal parameter of F
       ... G(..., H(..., X, ...) , ...) ...
                               # where H(...) is the j-th actual parameter of G

   there is a "dangerous" edge from the formal parameter F/i to the formal G/j.
   This reflects the fact that there is a flow from F/i to G/j. This flow is
   "dangerous" in the sense that it is size-increasing: X is transformed to
   H(..., X, ...). *)

type edge =
  | Safe
  | Dangerous

let successors_parameter (f : edge -> formal -> unit) x (param : parameter) =
  match param with
  | ParameterVar _ ->
      (* This is not an application. No successors. *)
      ()
  | ParameterApp (sym, params) ->
      let nt = value sym in
      (* If [x] occurs in the [i]-th actual parameter of this application,
         then there is an edge to the formal [nt, i]. Whether it is a safe
         or dangerous edge depends on whether [x] occurs shallow or deep. *)
      List.iteri (fun i param ->
93
        if Parameters.occurs_shallow x param then
94
          f Safe (nt, i)
95
        else if Parameters.occurs_deep x param then
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
          f Dangerous (nt, i)
      ) params
  | ParameterAnonymous _ ->
      assert false

let successors_producer f x ((_, param, _) : producer) =
  successors_parameter f x param

let successors_branch f x (branch : parameterized_branch) =
  List.iter (successors_producer f x) branch.pr_producers

let successors f ((nt, i) : formal) =
  let rule = try StringMap.find nt g.p_rules with Not_found -> assert false in
  let x  = try List.nth rule.pr_parameters i with Failure _ -> assert false in
  List.iter (successors_branch f x) rule.pr_branches

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

(* We now have a full description of the graph. *)

module G = struct
  type node = formal
  let n = Array.length formals
  let index = Misc.inverse formals
  let successors f = successors (fun _ target -> f target)
  let iter f = Array.iter f formals
end

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

126 127 128 129 130 131 132 133 134 135 136 137 138
(* Display the graph. *)

let () =
  if debug then
    G.iter (fun (x, i) ->
      successors (fun edge (y, j) ->
        let kind = match edge with Safe -> "safe" | Dangerous -> "dangerous" in
        Printf.eprintf "%s/%d ->(%s) %s/%d\n" x i kind y j
      ) (x, i)
    )

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

139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
(* Compute its strongly connected components, ignoring the distinction between
   safe and dangerous edges. *)

module T = Tarjan.Run(G)

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

(* The safety criterion is: no dangerous edge is part of a cycle. Indeed, if
   this criterion is satisfied, then expansion must terminate: only a finite
   number of well-sorted terms (involving toplevel symbols and applications)
   can arise. (This sentence is not a proof!) Conversely, if a dangerous edge
   appears in a cycle, then expansion will not terminate. (That is, unless the
   dangerous cycle is unreachable. We choose to reject it anyway in that case.)
   In other words, this criterion is sound and complete. *)

(* Checking that no dangerous edge is part of a cycle is done by examining the
   source and destination of every dangerous edge and ensuring that they lie
   in distinct components. *)

let () =
  G.iter (fun source ->
    successors (fun edge target ->
      match edge with
      | Safe ->
          ()
      | Dangerous ->
          if T.representative source = T.representative target then
            let (nt, i) = source in
            Error.error []
              "the parameterized nonterminal symbols in this grammar\n\
               cannot be expanded away: expansion would not terminate.\n\
               The %s formal parameter of \"%s\" grows without bound."
              (Misc.nth (i + 1)) nt

    ) source
174
  )
175 176 177 178 179 180 181 182 183 184

end (* of the functor *)

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

(* Re-package the above functor as a function. *)

let check g =
  let module T = Run(struct let g = g end) in
  ()