@@ -20,6 +20,44 @@ import Lean.Meta.Match.CaseArraySizes
import Lean . Meta . Match . CaseValues
import Lean . Meta . Match . NamedPatterns
/- !
This module implements the backend of match compilation. The elaborator has already elaborated
the patterns and the the expected type of the matcher is known.
The match compilation task is represented as a `Problem`, which is then processed interatively by
the `process` function. It has various “moves” which it tries in a particular order, to make progress
on the problem, possibly splitting it.
The high - level overview of moves are
* If no variables are left, process as leaf
* If there is an alternative, solve its constraints
* Else use `contradiction` to prove completeness of the match
* Process “independent prefixes” of patterns. These are patterns that can be processed without
affecting the aother alternatives, and without side effects in the sense of updating the `mvarId`.
These are
- variable patterns; substitute
- inaccessible patterns; add equality constraints
- as - patterns: substitute value and equality
After thes have been processed, we use `.inaccessible x` where `x` is the variable being matched
to mark them as “done”.
* If all patterns start with “done”, drop the first variable
* The first alt has only “done” patterns, drop remaining alts (they're overlapped)
* If the first alternative has its first refutable pattern not at the front, move it to the front.
* If we have both constructor and value patterns, expand the values to constructors.
* If next pattern is not a variable, but an expression, then
- if it is a constructor, behave a bit as if we just did a case split
- else move it to constraints
* If we have constructor patterns, or no alternatives, split by constructor
Use sparse splitting if not all constructors are present
* If match is empty (no alts), drop the variable
* If we have value patterns (e.g. strings), split by value
* If we have array literal patterns, split by array
If we reach this point, the match is not supported.
If only nat value patterns exist, we expand them for better error messages.
Throw error.
-/
public section
namespace Lean . Meta . Match
@@ -176,11 +214,6 @@ private def isNextVar (p : Problem) : Bool :=
| . fvar _ :: _ = > true
| _ = > false
private def hasAsPattern ( p : Problem ) : Bool : =
p . alts . any fun alt = > match alt . patterns with
| . as . . :: _ = > true
| _ = > false
private def hasCtorPattern ( p : Problem ) : Bool : =
p . alts . any fun alt = > match alt . patterns with
| . ctor . . :: _ = > true
@@ -191,6 +224,11 @@ private def hasValPattern (p : Problem) : Bool :=
| . val _ :: _ = > true
| _ = > false
private def hasInaccessiblePattern ( p : Problem ) : Bool : =
p . alts . any fun alt = > match alt . patterns with
| . inaccessible _ :: _ = > true
| _ = > false
private def hasNatValPattern ( p : Problem ) : MetaM Bool : =
p . alts . anyM fun alt = > do
match alt . patterns with
@@ -213,18 +251,6 @@ private def hasArrayLitPattern (p : Problem) : Bool :=
| . arrayLit . . :: _ = > true
| _ = > false
private def hasVarOrInaccessiblePattern ( p : Problem ) : Bool : =
p . alts . any fun alt = > match alt . patterns with
| . inaccessible _ :: _ = > true
| . var _ :: _ = > true
| _ = > false
private def isVariableTransition ( p : Problem ) : Bool : =
p . alts . all fun alt = > match alt . patterns with
| . inaccessible _ :: _ = > true
| . var _ :: _ = > true
| _ = > false
private def getInductiveVal? ( x : Expr ) : MetaM ( Option InductiveVal ) : = do
let xType ← inferType x
let xType ← whnfD xType
@@ -248,16 +274,15 @@ private def isConstructorTransition (p : Problem) : MetaM Bool := do
& & ( hasCtorPattern p | | p . alts . isEmpty )
& & p . alts . all fun alt = > match alt . patterns with
| . ctor . . :: _ = > true
| . var _ :: _ = > true
| . inaccessible _ :: _ = > true
| . inaccessible _ :: _ = > true -- should be a done pattern by now
| _ = > false
private def isValueTransition ( p : Problem ) : Bool : =
hasVar Pattern p & & hasVal Pattern p
& & p . alts . all fun alt = > match alt . patterns with
| . val _ :: _ = > true
| . var _ :: _ = > true
| _ = > false
hasVal Pattern p & & hasInaccessible Pattern p & &
p . alts . all fun alt = > match alt . patterns with
| . val _ :: _ = > true
| . inaccessible _ :: _ = > true -- should be a done pattern by now
| _ = > false
private def isValueOnlyTransitionCore ( p : Problem ) ( isValue : Expr → MetaM Bool ) : MetaM Bool : = do
if hasVarPattern p then return false
@@ -275,44 +300,36 @@ private def isBitVecValueTransition (p : Problem) : MetaM Bool :=
isValueOnlyTransitionCore p fun e = > return ( ← getBitVecValue? e ) . isSome
private def isArrayLitTransition ( p : Problem ) : Bool : =
hasArrayLitPattern p & & hasVar Pattern p
& & p . alts . all fun alt = > match alt . patterns with
| . arrayLit . . :: _ = > true
| . var _ :: _ = > true
| _ = > false
hasArrayLitPattern p & & hasInaccessible Pattern p & &
p . alts . all fun alt = > match alt . patterns with
| . arrayLit . . :: _ = > true
| . inaccessible _ :: _ = > true -- should be a done pattern by now
| _ = > false
private def hasCtorOrInaccessible ( p : Problem ) : Bool : =
private def hasCtor ( p : Problem ) : Bool : =
! isNextVar p | |
p . alts . any fun alt = > match alt . patterns with
| . ctor . . :: _ = > true
| . inaccessible _ :: _ = > true
| _ = > false
private def isNatValueTransition ( p : Problem ) : MetaM Bool : = do
return ( ← hasNatValPattern p ) & & hasCtorOrInaccessible p
return ( ← hasNatValPattern p ) & & hasCtor p
/--
Predicate for testing whether we need to expand `Int` value patterns into constructors.
There are two cases:
- We have constructor or inaccessible patterns. Example:
- We have constructor patterns. Example:
```
| 0, ...
| Int.toVal p, ...
...
```
- We don't have the `else` - case (i.e., varia ble pattern). This can happen
- We don't have the `else` - case (i.e., inaccessi ble pattern). This can happen
when the non - value cases are unreachable.
-/
private def isIntValueTransition ( p : Problem ) : MetaM Bool : = do
unless ( ← hasIntValPattern p ) do return false
return hasCtorOrInaccessible p | | ! hasVar Pattern p
private def processSkipInaccessible ( p : Problem ) : Problem : = Id . run do
let x :: xs : = p . vars | unreachable!
let alts : = p . alts . map fun alt = > Id . run do
let . inaccessible e :: ps : = alt . patterns | unreachable!
{ alt with patterns : = ps , cnstrs : = ( x , e ) :: alt . cnstrs }
{ p with alts : = alts , vars : = xs }
return hasCtor p | | ! hasInaccessible Pattern p
/--
If constraint is of the form `e ≋ x` where `x` is a free variable, reorient it
@@ -425,7 +442,10 @@ private partial def contradiction (mvarId : MVarId) : MetaM Bool := do
if let some fvarId : = isCtorIdxHasNotBit? localDecl . type then
trace [ Meta . Match . match ] " splitting ctorIdx assumption {localDecl.type} "
let subgoals ← mvarId . cases fvarId
return ← subgoals . allM ( contradiction · . mvarId )
-- NB: do not use `allM`, we want to process all cases to not leave
-- unsolved metavariables behind.
let allDone ← subgoals . mapM ( contradiction · . mvarId )
return allDone . all id
mvarId . admit
return false
@@ -443,62 +463,16 @@ where
| [ ] = >
let mvarId ← p . mvarId . exfalso
/- TODO: allow users to configure which tactic is used to close leaves. -/
unless ( ← contradiction mvarId ) do
if ( ← contradiction mvarId ) then
trace [ Meta . Match . match ] " contradiction succeeded "
else
trace [ Meta . Match . match ] " contradiction failed, missing alternative "
modify fun s = > { s with counterExamples : = p . examples :: s . counterExamples }
| alt :: overlapped = >
solveCnstrs p . mvarId alt
for otherAlt in overlapped do
modify fun s = > { s with overlaps : = s . overlaps . insert alt . idx otherAlt . idx }
private def processAsPattern ( p : Problem ) : MetaM Problem : = withGoalOf p do
let x :: _ : = p . vars | unreachable!
let alts ← p . alts . mapM fun alt = > do
match alt . patterns with
| . as fvarId p h :: ps = >
/- We used to use eagerly check the types here (using what was called `checkAndReplaceFVarId`),
but `x` and `fvarId` can have different types when dependent types are being used.
Let's consider the repro for issue #471
```
inductive vec : Nat → Type
| nil : vec 0
| cons : Int → vec n → vec n.succ
def vec_len : vec n → Nat
| vec.nil => 0
| x@(vec.cons h t) => vec_len t + 1
```
we reach the state
```
[Meta.Match.match] remaining variables: [x✝:(vec n✝)]
alternatives:
[n:(Nat), x:(vec (Nat.succ n)), h:(Int), t:(vec n)] | - [x@(vec.cons n h t)] => h_1 n x h t
[x✝:(vec n✝)] | - [x✝] => h_2 n✝ x✝
```
The variables `x✝:(vec n✝)` and `x:(vec (Nat.succ n))` have different types, but we perform the substitution anyway,
because we claim the "discrepancy" will be corrected after we process the pattern `(vec.cons n h t)`.
The right - hand - side is temporarily type incorrect, but we claim this is fine because it will be type correct again after
we the pattern `(vec.cons n h t)`. TODO: try to find a cleaner solution.
-/
let r ← mkEqRefl x
return { alt with patterns : = p :: ps } . replaceFVarId fvarId x | > . replaceFVarId h r
| _ = > return alt
return { p with alts : = alts }
private def processVariable ( p : Problem ) : MetaM Problem : = withGoalOf p do
let x :: xs : = p . vars | unreachable!
let alts ← p . alts . mapM fun alt = > do
match alt . patterns with
| . inaccessible e :: ps = > return { alt with patterns : = ps , cnstrs : = ( x , e ) :: alt . cnstrs }
| . var fvarId :: ps = >
withExistingLocalDecls alt . fvarDecls do
if ( ← isDefEqGuarded ( ← fvarId . getType ) ( ← inferType x ) ) then
return { alt with patterns : = ps } . replaceFVarId fvarId x
else
return { alt with patterns : = ps , cnstrs : = ( mkFVar fvarId , x ) :: alt . cnstrs }
| _ = > unreachable!
return { p with alts : = alts , vars : = xs }
trace [ Meta . Match . match ] " leaf closed "
/- !
Note that we decided to store pending constraints to address issues exposed by #1279 and #1361.
@@ -532,66 +506,11 @@ alternative `cnstrs` field.
private def inLocalDecls ( localDecls : List LocalDecl ) ( fvarId : FVarId ) : Bool : =
localDecls . any fun d = > d . fvarId = = fvarId
private def expandVarIntoCtor ( alt : Alt ) ( ctorName : Name ) : MetaM Alt : = do
let . var fvarId :: ps : = alt . patterns | unreachable!
let alt : = { alt with patterns : = ps }
withExistingLocalDecls alt . fvarDecls do
trace [ Meta . Match . unify ] " expandVarIntoCtor fvarId: {mkFVar fvarId}, ctorName: {ctorName}, alt: \n {← alt.toMessageData} "
let expectedType ← inferType ( mkFVar fvarId )
let expectedType ← whnfD expectedType
let ( ctorLevels , ctorParams ) ← getInductiveUniverseAndParams expectedType
let ctor : = mkAppN ( mkConst ctorName ctorLevels ) ctorParams
let ctorType ← inferType ctor
forallTelescopeReducing ctorType fun ctorFields resultType = > do
let ctor : = mkAppN ctor ctorFields
let alt : = alt . replaceFVarId fvarId ctor
let ctorFieldDecls ← ctorFields . mapM fun ctorField = > ctorField . fvarId! . getDecl
let newAltDecls : = ctorFieldDecls . toList + + alt . fvarDecls
let mut cnstrs : = alt . cnstrs
unless ( ← isDefEqGuarded resultType expectedType ) do
cnstrs : = ( resultType , expectedType ) :: cnstrs
trace [ Meta . Match . unify ] " expandVarIntoCtor {mkFVar fvarId} : {expectedType}, ctor: {ctor} "
let ctorFieldPatterns : = ctorFieldDecls . toList . map fun decl = > Pattern . var decl . fvarId
return { alt with fvarDecls : = newAltDecls , patterns : = ctorFieldPatterns + + alt . patterns , cnstrs }
private def expandInaccessibleIntoVar ( alt : Alt ) : MetaM Alt : = do
let . inaccessible e :: ps : = alt . patterns | unreachable!
withExistingLocalDecls alt . fvarDecls do
let type ← inferType e
withLocalDeclD `x type fun x = > do
trace [ Meta . Match . unify ] " expandInaccessibleIntoVar {x} : {type} := {e} "
return { alt with
fvarDecls : = ( ← x . fvarId! . getDecl ) :: alt . fvarDecls
patterns : = . var x . fvarId! :: ps
cnstrs : = ( x , e ) :: alt . cnstrs
}
private def hasRecursiveType ( x : Expr ) : MetaM Bool : = do
match ( ← getInductiveVal? x ) with
| some val = > return val . isRec
| _ = > return false
/-- Given `alt` s.t. the next pattern is an inaccessible pattern `e`,
try to normalize `e` into a constructor application.
If it is a constructor application of `ctorName`,
update the next patterns with the fields of the constructor.
Otherwise, move it to contraints, so that we fail unless some later step
eliminates this alternative.
-/
def processInaccessibleAsCtor ( alt : Alt ) ( ctorName : Name ) : MetaM Alt : = do
let . inaccessible e :: ps : = alt . patterns | unreachable!
trace [ Meta . Match . match ] " inaccessible step {e} as ctor {ctorName} "
withExistingLocalDecls alt . fvarDecls do
-- Try to push inaccessible annotations.
let e ← whnfD e
if let some ( ctorVal , ctorArgs ) ← constructorApp? e then
if ctorVal . name = = ctorName then
let fields : = ctorArgs . extract ctorVal . numParams ctorArgs . size
let fields : = fields . toList . map . inaccessible
return { alt with patterns : = fields + + ps }
let alt' ← expandInaccessibleIntoVar alt
expandVarIntoCtor alt' ctorName
private def hasNonTrivialExample ( p : Problem ) : Bool : =
p . examples . any fun | Example . underscore = > false | _ = > true
@@ -620,7 +539,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
-- We use a sparse case analysis only if there is at least one non-constructor pattern,
-- but not just because there are constructors missing (in that case we benefit from
-- the eager split in ruling out constructors by type or by a more explicit error message)
if backward . match . sparseCases . get ( ← getOptions ) & & hasVarOr InaccessiblePattern p then
if backward . match . sparseCases . get ( ← getOptions ) & & hasInaccessiblePattern p then
let ctors : = collectCtors p
trace [ Meta . Match . match ] " using sparse cases: {ctors} "
pure ( some ctors )
@@ -666,16 +585,14 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
let examples : = examples . map < | Example . applyFVarSubst subst
let newAlts : = p . alts . filter fun alt = > match alt . patterns with
| . ctor n . . :: _ = > n = = ctorName
| . var _ :: _ = > true
| . inaccessible _ :: _ = > true
| _ = > false
| _ = > unreachable!
let newAlts : = newAlts . map fun alt = > alt . applyFVarSubst subst
let newAlts ← newAlts . mapM fun alt = > do
match alt . patterns with
| . ctor _ _ _ fields :: ps = > return { alt with patterns : = fields + + ps }
| . var _ :: _ = > expandVarIntoCtor alt ctorName
| . inaccessible _ :: _ = > processInaccessibleAsCtor alt ctorName
| _ = > unreachable!
| . ctor _ _ _ fieldPat s :: ps = > return { alt with patterns : = fieldPat s + + ps }
| . inaccessible _ :: ps = > return { alt with patterns : = fields . map . inaccessible + + ps }
| _ = > unreachable!
return { p with mvarId : = subgoal . mvarId , vars : = newVars , alts : = newAlts , examples : = examples }
else
-- A catch-all case
@@ -693,6 +610,7 @@ private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
let x :: xs : = p . vars | unreachable!
if let some ( ctorVal , xArgs ) ← withTransparency . default < | constructorApp'? x then
if hasCtorPattern p then
let xFields : = xArgs . extract ctorVal . numParams xArgs . size
let alts ← p . alts . filterMapM fun alt = > do
match alt . patterns with
| . ctor ctorName _ _ fields :: ps = >
@@ -700,13 +618,13 @@ private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
return none
else
return some { alt with patterns : = fields + + ps }
| . inaccessible _ :: _ = > processInaccessibleAsCtor alt ctorVal . name
| . var _ :: _ = > expandVarIntoCtor alt ctorVal . name
| . inaccessible _ :: ps = >
return some { alt with patterns : = xFields . toList . map . i naccessible + + ps }
| _ = > unreachable!
let xFields : = xArgs . extract ctorVal . numParams xArgs . size
return { p with alts : = alts , vars : = xFields . toList + + xs }
let alts ← p . alts . mapM fun alt = > do
match alt . patterns with
| . inaccessible _ :: ps = > return { alt with patterns : = ps }
| p :: ps = > return { alt with patterns : = ps , cnstrs : = ( x , ← p . toExpr ) :: alt . cnstrs }
| _ = > unreachable!
return { p with alts : = alts , vars : = xs }
@@ -717,10 +635,10 @@ private def collectValues (p : Problem) : Array Expr :=
| . val v :: _ = > if values . contains v then values else values . push v
| _ = > values
private def isFirstPatternVar ( alt : Alt ) : Bool : =
private def isFirstPatternInaccessible ( alt : Alt ) : Bool : =
match alt . patterns with
| . var _ :: _ = > true
| _ = > false
| . inaccessible _ :: _ = > true
| _ = > false
private def Pattern . isRefutable : Pattern → Bool
| . var _ = > false
@@ -749,21 +667,19 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
let examples : = p . examples . map < | Example . replaceFVarId x . fvarId! ( Example . val value )
let examples : = examples . map < | Example . applyFVarSubst subst
let newAlts : = p . alts . filter fun alt = > match alt . patterns with
| . val v :: _ = > v = = value
| . var _ :: _ = > true
| _ = > false
| . val v :: _ = > v = = value
| . inaccessible _ :: _ = > true
| _ = > unreachable!
let newAlts : = newAlts . map fun alt = > alt . applyFVarSubst subst
let newAlts : = newAlts . map fun alt = > match alt . patterns with
| . val _ :: ps = > { alt with patterns : = ps }
| . var fvarId :: ps = >
let alt : = { alt with patterns : = ps }
alt . replaceFVarId fvarId value
| _ = > unreachable!
| . val _ :: ps = > { alt with patterns : = ps }
| . inaccessible _ :: ps = > { alt with patterns : = ps }
| _ = > unreachable!
let newVars : = xs . map fun x = > x . applyFVarSubst subst
return { p with mvarId : = subgoal . mvarId , vars : = newVars , alts : = newAlts , examples : = examples }
else
-- else branch for value
let newAlts : = p . alts . filter isFirstPatternVar
let newAlts : = p . alts . filter isFirstPatternInaccessible
return { p with mvarId : = subgoal . mvarId , alts : = newAlts , vars : = x :: xs }
private def collectArraySizes ( p : Problem ) : Array Nat : =
@@ -772,23 +688,6 @@ private def collectArraySizes (p : Problem) : Array Nat :=
| . arrayLit _ ps :: _ = > let sz : = ps . length ; if sizes . contains sz then sizes else sizes . push sz
| _ = > sizes
private def expandVarIntoArrayLit ( alt : Alt ) ( fvarId : FVarId ) ( arrayElemType : Expr ) ( arraySize : Nat ) : MetaM Alt : =
withExistingLocalDecls alt . fvarDecls do
let fvarDecl ← fvarId . getDecl
let varNamePrefix : = fvarDecl . userName
let rec loop ( n : Nat ) ( newVars : Array Expr ) : = do
match n with
| n + 1 = >
withLocalDeclD ( varNamePrefix . appendIndexAfter ( n + 1 ) ) arrayElemType fun x = >
loop n ( newVars . push x )
| 0 = >
let arrayLit ← mkArrayLit arrayElemType newVars . toList
let alt : = alt . replaceFVarId fvarId arrayLit
let newDecls ← newVars . toList . mapM fun newVar = > newVar . fvarId! . getDecl
let newPatterns : = newVars . toList . map fun newVar = > . var newVar . fvarId!
return { alt with fvarDecls : = newDecls + + alt . fvarDecls , patterns : = newPatterns + + alt . patterns }
loop arraySize # [ ]
private def processArrayLit ( p : Problem ) : MetaM ( Array Problem ) : = do
trace [ Meta . Match . match ] " array literal step "
let x :: xs : = p . vars | unreachable!
@@ -805,21 +704,21 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
let examples : = p . examples . map < | Example . replaceFVarId x . fvarId! subex
let examples : = examples . map < | Example . applyFVarSubst subst
let newAlts : = p . alts . filter fun alt = > match alt . patterns with
| . arrayLit _ ps :: _ = > ps . length = = size
| . var _ :: _ = > true
| _ = > false
| . arrayLit _ ps :: _ = > ps . length = = size
| . inaccessible _ :: _ = > true
| _ = > unreachable!
let newAlts : = newAlts . map fun alt = > alt . applyFVarSubst subst
let newAlts ← newAlts . mapM fun alt = > do
let newAlts : = newAlts . map fun alt = >
match alt . patterns with
| . arrayLit _ pats :: ps = > return { alt with patterns : = pats + + ps }
| . var fvarId :: ps = >
let α ← getArrayArgType < | subst . apply x
expandVarIntoArrayLit { alt with patterns : = ps } fvarId α size
| . arrayLit _ pats :: ps = > { alt with patterns : = pats + + ps }
| . inaccessible _ :: ps = >
let patterns : = elems . map ( fun elem = > . inaccessible ( mkFVar elem ) ) + + ps
{ alt with patterns }
| _ = > unreachable!
return { p with mvarId : = subgoal . mvarId , vars : = newVars , alts : = newAlts , examples : = examples }
else
-- else branch
let newAlts : = p . alts . filter isFirstPatternVar
let newAlts : = p . alts . filter isFirstPatternInaccessible
return { p with mvarId : = subgoal . mvarId , alts : = newAlts , vars : = x :: xs }
private def expandNatValuePattern ( p : Problem ) : MetaM Problem : = do
@@ -934,6 +833,107 @@ def processExFalso (p : Problem) : MetaM Problem := do
let mvarId' ← p . mvarId . exfalso
return { p with mvarId : = mvarId' }
/--
Does any alternative have a pattern that can be independently handled (variable, inaccessible,
as - pattern) before any refutable pattern?
-/
def hasIndependentPatterns ( p : Problem ) : Bool : =
p . alts . any fun alt = > Id . run do
for v in p . vars , p in alt . patterns do
match p with
| . inaccessible e = >
if e = = v then
-- Skip inaccessible pattern that's are equal to the variable, these are “done”
continue
else
return true
| . var . . | . as . . = > return true
| . ctor . . | . val . . | . arrayLit . . = > return false
return false
def processIndependentPatterns ( p : Problem ) : MetaM Problem : = withGoalOf p do
let alts' ← p . alts . mapM fun alt = > do
-- We process only one pattern at a time, for code simplicity and better tracing
-- of the main loop
let mut donePrefix : = 0
for var in p . vars , pat in alt . patterns do
match pat with
| . inaccessible e = >
if e = = var then
donePrefix : = donePrefix + 1
else
break
| _ = > break
match alt . patterns . drop donePrefix with
| [ ] = >
-- All done here
return alt
| pat :: remainingPats = >
let v : = p . vars [ donePrefix ] !
match pat with
| . inaccessible e = >
trace [ Meta . Match . match ] " processing inaccessible pattern "
let patterns : = ( p . vars . take ( donePrefix + 1 ) ) . map . inaccessible + + remainingPats
let cnstrs : = ( v , e ) :: alt . cnstrs
return { alt with patterns , cnstrs }
| . var fvarId = >
trace [ Meta . Match . match ] " processing variable pattern "
let patterns : = ( p . vars . take ( donePrefix + 1 ) ) . map . inaccessible + + remainingPats
let alt' ← withExistingLocalDecls alt . fvarDecls do
if ( ← isDefEqGuarded ( ← fvarId . getType ) ( ← inferType v ) ) then
return { alt with patterns } . replaceFVarId fvarId v
else
let cnstrs : = ( mkFVar fvarId , v ) :: alt . cnstrs
return { alt with patterns , cnstrs }
return alt'
| . as fvarId pat h = >
let patterns : = ( p . vars . take donePrefix ) . map . inaccessible + + [ pat ] + + remainingPats
/- We used to use eagerly check the types here (using what was called `checkAndReplaceFVarId`),
but `x` and `fvarId` can have different types when dependent types are being used.
Let's consider the repro for issue #471
```
inductive vec : Nat → Type
| nil : vec 0
| cons : Int → vec n → vec n.succ
def vec_len : vec n → Nat
| vec.nil => 0
| x@(vec.cons h t) => vec_len t + 1
```
we reach the state
```
[Meta.Match.match] remaining variables: [x✝:(vec n✝)]
alternatives:
[n:(Nat), x:(vec (Nat.succ n)), h:(Int), t:(vec n)] | - [x@(vec.cons n h t)] => h_1 n x h t
[x✝:(vec n✝)] | - [x✝] => h_2 n✝ x✝
```
The variables `x✝:(vec n✝)` and `x:(vec (Nat.succ n))` have different types, but we perform the substitution anyway,
because we claim the "discrepancy" will be corrected after we process the pattern `(vec.cons n h t)`.
The right - hand - side is temporarily type incorrect, but we claim this is fine because it will be type correct again after
we the pattern `(vec.cons n h t)`. TODO: try to find a cleaner solution.
-/
let r ← mkEqRefl v
return { alt with patterns } . replaceFVarId fvarId v | > . replaceFVarId h r
| . ctor . . | . val . . | . arrayLit . . = >
return alt
return { p with alts : = alts' }
private def isFirstVarDoneTransition ( p : Problem ) : Bool : = Id . run do
if p . alts . isEmpty then
return false
let x :: _ : = p . vars | unreachable!
return p . alts . all fun alt = > Id . run do
let p :: _ : = alt . patterns | unreachable!
return match p with
| . inaccessible e = > e = = x
| _ = > false
private def processFirstVarDone ( p : Problem ) : Problem : =
{ p with
vars : = p . vars . tail!
alts : = p . alts . map fun alt = > { alt with patterns : = alt . patterns . tail! } }
private def tracedForM ( xs : Array α ) ( process : α → StateRefT State MetaM Unit ) : StateRefT State MetaM Unit : =
if xs . size > 1 then
for x in xs , i in [ : xs . size ] do
@@ -956,9 +956,15 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
process p
return
if hasAs Pattern p then
traceStep ( " as- pattern" )
let p ← processAs Pattern p
if hasIndependent Patterns p then
traceStep ( " processing independent prefixes of patterns " )
let p ← processIndependent Patterns p
process p
return
if isFirstVarDoneTransition p then
traceStep ( " first var done " )
let p : = processFirstVarDone p
process p
return
@@ -1010,9 +1016,11 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
tracedForM ps process
return
if isVariableTransition p then
traceStep ( " variable " )
let p ← processV ariable p
if p . alts . isEmpty then
-- Note that for inductive types, `isConstructorTransition` does something on empty matches
-- For all others, drop the v ariable here
traceStep ( " empty match transition " )
let p : = { p with vars : = p . vars . tail! }
process p
return
