@@ -1226,30 +1226,20 @@ class ComparableType extends NamedType {
12261226}
12271227
12281228pragma [ nomagic]
1229- private predicate unpackTupleType ( TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents ) {
1229+ private predicate unpackTupleType (
1230+ TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents
1231+ ) {
12301232 nComponents = count ( int i | component_types ( tt , i , _, _) ) and
1231- (
1232- if nComponents >= 1
1233- then c0 = MkSomeType ( tt .getComponentType ( 0 ) )
1234- else c0 = MkNoType ( )
1235- ) and
1236- (
1237- if nComponents >= 2
1238- then c1 = MkSomeType ( tt .getComponentType ( 1 ) )
1239- else c1 = MkNoType ( )
1240- ) and
1241- (
1242- if nComponents >= 3
1243- then c2 = MkSomeType ( tt .getComponentType ( 2 ) )
1244- else c2 = MkNoType ( )
1245- )
1233+ ( if nComponents >= 1 then c0 = MkSomeType ( tt .getComponentType ( 0 ) ) else c0 = MkNoType ( ) ) and
1234+ ( if nComponents >= 2 then c1 = MkSomeType ( tt .getComponentType ( 1 ) ) else c1 = MkNoType ( ) ) and
1235+ ( if nComponents >= 3 then c2 = MkSomeType ( tt .getComponentType ( 2 ) ) else c2 = MkNoType ( ) )
12461236}
12471237
12481238pragma [ nomagic]
1249- private predicate unpackAndUnaliasTupleType ( TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents ) {
1250- exists (
1251- OptType c0a , OptType c1a , OptType c2a
1252- |
1239+ private predicate unpackAndUnaliasTupleType (
1240+ TupleType tt , TOptType c0 , TOptType c1 , TOptType c2 , int nComponents
1241+ ) {
1242+ exists ( OptType c0a , OptType c1a , OptType c2a |
12531243 unpackTupleType ( tt , c0a , c1a , c2a , nComponents ) and
12541244 c0 = c0a .getDeepUnaliasedType ( ) and
12551245 c1 = c1a .getDeepUnaliasedType ( ) and
@@ -1263,9 +1253,7 @@ class TupleType extends @tupletype, CompositeType {
12631253 Type getComponentType ( int i ) { component_types ( this , i , _, result ) }
12641254
12651255 private TupleType getCandidateDeepUnaliasedType ( ) {
1266- exists (
1267- OptType c0 , OptType c1 , OptType c2 , int nComponents
1268- |
1256+ exists ( OptType c0 , OptType c1 , OptType c2 , int nComponents |
12691257 unpackAndUnaliasTupleType ( this , c0 , c1 , c2 , nComponents ) and
12701258 unpackTupleType ( result , c0 , c1 , c2 , nComponents )
12711259 )
@@ -1279,9 +1267,7 @@ class TupleType extends @tupletype, CompositeType {
12791267 or
12801268 this .isDeepUnaliasedTypeUpTo ( tt , i - 1 )
12811269 ) and
1282- exists ( Type tp | component_types ( this , i , _, tp ) |
1283- component_types ( tt , i , _, tp .getDeepUnaliasedType ( ) )
1284- )
1270+ tt .getComponentType ( i ) = this .getComponentType ( i ) .getDeepUnaliasedType ( )
12851271 }
12861272
12871273 override TupleType getDeepUnaliasedType ( ) {
0 commit comments