Lean.Elab.Tactic.ElabTerm

source

def Lean.Elab.Tactic.elabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) :

Lean.Elab.Tactic.TacticM Lean.Expr

Equations

Lean.Elab.Tactic.elabTerm stx expectedType? mayPostpone = Lean.withRef stx do let e ← liftM (Lean.Elab.Term.elabTerm stx expectedType? true true) liftM (Lean.Elab.Term.synthesizeSyntheticMVars mayPostpone false) liftM (Lean.Meta.instantiateMVars e)

source

def Lean.Elab.Tactic.elabTermEnsuringType (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) :

Lean.Elab.Tactic.TacticM Lean.Expr

Equations

Lean.Elab.Tactic.elabTermEnsuringType stx expectedType? mayPostpone = do let e ← Lean.Elab.Tactic.elabTerm stx expectedType? mayPostpone match expectedType? with | none => pure e | some expectedType => do let eType ← liftM (Lean.Meta.inferType e) let a ← Lean.Meta.withAssignableSyntheticOpaque (liftM (Lean.Meta.isDefEq eType expectedType)) let _do_jp : PUnit → Lean.Elab.Tactic.TacticM Lean.Expr := fun y => pure e if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← liftM (Lean.Elab.Term.throwTypeMismatchError none expectedType eType e none none) _do_jp y

source

def Lean.Elab.Tactic.closeMainGoalUsing (x : Lean.Expr → Lean.Elab.Tactic.TacticM Lean.Expr) (checkUnassigned : optParam Bool true) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.closeMainGoalUsing x checkUnassigned = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainTarget let a ← x a Lean.Elab.Tactic.closeMainGoal a checkUnassigned

source

def Lean.Elab.Tactic.logUnassignedAndAbort (mvarIds : Array Lean.MVarId) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.logUnassignedAndAbort mvarIds = do let a ← liftM (Lean.Elab.Term.logUnassignedUsingErrorInfos mvarIds none) if a = true then Lean.Elab.throwAbortTactic else pure PUnit.unit

source

def Lean.Elab.Tactic.filterOldMVars (mvarIds : Array Lean.MVarId) (mvarCounterSaved : Nat) :

Lean.MetaM (Array Lean.MVarId)

Equations

Lean.Elab.Tactic.filterOldMVars mvarIds mvarCounterSaved = do let mctx ← Lean.getMCtx pure (Array.filter (fun mvarId => decide ((Lean.MetavarContext.getDecl mctx mvarId).index ≥ mvarCounterSaved)) mvarIds 0 (Array.size mvarIds))

source

def Lean.Elab.Tactic.evalExact :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalExact stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.exact = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; Lean.Elab.Tactic.closeMainGoalUsing (fun type => do let a ← Lean.getMCtx let mvarCounterSaved : Nat := a.mvarCounter let r ← Lean.Elab.Tactic.elabTermEnsuringType e (some type) false let a ← liftM (Lean.Meta.getMVars r) let a ← liftM (Lean.Elab.Tactic.filterOldMVars a mvarCounterSaved) Lean.Elab.Tactic.logUnassignedAndAbort a pure r) false else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.elabTermWithHoles (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (tagSuffix : Lean.Name) (allowNaturalHoles : optParam Bool false) :

Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)

Equations

Lean.Elab.Tactic.elabTermWithHoles stx expectedType? tagSuffix allowNaturalHoles = do let a ← Lean.getMCtx let mvarCounterSaved : Nat := a.mvarCounter let val ← Lean.Elab.Tactic.elabTermEnsuringType stx expectedType? false let newMVarIds ← liftM (Lean.Meta.getMVarsNoDelayed val) let newMVarIds ← Array.filterM (fun mvarId => do let a ← liftM (Lean.Elab.Term.isLetRecAuxMVar mvarId) pure !a) newMVarIds 0 (Array.size newMVarIds) let _do_jp : List Lean.MVarId → Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId) := fun newMVarIds => do let a ← Lean.Elab.Tactic.getMainTag Lean.Elab.Tactic.tagUntaggedGoals a tagSuffix newMVarIds pure (val, newMVarIds) if allowNaturalHoles = true then do let y ← pure (Array.toList newMVarIds) _do_jp y else do let naturalMVarIds ← Array.filterM (fun mvarId => do let a ← liftM (Lean.Meta.getMVarDecl mvarId) pure (Lean.MetavarKind.isNatural a.kind)) newMVarIds 0 (Array.size newMVarIds) let syntheticMVarIds ← Array.filterM (fun mvarId => do let a ← liftM (Lean.Meta.getMVarDecl mvarId) pure !Lean.MetavarKind.isNatural a.kind) newMVarIds 0 (Array.size newMVarIds) let naturalMVarIds ← liftM (Lean.Elab.Tactic.filterOldMVars naturalMVarIds mvarCounterSaved) Lean.Elab.Tactic.logUnassignedAndAbort naturalMVarIds let y ← pure (Array.toList syntheticMVarIds) _do_jp y

