/-
Copyright (c) 2021 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import Mathlib.Tactic.RunCmd
import Lean.Elab.Tactic.Conv.Basic
import Std.Lean.Parser

/-!
Additional `conv` tactics.
-/

namespace Mathlib.Tactic.Conv
open Lean Parser.Tactic Parser.Tactic.Conv Elab.Tactic Meta

syntax (name := convLHS: ParserDescr
convLHS) "conv_lhs" (" at " ident: Parser.Parser
ident)? (" in " (occs: ParserDescr
occs)? term: Parser.Category
term)? " => " convSeq: ParserDescr
convSeq : tactic: Parser.Category
tactic
macro_rules
  | `(tactic| conv_lhs $[at $id: ?m.255
id]? $[in $[$occs: ?m.564 x✝
occs]? $pat: ?m.752
pat]? => $seq: ?m.848
seq) =>
    `(tactic| conv $[at $id: TSyntax `ident
id]? $[in $[$occs: TSyntax `Lean.Parser.Tactic.Conv.occs
occs]? $pat: TSyntax `term
pat]? => lhs; ($seq: ?m.848
seq:convSeq: ParserDescr
convSeq))

syntax (name := convRHS: ParserDescr
convRHS) "conv_rhs" (" at " ident: Parser.Parser
ident)? (" in " (occs: ParserDescr
occs)? term: Parser.Category
term)? " => " convSeq: ParserDescr
convSeq : tactic: Parser.Category
tactic
macro_rules
  | `(tactic| conv_rhs $[at $id: ?m.6014
id]? $[in $[$occs: ?m.6422
occs]? $pat: ?m.6511
pat]? => $seq: ?m.6607
seq) =>
    `(tactic| conv $[at $id: TSyntax `ident
id]? $[in $[$occs: TSyntax `Lean.Parser.Tactic.Conv.occs
occs]? $pat: TSyntax `term
pat]? => rhs; ($seq: ?m.6607
seq:convSeq: ParserDescr
convSeq))

macro "run_conv" e: ?m.11331
e:doSeq: Parser.Parser
doSeq : conv: Parser.Category
conv => `(conv| tactic' => run_tac $e: ?m.11331
e)

/--
* `discharge => tac` is a conv tactic which rewrites target `p` to `True` if `tac` is a tactic
  which proves the goal `⊢ p`.
* `discharge` without argument returns `⊢ p` as a subgoal.
-/
syntax (name := dischargeConv: ParserDescr
dischargeConv) "discharge" (" => " tacticSeq: Parser.Parser
tacticSeq)? : conv: Parser.Category
conv

/-- Elaborator for the `discharge` tactic. -/
@[tactic dischargeConv: ParserDescr
dischargeConv] def elabDischargeConv: Tactic
elabDischargeConv : Tactic: Type
Tactic := fun
  | `(conv| discharge $[=> $tac: ?m.13467
tac]?) => do
    let g: MVarId
g :: gs: List MVarId
gs ← getGoals: TacticM (List MVarId)
getGoals | throwNoGoalsToBeSolved: {α : Type} → TacticM α
throwNoGoalsToBeSolved
    let (theLhs: Expr
theLhs, theRhs: Expr
theRhs) ← Conv.getLhsRhsCore: MVarId → MetaM (Expr × Expr)
Conv.getLhsRhsCore g: MVarId
g
    let .true: Bool
.true ← isProp: Expr → MetaM Bool
isProp theLhs: Expr
theLhs | throwError "target is not a proposition": ?m.15027 ?m.15028
throwErrorthrowError "target is not a proposition": ?m.15027 ?m.15028
 "target is not a proposition"
    theRhs: Expr
theRhs.mvarId!: Expr → MVarId
mvarId!.assign: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → Expr → m Unit
assign (mkConst: Name → optParam (List Level) [] → Expr
mkConst ``True: Prop
True)
    let m: ?m.14347
m ← mkFreshExprMVar: Option Expr → optParam MetavarKind MetavarKind.natural → optParam Name Name.anonymous → MetaM Expr
mkFreshExprMVar theLhs: Expr
theLhs
    g: MVarId
g.assign: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → Expr → m Unit
assign (← mkEqTrue m): ?m.14401
(← mkEqTrue: Expr → MetaM Expr
mkEqTrue(← mkEqTrue m): ?m.14401
 m: ?m.14347
m(← mkEqTrue m): ?m.14401
)
    if let some: {α : Type ?u.14458} → α → Option α
some tac: TSyntax `Lean.Parser.Tactic.tacticSeq
tac := tac: ?m.13333 x✝²
tac then
      setGoals: List MVarId → TacticM Unit
setGoals [m: ?m.14347
m.mvarId!: Expr → MVarId
mvarId!]
      evalTactic: Syntax → TacticM Unit
evalTactic tac: TSyntax `Lean.Parser.Tactic.tacticSeq
tac; done: TacticM Unit
done
      setGoals: List MVarId → TacticM Unit
setGoals gs: List MVarId
gs
    else
      setGoals: List MVarId → TacticM Unit
setGoals (m: ?m.14347
m.mvarId!: Expr → MVarId
mvarId! :: gs: List MVarId
gs)
  | _ => Elab.throwUnsupportedSyntax: {m : Type ?u.13510 → Type ?u.13509} → {α : Type ?u.13510} → [inst : MonadExceptOf Exception m] → m α
Elab.throwUnsupportedSyntax

/-- Use `refine` in `conv` mode. -/
macro "refine " e: ?m.19162
e:term: Parser.Category
term : conv: Parser.Category
conv => `(conv| tactic => refine $e: ?m.19162
e)

open Elab Tactic
/--
The command `#conv tac => e` will run a conv tactic `tac` on `e`, and display the resulting
expression (discarding the proof).
For example, `#conv rw [true_and] => True ∧ False` displays `False`.
There are also shorthand commands for several common conv tactics:

* `#whnf e` is short for `#conv whnf => e`
* `#simp e` is short for `#conv simp => e`
* `#norm_num e` is short for `#conv norm_num => e`
* `#push_neg e` is short for `#conv push_neg => e`
-/
elab tk: ?m.21177
tk:"#conv " conv: ?m.21170
conv:conv: Parser.Category
conv " => " e: ?m.21158
e:term: Parser.Category
term : command: Parser.Category
command =>
  Command.runTermElabM: {α : Type} → (Array Expr → TermElabM α) → Command.CommandElabM α
Command.runTermElabM fun _: ?m.21185
_ ↦ do
    let e: ?m.21371
e ← Elab.Term.elabTermAndSynthesize: Syntax → Option Expr → TermElabM Expr
Elab.Term.elabTermAndSynthesize e: ?m.21158
e none: {α : Type ?u.21360} → Option α
none
    let (rhs: Expr
rhs, g: Expr
g) ← Conv.mkConvGoalFor: Expr → optParam Name Name.anonymous → MetaM (Expr × Expr)
Conv.mkConvGoalFor e: ?m.21371
e
    _: ?m.22876
_ ← Tactic.run: MVarId → TacticM Unit → TermElabM (List MVarId)
Tactic.run g: Expr
g.mvarId!: Expr → MVarId
mvarId! do
      evalTactic: Syntax → TacticM Unit
evalTactic conv: ?m.21170
conv
      for mvarId: ?m.21896
mvarId in (← getGoals): ?m.21798
(← getGoals: TacticM (List MVarId)
getGoals(← getGoals): ?m.21798
) do
        liftM: {m : Type ?u.21937 → Type ?u.21936} →
  {n : Type ?u.21937 → Type ?u.21935} → [self : MonadLiftT m n] → {α : Type ?u.21937} → m α → n α
liftM <| mvarId: ?m.21896
mvarId.refl: MVarId → MetaM Unit
refl <|> mvarId: ?m.21896
mvarId.inferInstance: MVarId → MetaM Unit
inferInstance <|> pure: {f : Type ?u.21983 → Type ?u.21982} → [self : Pure f] → {α : Type ?u.21983} → α → f α
pure (): Unit
()
      pruneSolvedGoals: TacticM Unit
pruneSolvedGoals
      let e': ?m.22532
e' ← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars rhs: Expr
rhs
      logInfoAt: {m : Type → Type} →
  [inst : Monad m] →
    [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → Syntax → MessageData → m Unit
logInfoAt tk: ?m.21177
tk e': ?m.22532
e'

@[inherit_doc Parser.Tactic.withReducible: ParserDescr
Parser.Tactic.withReducible]
macro (name := withReducible: ParserDescr
withReducible) tk: ?m.26385
tk:"with_reducible " s: ?m.26376
s:convSeq: ParserDescr
convSeq : conv: Parser.Category
conv =>
  `(conv| tactic' => with_reducible%$tk: ?m.26385
tk conv' => $s: ?m.26376
s)

/--
The command `#whnf e` evaluates `e` to Weak Head Normal Form, which means that the "head"
of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type.
It is similar to `#reduce e`, but it does not reduce the expression completely,
only until the first constructor is exposed. For example:
```
open Nat List
set_option pp.notation false
#whnf [1, 2, 3].map succ
-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
#reduce [1, 2, 3].map succ
-- cons 2 (cons 3 (cons 4 nil))
```
The head of this expression is the `List.cons` constructor,
so we can see from this much that the list is not empty,
but the subterms `Nat.succ 1` and `List.map Nat.succ (List.cons 2 (List.cons 3 List.nil))` are
still unevaluated. `#reduce` is equivalent to using `#whnf` on every subexpression.
-/
macro tk: ?m.28502
tk:"#whnf " e: ?m.28493
e:term: Parser.Category
term : command: Parser.Category
command => `(command: Parser.Category
command| #conv%$tk: ?m.28502
tk whnf => $e: ?m.28493
e)

/--
The command `#whnfR e` evaluates `e` to Weak Head Normal Form with Reducible transparency,
that is, it uses `whnf` but only unfolding reducible definitions.
-/
macro tk: ?m.30326
tk:"#whnfR " e: ?m.30317
e:term: Parser.Category
term : command: Parser.Category
command => `(command: Parser.Category
command| #conv%$tk: ?m.30326
tk with_reducible whnf => $e: ?m.30317
e)

/--
* `#simp => e` runs `simp` on the expression `e` and displays the resulting expression after
  simplification.
* `#simp only [lems] => e` runs `simp only [lems]` on `e`.
* The `=>` is optional, so `#simp e` and `#simp only [lems] e` have the same behavior.
  It is mostly useful for disambiguating the expression `e` from the lemmas.
-/
syntax "#simp" (&: String → Bool → ParserDescr
&" only")? (simpArgs: ParserDescr
simpArgs)? " =>"? ppSpace: Parser.Parser
ppSpace term: Parser.Category
term : command: Parser.Category
command
macro_rules
  | `(#simp%$tk: ?m.33141
tk $[only%$o: ?m.32428
o]? $[[$args: ?m.32855
args,*]]? $[=>]? $e: ?m.33133
e) =>
    `(#conv%$tk: ?m.33141
tk simp $[only%$o: Syntax
o]? $[[$args: ?m.32733 x✝¹
args,*]]? => $e: ?m.33133
e)