Add more checks ensuring that generators work correctly (Statix spec)

- Check that context-free productions are either a valid injection,
  bracket, or rejection, or a production with a constructor.
- Disallow optionals, alterations, and sequences in context-free syntax.
- Warn when using a constructor in lexical syntax.

org.metaborg.meta.lang.template/trans/statix/main.str

@@ -28,6 +28,7 @@ signature constructors // Types
   INJ      : list(TYPE) * TYPE -> TYPE
   ITER     : TYPE              -> TYPE
   TERMINAL : TYPE
+  LAYOUT   : TYPE
 
 rules // Types
 
@@ -40,7 +41,7 @@ rules // Types
 
   fail-msg(|msg) = err-msg(|$[get-type: [msg]]); fail
 
-  remove-unnecessary-types = remove-all(?TERMINAL())
+  remove-unnecessary-types = remove-all(?TERMINAL() + ?LAYOUT())
 
   to-compatible-type:
     SORT(occ) -> SortType(<stx-get-occurrence-terms; Hd> occ)

org.metaborg.meta.lang.template/trans/statix/production.stx

@@ -2,30 +2,63 @@ module statix/production
 
 imports
 
+  statix/util
+  statix/name
   statix/type
   statix/attribute
   statix/sort_cons
 
 rules
 
-  injectionProductionOK: TYPE * Attributes * SymbolDef
-  // Disabled for now: produces spurious errors in some cases.
-  //injectionProductionOK(PROD([_, _|_], SORT(_)), attrs, loc) :-
-  //  try { hasAttribute(Reject(), attrs) == TRUE() } | warning $[Missing constructor name: the generated pretty printer might not work properly] @loc.
-  injectionProductionOK(_, _, _).
-
-  // TODO: error: Missing bracket attribute or constructor name
-  // - LHS must be a single sort (injection)
-  // - RHS must be in the form of '(' Sort ')'
-  // - attributes must NOT contain Bracket() nor Reject()
-
-  // TODO: warning: Illegal use of the {bracket} attribute
-  // - HS must be a single sort (injection)
-  // - RHS must NOT be in the form of '(' Sort ')'
-  // - attributes must contain Bracket()
-  // - attributes must NOT contain Reject()
-
-  // TODO: warning: Illegal use of the {bracket} attribute
-  // - LHS must be a sort + constructor (not an injection)
-  // - attributes must contain Bracket()
-  // - attributes must NOT contain Reject()
+  symbolDefProductionOK: SORT_KIND * TYPE * Attributes * SymbolDef
+
+  symbolDefProductionOK(CONTEXTFREE(), INJ(ts@[_, _, _|_], SORT(_)), attrs, symbolDef) :-
+    try { 
+      bOr(hasAttribute(Reject(), attrs), hasAttribute(Bracket(), attrs)) == TRUE()
+    } | error $[Missing constructor; add a constructor to this production, turn it into an injection in the form of A = B, or turn it into a bracket rule in the form of A = "(" A ")" {bracket}]@symbolDef,
+    try { containsOpt(ts) == FALSE() } | error $[Optionals (A?) are not allowed in context-free syntax]@symbolDef,
+    try { containsAlt(ts) == FALSE() } | error $[Alternations (A | B) are not allowed in context-free syntax]@symbolDef,
+    try { containsSeq(ts) == FALSE() } | error $[Sequences ((A B ... Z)) are not allowed in context-free syntax]@symbolDef.
+  symbolDefProductionOK(CONTEXTFREE(), INJ(ts@[_, _|_], SORT(_)), attrs, symbolDef) :-
+    try { 
+      bOr(hasAttribute(Reject(), attrs), hasAttribute(Bracket(), attrs)) == TRUE()
+    } | error $[Missing constructor; either add a constructor to this production, or turn it into an injection in the form of A = B]@symbolDef,
+    try { containsOpt(ts) == FALSE() } | error $[Optionals (A?) are not allowed in context-free syntax]@symbolDef,
+    try { containsAlt(ts) == FALSE() } | error $[Alternations (A | B) are not allowed in context-free syntax]@symbolDef,
+    try { containsSeq(ts) == FALSE() } | error $[Sequences ((A B ... Z)) are not allowed in context-free syntax]@symbolDef.
+  symbolDefProductionOK(CONTEXTFREE(), INJ(ts, _), _, symbolDef) :-
+    try { containsOpt(ts) == FALSE() } | error $[Optionals (A?) are not allowed in context-free syntax]@symbolDef,
+    try { containsAlt(ts) == FALSE() } | error $[Alternations (A | B) are not allowed in context-free syntax]@symbolDef,
+    try { containsSeq(ts) == FALSE() } | error $[Sequences ((A B ... Z)) are not allowed in context-free syntax]@symbolDef.
+
+  symbolDefProductionOK(_, _, _, _).
+
+rules
+
+  sortConsProductionOK: SORT_KIND * TYPE * Attributes * SortCons
+
+  sortConsProductionOK(CONTEXTFREE(), PROD(ts, _), _, sortCons) :-
+    try { containsOpt(ts) == FALSE() } | error $[Optionals (A?) are not allowed in context-free syntax]@sortCons,
+    try { containsAlt(ts) == FALSE() } | error $[Alternations (A | B) are not allowed in context-free syntax]@sortCons,
+    try { containsSeq(ts) == FALSE() } | error $[Sequences ((A B ... Z)) are not allowed in context-free syntax]@sortCons.
+  sortConsProductionOK(LEXICAL(), PROD(_, _), _, sortCons) :-
+    try { false } | warning $[Constructor in lexical syntax; remove this constructor from the production]@sortCons.
+
+  sortConsProductionOK(_, _, _, _).
+
+rules
+
+  containsOpt: list(TYPE) -> BOOL
+  containsOpt([OPT(_)|ts]) = TRUE().
+  containsOpt([_|ts])      = containsOpt(ts).
+  containsOpt([])          = FALSE().
+
+  containsAlt: list(TYPE) -> BOOL
+  containsAlt([ALT(_, _)|ts]) = TRUE().
+  containsAlt([_|ts])         = containsAlt(ts).
+  containsAlt([])             = FALSE().
+
+  containsSeq: list(TYPE) -> BOOL
+  containsSeq([SEQ(_, _)|ts]) = TRUE().
+  containsSeq([_|ts])         = containsSeq(ts).
+  containsSeq([])             = FALSE().