source

def Lean.Elab.Tactic.refineCore (stx : Lean.Syntax) (tagSuffix : Lean.Name) (allowNaturalHoles : Bool) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.refineCore stx tagSuffix allowNaturalHoles = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainTarget let discr ← Lean.Elab.Tactic.elabTermWithHoles stx (some a) tagSuffix allowNaturalHoles let x : Lean.Expr × List Lean.MVarId := discr match x with | (val, mvarIds') => do let a ← Lean.Elab.Tactic.getMainGoal liftM (Lean.Meta.assignExprMVar a val) Lean.Elab.Tactic.replaceMainGoal mvarIds'

source

def Lean.Elab.Tactic.evalRefine :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRefine stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.refine = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; Lean.Elab.Tactic.refineCore e `refine false else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalRefine' :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRefine' stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.refine' = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; Lean.Elab.Tactic.refineCore e `refine' true else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalSpecialize :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalSpecialize stx = Lean.Elab.Tactic.withMainContext (let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.specialize = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; do let discr ← Lean.Elab.Tactic.elabTermWithHoles e none `specialize true let x : Lean.Expr × List Lean.MVarId := discr match x with | (e, mvarIds') => let h := Lean.Expr.getAppFn e; if Lean.Expr.isFVar h = true then do let localDecl ← liftM (Lean.Meta.getLocalDecl (Lean.Expr.fvarId! h)) let a ← Lean.Elab.Tactic.getMainGoal let a_1 ← liftM (Lean.Meta.inferType e) let mvarId ← liftM (Lean.Meta.assert a (Lean.LocalDecl.userName localDecl) (Lean.Expr.headBeta a_1) e) let discr ← liftM (Lean.Meta.intro1P mvarId) let x : Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => do let mvarId ← liftM (Lean.Meta.tryClear mvarId (Lean.Expr.fvarId! h)) Lean.Elab.Tactic.replaceMainGoal (mvarId :: mvarIds') else Lean.throwError (Lean.toMessageData "'specialize' requires a term of the form `h x_1 .. x_n` where `h` appears in the local context") else let discr := stx; Lean.Elab.throwUnsupportedSyntax)

source

def Lean.Elab.Tactic.elabTermForApply (stx : Lean.Syntax) (mayPostpone : optParam Bool true) :

Lean.Elab.Tactic.TacticM Lean.Expr

Equations

Lean.Elab.Tactic.elabTermForApply stx mayPostpone = let _do_jp := fun y => Lean.Elab.Tactic.elabTerm stx none mayPostpone; if Lean.Syntax.isIdent stx = true then do let a ← liftM (Lean.Elab.Term.resolveId? stx "term" true) match a with | some e => pure e | x => do let y ← pure () _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Tactic.evalApplyLikeTactic (tac : Lean.MVarId → Lean.Expr → Lean.MetaM (List Lean.MVarId)) (e : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.evalApplyLikeTactic tac e = Lean.Elab.Tactic.withMainContext do let val ← Lean.Elab.Tactic.elabTermForApply e true let a ← Lean.Elab.Tactic.getMainGoal let mvarIds' ← liftM (tac a val) liftM (Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false) Lean.Elab.Tactic.replaceMainGoal mvarIds'

source

def Lean.Elab.Tactic.evalApply :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalApply stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.apply = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; Lean.Elab.Tactic.evalApplyLikeTactic Lean.Meta.apply e else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.getFVarId (id : Lean.Syntax) :

Lean.Elab.Tactic.TacticM Lean.FVarId

Equations

Lean.Elab.Tactic.getFVarId id = Lean.withRef id do let e ← Lean.Elab.Tactic.withMainContext (Lean.Elab.Tactic.elabTermForApply id false) match e with | Lean.Expr.fvar fvarId x => pure fvarId | x => Lean.throwError (Lean.toMessageData "unexpected term '" ++ Lean.toMessageData e ++ Lean.toMessageData "'; expected single reference to variable")

source

def Lean.Elab.Tactic.evalConstructor :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalConstructor stx = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.getMainGoal let mvarIds' ← liftM (Lean.Meta.constructor a) liftM (Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false) Lean.Elab.Tactic.replaceMainGoal mvarIds'

source

def Lean.Elab.Tactic.getFVarIds (ids : Array Lean.Syntax) :

Lean.Elab.Tactic.TacticM (Array Lean.FVarId)

Equations

Lean.Elab.Tactic.getFVarIds ids = Lean.Elab.Tactic.withMainContext (Array.mapM Lean.Elab.Tactic.getFVarId ids)

source

def Lean.Elab.Tactic.evalExistsIntro :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalExistsIntro stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.existsIntro = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; Lean.Elab.Tactic.evalApplyLikeTactic (fun mvarId e => do let a ← Lean.Meta.existsIntro mvarId e pure [a]) e else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalWithReducible :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalWithReducible stx = Lean.Meta.withReducible (Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 1))

source

def Lean.Elab.Tactic.evalWithReducibleAndInstances :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalWithReducibleAndInstances stx = Lean.Meta.withReducibleAndInstances (Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 1))

