@@ -281,43 +281,36 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
281281 /** Gets the type at `path` in the type tree. */
282282 Type getTypeAt ( TypePath path ) ;
283283
284- /** Gets a textual representation of this type. */
284+ /** Gets a textual representation of this type tree . */
285285 string toString ( ) ;
286286
287- /** Gets the location of this type. */
287+ /** Gets the location of this type tree . */
288288 Location getLocation ( ) ;
289289 }
290290
291- /** Provides the input to `Make2`. */
292- signature module InputSig2 {
293- /** A type mention, for example a type annotation in a local variable declaration. */
294- class TypeMention {
295- /**
296- * Gets the type being mentioned at `path` inside this type mention.
297- *
298- * For example, in
299- *
300- * ```csharp
301- * C<int> x = ...
302- * ```
303- *
304- * the type mention in the declaration of `x` resolves to the following
305- * types:
306- *
307- * `TypePath` | `Type`
308- * ---------- | -------
309- * `""` | ``C`1``
310- * `"0"` | `int`
311- */
312- Type resolveTypeAt ( TypePath path ) ;
313-
314- /** Gets a textual representation of this type mention. */
315- string toString ( ) ;
316-
317- /** Gets the location of this type mention. */
318- Location getLocation ( ) ;
319- }
320-
291+ /**
292+ * Provides the input to `Make2`.
293+ *
294+ * The `TypeMention` parameter is used to build the base type hierarchy based on
295+ * `getABaseTypeMention` and to construct the constraint satisfaction
296+ * hierarchy based on `conditionSatisfiesConstraint`.
297+ *
298+ * It will usually be based on syntactic occurrences of types in the source
299+ * code. For example, in
300+ *
301+ * ```csharp
302+ * class C<T> : Base<T>, Interface { }
303+ * ```
304+ *
305+ * a type mention would exist for `Base<T>` and resolve to the following
306+ * types:
307+ *
308+ * `TypePath` | `Type`
309+ * ---------- | -------
310+ * `""` | ``Base`1``
311+ * `"0"` | `T`
312+ */
313+ signature module InputSig2< HasTypeTreeSig TypeMention> {
321314 /**
322315 * Gets a base type mention of `t`, if any. Example:
323316 *
@@ -394,22 +387,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
394387 ) ;
395388 }
396389
397- module Make2< InputSig2 Input2> {
390+ module Make2< HasTypeTreeSig TypeMention , InputSig2< TypeMention > Input2> {
398391 private import Input2
399392
400- final private class FinalTypeMention = TypeMention ;
401-
402- /** An adapter for type mentions to implement `HasTypeTreeSig`. */
403- final class TypeMentionTypeTree extends FinalTypeMention {
404- Type getTypeAt ( TypePath path ) { result = this .resolveTypeAt ( path ) }
405- }
406-
407393 /** Gets the type at the empty path of `tm`. */
408394 bindingset [ tm]
409395 pragma [ inline_late]
410- private Type resolveTypeMentionRoot ( TypeMention tm ) {
411- result = tm .resolveTypeAt ( TypePath:: nil ( ) )
412- }
396+ private Type getTypeMentionRoot ( TypeMention tm ) { result = tm .getTypeAt ( TypePath:: nil ( ) ) }
413397
414398 /** Provides the input to `IsInstantiationOf`. */
415399 signature module IsInstantiationOfInputSig< HasTypeTreeSig App, HasTypeTreeSig Constraint> {
@@ -467,25 +451,25 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
467451 }
468452
469453 pragma [ nomagic]
470- private Type resolveTypeAt ( App app , TypeAbstraction abs , Constraint constraint , TypePath path ) {
454+ private Type getTypeAt ( App app , TypeAbstraction abs , Constraint constraint , TypePath path ) {
471455 potentialInstantiationOf ( app , abs , constraint ) and
472456 result = constraint .getTypeAt ( path )
473457 }
474458
475459 pragma [ nomagic]
476- private Type resolveNthTypeAt (
460+ private Type getNthTypeAt (
477461 App app , TypeAbstraction abs , Constraint constraint , int i , TypePath path
478462 ) {
479463 path = getNthPath ( constraint , i ) and
480- result = resolveTypeAt ( app , abs , constraint , path )
464+ result = getTypeAt ( app , abs , constraint , path )
481465 }
482466
483467 pragma [ nomagic]
484468 private predicate satisfiesConcreteTypesToIndex (
485469 App app , TypeAbstraction abs , Constraint constraint , int i
486470 ) {
487471 exists ( Type t , TypePath path |
488- t = resolveNthTypeAt ( app , abs , constraint , i , path ) and
472+ t = getNthTypeAt ( app , abs , constraint , i , path ) and
489473 if t = abs .getATypeParameter ( ) then any ( ) else app .getTypeAt ( path ) = t
490474 ) and
491475 // Recurse unless we are at the first path
@@ -622,7 +606,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
622606 ) {
623607 // `app` and `constraint` differ on a concrete type
624608 exists ( Type t , Type t2 |
625- t = resolveTypeAt ( app , abs , constraint , path ) and
609+ t = getTypeAt ( app , abs , constraint , path ) and
626610 not t = abs .getATypeParameter ( ) and
627611 app .getTypeAt ( path ) = t2 and
628612 t2 != t
@@ -645,29 +629,27 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
645629 TypeMention tm1 , TypeMention tm2 , TypeParameter tp , TypePath path , Type t
646630 ) {
647631 exists ( TypePath prefix |
648- tm2 .resolveTypeAt ( prefix ) = tp and t = tm1 .resolveTypeAt ( prefix .appendInverse ( path ) )
632+ tm2 .getTypeAt ( prefix ) = tp and t = tm1 .getTypeAt ( prefix .appendInverse ( path ) )
649633 )
650634 }
651635
652636 private module IsInstantiationOfInput implements
653- IsInstantiationOfInputSig< TypeMentionTypeTree , TypeMentionTypeTree >
637+ IsInstantiationOfInputSig< TypeMention , TypeMention >
654638 {
655639 pragma [ nomagic]
656- private predicate typeCondition (
657- Type type , TypeAbstraction abs , TypeMentionTypeTree condition
658- ) {
640+ private predicate typeCondition ( Type type , TypeAbstraction abs , TypeMention condition ) {
659641 conditionSatisfiesConstraint ( abs , condition , _, _) and
660- type = resolveTypeMentionRoot ( condition )
642+ type = getTypeMentionRoot ( condition )
661643 }
662644
663645 pragma [ nomagic]
664- private predicate typeConstraint ( Type type , TypeMentionTypeTree constraint ) {
646+ private predicate typeConstraint ( Type type , TypeMention constraint ) {
665647 conditionSatisfiesConstraint ( _, _, constraint , _) and
666- type = resolveTypeMentionRoot ( constraint )
648+ type = getTypeMentionRoot ( constraint )
667649 }
668650
669651 predicate potentialInstantiationOf (
670- TypeMentionTypeTree constraint , TypeAbstraction abs , TypeMentionTypeTree condition
652+ TypeMention constraint , TypeAbstraction abs , TypeMention condition
671653 ) {
672654 exists ( Type type |
673655 typeConstraint ( type , constraint ) and typeCondition ( type , abs , condition )
@@ -684,14 +666,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
684666 ) {
685667 // base case
686668 conditionSatisfiesConstraint ( abs , condition , constraint , _) and
687- constraint .resolveTypeAt ( path ) = t
669+ constraint .getTypeAt ( path ) = t
688670 or
689671 // recursive case
690672 exists ( TypeAbstraction midAbs , TypeMention midConstraint , TypeMention midCondition |
691673 conditionSatisfiesConstraint ( abs , condition , midConstraint , true ) and
692674 // NOTE: `midAbs` describe the free type variables in `midCondition`, hence
693675 // we use that for instantiation check.
694- IsInstantiationOf< TypeMentionTypeTree , TypeMentionTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( midConstraint ,
676+ IsInstantiationOf< TypeMention , TypeMention , IsInstantiationOfInput > :: isInstantiationOf ( midConstraint ,
695677 midAbs , midCondition )
696678 |
697679 conditionSatisfiesConstraintTypeAt ( midAbs , midCondition , constraint , path , t ) and
@@ -716,8 +698,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
716698 TypeMention constraint
717699 ) {
718700 conditionSatisfiesConstraintTypeAt ( abs , condition , constraint , _, _) and
719- conditionRoot = resolveTypeMentionRoot ( condition ) and
720- constraintRoot = resolveTypeMentionRoot ( constraint )
701+ conditionRoot = getTypeMentionRoot ( condition ) and
702+ constraintRoot = getTypeMentionRoot ( constraint )
721703 }
722704
723705 /**
@@ -778,10 +760,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
778760 |
779761 // immediate base class
780762 baseMention = immediateBaseMention and
781- t = immediateBaseMention .resolveTypeAt ( path )
763+ t = immediateBaseMention .getTypeAt ( path )
782764 or
783765 // transitive base class
784- exists ( Type immediateBase | immediateBase = resolveTypeMentionRoot ( immediateBaseMention ) |
766+ exists ( Type immediateBase | immediateBase = getTypeMentionRoot ( immediateBaseMention ) |
785767 baseTypeMentionHasNonTypeParameterAt ( immediateBase , baseMention , path , t )
786768 or
787769 exists ( TypePath path0 , TypePath prefix , TypePath suffix , TypeParameter tp |
@@ -811,7 +793,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
811793 */
812794
813795 baseTypeMentionHasTypeParameterAt ( immediateBase , baseMention , prefix , tp ) and
814- t = immediateBaseMention .resolveTypeAt ( path0 ) and
796+ t = immediateBaseMention .getTypeAt ( path0 ) and
815797 path0 .isCons ( tp , suffix ) and
816798 path = prefix .append ( suffix )
817799 )
@@ -862,11 +844,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
862844 }
863845
864846 private module IsInstantiationOfInput implements
865- IsInstantiationOfInputSig< HasTypeTree , TypeMentionTypeTree >
847+ IsInstantiationOfInputSig< HasTypeTree , TypeMention >
866848 {
867- predicate potentialInstantiationOf (
868- HasTypeTree tt , TypeAbstraction abs , TypeMentionTypeTree cond
869- ) {
849+ predicate potentialInstantiationOf ( HasTypeTree tt , TypeAbstraction abs , TypeMention cond ) {
870850 exists ( Type constraint , Type type |
871851 hasTypeConstraint ( tt , type , constraint ) and
872852 rootTypesSatisfaction ( type , constraint , abs , cond , _) and
@@ -875,13 +855,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
875855 )
876856 }
877857
878- predicate relevantConstraint ( TypeMentionTypeTree constraint ) {
858+ predicate relevantConstraint ( TypeMention constraint ) {
879859 rootTypesSatisfaction ( _, _, _, constraint , _)
880860 }
881861 }
882862
883863 private module SatisfiesConstraintIsInstantiationOf =
884- IsInstantiationOf< HasTypeTree , TypeMentionTypeTree , IsInstantiationOfInput > ;
864+ IsInstantiationOf< HasTypeTree , TypeMention , IsInstantiationOfInput > ;
885865
886866 /**
887867 * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
@@ -897,8 +877,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
897877 //
898878 // not exists(countConstraintImplementations(type, constraint)) and
899879 // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
900- // resolveTypeMentionRoot (condition) = abs.getATypeParameter() and
901- // constraint = resolveTypeMentionRoot (constraintMention)
880+ // getTypeMentionRoot (condition) = abs.getATypeParameter() and
881+ // constraint = getTypeMentionRoot (constraintMention)
902882 // or
903883 countConstraintImplementations ( type , constraint ) > 0 and
904884 rootTypesSatisfaction ( type , constraint , abs , condition , constraintMention ) and
@@ -935,9 +915,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
935915 // or
936916 // forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
937917 // conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
938- // resolveTypeMentionRoot (condition) = abs.getATypeParameter()
918+ // getTypeMentionRoot (condition) = abs.getATypeParameter()
939919 // |
940- // not constraint = resolveTypeMentionRoot (constraintMention)
920+ // not constraint = getTypeMentionRoot (constraintMention)
941921 // )
942922 // ) and
943923 (
@@ -973,7 +953,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
973953 exists ( TypeMention sub , TypeParameter tp |
974954 satisfiesConstraintTypeMention0 ( tt , constraint , abs , sub , path , tp ) and
975955 tp = abs .getATypeParameter ( ) and
976- sub .resolveTypeAt ( pathToTypeParamInSub ) = tp
956+ sub .getTypeAt ( pathToTypeParamInSub ) = tp
977957 )
978958 }
979959
@@ -1265,7 +1245,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
12651245 Access a , AccessEnvironment e , AccessPosition apos , TypeMention baseMention ,
12661246 TypePath path , Type t
12671247 ) {
1268- relevantAccess ( a , e , apos , resolveTypeMentionRoot ( baseMention ) ) and
1248+ relevantAccess ( a , e , apos , getTypeMentionRoot ( baseMention ) ) and
12691249 exists ( Type sub | sub = a .getInferredType ( e , apos , TypePath:: nil ( ) ) |
12701250 baseTypeMentionHasNonTypeParameterAt ( sub , baseMention , path , t )
12711251 or
@@ -1351,7 +1331,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13511331 ) {
13521332 exists ( TypeMention tm |
13531333 AccessBaseType:: hasBaseTypeMention ( a , e , apos , tm , path , t ) and
1354- base = resolveTypeMentionRoot ( tm )
1334+ base = getTypeMentionRoot ( tm )
13551335 )
13561336 }
13571337
@@ -1680,7 +1660,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
16801660 }
16811661
16821662 query predicate illFormedTypeMention ( TypeMention tm ) {
1683- not exists ( tm .resolveTypeAt ( TypePath:: nil ( ) ) ) and exists ( tm .getLocation ( ) )
1663+ not exists ( tm .getTypeAt ( TypePath:: nil ( ) ) ) and exists ( tm .getLocation ( ) )
16841664 }
16851665 }
16861666 }
0 commit comments