org.metaborg.meta.lang.template/trans/statix/section/priority.stx

@@ -61,5 +61,5 @@ rules
   priorityProductionOK: scope * PriorityProduction
   // TODO: these should not declare new productions, but instead should be checked against existing ones?
   priorityProductionOK(s, PriorityProduction_SdfProduction(sdfProduction)) :- typeOfSdfProduction(s, CONTEXTFREE(), sdfProduction) == _.
-  priorityProductionOK(s, PriorityProduction_Production(production))       :- productionOK(s, CONTEXTFREE(), production).
+  priorityProductionOK(s, PriorityProduction_Production(production))       :- kernelProductionOK(s, CONTEXTFREE(), production).
   priorityProductionsOK maps priorityProductionOK(*, list(*))

org.metaborg.meta.lang.template/trans/statix/section/syntax.stx

@@ -41,25 +41,25 @@ signature
 
 rules
 
-  grammarOK(s, Syntax(productions))                    :- productionsOK(s, KERNEL(), productions).
-  grammarOK(s, Lexical(productions))                   :- productionsOK(s, LEXICAL(), productions).
-  grammarOK(s, Contextfree(productions))               :- productionsOK(s, CONTEXTFREE(), productions).
-  grammarOK(s, Variables(productions))                 :- productionsOK(s, VAR(), productions).
-  grammarOK(s, LexVariables(productions))              :- productionsOK(s, VAR(), productions).
+  grammarOK(s, Syntax(productions))                    :- kernelProductionsOK(s, KERNEL(), productions).
+  grammarOK(s, Lexical(productions))                   :- kernelProductionsOK(s, LEXICAL(), productions).
+  grammarOK(s, Contextfree(productions))               :- kernelProductionsOK(s, CONTEXTFREE(), productions).
+  grammarOK(s, Variables(productions))                 :- kernelProductionsOK(s, VAR(), productions).
+  grammarOK(s, LexVariables(productions))              :- kernelProductionsOK(s, VAR(), productions).
   grammarOK(s, VariablesProductive(sdfProductions))    :- typeOfSdfProductions(s, VAR(), sdfProductions) == _.
   grammarOK(s, LexVariablesProductive(sdfProductions)) :- typeOfSdfProductions(s, VAR(), sdfProductions) == _.
   grammarOK(s, Kernel(sdfProductions))                 :- typeOfSdfProductions(s, KERNEL(), sdfProductions) == _.
   grammarOK(s, LexicalSyntax(sdfProductions))          :- typeOfSdfProductions(s, LEXICAL(), sdfProductions) == _.
   grammarOK(s, ContextFreeSyntax(generalProductions))  :- generalProductionsOK(s, CONTEXTFREE(), generalProductions).
 
