From 64b7b857f13ea5fd59f6fd5490582f53ff7e676b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Jul 2022 07:38:47 -0400
Subject: [PATCH] chore: ICERM attribute demo

---
 tests/pkg/user_attr/UserAttr/BlaAttr.lean | 15 ++++++++
 tests/pkg/user_attr/UserAttr/Tst.lean     | 43 ++++++++++++++++++-----
 2 files changed, 50 insertions(+), 8 deletions(-)

diff --git a/tests/pkg/user_attr/UserAttr/BlaAttr.lean b/tests/pkg/user_attr/UserAttr/BlaAttr.lean
index e6d9b1df4d..d4a57f5a60 100644
--- a/tests/pkg/user_attr/UserAttr/BlaAttr.lean
+++ b/tests/pkg/user_attr/UserAttr/BlaAttr.lean
@@ -5,3 +5,18 @@ open Lean
 initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"
 
 register_simp_attr my_simp "my own simp attribute"
+
+syntax (name := foo) "foo" num "important"? : attr
+
+initialize fooAttr : ParametricAttribute (Nat × Bool) ←
+  registerParametricAttribute {
+    name := `foo
+    descr := "parametric attribute containing a priority and flag"
+    getParam := fun _ stx =>
+      match stx with
+      | `(attr| foo $prio:num $[important%$imp]?) => 
+        return (prio.getNat, imp.isSome)
+      | _  => throwError "unexpected foo attribute" 
+    afterSet := fun declName _ => do
+      IO.println s!"set attribute [foo] at {declName}"
+  }
diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean
index 1a08e5f333..cb8ce3849c 100644
--- a/tests/pkg/user_attr/UserAttr/Tst.lean
+++ b/tests/pkg/user_attr/UserAttr/Tst.lean
@@ -4,6 +4,24 @@ import UserAttr.BlaAttr
 @[bla] def f (x : Nat) := x + 2
 @[bla] 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
+def hasBlaAttr (declName : Name) : CoreM Bool :=
+  return blaAttr.hasTag (← getEnv) declName
+
+#eval hasBlaAttr ``f
+#eval hasBlaAttr ``id
+
+open Lean in
+def getFooAttrInfo? (declName : Name) : CoreM (Option (Nat × Bool)) := 
+  return fooAttr.getParam (← getEnv) declName
+
+#eval getFooAttrInfo? ``f
+#eval getFooAttrInfo? ``h1
+#eval getFooAttrInfo? ``h2
+
 @[my_simp] theorem f_eq : f x = x + 2 := rfl
 @[my_simp] theorem g_eq : g x = x + 1 := rfl
 
@@ -23,13 +41,12 @@ macro "my_simp" : tactic => `(simp [my_simp])
 example : f x = id (x + 2) := by
   my_simp
 
-
 @[simp low, my_simp low]
-theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry
+axiom expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y
 @[simp high, my_simp high]
-theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry
+axiom expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z 
 @[simp, my_simp]
-theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry
+axiom lassoc_add (x y z : Nat) : x + (y + z) = x + y + z
 
 set_option trace.Meta.Tactic.simp.rewrite true
 
@@ -39,12 +56,22 @@ theorem ex1 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by
 -- 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
-open Lean.Meta
+open Lean Meta in
 def checkProofs : MetaM Unit := do
-  let ConstantInfo.thmInfo info1 ← getConstInfo `ex1 | throwError "unexpected"
-  let ConstantInfo.thmInfo info2 ← getConstInfo `ex2 | throwError "unexpected"
+  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 lemmaName => acc.push lemmaName
+  for thmName in thmNames do
+    IO.println thmName
+
+#eval showThmsOf `my_simp