@@ -62,7 +62,7 @@ abstract class ConditionalCompletion extends NormalCompletion {
62
62
abstract ConditionalCompletion getDual ( ) ;
63
63
}
64
64
65
- /** Holds if node `le` has the Boolean constant value `value`. */
65
+ /** Holds if node `le` has the constant Boolean value `value`. */
66
66
private predicate isBooleanConstant ( LiteralExpr le , Boolean value ) {
67
67
le .getTextValue ( ) = value .toString ( )
68
68
}
@@ -117,13 +117,56 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
117
117
override string toString ( ) { result = "boolean(" + value + ")" }
118
118
}
119
119
120
+ /** Holds if `pat` is guaranteed to match. */
121
+ pragma [ nomagic]
122
+ private predicate isIrrefutablePattern ( Pat pat ) {
123
+ (
124
+ pat instanceof WildcardPat
125
+ or
126
+ pat = any ( IdentPat ip | not ip .hasPat ( ) and ip = any ( Variable v ) .getPat ( ) )
127
+ or
128
+ pat instanceof RestPat
129
+ or
130
+ // `let` statements without an `else` branch must be irrefutible
131
+ pat = any ( LetStmt let | not let .hasLetElse ( ) ) .getPat ( )
132
+ or
133
+ // `match` expressions must be irrefutible, so last arm cannot fail
134
+ pat = any ( MatchExpr me ) .getLastArm ( ) .getPat ( )
135
+ or
136
+ // parameter patterns must be irrefutible
137
+ pat = any ( Param p ) .getPat ( )
138
+ ) and
139
+ not pat = any ( ForExpr for ) .getPat ( ) // workaround until `for` loops are desugared
140
+ or
141
+ exists ( Pat parent | isIrrefutablePattern ( parent ) |
142
+ pat = parent .( BoxPat ) .getPat ( )
143
+ or
144
+ pat = parent .( IdentPat ) .getPat ( )
145
+ or
146
+ pat = parent .( ParenPat ) .getPat ( )
147
+ or
148
+ pat = parent .( RecordPat ) .getRecordPatFieldList ( ) .getField ( _) .getPat ( )
149
+ or
150
+ pat = parent .( RefPat ) .getPat ( )
151
+ or
152
+ pat = parent .( TuplePat ) .getAField ( )
153
+ or
154
+ pat = parent .( TupleStructPat ) .getAField ( )
155
+ or
156
+ pat = parent .( OrPat ) .getLastPat ( )
157
+ )
158
+ }
159
+
120
160
/**
121
161
* A completion that represents the result of a pattern match.
122
162
*/
123
163
class MatchCompletion extends TMatchCompletion , ConditionalCompletion {
124
164
MatchCompletion ( ) { this = TMatchCompletion ( value ) }
125
165
126
- override predicate isValidForSpecific ( AstNode e ) { e instanceof Pat }
166
+ override predicate isValidForSpecific ( AstNode e ) {
167
+ e instanceof Pat and
168
+ if isIrrefutablePattern ( e ) then value = true else any ( )
169
+ }
127
170
128
171
override MatchSuccessor getAMatchingSuccessorType ( ) { result .getValue ( ) = value }
129
172
0 commit comments