-  productionOK: scope * SORT_KIND * Production
-  productionOK(s, Kexpected, Prod(symbols, symbol, _)) :- {Kactual sProd}
+  kernelProductionOK: scope * SORT_KIND * Production
+  kernelProductionOK(s, Kexpected, Prod(symbols, symbol, _)) :- {Kactual sProd}
     kindOfSymbol(s, symbol) == Kactual,
     try { Kactual == Kexpected } | error $[Sort of production is of kind [Kactual], but expected it to be of kind [Kexpected] due to the section the production is defined in]@symbol,
     new sProd, sProd -P-> s,
     typesOfSymbols(sProd, symbols) == _,
     typeOfSymbol(sProd, symbol) == _.
-  productionsOK maps productionOK(*, *, list(*))
+  kernelProductionsOK maps kernelProductionOK(*, *, list(*))
 
   generalProductionOK: scope * SORT_KIND * GeneralProduction
   generalProductionOK(s, Kexpected, GeneralProduction_SdfProduction(sdfProduction))           :-
@@ -76,13 +76,14 @@ rules
     new sProd, sProd -P-> s,
     typesOfSymbols(sProd, symbols) == Tsymbols,
     Tprod == INJ(Tsymbols, Tsort),
-    injectionProductionOK(Tprod, attrs, symbolDef),
+    symbolDefProductionOK(Kexpected, removeLayoutFromProdResult(Tprod), attrs, symbolDef),
     @rhs.type := Tprod.
-  typeOfSdfProduction(s, Kexpected, SdfProductionWithCons(sortCons, rhs@Rhs(symbols), _)) = Tprod :- {Kactual sProd Tsymbols Tsort}
+  typeOfSdfProduction(s, Kexpected, SdfProductionWithCons(sortCons, rhs@Rhs(symbols), attrs)) = Tprod :- {Kactual sProd Tsymbols Tsort}
     kindOfSortCons(s, sortCons) == Kactual,
     try { Kactual == Kexpected } | error $[Sort of production is of kind [Kactual], but expected it to be of kind [Kexpected] due to the section the production is defined in]@sortCons,
     declareSortCons(s, Tsymbols, sortCons) == Tprod,
     new sProd, sProd -P-> s,
     typesOfSymbols(sProd, symbols) == Tsymbols,
+    sortConsProductionOK(Kexpected, removeLayoutFromProdResult(Tprod), attrs, sortCons),
     @rhs.type := Tprod.
   typeOfSdfProductions maps typeOfSdfProduction(*, *, list(*)) = list(*)

org.metaborg.meta.lang.template/trans/statix/section/template.stx

@@ -54,14 +54,15 @@ rules
     new sProd, sProd -P-> s,
     typeOfTemplate(sProd, template) == Tsymbols,
     Tprod == INJ(Tsymbols, Tsort),
-    injectionProductionOK(Tprod, attrs, symbolDef),
+    symbolDefProductionOK(Kexpected, removeLayoutFromProdResult(Tprod), attrs, symbolDef),
     @template.type := Tprod.
