Improvements to checks (Statix spec)

- Remove number of non-terminal counting since it was not used. - Exhaustively check the type hierarchy of a sort to check for legacy constructs in context-free syntax, and reduce duplication for these checks. - Error on {bracket} in lexical syntax. - Error on {bracket} with constructor.
metaborg · Sep 30, 2021 · 616a8b0 · 616a8b0
1 parent 1c9e255
commit 616a8b0
Show file tree

Hide file tree

Showing 5 changed files with 200 additions and 163 deletions.
diff --git a/org.metaborg.meta.lang.template/trans/statix/attribute.stx b/org.metaborg.meta.lang.template/trans/statix/attribute.stx
@@ -65,123 +65,123 @@ signature
 
 rules
 
-  attributesOk : scope * int * Attributes
-  attributesOk(s, numNonTerminals, attrs) :-
-    singleAttributesOk(s, numNonTerminals, attributes(attrs)).
-
-  attributeOk : scope * int * Attribute
-  attributeOk(s, numNonTerminals, LayoutConstraint(constraint)) :-
-    constraintOk(s, numNonTerminals, constraint).
-  attributeOk(_, _, _).
-  singleAttributesOk maps attributeOk(*, *, list(*))
+  attributesOk : scope * Attributes
+  attributesOk(s, attrs) :-
+    singleAttributesOk(s, attributes(attrs)).
+
+  attributeOk : scope * Attribute
+  attributeOk(s, LayoutConstraint(constraint)) :-
+    constraintOk(s, constraint).
+  attributeOk(_, _).
+  singleAttributesOk maps attributeOk(*, list(*))
 
 rules
 
-  constraintTreeRefOk : scope * int * ConstraintTreeRef
-  constraintTreeRefOk(s, numNonTerminals, PosRef(index)). //:-
+  constraintTreeRefOk : scope * ConstraintTreeRef
+  constraintTreeRefOk(s, PosRef(index)). //:-
     // disabled: cannot check indices as parser does some tokenization on template syntax that is not apparent from the
     // surface syntax.
     //try { index #< numNonTerminals } | error $[Index [index] (0-based) exeeds the number of non-layout elements [numNonTerminals]. Change the index to be < [numNonTerminals]].
-  constraintTreeRefOk(s, numNonTerminals, LiteralRef(literal)).
+  constraintTreeRefOk(s, LiteralRef(literal)).
     // TODO: check literal
-  constraintTreeRefOk(s, numNonTerminals, LabelRef(label)) :-
+  constraintTreeRefOk(s, LabelRef(label)) :-
     resolveLabel(s, label). 
-  constraintTreeRefsOk maps constraintTreeRefOk(*, *, list(*))
-
-  constraintTokenOk : scope * int * ConstraintToken
-  constraintTokenOk(s, numNonTerminals, First(ref)) :-
-    constraintTreeRefOk(s, numNonTerminals, ref).
-  constraintTokenOk(s, numNonTerminals, Left(ref)) :-
-    constraintTreeRefOk(s, numNonTerminals, ref).
-  constraintTokenOk(s, numNonTerminals, Right(ref)) :-
-    constraintTreeRefOk(s, numNonTerminals, ref).
-  constraintTokenOk(s, numNonTerminals, Last(ref)) :-
-    constraintTreeRefOk(s, numNonTerminals, ref).
+  constraintTreeRefsOk maps constraintTreeRefOk(*, list(*))
+
+  constraintTokenOk : scope * ConstraintToken
+  constraintTokenOk(s, First(ref)) :-
+    constraintTreeRefOk(s, ref).
+  constraintTokenOk(s, Left(ref)) :-
+    constraintTreeRefOk(s, ref).
+  constraintTokenOk(s, Right(ref)) :-
+    constraintTreeRefOk(s, ref).
+  constraintTokenOk(s, Last(ref)) :-
+    constraintTreeRefOk(s, ref).
 
