diff --git a/src/parameterizedGrammar.ml b/src/parameterizedGrammar.ml index a015fcd168831c93414d2aee9ea5aeab003c6706..7c21c7859e664d5b0fd7420dc333def15b3e721d 100644 --- a/src/parameterizedGrammar.ml +++ b/src/parameterizedGrammar.ml @@ -3,7 +3,29 @@ open Syntax open UnparameterizedSyntax open Misc -(* Inference for non terminals. *) +(* Inside its own definition, a parameterized nonterminal symbol foo(X, Y) + can be applied only to its formal parameters: that is, using foo(X, Y) + is permitted, but using foo(Y, X) or foo(X, list(Y)) is not. + + If foo(X, Y) is defined in a mutually recursive manner with bar(X, Y), + then this restriction extends to both foo and bar. Furthermore, in such + a case, foo and bar must have the same arity, that is, the same formal + parameters. + + These conditions are sufficient to ensure the termination of expansion. + + For example: + C(x) : ... // This definition does not involve A or B. + A(x,y) : B(x,y) C(Y) // This mutually recursive definition is ok. + B(x,y) : A(x,y) + D(x) : E(D(x)) // This one is incorrect. + E(y) : D(y) + +*) + +(* -------------------------------------------------------------------------- *) + +(* Sort inference for nonterminal symbols. *) (* Unification variables convey [variable_info] to describe the multi-equation they take part of. *) diff --git a/src/unparameterizedSyntax.ml b/src/unparameterizedSyntax.ml index 2e85c72e5429fcd3847339ab870bf6d54bcc0d9d..1b780dbfa95c7836d2cbcbcca5b918cae750a082 100644 --- a/src/unparameterizedSyntax.ml +++ b/src/unparameterizedSyntax.ml @@ -1,18 +1,3 @@ -(* A parameterized branch may instantiate parameterized non terminals. - If the parameterized branch contributes to the definition of a - parameterized terminal, then the instantiation of parameterized - non terminals that are defined simultaneously must only be done with - formal parameters. - Furthermore, all the parameterized non terminals that are in a common - mutual recursive definition must have the same arity. - These conditions are sufficient to ensure termination of expansion. - For example: - C[x] : ... // This definition does not involve A or B. - A[x,y] : B[x,y] C[Y] // This mutual recursive definition is ok. - B[x,y] : A[x,y] - D[x] : E[D[x]] // This one is incorrect. - E[y] : D[y] -*) open Syntax type producer =