@@ -171,15 +171,20 @@ module Public {
171
171
)
172
172
}
173
173
174
+ private newtype TRequiredSummaryComponentStack = MkRequiredSummaryComponentStack ( )
175
+
174
176
/**
175
177
* A class that exists for QL technical reasons only (the IPA type used
176
178
* to represent component stacks needs to be bounded).
177
179
*/
178
- abstract class RequiredSummaryComponentStack extends SummaryComponentStack {
180
+ class RequiredSummaryComponentStack extends TRequiredSummaryComponentStack {
181
+ /** Gets a textual representation of this element. */
182
+ string toString ( ) { none ( ) }
183
+
179
184
/**
180
185
* Holds if the stack obtained by pushing `head` onto `tail` is required.
181
186
*/
182
- abstract predicate required ( SummaryComponent c ) ;
187
+ predicate required ( SummaryComponent head , SummaryComponentStack tail ) { none ( ) }
183
188
}
184
189
185
190
/** A callable with a flow summary. */
@@ -240,9 +245,9 @@ module Private {
240
245
newtype TSummaryComponentStack =
241
246
TSingletonSummaryComponentStack ( SummaryComponent c ) or
242
247
TConsSummaryComponentStack ( SummaryComponent head , SummaryComponentStack tail ) {
243
- tail . ( RequiredSummaryComponentStack ) .required ( head )
248
+ any ( RequiredSummaryComponentStack x ) .required ( head , tail )
244
249
or
245
- tail . ( RequiredSummaryComponentStack ) .required ( TParameterSummaryComponent ( _) ) and
250
+ any ( RequiredSummaryComponentStack x ) .required ( TParameterSummaryComponent ( _) , tail ) and
246
251
head = thisParam ( )
247
252
or
248
253
derivedFluentFlowPush ( _, _, _, head , tail , _)
@@ -890,9 +895,9 @@ module Private {
890
895
}
891
896
892
897
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
+ }
896
901
}
897
902
898
903
private class SummarizedCallableExternal extends SummarizedCallable {
0 commit comments