-  constraintExpOk : scope * int * ConstraintExp
-  constraintExpOk(s, numNonTerminals, Mul(exp1, exp2)) :-
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintExpOk(s, numNonTerminals, Div(exp1, exp2)) :-
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintExpOk(s, numNonTerminals, Add(exp1, exp2)) :-
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintExpOk(s, numNonTerminals, Sub(exp1, exp2)) :-
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintExpOk(s, numNonTerminals, ConstraintExpLine(token)) :-
-    constraintTokenOk(s, numNonTerminals, token).
-  constraintExpOk(s, numNonTerminals, Col(token)) :-
-    constraintTokenOk(s, numNonTerminals, token).
-  constraintExpOk(s, numNonTerminals, Num(Digits(index))).
+  constraintExpOk : scope * ConstraintExp
+  constraintExpOk(s, Mul(exp1, exp2)) :-
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintExpOk(s, Div(exp1, exp2)) :-
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintExpOk(s, Add(exp1, exp2)) :-
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintExpOk(s, Sub(exp1, exp2)) :-
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintExpOk(s, ConstraintExpLine(token)) :-
+    constraintTokenOk(s, token).
+  constraintExpOk(s, Col(token)) :-
+    constraintTokenOk(s, token).
+  constraintExpOk(s, Num(Digits(index))).
     // TODO: check index
 
