@@ -171,15 +171,20 @@ module Public {
171171 )
172172 }
173173
174+ private newtype TRequiredSummaryComponentStack = MkRequiredSummaryComponentStack ( )
175+
174176 /**
175177 * A class that exists for QL technical reasons only (the IPA type used
176178 * to represent component stacks needs to be bounded).
177179 */
178- abstract class RequiredSummaryComponentStack extends SummaryComponentStack {
180+ class RequiredSummaryComponentStack extends TRequiredSummaryComponentStack {
181+ /** Gets a textual representation of this element. */
182+ string toString ( ) { none ( ) }
183+
179184 /**
180185 * Holds if the stack obtained by pushing `head` onto `tail` is required.
181186 */
182- abstract predicate required ( SummaryComponent c ) ;
187+ predicate required ( SummaryComponent head , SummaryComponentStack tail ) { none ( ) }
183188 }
184189
185190 /** A callable with a flow summary. */
@@ -240,9 +245,9 @@ module Private {
240245 newtype TSummaryComponentStack =
241246 TSingletonSummaryComponentStack ( SummaryComponent c ) or
242247 TConsSummaryComponentStack ( SummaryComponent head , SummaryComponentStack tail ) {
243- tail . ( RequiredSummaryComponentStack ) .required ( head )
248+ any ( RequiredSummaryComponentStack x ) .required ( head , tail )
244249 or
245- tail . ( RequiredSummaryComponentStack ) .required ( TParameterSummaryComponent ( _) ) and
250+ any ( RequiredSummaryComponentStack x ) .required ( TParameterSummaryComponent ( _) , tail ) and
246251 head = thisParam ( )
247252 or
248253 derivedFluentFlowPush ( _, _, _, head , tail , _)
@@ -890,9 +895,9 @@ module Private {
890895 }
891896
892897 private class MkStack extends RequiredSummaryComponentStack {
893- MkStack ( ) { interpretSpec ( _ , _ , _ , this ) }
894-
895- override predicate required ( SummaryComponent c ) { interpretSpec ( _ , _ , c , this ) }
898+ override predicate required ( SummaryComponent head , SummaryComponentStack tail ) {
899+ interpretSpec ( _ , _ , head , tail )
900+ }
896901 }
897902
898903 private class SummarizedCallableExternal extends SummarizedCallable {
0 commit comments