From 84ff8d4a042095955f52fd33922a2c7cb8b0f76a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Aug 2022 17:38:36 -0700 Subject: [PATCH] feat: store pending contraints during dependent pattern matching It is a better solution for issues #1361 and #1279, and it was on the to-do list for a while. --- src/Lean/Meta/Match/Basic.lean | 41 ++- src/Lean/Meta/Match/Match.lean | 410 ++++++++++++++-------------- tests/lean/match1.lean.expected.out | 8 +- tests/lean/run/1361b.lean | 13 + tests/lean/run/depElim1.lean | 24 -- 5 files changed, 258 insertions(+), 238 deletions(-) create mode 100644 tests/lean/run/1361b.lean diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean index b7aa73012b..8a7109ce18 100644 --- a/src/Lean/Meta/Match/Basic.lean +++ b/src/Lean/Meta/Match/Basic.lean @@ -127,27 +127,52 @@ def instantiateAltLHSMVars (altLHS : AltLHS) : MetaM AltLHS := patterns := (← altLHS.patterns.mapM instantiatePatternMVars) } +/-- `Match` alternative -/ structure Alt where + /-- `Syntax` object for providing position information -/ ref : Syntax - idx : Nat -- for generating error messages + /-- + Orginal alternative index. Alternatives can be split, this index is the original + position of the alternative that generated this one. + -/ + idx : Nat + /-- + Right-hand-side of the alternative. + -/ rhs : Expr + /-- + Alternative pattern variables. + -/ fvarDecls : List LocalDecl + /-- + Alternative patterns. + -/ patterns : List Pattern + /-- + Pending constraints `lhs ≋ rhs` that need to be solved before the alternative + is considered acceptable. We generate them when processing inaccessible patterns. + Note that `lhs` and `rhs` often have different types. + After we perform additional case analysis, their types become definitionally equal. + -/ + cnstrs : List (Expr × Expr) deriving Inhabited namespace Alt partial def toMessageData (alt : Alt) : MetaM MessageData := do withExistingLocalDecls alt.fvarDecls do - let msg : List MessageData := alt.fvarDecls.map fun d => m!"{d.toExpr}:({d.type})" - let msg : MessageData := m!"{msg} |- {alt.patterns.map Pattern.toMessageData} => {alt.rhs}" + let msg := alt.fvarDecls.map fun d => m!"{d.toExpr}:({d.type})" + let mut msg := m!"{msg} |- {alt.patterns.map Pattern.toMessageData} => {alt.rhs}" + for (lhs, rhs) in alt.cnstrs do + msg := m!"{msg}\n | {lhs} ≋ {rhs}" addMessageContext msg def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt := { alt with patterns := alt.patterns.map fun p => p.applyFVarSubst s, fvarDecls := alt.fvarDecls.map fun d => d.applyFVarSubst s, - rhs := alt.rhs.applyFVarSubst s } + rhs := alt.rhs.applyFVarSubst s + cnstrs := alt.cnstrs.map fun (lhs, rhs) => (lhs.applyFVarSubst s, rhs.applyFVarSubst s) } def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt := { alt with @@ -156,7 +181,11 @@ def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt := fvarDecls := let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId decls.map (·.replaceFVarId fvarId v) - } + cnstrs := alt.cnstrs.map fun (lhs, rhs) => (lhs.replaceFVarId fvarId v, rhs.replaceFVarId fvarId v) } + +/-- Return `true` if `fvarId` is one of the alternative pattern variables -/ +def isLocalDecl (fvarId : FVarId) (alt : Alt) : Bool := + alt.fvarDecls.any fun d => d.fvarId == fvarId /-- Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`. @@ -209,7 +238,7 @@ def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt : withExistingLocalDecls alt.fvarDecls do let (expectedType, givenType) ← addPPExplicitToExposeDiff vType fvarDecl.type throwErrorAt alt.ref "type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr givenType}\nexpected type{indentExpr expectedType}" - pure $ replaceFVarId fvarId v alt + return replaceFVarId fvarId v alt end Alt diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index e481033237..45323ac56c 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -66,18 +66,9 @@ where let rhs := if hasParams then mkAppN minor xs else mkApp minor (mkConst `Unit.unit) let minors := minors.push (minor, minorNumParams) let fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars - let alts := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts + let alts := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns, cnstrs := [] } :: alts loop lhss alts minors -def assignGoalOf (p : Problem) (e : Expr) : MetaM Unit := - withGoalOf p do - let mvar := mkMVar p.mvarId - let mvarType ← inferType mvar - let eType ← inferType e - unless (← isDefEq mvarType eType) do - throwError "dependent elimination failed, type mismatch when solving alternative with type{indentExpr eType}\nbut expected{indentExpr mvarType}" - p.mvarId.assign e - structure State where used : Std.HashSet Nat := {} -- used alternatives counterExamples : List (List Example) := [] @@ -159,24 +150,109 @@ private def isNatValueTransition (p : Problem) : Bool := | _ => false) private def processSkipInaccessible (p : Problem) : Problem := Id.run do - let _ :: xs := p.vars | unreachable! + let x :: xs := p.vars | unreachable! let alts := p.alts.map fun alt => Id.run do - let .inaccessible _ :: ps := alt.patterns | unreachable! - { alt with patterns := ps } + let .inaccessible e :: ps := alt.patterns | unreachable! + { alt with patterns := ps, cnstrs := (x, e) :: alt.cnstrs } { p with alts := alts, vars := xs } -private def processLeaf (p : Problem) : StateRefT State MetaM Unit := do - match p.alts with - | [] => - /- TODO: allow users to configure which tactic is used to close leaves. -/ - unless (← p.mvarId.contradictionCore {}) do - trace[Meta.Match.match] "missing alternative" - p.mvarId.admit - modify fun s => { s with counterExamples := p.examples :: s.counterExamples } - | alt :: _ => - -- TODO: check whether we have unassigned metavars in rhs - liftM <| assignGoalOf p alt.rhs - modify fun s => { s with used := s.used.insert alt.idx } +/-- +If contraint is of the form `e ≋ x` where `x` is a free variable, reorient it +as `x ≋ e` If +- `x` is an `alt`-local declaration +- `e` is not a free variable. +-/ +private def reorientCnstrs (alt : Alt) : Alt := + let cnstrs := alt.cnstrs.map fun (lhs, rhs) => + if rhs.isFVar && alt.isLocalDecl rhs.fvarId! then + (rhs, lhs) + else if !lhs.isFVar && rhs.isFVar then + (rhs, lhs) + else + (lhs, rhs) + { alt with cnstrs } + +/-- +Remove constraints of the form `lhs ≋ rhs` where `lhs` and `rhs` are definitionally equal, +or `lhs` is a free variable. +-/ +private def filterTrivialCnstrs (alt : Alt) : MetaM Alt := do + let cnstrs ← withExistingLocalDecls alt.fvarDecls do + alt.cnstrs.filterM fun (lhs, rhs) => do + if (← isDefEqGuarded lhs rhs) then + return false + else if lhs.isFVar then + return false + else + return true + return { alt with cnstrs } + +/-- +Find an alternative constraint of the form `x ≋ e` where `x` is an alternative +local declarations, and `x` and `e` have definitionally equal types. +Then, replace `x` with `e` in the alternative, and return it. +Return `none` if the alternative does not contain a constraint of this form. +-/ +private def solveSomeLocalFVarIdCnstr? (alt : Alt) : MetaM (Option Alt) := + withExistingLocalDecls alt.fvarDecls do + let (some (fvarId, val), cnstrs) ← go alt.cnstrs | return none + trace[Meta.Match.match] "found cnstr to solve {mkFVar fvarId} ↦ {val}" + return some <| { alt with cnstrs }.replaceFVarId fvarId val +where + go (cnstrs : List (Expr × Expr)) := do + match cnstrs with + | [] => return (none, []) + | (lhs, rhs) :: cnstrs => + if lhs.isFVar && alt.isLocalDecl lhs.fvarId! then + if !(← dependsOn rhs lhs.fvarId!) && (← isDefEqGuarded (← inferType lhs) (← inferType rhs)) then + return (some (lhs.fvarId!, rhs), cnstrs) + let (p, cnstrs) ← go cnstrs + return (p, (lhs, rhs) :: cnstrs) + +/-- +Solve pending alternative constraints. If all constraints can be solved perform assignment +`mvarId := alt.rhs`, and return true. +-/ +private partial def solveCnstrs (mvarId : MVarId) (alt : Alt) : StateRefT State MetaM Bool := do + go (reorientCnstrs alt) +where + go (alt : Alt) : StateRefT State MetaM Bool := do + match (← solveSomeLocalFVarIdCnstr? alt) with + | some alt => go alt + | none => + let alt ← filterTrivialCnstrs alt + if alt.cnstrs.isEmpty then + let eType ← inferType alt.rhs + let targetType ← mvarId.getType + unless (← isDefEqGuarded targetType eType) do + trace[Meta.Match.match] "assignGoalOf failed {eType} =?= {targetType}" + throwError "dependent elimination failed, type mismatch when solving alternative with type{indentExpr eType}\nbut expected{indentExpr targetType}" + mvarId.assign alt.rhs + modify fun s => { s with used := s.used.insert alt.idx } + return true + else + trace[Meta.Match.match] "alt has unsolved cnstrs:\n{← alt.toMessageData}" + return false + +/-- +Try to solve the problem by using the first alternative whose pending constraints can be resolved. +-/ +private def processLeaf (p : Problem) : StateRefT State MetaM Unit := + p.mvarId.withContext do + withPPForTacticGoal do trace[Meta.Match.match] "local context at processLeaf:\n{(← mkFreshTypeMVar).mvarId!}" + go p.alts +where + go (alts : List Alt) : StateRefT State MetaM Unit := do + match alts with + | [] => + /- TODO: allow users to configure which tactic is used to close leaves. -/ + unless (← p.mvarId.contradictionCore {}) do + trace[Meta.Match.match] "missing alternative" + p.mvarId.admit + modify fun s => { s with counterExamples := p.examples :: s.counterExamples } + | alt :: alts => + unless (← solveCnstrs p.mvarId alt) do + go alts private def processAsPattern (p : Problem) : MetaM Problem := withGoalOf p do let x :: _ := p.vars | unreachable! @@ -216,62 +292,43 @@ 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 _ :: ps => return { alt with patterns := ps } - | .var fvarId :: ps => ({ alt with patterns := ps }).checkAndReplaceFVarId fvarId x - | _ => unreachable! + | .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 } -/- - TODO: FIX the following issue. +/-! +Note that we decided to store pending constraints to address issues exposed by #1279 and #1361. +Here is a simplified version of the example on this issue (see test: `1279_simplified.lean`) +```lean +inductive Arrow : Type → Type → Type 1 + | id : Arrow a a + | unit : Arrow Unit Unit + | comp : Arrow β γ → Arrow α β → Arrow α γ +deriving Repr - `fvarId` is not an alternative variable, and we used to return `false` here, but it is incorrect, and may - incorrectly discard applicable alternatives. It was buggy because of the way we handle inaccessible patterns - in variable transitions. The bug was exposed by issue #1279 - Here is a simplified version of the example on this issue (see test: `1279_simplified.lean`) - ```lean - inductive Arrow : Type → Type → Type 1 - | id : Arrow a a - | unit : Arrow Unit Unit - | comp : Arrow β γ → Arrow α β → Arrow α γ - deriving Repr - - def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ := - match f, g with - | id, g => g - | f, id => f - | f, g => comp f g - ``` - The initial state for the `match`-expression above is - ```lean - [Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)] - alternatives: - [β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g - [γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f - [β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g - ``` - The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives. - The constraint `β✝ === α` in the second alternative is lost. Note that `α` is not an alternative variable. - After applying the variable-transition step twice, we reach the following state - ```lean - [Meta.Match.match] remaining variables: [f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)] - alternatives: - [g:(Arrow α β✝)] |- [(Arrow.id .(β✝)), g] => h_1 β✝ g - [f:(Arrow α γ✝)] |- [f, (Arrow.id .(α))] => h_2 γ✝ f - [f:(Arrow β✝ γ✝), g:(Arrow α β✝)] |- [f, g] => h_3 β✝ γ✝ f g - ``` - A constructor-transition should be used, and the functions `expandVarIntoCtor?` is required for the second and - third alternatives. There are 3 constructors, in the `Arrow.id` case, we use unify to solve - ``` - Arrow a a =?= Arrow α β✝ - ``` - Where `a` is new alternative variable corresponding to the `Arrow.id` field. - The first assignment is fine `a := α`. - In the second assignment we have `α := β✝` where both `α` and `β✝` are not alternative variables. - We did not store information that `β✝ === α` in the first step, and the alternative was being incorrectly discarded. - Returning `true` here "solves" the problem, but it is a bit hackish. We see two possible improvements: - - We store the constraint `β✝ === α`. - - We postpone variable-transition steps. - It is unclear at this point what is the best solution. We should keep accumulating problematic examples. +def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ := + match f, g with + | id, g => g + | f, id => f + | f, g => comp f g +``` +The initial state for the `match`-expression above is +```lean +[Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)] +alternatives: + [β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g + [γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f + [β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g +``` +The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives. +The constraint `β✝ ≋ α` in the second alternative used to be discarded. We now store it at the +alternative `cnstrs` field. -/ private def inLocalDecls (localDecls : List LocalDecl) (fvarId : FVarId) : Bool := @@ -285,23 +342,17 @@ private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : let (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType let ctor := mkAppN (mkConst ctorName ctorLevels) ctorParams let ctorType ← inferType ctor - let ctorAbst? ← withNewMCtxDepth do - let (ctorFields, _, resultType) ← forallMetaTelescopeReducing ctorType - unless (← isDefEq resultType expectedType) do - return none - return some (← abstractMVars (mkAppN ctor ctorFields)) - let some ctorAbst := ctorAbst? | return none - lambdaTelescope ctorAbst.expr fun newFVars ctor => do - let ctorArgs := ctor.getAppArgs - let ctorFields := ctorArgs[ctorParams.size:].toArray + forallTelescopeReducing ctorType fun ctorFields resultType => do + let ctor := mkAppN ctor ctorFields let alt := alt.replaceFVarId fvarId ctor - let newAltDecls ← newFVars.mapM fun newFVar => newFVar.fvarId!.getDecl - let newAltDecls := newAltDecls.toList ++ alt.fvarDecls + 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 := ctorFields.toList.map fun ctorField => match ctorField with - | .fvar fvarId => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible ctorField - | _ => Pattern.inaccessible ctorField - return some { alt with fvarDecls := newAltDecls, patterns := ctorFieldPatterns ++ alt.patterns } + let ctorFieldPatterns := ctorFieldDecls.toList.map fun decl => Pattern.var decl.fvarId + return some { alt with fvarDecls := newAltDecls, patterns := ctorFieldPatterns ++ alt.patterns, cnstrs } private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do let xType ← inferType x @@ -411,34 +462,32 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do | _ => unreachable! return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples } +private def altsAreCtorLike (p : Problem) : MetaM Bool := withGoalOf p do + p.alts.allM fun alt => do match alt.patterns with + | .ctor .. :: _ => return true + | .inaccessible e :: _ => return (← whnfD e).isConstructorApp (← getEnv) + | _ => return false + private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do let x :: xs := p.vars | unreachable! - let x ← whnfD x - let env ← getEnv - match x.constructorApp? env with - | some (ctorVal, xArgs) => - let alts ← p.alts.filterMapM fun alt => do - match alt.patterns with - | .ctor n _ _ fields :: ps => - if n != ctorVal.name then - return none - else - return some { alt with patterns := fields ++ ps } - | .inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name - | p :: _ => throwError "failed to compile pattern matching, inaccessible pattern or constructor expected{indentD p.toMessageData}" - | _ => unreachable! - let xFields := xArgs.extract ctorVal.numParams xArgs.size - return { p with alts := alts, vars := xFields.toList ++ xs } - | none => - let alts ← p.alts.filterMapM fun alt => match alt.patterns with - | .inaccessible e :: ps => do - if (← isDefEq x e) then - return some { alt with patterns := ps } - else - return none - | p :: _ => throwError "failed to compile pattern matching, unexpected pattern{indentD p.toMessageData}\ndiscriminant{indentExpr x}" - | _ => unreachable! - return { p with alts := alts, vars := xs } + if let some (ctorVal, xArgs) := (← whnfD x).constructorApp? (← getEnv) then + if (← altsAreCtorLike p) then + let alts ← p.alts.filterMapM fun alt => do + match alt.patterns with + | .ctor ctorName _ _ fields :: ps => + if ctorName != ctorVal.name then + return none + else + return some { alt with patterns := fields ++ ps } + | .inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name + | _ => 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 + | p :: ps => return { alt with patterns := ps, cnstrs := (x, ← p.toExpr) :: alt.cnstrs } + | _ => unreachable! + return { p with alts := alts, vars := xs } private def collectValues (p : Problem) : Array Expr := p.alts.foldl (init := #[]) fun values alt => @@ -601,91 +650,44 @@ private def moveToFront (p : Problem) (i : Nat) : Problem := else p -private partial def process (p : Problem) : StateRefT State MetaM Unit := - search 0 -where - /-- If `p.vars` is empty, then we are done. Otherwise, we process `p.vars[0]`. -/ - tryToProcess (p : Problem) : StateRefT State MetaM Unit := withIncRecDepth do - traceState p - let isInductive ← isCurrVarInductive p - if isDone p then - processLeaf p - else if hasAsPattern p then - traceStep ("as-pattern") - let p ← processAsPattern p - process p - else if isNatValueTransition p then - traceStep ("nat value to constructor") - process (expandNatValuePattern p) - else if !isNextVar p then - traceStep ("non variable") - let p ← processNonVariable p - process p - else if isInductive && isConstructorTransition p then - let ps ← processConstructor p - ps.forM process - else if isVariableTransition p then - traceStep ("variable") - let p ← processVariable p - process p - else if isValueTransition p then - let ps ← processValue p - ps.forM process - else if isArrayLitTransition p then - let ps ← processArrayLit p - ps.forM process - else if hasNatValPattern p then - -- This branch is reachable when `p`, for example, is just values without an else-alternative. - -- We added it just to get better error messages. - traceStep ("nat value to constructor") - process (expandNatValuePattern p) - else - checkNextPatternTypes p - throwNonSupported p - - /-- Return `true` if `type` does not depend on the first `i` elements in `xs` -/ - checkVarDeps (xs : List Expr) (i : Nat) (type : Expr) : MetaM Bool := do - match i, xs with - | 0, _ => return true - | _, [] => unreachable! - | i+1, x::xs => - if x.isFVar then - if (← dependsOn type x.fvarId!) then - return false - checkVarDeps xs i type - - /-- - Auxiliary method for `search`. Find next variable to "try". - `i` is the position of the variable s.t. `tryToProcess` failed. - We only consider variables that do not depend on other variables at `p.vars`. -/ - findNext (i : Nat) : MetaM (Option Nat) := do - if h : i < p.vars.length then - let x := p.vars.get ⟨i, h⟩ - if (← checkVarDeps p.vars i (← inferType x)) then - return i - else - findNext (i+1) - else - return none - - /-- - Auxiliary method for trying the next variable to process. - It moves variable `#i` to the front of the to-do list and invokes `tryToProcess`. - Note that for non-dependent elimination, variable `#0` always work. - If variable `#i` fails, we use `findNext` to select the next variable to try. - Remark: the "missing cases" error is not considered a failure. -/ - search (i : Nat) : StateRefT State MetaM Unit := do - let s₁ ← getThe Meta.State - let s₂ ← get - let p' := moveToFront p i - try - tryToProcess p' - catch ex => - match (← withGoalOf p <| findNext (i+1)) with - | none => throw ex - | some j => - trace[Meta.Match.match] "failed with #{i}, trying #{j}{indentD ex.toMessageData}" - set s₁; set s₂; search j +private partial def process (p : Problem) : StateRefT State MetaM Unit := do + traceState p + let isInductive ← isCurrVarInductive p + if isDone p then + traceStep ("leaf") + processLeaf p + else if hasAsPattern p then + traceStep ("as-pattern") + let p ← processAsPattern p + process p + else if isNatValueTransition p then + traceStep ("nat value to constructor") + process (expandNatValuePattern p) + else if !isNextVar p then + traceStep ("non variable") + let p ← processNonVariable p + process p + else if isInductive && isConstructorTransition p then + let ps ← processConstructor p + ps.forM process + else if isVariableTransition p then + traceStep ("variable") + let p ← processVariable p + process p + else if isValueTransition p then + let ps ← processValue p + ps.forM process + else if isArrayLitTransition p then + let ps ← processArrayLit p + ps.forM process + else if hasNatValPattern p then + -- This branch is reachable when `p`, for example, is just values without an else-alternative. + -- We added it just to get better error messages. + traceStep ("nat value to constructor") + process (expandNatValuePattern p) + else + checkNextPatternTypes p + throwNonSupported p private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (Option Nat) := if uElim == levelZero then diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index 0adbb091df..30a26b16b6 100644 --- a/tests/lean/match1.lean.expected.out +++ b/tests/lean/match1.lean.expected.out @@ -10,10 +10,10 @@ 4 ---- inv 10 -match1.lean:82:0-82:73: error: type mismatch during dependent match-elimination at pattern variable 'w' with type - VecPred P Vec.nil -expected type - VecPred P tail✝ +match1.lean:82:0-82:73: error: dependent elimination failed, type mismatch when solving alternative with type + motive 0 (Vec.cons head✝ Vec.nil) (_ : VecPred P (Vec.cons head✝ Vec.nil)) +but expected + motive _fun_discr✝ (Vec.cons head✝ tail✝) (_ : VecPred P (Vec.cons head✝ tail✝)) [false, true, true] match1.lean:119:0-119:41: error: dependent match elimination failed, inaccessible pattern found .(j + j) diff --git a/tests/lean/run/1361b.lean b/tests/lean/run/1361b.lean new file mode 100644 index 0000000000..f3b73957f5 --- /dev/null +++ b/tests/lean/run/1361b.lean @@ -0,0 +1,13 @@ +def Multiset (α: Type) : Type := sorry +def Multiset.ndinsert [DecidableEq α](a : α): Multiset α → Multiset α := sorry +def Finset (α : Type _) : Type := @Subtype (Multiset α) sorry +def Finset.insert [DecidableEq α](a : α): Finset α → Finset α +| ⟨ms, prop⟩ => ⟨ms.ndinsert a, sorry⟩ + +inductive Bar : Finset Nat → Type +| insert : Bar (Finset.insert n Γ) +| empty : Bar Γ + +example {Γ: Finset Nat}: ∀ (p: Bar Γ), Nat +| Bar.empty => 1 -- missing cases: (@Bar.insert _ (Subtype.mk _ _)) +| _ => 2 -- redundant alternative diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean index 8310742c55..e3c9978d01 100644 --- a/tests/lean/run/depElim1.lean +++ b/tests/lean/run/depElim1.lean @@ -216,27 +216,3 @@ def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) : #eval test `ex3 2 `elimTest3 #print elimTest3 - -def ex4 (α : Type u) (n : Nat) (xs : Vec α n) : - LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0)) -× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (inaccessible (n+1)) × Pat xs) := -default - -#eval test `ex4 2 `elimTest4 -#print elimTest4 - -def ex5 (α : Type u) (n : Nat) (xs : Vec α n) : - LHS (Pat Nat.zero × Pat (Vec.nil : Vec α 0)) -× LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (Nat.succ n) × Pat xs) := -default - -#eval test `ex5 2 `elimTest5 -#print elimTest5 - -def ex6 (α : Type u) (n : Nat) (xs : Vec α n) : - LHS (Pat (inaccessible Nat.zero) × Pat (Vec.nil : Vec α 0)) -× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) := -default - --- set_option trace.Meta.Match.match true --- set_option trace.Meta.Match.debug true