source

def Lean.Elab.Tactic.elabAsFVar (stx : Lean.Syntax) (userName? : optParam (Option Lean.Name) none) :

Lean.Elab.Tactic.TacticM Lean.FVarId

Equations

Lean.Elab.Tactic.elabAsFVar stx userName? = Lean.Elab.Tactic.withMainContext do let e ← Lean.Elab.Tactic.elabTerm stx none false match e with | Lean.Expr.fvar fvarId x => pure fvarId | x => do let type ← liftM (Lean.Meta.inferType e) let intro : Lean.Name → Bool → Lean.Elab.Tactic.TacticM Lean.FVarId := fun userName preserveBinderNames => do let mvarId ← Lean.Elab.Tactic.getMainGoal let discr ← Lean.Meta.liftMetaM do let mvarId ← Lean.Meta.assert mvarId userName type e Lean.Meta.intro1Core mvarId preserveBinderNames let x : Lean.FVarId × Lean.MVarId := discr match x with | (fvarId, mvarId) => do Lean.Elab.Tactic.replaceMainGoal [mvarId] pure fvarId match userName? with | none => intro `h false | some userName => intro userName true

source

def Lean.Elab.Tactic.evalRename :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalRename stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.rename = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr_4 := Lean.Syntax.getArg discr 3; cond (Lean.Syntax.isOfKind discr_4 `ident) (let h := discr_4; let typeStx := discr_2; Lean.Elab.Tactic.withMainContext do let fvarId ← Lean.Elab.withoutModifyingStateWithInfoAndMessages (Lean.Meta.withNewMCtxDepth do let type ← Lean.Elab.Tactic.elabTerm typeStx none true let a ← Lean.getLCtx let fvarId? ← Lean.LocalContext.findDeclRevM? a fun localDecl => do let a ← liftM (Lean.Meta.isDefEq type (Lean.LocalDecl.type localDecl)) if a = true then pure (some (Lean.LocalDecl.fvarId localDecl)) else pure none match fvarId? with | none => Lean.throwError (Lean.toMessageData "failed to find a hypothesis with type" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") | some fvarId => pure fvarId) let a ← Lean.Elab.Tactic.getMainGoal let a ← liftM (Lean.Meta.rename a fvarId (Lean.Syntax.getId h)) Lean.Elab.Tactic.replaceMainGoal [a]) (let discr := Lean.Syntax.getArg discr 3; Lean.Elab.throwUnsupportedSyntax) else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.evalDecide :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalDecide stx = Lean.Elab.Tactic.closeMainGoalUsing (fun expectedType => do let expectedType ← liftM (Lean.Elab.Tactic.preprocessPropToDecide expectedType) let d ← liftM (Lean.Meta.mkDecide expectedType) let d ← liftM (Lean.Meta.instantiateMVars d) let r ← Lean.Meta.withDefault (liftM (Lean.Meta.whnf d)) let _do_jp : PUnit → Lean.Elab.Tactic.TacticM Lean.Expr := fun y => let s := Lean.Expr.appArg! d; do let rflPrf ← liftM (Lean.Meta.mkEqRefl (Lean.toExpr true)) pure (Lean.mkApp3 (Lean.mkConst `of_decide_eq_true) expectedType s rflPrf) if Lean.Expr.isConstOf r `Bool.true = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "failed to reduce to 'true'" ++ Lean.toMessageData (Lean.indentExpr r) ++ Lean.toMessageData "") _do_jp y) true

source

def Lean.Elab.Tactic.evalNativeDecide :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalNativeDecide stx = Lean.Elab.Tactic.closeMainGoalUsing (fun expectedType => do let expectedType ← liftM (Lean.Elab.Tactic.preprocessPropToDecide expectedType) let d ← liftM (Lean.Meta.mkDecide expectedType) let auxDeclName ← liftM (Lean.Elab.Tactic.mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d) let rflPrf ← liftM (Lean.Meta.mkEqRefl (Lean.toExpr true)) let s : Lean.Expr := Lean.Expr.appArg! d pure (Lean.mkApp3 (Lean.mkConst `of_decide_eq_true) expectedType s (Lean.mkApp3 (Lean.mkConst `Lean.ofReduceBool) (Lean.mkConst auxDeclName) (Lean.toExpr true) rflPrf))) true