module

public import UserAttr.BlaAttr
meta import Lean
import all Lean.ExtraModUses

public section

-- Like in extraModUses.lean, but there we do not have registered custom attributes
meta def resetExtraModUses : Lean.CoreM Unit := do
  Lean.modifyEnv (Lean.PersistentEnvExtension.setState Lean.extraModUses · ⟨[], ∅⟩)
  Lean.modifyEnv (Lean.PersistentEnvExtension.setState Lean.isExtraRevModUseExt · ⟨[], ()⟩)

attribute [-simp] Nat.add_left_cancel_iff Nat.add_right_cancel_iff

@[bla, expose] def f (x : Nat) := x + 2
@[bla, expose] def g (x : Nat) := x + 1

@[foo 10] def h1 (x : Nat) := 2*x + 1
@[foo 20 important] def h2 (x : Nat) := 2*x + 1

open Lean in
meta def hasBlaAttr (declName : Name) : CoreM Bool :=
  return blaAttr.hasTag (← getEnv) declName

#eval hasBlaAttr ``f
#eval hasBlaAttr ``id

open Lean in
meta def getFooAttrInfo? (declName : Name) : CoreM (Option (Nat × Bool)) :=
  return fooAttr.getParam? (← getEnv) declName

#eval getFooAttrInfo? ``f
#eval getFooAttrInfo? ``h1
#eval getFooAttrInfo? ``h2

#eval resetExtraModUses
/--
trace: [extraModUses] recording private regular extra mod use UserAttr.BlaAttr of ext
-/
#guard_msgs (substring := true) in
set_option trace.extraModUses true in
@[my_simp] theorem f_eq : f x = x + 2 := rfl
@[my_simp] theorem g_eq : g x = x + 1 := rfl

example : f x + g x = 2*x + 3 := by
  fail_if_success simp +arith -- does not apply f_eq and g_eq
  simp +arith [f, g]

#eval resetExtraModUses
/--
trace: [extraModUses] recording private regular extra mod use UserAttr.BlaAttr of ext
-/
#guard_msgs (substring := true) in
set_option trace.extraModUses true in
example : f x + g x = 2*x + 3 := by
  simp +arith [my_simp]

example : f x = id (x + 2) := by
  simp
  simp [my_simp]

macro "my_simp" : tactic => `(tactic| simp [my_simp])

example : f x = id (x + 2) := by
  my_simp

@[simp low, my_simp low]
axiom expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y
@[simp high, my_simp high]
axiom expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z
@[simp, my_simp]
axiom lassoc_add (x y z : Nat) : x + (y + z) = x + y + z

set_option trace.Meta.Tactic.simp.rewrite true

-- Rewrites: expand_mul_add -> expand_mul_add -> lassoc_add
theorem ex1 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by simp only [my_simp]

-- Rewrites: expand_add_mul -> expand_mul_add -> lassoc_add
theorem ex2 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by simp

open Lean Meta in
def checkProofs : MetaM Unit := do
  let .thmInfo info1 ← getConstInfo `ex1 | throwError "unexpected"
  let .thmInfo info2 ← getConstInfo `ex2 | throwError "unexpected"
  unless info1.value == info2.value do
    throwError "unexpected values"

#eval checkProofs

open Lean Meta in
def showThmsOf (simpAttrName : Name) : MetaM Unit := do
  let some simpExt ← getSimpExtension? simpAttrName
    | throwError "`{simpAttrName}` is not a simp attribute"
  let thms ← simpExt.getTheorems
  let thmNames := thms.lemmaNames.fold (init := #[]) fun acc origin => acc.push origin.key
  for thmName in thmNames do
    IO.println thmName

#eval showThmsOf `my_simp

def boo (x : Nat) : Nat :=
  x + 10

open Lean Meta in
simproc [my_simp] reduceBoo (boo _) := fun e => do
  unless e.isAppOfArity ``boo 1 do return .continue
  let some n ← Nat.fromExpr? e.appArg! | return .continue
  return .done { expr := mkNatLit (n+10) }

example : f x + boo 2 = id (x + 2) + 12 := by
  simp
  simp [my_simp] -- Applies the simp and simproc sets


namespace TraceAdd

set_option trace.Meta.Tactic.simp.rewrite false

/-- info: trace_add attribute added to TraceAdd.foo -/
#guard_msgs in
@[trace_add] def foo := 1

/-- info: trace_add attribute added to TraceAdd.foo -/
#guard_msgs in
attribute [trace_add] foo

/-- info: trace_add attribute added to TraceAdd.structural -/
#guard_msgs in
@[trace_add] def structural : Nat → Nat
  | 0 => 0
  | n+1 => structural n+1
termination_by structural n => n

/-- info: trace_add attribute added to TraceAdd.wf -/
#guard_msgs in
@[trace_add] def wf : Nat → Nat
  | 0 => 0
  | n+1 => wf n+1
termination_by n => n

/--
info: trace_add attribute added to TraceAdd.mutual_structural_1
---
info: trace_add attribute added to TraceAdd.mutual_structural_2
-/
#guard_msgs in
mutual
@[trace_add] def mutual_structural_1 : Nat → Nat
  | 0 => 0
  | n+1 => mutual_structural_2 n+1
termination_by structural n => n
@[trace_add] def mutual_structural_2 : Nat → Nat
  | 0 => 0
  | n+1 => mutual_structural_1 n+1
termination_by structural n => n
end

/--
info: trace_add attribute added to TraceAdd.mutual_wf_1._mutual
---
info: trace_add attribute added to TraceAdd.mutual_wf_1
---
info: trace_add attribute added to TraceAdd.mutual_wf_2
-/
#guard_msgs in
mutual
@[trace_add] def mutual_wf_1 : Nat → Nat
  | 0 => 0
  | n+1 => mutual_wf_2 n+1
termination_by n => n
@[trace_add] def mutual_wf_2 : Nat → Nat
  | 0 => 0
  | n+1 => mutual_wf_1 n+1
termination_by n => n
end

end TraceAdd

namespace GrindAttr

opaque f : Nat → Nat
opaque g : Nat → Nat
opaque foo : Nat → Nat → Nat
opaque boo : Nat → Nat → Nat

@[my_grind] theorem fax : f (f x) = f x := sorry

@[my_grind =] theorem fax2 : f (f (f x)) = f x := by
  fail_if_success grind
  grind [my_grind]

@[my_grind? .] theorem fg : g (f x) = x := sorry

@[my_grind? =] theorem fax3 : f (f (f x)) = f x := sorry

@[my_grind!? .] theorem fax4 : f (f (f x)) = f x := sorry

theorem fooAx : foo x (f x) = x := sorry

grind_pattern fooAx => foo x (f x)

example : foo x (f (f x)) = x := by
  fail_if_success grind only [my_grind]
  grind only [my_grind, usr fooAx]

grind_pattern [my_grind] fooAx => foo x (f x)

#eval resetExtraModUses
/--
[extraModUses] recording private regular extra mod use UserAttr.BlaAttr of ext
-/
#guard_msgs (substring := true) in
set_option trace.extraModUses true in
example : foo x (f (f x)) = x := by
  grind only [my_grind]

theorem booAx : boo (f x) (f x) = x := sorry

grind_pattern [my_grind] booAx => boo (f x) (f x)

example : boo (f (f (f x))) (f (f x)) = x := by
  grind only [my_grind]


end GrindAttr


namespace Issue13433
/-!
Attributes with `beforeElaboration` were not being applied to `inductive` or `structure` commands
-/

/--
info: declaration `Issue13433.A` tagged `myattr_beforeElaboration`, not in environment
---
info: declaration `Issue13433.A` tagged `myattr_afterTypeChecking`, already in environment
---
info: declaration `Issue13433.A` tagged `myattr_afterCompilation`, already in environment
-/
#guard_msgs in
@[myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation]
structure A where
/--
info: declaration `Issue13433.A` tagged `myattr_beforeElaboration`, already in environment
---
info: declaration `Issue13433.A` tagged `myattr_afterTypeChecking`, already in environment
---
info: declaration `Issue13433.A` tagged `myattr_afterCompilation`, already in environment
-/
#guard_msgs in attribute [myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] A

/--
info: declaration `Issue13433.B` tagged `myattr_beforeElaboration`, not in environment
---
info: declaration `Issue13433.B` tagged `myattr_afterTypeChecking`, already in environment
---
info: declaration `Issue13433.B` tagged `myattr_afterCompilation`, already in environment
-/
#guard_msgs in
@[myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation]
inductive B where
/--
info: declaration `Issue13433.B` tagged `myattr_beforeElaboration`, already in environment
---
info: declaration `Issue13433.B` tagged `myattr_afterTypeChecking`, already in environment
---
info: declaration `Issue13433.B` tagged `myattr_afterCompilation`, already in environment
-/
#guard_msgs in attribute [myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] B

/--
info: declaration `Issue13433.C` tagged `myattr_beforeElaboration`, not in environment
---
info: declaration `Issue13433.C` tagged `myattr_afterTypeChecking`, already in environment
---
info: declaration `Issue13433.C` tagged `myattr_afterCompilation`, already in environment
-/
#guard_msgs in
@[myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation]
coinductive C : Prop where
/--
info: declaration `Issue13433.C` tagged `myattr_beforeElaboration`, already in environment
---
info: declaration `Issue13433.C` tagged `myattr_afterTypeChecking`, already in environment
---
info: declaration `Issue13433.C` tagged `myattr_afterCompilation`, already in environment
-/
#guard_msgs in attribute [myattr_beforeElaboration, myattr_afterTypeChecking, myattr_afterCompilation] C

end Issue13433