Lean.Elab.Tactic.Conv.Basic

source

def Lean.Elab.Tactic.Conv.mkConvGoalFor (lhs : Lean.Expr) :

Lean.MetaM (Lean.Expr × Lean.Expr)

Equations

Lean.Elab.Tactic.Conv.mkConvGoalFor lhs = do let lhsType ← Lean.Meta.inferType lhs let rhs ← Lean.Meta.mkFreshExprMVar (some lhsType) Lean.MetavarKind.natural Lean.Name.anonymous let a ← Lean.Meta.mkEq lhs rhs let targetNew : Lean.Expr := Lean.mkLHSGoal a let newGoal ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar targetNew Lean.Name.anonymous pure (rhs, newGoal)

source

def Lean.Elab.Tactic.Conv.markAsConvGoal (mvarId : Lean.MVarId) :

Lean.MetaM Lean.MVarId

Equations

Lean.Elab.Tactic.Conv.markAsConvGoal mvarId = do let target ← Lean.Meta.getMVarType mvarId let _do_jp : PUnit → Lean.MetaM Lean.MVarId := fun y => do let a ← Lean.Meta.getMVarType mvarId Lean.Meta.replaceTargetDefEq mvarId (Lean.mkLHSGoal a) if Option.isSome (Lean.isLHSGoal? target) = true then pure mvarId else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Tactic.Conv.convert (lhs : Lean.Expr) (conv : Lean.Elab.Tactic.TacticM Unit) :

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

Equations

Lean.Elab.Tactic.Conv.convert lhs conv = do let discr ← liftM (Lean.Elab.Tactic.Conv.mkConvGoalFor lhs) let x : Lean.Expr × Lean.Expr := discr match x with | (rhs, newGoal) => do let savedGoals ← Lean.Elab.Tactic.getGoals tryFinally (do Lean.Elab.Tactic.setGoals [Lean.Expr.mvarId! newGoal] conv let a ← Lean.Elab.Tactic.getGoals let r ← let col := a; forIn col PUnit.unit fun mvarId r => do tryCatch (liftM (Lean.Meta.applyRefl mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "refl failed"))) fun x => pure () pure (ForInStep.yield PUnit.unit) let x : PUnit := r Lean.Elab.Tactic.pruneSolvedGoals let a ← Lean.Elab.Tactic.getGoals let _do_jp : PUnit → Lean.Elab.Tactic.TacticM PUnit := fun y => pure () if List.isEmpty a = true then do let y ← pure PUnit.unit _do_jp y else do let a ← Lean.Elab.Tactic.getGoals let y ← Lean.throwError (Lean.toMessageData "convert tactic failed, there are unsolved goals\n" ++ Lean.toMessageData (Lean.Elab.goalsToMessageData a) ++ Lean.toMessageData "") _do_jp y) (Lean.Elab.Tactic.setGoals savedGoals) let a ← liftM (Lean.Meta.instantiateMVars rhs) let a_1 ← liftM (Lean.Meta.instantiateMVars newGoal) pure (a, a_1)

source

def Lean.Elab.Tactic.Conv.getLhsRhsCore (mvarId : Lean.MVarId) :

Lean.MetaM (Lean.Expr × Lean.Expr)

Equations

Lean.Elab.Tactic.Conv.getLhsRhsCore mvarId = Lean.Meta.withMVarContext mvarId do let a ← Lean.Meta.getMVarType mvarId let discr ← Lean.Meta.matchEq? a match discr with | some (x, lhs, rhs) => pure (lhs, rhs) | x => Lean.throwError (Lean.toMessageData "invalid 'conv' goal")

source

def Lean.Elab.Tactic.Conv.getLhsRhs :

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

Equations

Lean.Elab.Tactic.Conv.getLhsRhs = do let a ← Lean.Elab.Tactic.getMainGoal liftM (Lean.Elab.Tactic.Conv.getLhsRhsCore a)

source

