chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
eacdb5ff83
commit
4df4ec809a
1 changed files with 188 additions and 176 deletions
|
|
@ -9,33 +9,32 @@ import Lean.Meta.Tactic.Induction
|
|||
import Lean.Meta.Tactic.Cases
|
||||
import Lean.Elab.Tactic.ElabTerm
|
||||
import Lean.Elab.Tactic.Generalize
|
||||
new_frontend
|
||||
|
||||
namespace Lean
|
||||
namespace Elab
|
||||
namespace Tactic
|
||||
|
||||
namespace Lean.Elab.Tactic
|
||||
open Meta
|
||||
|
||||
-- Recall that
|
||||
-- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
|
||||
|
||||
private def getAuxHypothesisName (stx : Syntax) : Option Name :=
|
||||
if ((stx.getArg 1).getArg 0).isNone then none
|
||||
else some (((stx.getArg 1).getArg 0).getIdAt 0)
|
||||
if stx.getArg 1 $.getArg 0 $.isNone then
|
||||
none
|
||||
else
|
||||
some $ stx.getArg 1 $.getArg 0 $.getIdAt 0
|
||||
|
||||
private def getMajor (stx : Syntax) : Syntax :=
|
||||
(stx.getArg 1).getArg 1
|
||||
stx.getArg 1 $.getArg 1
|
||||
|
||||
private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
|
||||
match h? with
|
||||
| none => withMainMVarContext $ elabTerm major none
|
||||
| some h => withMainMVarContext do
|
||||
lctx ← getLCtx;
|
||||
let x := lctx.getUnusedName `x;
|
||||
major ← elabTerm major none;
|
||||
evalGeneralizeAux h? major x;
|
||||
let lctx ← getLCtx
|
||||
let x := lctx.getUnusedName `x
|
||||
let major ← elabTerm major none
|
||||
evalGeneralizeAux h? major x
|
||||
withMainMVarContext do
|
||||
lctx ← getLCtx;
|
||||
let lctx ← getLCtx
|
||||
match lctx.findFromUserName? x with
|
||||
| some decl => pure decl.toExpr
|
||||
| none => throwError "failed to generalize"
|
||||
|
|
@ -43,10 +42,10 @@ match h? with
|
|||
private def generalizeMajor (major : Expr) : TacticM Expr := do
|
||||
match major with
|
||||
| Expr.fvar _ _ => pure major
|
||||
| _ => do
|
||||
| _ =>
|
||||
liftMetaTacticAux fun mvarId => do
|
||||
mvarId ← Meta.generalize mvarId major `x false;
|
||||
(fvarId, mvarId) ← Meta.intro1 mvarId;
|
||||
mvarId ← Meta.generalize mvarId major `x false
|
||||
let (fvarId, mvarId) ← Meta.intro1 mvarId
|
||||
pure (mkFVar fvarId, [mvarId])
|
||||
|
||||
/-
|
||||
|
|
@ -58,24 +57,25 @@ match major with
|
|||
`stx` is syntax for `induction`. -/
|
||||
private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
|
||||
withRef stx $
|
||||
let generalizingStx := stx.getArg 3;
|
||||
if generalizingStx.isNone then pure #[]
|
||||
let generalizingStx := stx.getArg 3
|
||||
if generalizingStx.isNone then
|
||||
pure #[]
|
||||
else withMainMVarContext do
|
||||
trace `Elab.induction fun _ => generalizingStx;
|
||||
let vars := (generalizingStx.getArg 1).getArgs;
|
||||
trace `Elab.induction fun _ => generalizingStx
|
||||
let vars := (generalizingStx.getArg 1).getArgs
|
||||
getFVarIds vars
|
||||
|
||||
-- process `generalizingVars` subterm of induction Syntax `stx`.
|
||||
private def generalizeVars (stx : Syntax) (major : Expr) : TacticM Nat := do
|
||||
fvarIds ← getGeneralizingFVarIds stx;
|
||||
let fvarIds ← getGeneralizingFVarIds stx
|
||||
liftMetaTacticAux fun mvarId => do
|
||||
(fvarIds, mvarId') ← Meta.revert mvarId fvarIds;
|
||||
when (fvarIds.contains major.fvarId!) $
|
||||
Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized";
|
||||
let (fvarIds, mvarId') ← Meta.revert mvarId fvarIds
|
||||
if fvarIds.contains major.fvarId! then
|
||||
Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized"
|
||||
pure (fvarIds.size, [mvarId'])
|
||||
|
||||
private def getAlts (withAlts : Syntax) : Array Syntax :=
|
||||
(withAlts.getArg 2).getSepArgs
|
||||
withAlts.getArg 2 $.getSepArgs
|
||||
|
||||
/-
|
||||
Given an `inductionAlt` of the form
|
||||
|
|
@ -93,12 +93,12 @@ private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3
|
|||
```
|
||||
esnure the first `ident'` is `_` or a constructor name.
|
||||
-/
|
||||
private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit :=
|
||||
alts.forM $ fun alt => do
|
||||
let n := getAltName alt;
|
||||
withRef alt $ trace `Elab.checkAlt $ fun _ => n ++ ", " ++ alt;
|
||||
unless (n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName)) $
|
||||
throwErrorAt (alt.getArg 0) ("invalid constructor name '" ++ toString n ++ "'")
|
||||
private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit := do
|
||||
for alt in alts do
|
||||
let n := getAltName alt
|
||||
withRef alt $ trace[Elab.checkAlt]! msg!"{n} , {alt}"
|
||||
unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
|
||||
throwErrorAt (alt.getArg 0) msg!"invalid constructor name '{n}'"
|
||||
|
||||
structure RecInfo :=
|
||||
(recName : Name)
|
||||
|
|
@ -106,76 +106,86 @@ structure RecInfo :=
|
|||
(altRHSs : Array Syntax := #[]) -- RHS for each minor premise
|
||||
|
||||
def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
|
||||
liftMetaMAtMain $ fun mvarId => do
|
||||
majorType ← inferType major;
|
||||
majorType ← whnf majorType;
|
||||
liftMetaMAtMain fun mvarId => do
|
||||
let majorType ← inferType major
|
||||
let majorType ← whnf majorType
|
||||
matchConstInduct majorType.getAppFn
|
||||
(fun _ => Meta.throwTacticEx `induction mvarId ("major premise type is not an inductive type " ++ indentExpr majorType))
|
||||
(fun _ => Meta.throwTacticEx `induction mvarId msg!"major premise type is not an inductive type {indentExpr majorType}")
|
||||
(fun val _ => pure val)
|
||||
|
||||
private partial def getRecFromUsingLoop (baseRecName : Name) : Expr → TacticM (Option Meta.RecursorInfo)
|
||||
| majorType => do
|
||||
let continue (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do {
|
||||
majorType? ← unfoldDefinition? majorType;
|
||||
let finalize (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do
|
||||
let majorType? ← unfoldDefinition? majorType
|
||||
match majorType? with
|
||||
| some majorType => withIncRecDepth $ getRecFromUsingLoop majorType
|
||||
| some majorType => withIncRecDepth $ getRecFromUsingLoop baseRecName majorType
|
||||
| none => pure none
|
||||
};
|
||||
majorType ← whnfCore majorType;
|
||||
let majorType ← whnfCore majorType
|
||||
match majorType.getAppFn with
|
||||
| Expr.const name _ _ => do
|
||||
let candidate := name ++ baseRecName;
|
||||
env ← getEnv;
|
||||
match env.find? candidate with
|
||||
| Expr.const name _ _ =>
|
||||
let candidate := name ++ baseRecName
|
||||
match (← getEnv).find? candidate with
|
||||
| some _ =>
|
||||
catch
|
||||
(liftMetaMAtMain fun _ => do info ← Meta.mkRecursorInfo candidate; pure (some info))
|
||||
(fun _ => continue majorType)
|
||||
| none => continue majorType
|
||||
| _ => continue majorType
|
||||
try
|
||||
liftMetaMAtMain fun _ => do
|
||||
let info ← Meta.mkRecursorInfo candidate
|
||||
pure (some info)
|
||||
catch _ =>
|
||||
finalize majorType
|
||||
| none => finalize majorType
|
||||
| _ => finalize majorType
|
||||
|
||||
def getRecFromUsing (major : Expr) (baseRecName : Name) : TacticM Meta.RecursorInfo := do
|
||||
majorType ← inferType major;
|
||||
recInfo? ← getRecFromUsingLoop baseRecName majorType;
|
||||
match recInfo? with
|
||||
match ← getRecFromUsingLoop baseRecName (← inferType major) with
|
||||
| some recInfo => pure recInfo
|
||||
| none => do
|
||||
recName ← resolveGlobalConstNoOverload baseRecName;
|
||||
catch
|
||||
(liftMetaMAtMain fun _ => Meta.mkRecursorInfo recName)
|
||||
(fun _ => throwError ("invalid recursor name '" ++ baseRecName ++ "'"))
|
||||
| none =>
|
||||
let recName ← resolveGlobalConstNoOverload baseRecName
|
||||
try
|
||||
liftMetaMAtMain fun _ => Meta.mkRecursorInfo recName
|
||||
catch _ =>
|
||||
throwError msg!"invalid recursor name '{baseRecName}'"
|
||||
|
||||
/- Create `RecInfo` assuming builtin recursor -/
|
||||
private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do
|
||||
indVal ← getInductiveValFromMajor major;
|
||||
let recName := mkRecFor indVal.name;
|
||||
if withAlts.isNone then pure ({ recName := recName }, #[])
|
||||
else do
|
||||
let ctorNames := indVal.ctors;
|
||||
let alts := getAlts withAlts;
|
||||
checkAltCtorNames alts ctorNames;
|
||||
(altVars, altRHSs, remainingAlts, _) ← ctorNames.foldlM
|
||||
(fun (result : Array (List Name) × Array Syntax × Array Syntax × Option Syntax) (ctorName : Name) => do
|
||||
let (altVars, altRHSs, remainingAlts, prevAnonymousAlt?) := result;
|
||||
match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
|
||||
| some idx =>
|
||||
let newAlt := remainingAlts.get! idx;
|
||||
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, prevAnonymousAlt?)
|
||||
| none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
|
||||
let indVal ← getInductiveValFromMajor major
|
||||
let recName := mkRecFor indVal.name
|
||||
if withAlts.isNone then
|
||||
pure ({ recName := recName }, #[])
|
||||
else
|
||||
let ctorNames := indVal.ctors
|
||||
let alts := getAlts withAlts
|
||||
checkAltCtorNames alts ctorNames
|
||||
let altVars := #[]
|
||||
let altRHSs := #[]
|
||||
let remainingAlts := alts
|
||||
let prevAnonymousAlt? := none
|
||||
for ctorName in ctorNames do
|
||||
match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
|
||||
| some idx =>
|
||||
let newAlt := remainingAlts[idx]
|
||||
altVars := altVars.push (getAltVarNames newAlt).toList
|
||||
altRHSs := altRHSs.push (getAltRHS newAlt)
|
||||
remainingAlts := remainingAlts.eraseIdx idx
|
||||
| none =>
|
||||
match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
|
||||
| some idx =>
|
||||
let newAlt := remainingAlts.get! idx;
|
||||
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, some newAlt)
|
||||
let newAlt := remainingAlts[idx]
|
||||
altVars := altVars.push (getAltVarNames newAlt).toList
|
||||
altRHSs := altRHSs.push (getAltRHS newAlt)
|
||||
remainingAlts := remainingAlts.eraseIdx idx
|
||||
prevAnonymousAlt? := some newAlt
|
||||
| none => match prevAnonymousAlt? with
|
||||
| some alt =>
|
||||
pure (altVars.push (getAltVarNames alt).toList, altRHSs.push (getAltRHS alt), remainingAlts, prevAnonymousAlt?)
|
||||
altVars := altVars.push (getAltVarNames alt).toList
|
||||
altRHSs := altRHSs.push (getAltRHS alt)
|
||||
| none =>
|
||||
if allowMissingAlts then
|
||||
pure (altVars.push [], altRHSs.push Syntax.missing, remainingAlts, prevAnonymousAlt?)
|
||||
altVars := altVars.push []
|
||||
altRHSs := altRHSs.push Syntax.missing
|
||||
else
|
||||
throwError ("alternative for constructor '" ++ toString ctorName ++ "' is missing"))
|
||||
(#[], #[], alts, none);
|
||||
unless remainingAlts.isEmpty $
|
||||
throwErrorAt (remainingAlts.get! 0) "unused alternative";
|
||||
throwError msg!"alternative for constructor '{ctorName}' is missing"
|
||||
unless remainingAlts.isEmpty do
|
||||
throwErrorAt remainingAlts[0] "unused alternative"
|
||||
pure ({ recName := recName, altVars := altVars, altRHSs := altRHSs }, ctorNames.toArray)
|
||||
|
||||
/-
|
||||
|
|
@ -188,42 +198,49 @@ else do
|
|||
usingRec : Parser := optional (" using " >> ident)
|
||||
``` -/
|
||||
private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo :=
|
||||
withRef stx $
|
||||
let usingRecStx := stx.getArg 2;
|
||||
let withAlts := stx.getArg 4;
|
||||
if usingRecStx.isNone then do
|
||||
(rinfo, _) ← getRecInfoDefault major withAlts false;
|
||||
withRef stx do
|
||||
let usingRecStx := stx.getArg 2
|
||||
let withAlts := stx.getArg 4
|
||||
if usingRecStx.isNone then
|
||||
let (rinfo, _) ← getRecInfoDefault major withAlts false
|
||||
pure rinfo
|
||||
else do
|
||||
let baseRecName := (usingRecStx.getIdAt 1).eraseMacroScopes;
|
||||
recInfo ← getRecFromUsing major baseRecName;
|
||||
let recName := recInfo.recursorName;
|
||||
if withAlts.isNone then pure { recName := recName }
|
||||
else do
|
||||
let alts := getAlts withAlts;
|
||||
paramNames ← liftMetaMAtMain $ fun _ => getParamNames recInfo.recursorName;
|
||||
(altVars, altRHSs, remainingAlts, _) ← paramNames.size.foldM
|
||||
(fun (i : Nat) (result : Array (List Name) × Array Syntax × Array Syntax × Option Syntax) =>
|
||||
if recInfo.isMinor i then
|
||||
let paramName := paramNames.get! i;
|
||||
let (altVars, altRHSs, remainingAlts, prevAnonymousAlt?) := result;
|
||||
match remainingAlts.findIdx? (fun alt => getAltName alt == paramName) with
|
||||
else
|
||||
let baseRecName := usingRecStx.getIdAt 1 $.eraseMacroScopes
|
||||
let recInfo ← getRecFromUsing major baseRecName
|
||||
let recName := recInfo.recursorName
|
||||
if withAlts.isNone then
|
||||
pure { recName := recName }
|
||||
else
|
||||
let alts := getAlts withAlts
|
||||
let paramNames ← liftMetaMAtMain fun _ => getParamNames recInfo.recursorName
|
||||
let altVars := #[]
|
||||
let altRHSs := #[]
|
||||
let remainingAlts := alts
|
||||
let prevAnonymousAlt? := none
|
||||
for i in [:paramNames.size] do
|
||||
if recInfo.isMinor i then
|
||||
let paramName := paramNames[i]
|
||||
match remainingAlts.findIdx? (fun alt => getAltName alt == paramName) with
|
||||
| some idx =>
|
||||
let newAlt := remainingAlts[idx]
|
||||
altVars := altVars.push (getAltVarNames newAlt).toList
|
||||
altRHSs := altRHSs.push (getAltRHS newAlt)
|
||||
remainingAlts := remainingAlts.eraseIdx idx
|
||||
| none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
|
||||
| some idx =>
|
||||
let newAlt := remainingAlts.get! idx;
|
||||
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, prevAnonymousAlt?)
|
||||
| none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
|
||||
| some idx =>
|
||||
let newAlt := remainingAlts.get! idx;
|
||||
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, some newAlt)
|
||||
| none => match prevAnonymousAlt? with
|
||||
| some alt =>
|
||||
pure (altVars.push (getAltVarNames alt).toList, altRHSs.push (getAltRHS alt), remainingAlts, prevAnonymousAlt?)
|
||||
| none => throwError ("alternative for minor premise '" ++ toString paramName ++ "' is missing")
|
||||
else
|
||||
pure result)
|
||||
(#[], #[], alts, none);
|
||||
unless remainingAlts.isEmpty $
|
||||
throwErrorAt (remainingAlts.get! 0) "unused alternative";
|
||||
let newAlt := remainingAlts[idx]
|
||||
altVars := altVars.push (getAltVarNames newAlt).toList
|
||||
altRHSs := altRHSs.push (getAltRHS newAlt)
|
||||
remainingAlts := remainingAlts.eraseIdx idx
|
||||
prevAnonymousAlt? := some newAlt
|
||||
| none => match prevAnonymousAlt? with
|
||||
| some alt =>
|
||||
altVars := altVars.push (getAltVarNames alt).toList
|
||||
altRHSs := altRHSs.push (getAltRHS alt)
|
||||
| none =>
|
||||
throwError msg!"alternative for minor premise '{paramName}' is missing"
|
||||
unless remainingAlts.isEmpty do
|
||||
throwErrorAt remainingAlts[0] "unused alternative"
|
||||
pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
|
||||
|
||||
-- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
|
||||
|
|
@ -232,85 +249,80 @@ rhs.isOfKind `Lean.Parser.Term.syntheticHole || rhs.isOfKind `Lean.Parser.Term.h
|
|||
|
||||
private def processResult (altRHSs : Array Syntax) (result : Array Meta.InductionSubgoal) : TacticM Unit := do
|
||||
if altRHSs.isEmpty then
|
||||
setGoals $ result.toList.map $ fun s => s.mvarId
|
||||
else do
|
||||
unless (altRHSs.size == result.size) $
|
||||
throwError ("mistmatch on the number of subgoals produced (" ++ toString result.size ++ ") and " ++
|
||||
"alternatives provided (" ++ toString altRHSs.size ++ ")");
|
||||
gs ← result.size.foldM
|
||||
(fun i gs => do
|
||||
let subgoal := result.get! i;
|
||||
let rhs := altRHSs.get! i;
|
||||
let ref := rhs;
|
||||
let mvarId := subgoal.mvarId;
|
||||
if isHoleRHS rhs then withMVarContext mvarId $ withRef rhs do
|
||||
mvarDecl ← getMVarDecl mvarId;
|
||||
val ← elabTermEnsuringType rhs mvarDecl.type;
|
||||
assignExprMVar mvarId val;
|
||||
gs' ← getMVarsNoDelayed val;
|
||||
let gs' := gs'.toList;
|
||||
tagUntaggedGoals mvarDecl.userName `induction gs';
|
||||
pure (gs ++ gs')
|
||||
else do
|
||||
setGoals [mvarId];
|
||||
evalTactic rhs;
|
||||
done;
|
||||
pure gs)
|
||||
[];
|
||||
setGoals $ result.toList.map fun s => s.mvarId
|
||||
else
|
||||
unless altRHSs.size == result.size do
|
||||
throwError msg!"mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
|
||||
let gs := []
|
||||
for i in [:result.size] do
|
||||
let subgoal := result[i]
|
||||
let rhs := altRHSs[i]
|
||||
let ref := rhs
|
||||
let mvarId := subgoal.mvarId
|
||||
if isHoleRHS rhs then
|
||||
let gs' ← withMVarContext mvarId $ withRef rhs do
|
||||
let mvarDecl ← getMVarDecl mvarId
|
||||
let val ← elabTermEnsuringType rhs mvarDecl.type
|
||||
assignExprMVar mvarId val
|
||||
let gs' ← getMVarsNoDelayed val
|
||||
let gs' := gs'.toList
|
||||
tagUntaggedGoals mvarDecl.userName `induction gs'
|
||||
pure gs'
|
||||
gs := gs ++ gs'
|
||||
else
|
||||
setGoals [mvarId]
|
||||
evalTactic rhs
|
||||
done
|
||||
setGoals gs
|
||||
|
||||
@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic :=
|
||||
fun stx => focusAux $ do
|
||||
let h? := getAuxHypothesisName stx;
|
||||
major ← elabMajor h? (getMajor stx);
|
||||
major ← generalizeMajor major;
|
||||
n ← generalizeVars stx major;
|
||||
recInfo ← getRecInfo stx major;
|
||||
(mvarId, _) ← getMainGoal;
|
||||
result ← liftMetaM $ Meta.induction mvarId major.fvarId! recInfo.recName recInfo.altVars;
|
||||
fun stx => focusAux do
|
||||
let h? := getAuxHypothesisName stx
|
||||
let major ← elabMajor h? (getMajor stx)
|
||||
let major ← generalizeMajor major
|
||||
let n ← generalizeVars stx major
|
||||
let recInfo ← getRecInfo stx major
|
||||
let (mvarId, _) ← getMainGoal
|
||||
let result ← Meta.induction mvarId major.fvarId! recInfo.recName recInfo.altVars
|
||||
processResult recInfo.altRHSs result
|
||||
|
||||
private partial def checkCasesResultAux (casesResult : Array Meta.CasesSubgoal) (ctorNames : Array Name) (altRHSs : Array Syntax)
|
||||
: Nat → Nat → TacticM Unit
|
||||
| i, j =>
|
||||
private partial def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ctorNames : Array Name) (altRHSs : Array Syntax) : TacticM Unit := do
|
||||
let rec loop (i j : Nat) : TacticM Unit :=
|
||||
if h : j < altRHSs.size then do
|
||||
let altRHS := altRHSs.get ⟨j, h⟩;
|
||||
let altRHS := altRHSs.get ⟨j, h⟩
|
||||
if altRHS.isMissing then
|
||||
checkCasesResultAux i (j+1)
|
||||
loop i (j+1)
|
||||
else
|
||||
let ctorName := ctorNames.get! j;
|
||||
let ctorName := ctorNames.get! j
|
||||
if h : i < casesResult.size then
|
||||
let subgoal := casesResult.get ⟨i, h⟩;
|
||||
let subgoal := casesResult.get ⟨i, h⟩
|
||||
if ctorName == subgoal.ctorName then
|
||||
checkCasesResultAux (i+1) (j+1)
|
||||
loop (i+1) (j+1)
|
||||
else
|
||||
throwError ("alternative for '" ++ subgoal.ctorName ++ "' has not been provided")
|
||||
throwError msg!"alternative for '{subgoal.ctorName}' has not been provided"
|
||||
else
|
||||
throwError ("alternative for '" ++ ctorName ++ "' is not needed")
|
||||
throwError msg!"alternative for '{ctorName}' is not needed"
|
||||
else if h : i < casesResult.size then
|
||||
let subgoal := casesResult.get ⟨i, h⟩;
|
||||
throwError ("alternative for '" ++ subgoal.ctorName ++ "' has not been provided")
|
||||
let subgoal := casesResult.get ⟨i, h⟩
|
||||
throwError msg!"alternative for '{subgoal.ctorName}' has not been provided"
|
||||
else
|
||||
pure ()
|
||||
|
||||
private def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ctorNames : Array Name) (altRHSs : Array Syntax) : TacticM Unit :=
|
||||
unless altRHSs.isEmpty $ checkCasesResultAux casesResult ctorNames altRHSs 0 0
|
||||
unless altRHSs.isEmpty do
|
||||
loop 0 0
|
||||
|
||||
@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic :=
|
||||
fun stx => focusAux $ do
|
||||
fun stx => focusAux do
|
||||
-- parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
|
||||
let h? := getAuxHypothesisName stx;
|
||||
major ← elabMajor h? (getMajor stx);
|
||||
major ← generalizeMajor major;
|
||||
(mvarId, _) ← getMainGoal;
|
||||
let withAlts := stx.getArg 2;
|
||||
(recInfo, ctorNames) ← getRecInfoDefault major withAlts true;
|
||||
result ← liftMetaM $ Meta.cases mvarId major.fvarId! recInfo.altVars;
|
||||
checkCasesResult result ctorNames recInfo.altRHSs;
|
||||
let result := result.map (fun s => s.toInductionSubgoal);
|
||||
let altRHSs := recInfo.altRHSs.filter $ fun stx => !stx.isMissing;
|
||||
let h? := getAuxHypothesisName stx
|
||||
let major ← elabMajor h? (getMajor stx)
|
||||
let major ← generalizeMajor major
|
||||
let (mvarId, _) ← getMainGoal
|
||||
let withAlts := stx.getArg 2
|
||||
let (recInfo, ctorNames) ← getRecInfoDefault major withAlts true
|
||||
let result ← Meta.cases mvarId major.fvarId! recInfo.altVars
|
||||
checkCasesResult result ctorNames recInfo.altRHSs
|
||||
let result := result.map (fun s => s.toInductionSubgoal)
|
||||
let altRHSs := recInfo.altRHSs.filter fun stx => !stx.isMissing
|
||||
processResult altRHSs result
|
||||
|
||||
end Tactic
|
||||
end Elab
|
||||
end Lean
|
||||
end Lean.Elab.Tactic
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue