/-
Copyright (c) 2021 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import Lean
import Mathlib.Tactic.Eqns
import Mathlib.Data.Subtype

/-!
# Irreducible definitions

This file defines an `irreducible_def` command,
which works almost like the `def` command
except that the introduced definition
does not reduce to the value.
Instead, the command
adds a `_def` lemma
which can be used for rewriting.

```
irreducible_def frobnicate (a b : Nat) :=
  a + b

example : frobnicate a 0 = a := by
  simp [frobnicate_def]
```

-/

namespace Lean.Elab.Command

open Term Meta

/-- `delta% t` elaborates to a head-delta reduced version of `t`. -/
elab "delta% " t: ?m.103
t:term: Parser.Category
term : term: Parser.Category
term <= expectedType: ?m.70
expectedType => do
  let t: ?m.355
t ← elabTerm: Syntax → Option Expr → optParam Bool true → optParam Bool true → TermElabM Expr
elabTerm t: ?m.103
t expectedType: ?m.70
expectedType
  synthesizeSyntheticMVars: optParam Bool true → optParam Bool false → TermElabM Unit
synthesizeSyntheticMVars
  let t: ?m.520
t ← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars t: ?m.355
t
  let some: {α : Type ?u.133} → α → Option α
some t: Expr
t ← delta?: Expr → (optParam (Name → Bool) fun x => true) → CoreM (Option Expr)
delta? t: ?m.520
t | throwError "cannot delta reduce {t: ?m.520
t}"
  pure: {f : Type ?u.736 → Type ?u.735} → [self : Pure f] → {α : Type ?u.736} → α → f α
pure t: Expr
t

/- `eta_helper f = (· + 3)` elabs to `∀ x, f x = x + 3` -/
local elab "eta_helper " t: ?m.2856
t:term: Parser.Category
term : term: Parser.Category
term => do
  let t: ?m.3060
t ← elabTerm: Syntax → Option Expr → optParam Bool true → optParam Bool true → TermElabM Expr
elabTerm t: ?m.2856
t none: {α : Type ?u.3049} → Option α
none
  let some: {α : Type ?u.3066} → α → Option α
some (_, lhs: Expr
lhs, rhs: Expr
rhs) := t: ?m.3060
t.eq?: Expr → Option (Expr × Expr × Expr)
eq? | throwError "not an equation: {t: ?m.3060
t}"
  synthesizeSyntheticMVars: optParam Bool true → optParam Bool false → TermElabM Unit
synthesizeSyntheticMVars
  let rhs: ?m.3278
rhs ← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars rhs: Expr
rhs
  lambdaTelescope: {n : Type → Type ?u.3280} →
  [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → Expr → (Array Expr → Expr → n α) → n α
lambdaTelescope rhs: ?m.3278
rhs fun xs: ?m.3321
xs rhs: ?m.3324
rhs ↦ do
    let lhs: ?m.3332
lhs := (mkAppN: Expr → Array Expr → Expr
mkAppN lhs: Expr
lhs xs: ?m.3321
xs).headBeta: Expr → Expr
headBeta
    mkForallFVars: Array Expr → Expr → optParam Bool false → optParam Bool true → optParam BinderInfo BinderInfo.implicit → MetaM Expr
mkForallFVars xs: ?m.3321
xs <|← mkEq: Expr → Expr → MetaM Expr
mkEq lhs: ?m.3332
lhs rhs: ?m.3324
rhs

/-- `val_proj x` elabs to the *primitive projection* `@x.val`.  -/
local elab "val_proj " e: ?m.6054
e:term: Parser.Category
term : term: Parser.Category
term => do
  let e: ?m.7102
e ← elabTerm: Syntax → Option Expr → optParam Bool true → optParam Bool true → TermElabM Expr
elabTerm (← `(($e : Subtype _))): ?m.6961
(← `(($e: ?m.6054
e(← `(($e : Subtype _))): ?m.6961
 : Subtype _))) none: {α : Type ?u.7091} → Option α
none
  return mkProj: Name → ℕ → Expr → Expr
mkProj ``Subtype: {α : Sort u} → (α → Prop) → Sort (max1u)
Subtype 0: ?m.7130
0 e: ?m.7102
e

/--
Executes the commands,
and stops after the first error.
In short, S-A-F-E.
-/
local syntax "stop_at_first_error" (ppLine: Parser.Parser
ppLine command: Parser.Category
command)* : command: Parser.Category
command
open Command in elab_rules : command
  | `(stop_at_first_error $[$cmds: ?m.10593
cmds]*) => do
    for cmd: ?m.10736
cmd in cmds: Array (TSyntax `command)
cmds do
      elabCommand: Syntax → CommandElabM Unit
elabCommand cmd: ?m.10736
cmd.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw
      if (← get): ?m.11002
(← get: {σ : outParam (Type ?u.10824)} → {m : Type ?u.10824 → Type ?u.10823} → [self : MonadState σ m] → m σ
get(← get): ?m.11002
).messages: State → MessageLog
messages.hasErrors: MessageLog → Bool
hasErrors then break: ?m.11099 ?m.11101
break

syntax irredDefLemma: ParserDescr
irredDefLemma := atomic: Parser.Parser → Parser.Parser
atomic("(" "lemma" " := ") ident: Parser.Parser
ident ")"

/--
Introduces an irreducible definition.
`irreducible_def foo := 42` generates
a constant `foo : Nat` as well as
a theorem `foo_def : foo = 42`.
-/
elab mods: ?m.13480
mods:declModifiers: Parser.Parser
declModifiers "irreducible_def" n_id: ?m.13470
n_id:declId: Parser.Parser
declId n_def: ?m.13456
n_def:(irredDefLemma: ParserDescr
irredDefLemma)?
    declSig: ?m.13449
declSig:optDeclSig: Parser.Parser
optDeclSig val: ?m.13440
val:declVal: Parser.Parser
declVal :
    command: Parser.Category
command => do
  let (n: TSyntax `ident
n, us: Option (Syntax.TSepArray `ident ",")
us) ← match n_id: ?m.13470
n_id with
    | `(Parser.Command.declId: Parser.Parser
Parser.Command.declId| $n: ?m.13992
n:ident $[.{$us: ?m.13654 x✝
us,*}]?) => pure: {f : Type ?u.14035 → Type ?u.14034} → [self : Pure f] → {α : Type ?u.14035} → α → f α
purepure (n, us): CommandElabM (?m.13516 y✝)
 (n: ?m.13992
npure (n, us): CommandElabM (?m.13516 y✝)
, us: ?m.13654 x✝
uspure (n, us): CommandElabM (?m.13516 y✝)
)
    | _ => throwUnsupportedSyntax: CommandElabM (?m.13516 y✝)
throwUnsupportedSyntax
  let us': ?m.14406
us' := us: Option (Syntax.TSepArray `ident ",")
us.getD: {α : Type ?u.14407} → Option α → α → α
getD { elemsAndSeps := #[]: Array ?m.14415
#[] }
  let n_def: ?m.14421
n_def ← match n_def: ?m.13456
n_def.getD: {α : Type ?u.14650} → Option α → α → α
getD ⟨mkNullNode: optParam (Array Syntax) #[] → Syntax
mkNullNode⟩ with
    | `(irredDefLemma: ParserDescr
irredDefLemma| (lemma := $id: ?m.14558
id)) => pure: {f : Type ?u.14601 → Type ?u.14600} → [self : Pure f] → {α : Type ?u.14601} → α → f α
purepure id: CommandElabM (?m.14425 y✝)
 id: ?m.14558
id
    | _ => pure: {f : Type ?u.14696 → Type ?u.14695} → [self : Pure f] → {α : Type ?u.14696} → α → f α
purepure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 <| mkIdent: Name → Ident
mkIdentpure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 <| (·.review: MacroScopesView → Name
reviewpure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)) <|
      pure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
letpure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 scopes: ?m.14730
scopespure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 := extractMacroScopes: Name → MacroScopesView
extractMacroScopespure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 n: TSyntax `ident
npure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
.getId: Ident → Name
getIdpure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
      { scopes: ?m.14730
scopespure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 pure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
withpure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 namepure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 := scopes: ?m.14730
scopespure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
.name: MacroScopesView → Name
namepure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
.appendAfter: Name → String → Name
appendAfterpure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 "_def": String
"_def"pure <| mkIdent <| (·.review) <|
      let scopes := extractMacroScopes n.getId
      { scopes with name := scopes.name.appendAfter "_def" }: CommandElabM (?m.14425 y✝)
 }
  let `(Parser.Command.declModifiersF: Parser.Parser
Parser.Command.declModifiersF|
      $[$doc: ?m.14884
doc:docComment: Parser.Parser
docComment]? $[@[$attrs: ?m.15427 x✝
attrs,*]]?
      $[$vis: ?m.16015
vis]? $[$nc: ?m.16205
nc:noncomputable: Parser.Parser
noncomputable]? $[$uns: ?m.16743
uns:unsafe: Parser.Parser
unsafe]?) := mods: ?m.13480
mods
    | throwError "unsupported modifiers {format: {α : Type ?u.20628} → [self : ToFormat α] → α → Format
format mods: ?m.13480
mods}"
  let attrs: ?m.17059
attrs := attrs: ?m.15427 x✝³
attrs.getD: {α : Type ?u.17060} → Option α → α → α
getD {}: ?m.17066
{}
  let prot: ?m.17111
prot := vis: ?m.15914 x✝²
vis.filter: {α : Type ?u.17112} → (α → Bool) → Option α → Option α
filter (· matches `(Parser.Command.visibility: Parser.Parser
Parser.Command.visibility| protected))
  let priv: ?m.17272
priv := vis: ?m.15914 x✝²
vis.filter: {α : Type ?u.17273} → (α → Bool) → Option α → Option α
filter (· matches `(Parser.Command.visibility: Parser.Parser
Parser.Command.visibility| private))
  elabCommand: Syntax → CommandElabM Unit
elabCommand <|<- `(stop_at_first_error
    $[$nc: ?m.16209 x✝¹
nc:noncomputable: Parser.Parser
noncomputable]? $[$uns: TSyntax `Lean.Parser.Command.unsafe
uns]? def definition$[.{$us: Option (Syntax.TSepArray `ident ",")
us,*}]? $declSig: ?m.13449
declSig:optDeclSig: Parser.Parser
optDeclSig $val: ?m.13440
val
    $[$nc: ?m.16209 x✝¹
nc:noncomputable: Parser.Parser
noncomputable]? $[$uns: TSyntax `Lean.Parser.Command.unsafe
uns]? opaque wrapped$[.{$us: Option (Syntax.TSepArray `ident ",")
us,*}]? : Subtype (Eq @definition.{$us': ?m.14406
us',*}) :=
      ⟨_, rfl⟩
    $[$doc: ?m.14888 x✝⁴
doc:docComment: Parser.Parser
docComment]? $[private%$priv: ?m.17272
priv]? $[$nc: TSyntax `Lean.Parser.Command.noncomputable
nc:noncomputable: Parser.Parser
noncomputable]? $[$uns: ?m.16640 x✝
uns]?
    def $n: TSyntax `ident
n:ident$[.{$us: Option (Syntax.TSepArray `ident ",")
us,*}]? :=
      val_proj @wrapped.{$us': ?m.14406
us',*}
    $[private%$priv: Syntax
priv]? $[$uns: TSyntax `Lean.Parser.Command.unsafe
uns:unsafe: Parser.Parser
unsafe]? theorem $n_def: ?m.14421
n_def:ident $[.{$us: Option (Syntax.TSepArray `ident ",")
us,*}]? :
        eta_helper Eq @$n: TSyntax `ident
n.{$us': ?m.14406
us',*} @(delta% @definition) := by
      intros
      delta $n: TSyntax `ident
n:ident
      rw [show wrapped = ⟨@definition.{$us': ?m.14406
us',*}, rfl⟩ from Subtype.ext wrapped.2.symm]
      rfl
    attribute [irreducible] $n: TSyntax `ident
n definition
    attribute [eqns $n_def: ?m.14421
n_def] $n: TSyntax `ident
n
    attribute [$attrs: ?m.17059
attrs:attrInstance,*] $n: TSyntax `ident
n)
  if prot: ?m.17111
prot.isSome: {α : Type ?u.19979} → Option α → Bool
isSome then
    modifyEnv: {m : Type → Type} → [self : MonadEnv m] → (Environment → Environment) → m Unit
modifyEnv (addProtected: Environment → Name → Environment
addProtected · ((← getCurrNamespace: {m : Type → Type} → [self : MonadResolveName m] → m Name
getCurrNamespace) ++ n: TSyntax `ident
n.getId: Ident → Name
getId))