@@ -5,68 +5,110 @@ private import TypeAbstraction
55private import TypeMention
66private import TypeInference
77
8- private newtype TFunctionPosition =
9- TArgumentFunctionPosition ( ArgumentPosition pos ) or
10- TReturnFunctionPosition ( )
8+ private signature predicate includeSelfSig ( ) ;
9+
10+ private module MkFunctionPosition< includeSelfSig / 0 includeSelf> {
11+ private newtype TFunctionPosition =
12+ TArgumentFunctionPosition ( ArgumentPosition pos ) {
13+ if pos .isSelf ( ) then includeSelf ( ) else any ( )
14+ } or
15+ TReturnFunctionPosition ( )
16+
17+ class FunctionPosition extends TFunctionPosition {
18+ int asPosition ( ) { result = this .asArgumentPosition ( ) .asPosition ( ) }
19+
20+ predicate isPosition ( ) { exists ( this .asPosition ( ) ) }
21+
22+ ArgumentPosition asArgumentPosition ( ) { this = TArgumentFunctionPosition ( result ) }
23+
24+ predicate isTypeQualifier ( ) { this .asArgumentPosition ( ) .isTypeQualifier ( ) }
25+
26+ predicate isReturn ( ) { this = TReturnFunctionPosition ( ) }
27+
28+ TypeMention getTypeMention ( Function f ) {
29+ result = f .getParam ( this .asPosition ( ) ) .getTypeRepr ( )
30+ or
31+ this .isReturn ( ) and
32+ result = getReturnTypeMention ( f )
33+ }
34+
35+ string toString ( ) {
36+ result = this .asArgumentPosition ( ) .toString ( )
37+ or
38+ this .isReturn ( ) and
39+ result = "(return)"
40+ }
41+ }
42+ }
43+
44+ private predicate any_ ( ) { any ( ) }
1145
1246/**
1347 * A position of a type related to a function.
1448 *
1549 * Either `self`, `return`, or a positional parameter index.
1650 */
17- class FunctionPosition extends TFunctionPosition {
51+ final class FunctionPosition extends MkFunctionPosition < any_ / 0 > :: FunctionPosition {
1852 predicate isSelf ( ) { this .asArgumentPosition ( ) .isSelf ( ) }
1953
20- int asPosition ( ) { result = this .asArgumentPosition ( ) .asPosition ( ) }
21-
22- predicate isPosition ( ) { exists ( this .asPosition ( ) ) }
23-
24- ArgumentPosition asArgumentPosition ( ) { this = TArgumentFunctionPosition ( result ) }
25-
26- predicate isTypeQualifier ( ) { this .asArgumentPosition ( ) .isTypeQualifier ( ) }
27-
2854 predicate isSelfOrTypeQualifier ( ) { this .isSelf ( ) or this .isTypeQualifier ( ) }
2955
30- predicate isReturn ( ) { this = TReturnFunctionPosition ( ) }
56+ override TypeMention getTypeMention ( Function f ) {
57+ result = super .getTypeMention ( f )
58+ or
59+ this .isSelf ( ) and
60+ result = getSelfParamTypeMention ( f .getSelfParam ( ) )
61+ }
3162
3263 /**
3364 * Gets the corresponding position when function call syntax is used, assuming
3465 * this position is for a method.
3566 */
36- FunctionPosition getFunctionCallAdjusted ( ) {
37- ( this .isReturn ( ) or this .isTypeQualifier ( ) ) and
38- result = this
67+ pragma [ nomagic]
68+ FunctionPositionAdj getFunctionCallAdjusted ( ) {
69+ this .isReturn ( ) and result .isReturn ( )
70+ or
71+ this .isTypeQualifier ( ) and
72+ result .isTypeQualifier ( )
3973 or
4074 this .isSelf ( ) and result .asPosition ( ) = 0
4175 or
4276 result .asPosition ( ) = this .asPosition ( ) + 1
4377 }
4478
79+ /**
80+ * Gets the corresponding position when function call syntax is used, assuming
81+ * this position is _not_ for a method.
82+ */
83+ pragma [ nomagic]
84+ FunctionPositionAdj asAdjusted ( ) {
85+ this .isReturn ( ) and result .isReturn ( )
86+ or
87+ this .isTypeQualifier ( ) and
88+ result .isTypeQualifier ( )
89+ or
90+ result .asPosition ( ) = this .asPosition ( )
91+ }
92+
4593 /**
4694 * Gets the corresponding position when `f` is invoked via function call
4795 * syntax.
4896 */
4997 bindingset [ f]
50- FunctionPosition getFunctionCallAdjusted ( Function f ) {
51- if f .hasSelfParam ( ) then result = this .getFunctionCallAdjusted ( ) else result = this
98+ FunctionPositionAdj getFunctionCallAdjusted ( Function f ) {
99+ if f .hasSelfParam ( ) then result = this .getFunctionCallAdjusted ( ) else result = this . asAdjusted ( )
52100 }
101+ }
53102
54- TypeMention getTypeMention ( Function f ) {
55- this .isSelf ( ) and
56- result = getSelfParamTypeMention ( f .getSelfParam ( ) )
57- or
58- result = f .getParam ( this .asPosition ( ) ) .getTypeRepr ( )
59- or
60- this .isReturn ( ) and
61- result = getReturnTypeMention ( f )
62- }
103+ private predicate none_ ( ) { none ( ) }
63104
64- string toString ( ) {
65- result = this .asArgumentPosition ( ) .toString ( )
66- or
67- this .isReturn ( ) and
68- result = "(return)"
69- }
105+ /**
106+ * A function-call adjust position of a type related to a function.
107+ *
108+ * Either `return` or a positional parameter index.
109+ */
110+ final class FunctionPositionAdj extends MkFunctionPosition< none_ / 0 > :: FunctionPosition {
111+ FunctionPosition asNonAdjusted ( ) { this = result .asAdjusted ( ) }
70112}
71113
72114/**
@@ -83,6 +125,20 @@ module FunctionPositionMatchingInput {
83125 }
84126}
85127
128+ /**
129+ * A helper module for implementing `Matching(WithEnvironment)InputSig` with
130+ * `DeclarationPosition = AccessPosition = FunctionPositionAdj`.
131+ */
132+ module FunctionPositionAdjMatchingInput {
133+ class DeclarationPosition = FunctionPositionAdj ;
134+
135+ class AccessPosition = DeclarationPosition ;
136+
137+ predicate accessDeclarationPositionMatch ( AccessPosition apos , DeclarationPosition dpos ) {
138+ apos = dpos
139+ }
140+ }
141+
86142private newtype TAssocFunctionType =
87143 /** An associated function `f` in `parent` should be specialized for `i` at `pos`. */
88144 MkAssocFunctionType (
@@ -323,15 +379,15 @@ signature module ArgsAreInstantiationsOfInputSig {
323379 * `posAdj` is one of the function-call adjusted positions in `f` in which the relevant
324380 * type occurs.
325381 */
326- predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ) ;
382+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPositionAdj posAdj ) ;
327383
328384 /** A call whose argument types are to be checked. */
329385 class Call {
330386 string toString ( ) ;
331387
332388 Location getLocation ( ) ;
333389
334- Type getArgType ( FunctionPosition posAdj , TypePath path ) ;
390+ Type getArgType ( FunctionPositionAdj posAdj , TypePath path ) ;
335391
336392 predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
337393 }
@@ -345,7 +401,7 @@ signature module ArgsAreInstantiationsOfInputSig {
345401module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
346402 pragma [ nomagic]
347403 private predicate toCheckRanked (
348- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj , int rnk
404+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPositionAdj posAdj , int rnk
349405 ) {
350406 Input:: toCheck ( i , f , tp , posAdj ) and
351407 tp =
@@ -359,7 +415,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
359415
360416 pragma [ nomagic]
361417 private predicate toCheck (
362- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ,
418+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPositionAdj posAdj ,
363419 AssocFunctionType t
364420 ) {
365421 exists ( FunctionPosition pos |
@@ -370,20 +426,20 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
370426 }
371427
372428 private newtype TCallAndPosAdj =
373- MkCallAndPosAdj ( Input:: Call call , FunctionPosition posAdj ) {
429+ MkCallAndPosAdj ( Input:: Call call , FunctionPositionAdj posAdj ) {
374430 exists ( call .getArgType ( posAdj , _) )
375431 }
376432
377433 /** A call tagged with a function-call adjusted position. */
378434 private class CallAndPosAdj extends MkCallAndPosAdj {
379435 Input:: Call call ;
380- FunctionPosition posAdj ;
436+ FunctionPositionAdj posAdj ;
381437
382438 CallAndPosAdj ( ) { this = MkCallAndPosAdj ( call , posAdj ) }
383439
384440 Input:: Call getCall ( ) { result = call }
385441
386- FunctionPosition getPosAdj ( ) { result = posAdj }
442+ FunctionPositionAdj getPosAdj ( ) { result = posAdj }
387443
388444 Location getLocation ( ) { result = call .getLocation ( ) }
389445
@@ -394,7 +450,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
394450
395451 pragma [ nomagic]
396452 private predicate potentialInstantiationOf0 (
397- CallAndPosAdj cp , Input:: Call call , TypeParameter tp , FunctionPosition posAdj , Function f ,
453+ CallAndPosAdj cp , Input:: Call call , TypeParameter tp , FunctionPositionAdj posAdj , Function f ,
398454 TypeAbstraction abs , AssocFunctionType constraint
399455 ) {
400456 cp = MkCallAndPosAdj ( call , pragma [ only_bind_into ] ( posAdj ) ) and
@@ -409,7 +465,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
409465 predicate potentialInstantiationOf (
410466 CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
411467 ) {
412- exists ( Input:: Call call , TypeParameter tp , FunctionPosition posAdj , int rnk , Function f |
468+ exists ( Input:: Call call , TypeParameter tp , FunctionPositionAdj posAdj , int rnk , Function f |
413469 potentialInstantiationOf0 ( cp , call , tp , posAdj , f , abs , constraint ) and
414470 toCheckRanked ( abs , f , tp , posAdj , rnk )
415471 |
@@ -429,7 +485,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
429485 private predicate argIsInstantiationOf (
430486 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
431487 ) {
432- exists ( FunctionPosition posAdj |
488+ exists ( FunctionPositionAdj posAdj |
433489 ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _) and
434490 toCheckRanked ( i , f , _, posAdj , rnk )
435491 )
@@ -480,7 +536,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
480536
481537 pragma [ nomagic]
482538 private predicate argsAreNotInstantiationsOf0 (
483- Input:: Call call , FunctionPosition posAdj , ImplOrTraitItemNode i
539+ Input:: Call call , FunctionPositionAdj posAdj , ImplOrTraitItemNode i
484540 ) {
485541 ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _, _)
486542 }
@@ -493,7 +549,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
493549 */
494550 pragma [ nomagic]
495551 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
496- exists ( FunctionPosition posAdj |
552+ exists ( FunctionPositionAdj posAdj |
497553 argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
498554 call .hasTargetCand ( i , f ) and
499555 Input:: toCheck ( i , f , _, posAdj )
0 commit comments