-  typeOfTemplateProduction(s, Kexpected, TemplateProductionWithCons(sortCons, template, _)) = Tprod :- {Kactual sProd Tsymbols Tsort}
+  typeOfTemplateProduction(s, Kexpected, TemplateProductionWithCons(sortCons, template, attrs)) = Tprod :- {Kactual sProd Tsymbols Tsort}
     kindOfSortCons(s, sortCons) == Kactual,
     try { Kactual == Kexpected } | error $[Sort of production is of kind [Kactual], but expected it to be of kind [Kexpected] due to the section the production is defined in]@sortCons,
     declareSortCons(s, Tsymbols, sortCons) == Tprod,
     new sProd, sProd -P-> s,
     typeOfTemplate(sProd, template) == Tsymbols,
+    sortConsProductionOK(Kexpected, removeLayoutFromProdResult(Tprod), attrs, sortCons),
     @template.type := Tprod.
   typeOfTemplateProductions maps typeOfTemplateProduction(*, *, list(*)) = list(*)
 
@@ -90,6 +91,9 @@ rules
   maybeTypeOfTemplatePart: scope * TemplatePart -> list(TYPE)
   maybeTypeOfTemplatePart(s, Angled(placeholder))  = [typeOfPlaceholder(s, placeholder)].
   maybeTypeOfTemplatePart(s, Squared(placeholder)) = [typeOfPlaceholder(s, placeholder)].
+  maybeTypeOfTemplatePart(s, String(_))            = [TERMINAL()].
+  maybeTypeOfTemplatePart(s, Escape(_))            = [TERMINAL()].
+  maybeTypeOfTemplatePart(s, Layout(_))            = [LAYOUT()].
   maybeTypeOfTemplatePart(s, _)                    = [].
 
   typeOfPlaceholder: scope * Placeholder -> TYPE

org.metaborg.meta.lang.template/trans/statix/symbol.stx

@@ -69,7 +69,7 @@ rules
     typeOfSymbol(s, symbol1) == T1,
     typeOfSymbol(s, symbol2) == T2.
 
-  typeOfSymbol(s, Layout())     = TERMINAL().
+  typeOfSymbol(s, Layout())     = LAYOUT().
   typeOfSymbol(s, CharClass(_)) = TERMINAL().
   typeOfSymbol(s, Lit(_))       = TERMINAL().
   typeOfSymbol(s, CiLit(_))     = TERMINAL().

org.metaborg.meta.lang.template/trans/statix/type.stx

@@ -9,6 +9,7 @@ signature
     ITER     : TYPE              -> TYPE
     ALT      : TYPE * TYPE       -> TYPE
     TERMINAL :                      TYPE
+    LAYOUT   :                      TYPE
     PROD     : list(TYPE) * TYPE -> TYPE
     INJ      : list(TYPE) * TYPE -> TYPE
     MOD      : scope             -> TYPE
@@ -35,3 +36,13 @@ rules
   flattenTypes : list(list(TYPE)) -> list(TYPE)
   flattenTypes([ts|tts]) = appendTypes(ts, flattenTypes(tts)).
   flattenTypes([      ]) = [].
+
+  removeLayout : list(TYPE) -> list(TYPE)
+  removeLayout([LAYOUT()|ts]) = removeLayout(ts).
+  removeLayout([t|ts])        = [t|removeLayout(ts)].
+  removeLayout([ ])           = [].
+
+  removeLayoutFromProdResult : TYPE -> TYPE
+  removeLayoutFromProdResult(PROD(ts, t)) = PROD(removeLayout(ts), t).
+  removeLayoutFromProdResult(INJ(ts, t))  = INJ(removeLayout(ts), t).
+  removeLayoutFromProdResult(t)           = t.

org.metaborg.meta.lang.template/trans/statix/util.stx

@@ -21,3 +21,7 @@ rules
   bOr: BOOL  * BOOL    -> BOOL
   bOr(FALSE(), FALSE()) = FALSE().
   bOr(_      , _      ) = TRUE().
+
+  bNot: BOOL -> BOOL
+  bNot(FALSE()) = TRUE().
+  bNot(TRUE())  = FALSE().