def Lean.Elab.Tactic.Conv.getLhs :

Lean.Elab.Tactic.TacticM Lean.Expr

Equations

Lean.Elab.Tactic.Conv.getLhs = do let a ← Lean.Elab.Tactic.Conv.getLhsRhs pure a.fst

source

def Lean.Elab.Tactic.Conv.getRhs :

Lean.Elab.Tactic.TacticM Lean.Expr

Equations

Lean.Elab.Tactic.Conv.getRhs = do let a ← Lean.Elab.Tactic.Conv.getLhsRhs pure a.snd

source

def Lean.Elab.Tactic.Conv.updateLhs (lhs' : Lean.Expr) (h : Lean.Expr) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.Conv.updateLhs lhs' h = do let rhs ← Lean.Elab.Tactic.Conv.getRhs let a ← liftM (Lean.Meta.mkEq lhs' rhs) let newGoal ← liftM (Lean.Meta.mkFreshExprSyntheticOpaqueMVar (Lean.mkLHSGoal a) Lean.Name.anonymous) let a ← Lean.Elab.Tactic.getMainGoal let a_1 ← liftM (Lean.Meta.mkEqTrans h newGoal) liftM (Lean.Meta.assignExprMVar a a_1) Lean.Elab.Tactic.replaceMainGoal [Lean.Expr.mvarId! newGoal]

source

def Lean.Elab.Tactic.Conv.changeLhs (lhs' : Lean.Expr) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.Conv.changeLhs lhs' = do let rhs ← Lean.Elab.Tactic.Conv.getRhs Lean.Elab.Tactic.liftMetaTactic1 fun mvarId => do let a ← Lean.Meta.mkEq lhs' rhs Lean.Internal.coeM (Lean.Meta.replaceTargetDefEq mvarId (Lean.mkLHSGoal a))

source

def Lean.Elab.Tactic.Conv.evalWhnf :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalWhnf stx = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.Conv.getLhs let a ← liftM (Lean.Meta.whnf a) Lean.Elab.Tactic.Conv.changeLhs a

source

def Lean.Elab.Tactic.Conv.evalReduce :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalReduce stx = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.Conv.getLhs let a ← liftM (Lean.Meta.reduce a true true true) Lean.Elab.Tactic.Conv.changeLhs a

source

def Lean.Elab.Tactic.Conv.evalConvSeq1Indented :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalConvSeq1Indented stx = Lean.Elab.Tactic.evalTacticSeq1Indented stx

source

def Lean.Elab.Tactic.Conv.evalConvSeqBracketed :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalConvSeqBracketed stx = do let initInfo ← Lean.Elab.Tactic.mkInitialTacticInfo (Lean.Syntax.getOp stx 0) Lean.withRef (Lean.Syntax.getOp stx 2) (Lean.Elab.Tactic.closeUsingOrAdmit do Lean.Elab.withInfoContext (pure ()) initInfo Lean.Elab.Tactic.evalManyTacticOptSemi (Lean.Syntax.getOp stx 1) let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.allGoals #[Lean.Syntax.atom info "all_goals", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticTry_ #[Lean.Syntax.atom info "try", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticRfl #[Lean.Syntax.atom info "rfl"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.atom info ")"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]) Lean.Elab.Tactic.evalTactic a)

source

def Lean.Elab.Tactic.Conv.evalNestedConv :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalNestedConv stx = Lean.Elab.Tactic.Conv.evalConvSeqBracketed (Lean.Syntax.getOp stx 0)

source

def Lean.Elab.Tactic.Conv.evalConvSeq :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalConvSeq stx = Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 0)

source

def Lean.Elab.Tactic.Conv.evalConvConvSeq :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalConvConvSeq stx = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.Conv.getLhs let discr ← Lean.Elab.Tactic.Conv.convert a (Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp (Lean.Syntax.getOp stx 2) 0)) let x : Lean.Expr × Lean.Expr := discr match x with | (lhsNew, proof) => Lean.Elab.Tactic.Conv.updateLhs lhsNew proof

source

def Lean.Elab.Tactic.Conv.evalParen :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalParen stx = Lean.Elab.Tactic.evalTactic (Lean.Syntax.getOp stx 1)

source

def Lean.Elab.Tactic.Conv.remarkAsConvGoal :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.Conv.remarkAsConvGoal = do let a ← Lean.Elab.Tactic.getUnsolvedGoals let newGoals ← List.mapM (fun mvarId => Lean.Meta.withMVarContext mvarId do let target ← liftM (Lean.Meta.getMVarType mvarId) let a ← liftM (Lean.Meta.matchEq? target) match a with | some (x, lhs, rhs) => if Lean.Expr.isMVar (Lean.Expr.getAppFn rhs) = true then liftM (Lean.Meta.replaceTargetDefEq mvarId (Lean.mkLHSGoal target)) else pure mvarId | x => pure mvarId) a Lean.Elab.Tactic.setGoals newGoals

source

def Lean.Elab.Tactic.Conv.evalNestedTacticCore :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalNestedTacticCore stx = let seq := Lean.Syntax.getOp stx 2; do Lean.Elab.Tactic.evalTactic seq Lean.Elab.Tactic.Conv.remarkAsConvGoal

source

def Lean.Elab.Tactic.Conv.evalNestedTactic :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalNestedTactic stx = let seq := Lean.Syntax.getOp stx 2; do let target ← Lean.Elab.Tactic.getMainTarget let _do_jp : Unit → Lean.Elab.Tactic.TacticM Unit := fun y => Lean.Elab.Tactic.focus do Lean.Elab.Tactic.evalTactic seq Lean.Elab.Tactic.Conv.remarkAsConvGoal match Lean.isLHSGoal? target with | some x => do let y ← Lean.Elab.Tactic.liftMetaTactic1 fun mvarId => Lean.Internal.coeM (Lean.Meta.replaceTargetDefEq mvarId (Lean.Expr.mdataExpr! target)) _do_jp y | x => do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Tactic.Conv.evalConv :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalConv stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.Conv.conv = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let yes := fun x loc? => let discr_3 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_3 2 = true then let discr_4 := Lean.Syntax.getArg discr_3 0; let discr_5 := Lean.Syntax.getArg discr_3 1; let discr_6 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let code := discr; let p := discr_5; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.Conv.conv #[Lean.Syntax.atom info "conv", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match loc? with | some loc? => #[Lean.Syntax.atom info "at", loc?] | none => Array.empty)), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.Conv.convSeq #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.Conv.convSeq1Indented #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.Conv.pattern #[Lean.Syntax.atom info "pattern", p], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `group #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.Conv.paren #[Lean.Syntax.atom info "(", code, Lean.Syntax.atom info ")"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]) Lean.Elab.Tactic.evalTactic a else let discr_4 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_4 0 = true then let discr_5 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; let code := discr; match loc? with | some loc => Lean.Elab.Tactic.Conv.convLocalDecl code (Lean.Syntax.getId loc) | x => Lean.Elab.Tactic.Conv.convTarget code else let discr_5 := Lean.Syntax.getArg discr 2; let discr_6 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax; if Lean.Syntax.isNone discr_2 = true then yes () none else let discr_3 := discr_2; if Lean.Syntax.matchesNull discr_3 2 = true then let discr := Lean.Syntax.getArg discr_3 0; let discr := Lean.Syntax.getArg discr_3 1; let loc? := discr; yes () (some loc?) else let discr_4 := discr_2; let discr_5 := Lean.Syntax.getArg discr 1; let discr_6 := Lean.Syntax.getArg discr 2; let discr_7 := Lean.Syntax.getArg discr 3; let discr := Lean.Syntax.getArg discr 4; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax

source

def Lean.Elab.Tactic.Conv.evalFirst :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalFirst = Lean.Elab.Tactic.evalFirst