-  constraintOk : scope * int * Constraint
-  constraintOk(s, numNonTerminals, Eq(exp1, exp2)) :- 
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintOk(s, numNonTerminals, Lt(exp1, exp2)) :- 
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintOk(s, numNonTerminals, Le(exp1, exp2)) :- 
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintOk(s, numNonTerminals, Gt(exp1, exp2)) :- 
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintOk(s, numNonTerminals, Ge(exp1, exp2)) :- 
-    constraintExpOk(s, numNonTerminals, exp1),
-    constraintExpOk(s, numNonTerminals, exp2).
-  constraintOk(s, numNonTerminals, Not(c)) :- 
-    constraintOk(s, numNonTerminals, c).
-  constraintOk(s, numNonTerminals, And(c1, c2)) :- 
-    constraintOk(s, numNonTerminals, c1),
-    constraintOk(s, numNonTerminals, c2).
-  constraintOk(s, numNonTerminals, Or(c1, c2)) :- 
-    constraintOk(s, numNonTerminals, c1),
-    constraintOk(s, numNonTerminals, c2).
-
-  constraintOk(s, numNonTerminals, Offside(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, Indent(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, Align(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, AlignList(ref)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref).
-  constraintOk(s, numNonTerminals, NewLineIndent(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, SingleLine(refs)) :- 
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-
-  constraintOk(s, numNonTerminals, PPOffside(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, PPIndent(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, PPAlign(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, PPAlignList(ref)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref).
-  constraintOk(s, numNonTerminals, PPNewLineIndent(ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
-  constraintOk(s, numNonTerminals, PPNewLineIndentBy(Digits(index), ref, refs)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref),
-    constraintTreeRefsOk(s, numNonTerminals, refs).
+  constraintOk : scope * Constraint
+  constraintOk(s, Eq(exp1, exp2)) :- 
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintOk(s, Lt(exp1, exp2)) :- 
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintOk(s, Le(exp1, exp2)) :- 
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintOk(s, Gt(exp1, exp2)) :- 
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintOk(s, Ge(exp1, exp2)) :- 
+    constraintExpOk(s, exp1),
+    constraintExpOk(s, exp2).
+  constraintOk(s, Not(c)) :- 
+    constraintOk(s, c).
+  constraintOk(s, And(c1, c2)) :- 
+    constraintOk(s, c1),
+    constraintOk(s, c2).
+  constraintOk(s, Or(c1, c2)) :- 
+    constraintOk(s, c1),
+    constraintOk(s, c2).
+
+  constraintOk(s, Offside(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, Indent(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, Align(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, AlignList(ref)) :- 
+    constraintTreeRefOk(s, ref).
+  constraintOk(s, NewLineIndent(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, SingleLine(refs)) :- 
+    constraintTreeRefsOk(s, refs).
+
+  constraintOk(s, PPOffside(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, PPIndent(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, PPAlign(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, PPAlignList(ref)) :- 
+    constraintTreeRefOk(s, ref).
+  constraintOk(s, PPNewLineIndent(ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
+  constraintOk(s, PPNewLineIndentBy(Digits(index), ref, refs)) :- 
+    constraintTreeRefOk(s, ref),
+    constraintTreeRefsOk(s, refs).
     // TODO: check index
-  constraintOk(s, numNonTerminals, PPNewLine(ref)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref).
-  constraintOk(s, numNonTerminals, PPNewLineBy(Digits(index), ref)) :- 
-    constraintTreeRefOk(s, numNonTerminals, ref).
+  constraintOk(s, PPNewLine(ref)) :- 
+    constraintTreeRefOk(s, ref).
+  constraintOk(s, PPNewLineBy(Digits(index), ref)) :- 
+    constraintTreeRefOk(s, ref).
     // TODO: check index
 
 rules

diff --git a/org.metaborg.meta.lang.template/trans/statix/production.stx b/org.metaborg.meta.lang.template/trans/statix/production.stx
@@ -8,57 +8,109 @@ imports
   statix/attribute
   statix/sort_cons
 
-rules
+rules // SymbolDef (no constructor) production checks
 
   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.
+    symbolDefCheckForLegacyTypesInContextFree(ts, 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.
+    symbolDefCheckForLegacyTypesInContextFree(ts, 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.
-
+    symbolDefCheckForLegacyTypesInContextFree(ts, symbolDef).
+
+  symbolDefProductionOK(LEXICAL(), _, attrs, symbolDef) :-
+    try { hasAttribute(Bracket(), attrs) == FALSE() } | error $[Bracket in lexical syntax; remove the bracket annotation from the production]@symbolDef.
+
   symbolDefProductionOK(_, _, _, _).
 
-rules
+rules // SortCons (constructor) production checks
 
   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(CONTEXTFREE(), PROD(ts, _), attrs, sortCons) :-
+    try { hasAttribute(Bracket(), attrs) == FALSE() } | error $[Bracket annotation on production with a constructor; either remove the constructor or the bracket annotation from the production]@sortCons,
+    sortConsCheckForLegacyTypesInContextFree(ts, sortCons).
+  sortConsProductionOK(LEXICAL(), PROD(_, _), attrs, sortCons) :-
+    try { false } | warning $[Constructor in lexical syntax; remove this constructor from the production]@sortCons,
+    try { hasAttribute(Bracket(), attrs) == FALSE() } | error $[Bracket in lexical syntax; remove the bracket annotation from the production]@sortCons.
 
   sortConsProductionOK(_, _, _, _).
 
-rules
+rules // Check for legacy symbols in context-free syntax 
 
-  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().
+  symbolDefCheckForLegacyTypesInContextFree: list(TYPE) * SymbolDef
+  symbolDefCheckForLegacyTypesInContextFree(ts, symbolDef) :- 
+    try { listContainsOpt(ts) == FALSE() } | error $[Optionals (A?) are not allowed in context-free syntax]@symbolDef,
+    try { listContainsAlt(ts) == FALSE() } | error $[Alternations (A | B) are not allowed in context-free syntax]@symbolDef,
+    try { listContainsSeq(ts) == FALSE() } | error $[Sequences ((A B ... Z)) are not allowed in context-free syntax]@symbolDef.
+
+  sortConsCheckForLegacyTypesInContextFree: list(TYPE) * SortCons
+  sortConsCheckForLegacyTypesInContextFree(ts, sortCons) :- 
+    try { listContainsOpt(ts) == FALSE() } | error $[Optionals (A?) are not allowed in context-free syntax]@sortCons,
+    try { listContainsAlt(ts) == FALSE() } | error $[Alternations (A | B) are not allowed in context-free syntax]@sortCons,
+    try { listContainsSeq(ts) == FALSE() } | error $[Sequences ((A B ... Z)) are not allowed in context-free syntax]@sortCons.
+
+rules // Opt symbol checking
+
+  typeIsOrContainsOpt: TYPE -> BOOL
+  typeIsOrContainsOpt(OPT(_))      = TRUE().
+  typeIsOrContainsOpt(SEQ(t, ts))  = bOr(isOpt(t), listContainsOpt(ts)).
+  typeIsOrContainsOpt(ITER(t))     = typeIsOrContainsOpt(t).
+  typeIsOrContainsOpt(ALT(t1, t2)) = bOr(isOpt(t1), isOpt(t2)).
+  typeIsOrContainsOpt(PROD(ts, t)) = bOr(listContainsOpt(ts), isOpt(t)).
+  typeIsOrContainsOpt(INJ(ts, t))  = bOr(listContainsOpt(ts), isOpt(t)).
+  typeIsOrContainsOpt(_)           = FALSE().
+
+  isOpt: TYPE -> BOOL
+  isOpt(OPT(_)) = TRUE().
+  isOpt(_)      = FALSE().
+
+  listContainsOpt: list(TYPE) -> BOOL
+  listContainsOpt([t|ts]) = bOr(typeIsOrContainsOpt(t), listContainsOpt(ts)).
+  listContainsOpt([])     = FALSE().
+
+rules // Alt symbol checking
+
+  typeIsOrContainsAlt: TYPE -> BOOL
+  typeIsOrContainsAlt(ALT(_, _))   = TRUE().
+  typeIsOrContainsAlt(SEQ(t, ts))  = bOr(isAlt(t), listContainsAlt(ts)).
+  typeIsOrContainsAlt(ITER(t))     = typeIsOrContainsAlt(t).
+  typeIsOrContainsAlt(OPT(t))      = isAlt(t).
+  typeIsOrContainsAlt(PROD(ts, t)) = bOr(listContainsAlt(ts), isAlt(t)).
+  typeIsOrContainsAlt(INJ(ts, t))  = bOr(listContainsAlt(ts), isAlt(t)).
+  typeIsOrContainsAlt(_)           = FALSE().
+
+  isAlt: TYPE -> BOOL
+  isAlt(ALT(_, _)) = TRUE().
+  isAlt(_)         = FALSE().
+
+  listContainsAlt: list(TYPE) -> BOOL
+  listContainsAlt([t|ts]) = bOr(typeIsOrContainsAlt(t), listContainsAlt(ts)).
+  listContainsAlt([])     = FALSE().
+
+rules // Seq symbol checking
+
+  typeIsOrContainsSeq: TYPE -> BOOL
+  typeIsOrContainsSeq(SEQ(_, _))   = TRUE().
+  typeIsOrContainsSeq(OPT(t))      = isSeq(t).
+  typeIsOrContainsSeq(ITER(t))     = typeIsOrContainsSeq(t).
+  typeIsOrContainsSeq(ALT(t1, t2)) = bOr(isSeq(t1), isSeq(t2)).
+  typeIsOrContainsSeq(PROD(ts, t)) = bOr(listContainsSeq(ts), isSeq(t)).
+  typeIsOrContainsSeq(INJ(ts, t))  = bOr(listContainsSeq(ts), isSeq(t)).
+  typeIsOrContainsSeq(_)           = FALSE().
+
+  isSeq: TYPE -> BOOL
+  isSeq(SEQ(_, _)) = TRUE().
+  isSeq(_)         = FALSE().
+
+  listContainsSeq: list(TYPE) -> BOOL
+  listContainsSeq([t|ts]) = bOr(typeIsOrContainsSeq(t), listContainsSeq(ts)).
+  listContainsSeq([])     = FALSE().
diff --git a/org.metaborg.meta.lang.template/trans/statix/section/syntax.stx b/org.metaborg.meta.lang.template/trans/statix/section/syntax.stx
@@ -77,17 +77,15 @@ rules
     typesOfSymbols(sProd, symbols) == Tsymbols,
     Tprod == INJ(Tsymbols, Tsort),
     @rhs.type := Tprod,
-    TprodNoLayout == removeLayoutFromProdResult(Tprod),
-    symbolDefProductionOK(Kexpected, TprodNoLayout, attrs, symbolDef),
-    attributesOk(sProd, countProdResult(TprodNoLayout), attrs).
+    symbolDefProductionOK(Kexpected, removeLayoutFromProdResult(Tprod), attrs, symbolDef),
+    attributesOk(sProd, attrs).
   typeOfSdfProduction(s, Kexpected, SdfProductionWithCons(sortCons, rhs@Rhs(symbols), attrs)) = Tprod :- {Kactual sProd Tsymbols Tsort TprodNoLayout}
     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,
     @rhs.type := Tprod,
-    TprodNoLayout == removeLayoutFromProdResult(Tprod),
-    sortConsProductionOK(Kexpected, TprodNoLayout, attrs, sortCons),
-    attributesOk(sProd, countProdResult(TprodNoLayout), attrs).
+    sortConsProductionOK(Kexpected, removeLayoutFromProdResult(Tprod), attrs, sortCons),
+    attributesOk(sProd, attrs).
   typeOfSdfProductions maps typeOfSdfProduction(*, *, list(*)) = list(*)