From 793d493df0e1b540c1608f2bdda8cbbbb07941ce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Sep 2021 13:45:28 -0700
Subject: [PATCH] feat: equation theorem manager

---
 src/Lean/Meta.lean      |  1 +
 src/Lean/Meta/Eqns.lean | 90 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 91 insertions(+)
 create mode 100644 src/Lean/Meta/Eqns.lean

diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean
index db84e59679..b45a98a1a6 100644
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -38,3 +38,4 @@ import Lean.Meta.Injective
 import Lean.Meta.Structure
 import Lean.Meta.Constructions
 import Lean.Meta.CongrTheorems
+import Lean.Meta.Eqns
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
new file mode 100644
index 0000000000..875bb7e00e
--- /dev/null
+++ b/src/Lean/Meta/Eqns.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+
+def GetEqnsFn := Name → MetaM (Option (Array Name))
+
+private builtin_initialize getEqnsFnsRef : IO.Ref (List GetEqnsFn) ← IO.mkRef []
+
+/--
+  Register a new function for retrieving equation theorems.
+  We generate equations theorems on demand, and they are generated by more than one module.
+  For example, the structural and well-founded recursion modules generate them.
+  Most recent getters are tried first.
+
+  A getter returns an `Option (Array Name)`. The result is `none` if the getter failed.
+  Otherwise, it is a sequence of theorem names where each one of them corresponds to
+  an alternative. Example: the definition
+
+  ```
+  def f (xs : List Nat) : List Nat :=
+    match xs with
+    | [] => []
+    | x::xs => (x+1)::f xs
+  ```
+  should have two equational theorems associated with it
+  ```
+  f [] = []
+  ```
+  and
+  ```
+  (x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
+  ```
+-/
+def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
+  getEqnsFnsRef.modify (f :: ·)
+
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  for f in (← getEqnsFnsRef.get) do
+    if let some r ← f declName then
+      return some r
+  return none
+
+def GetUnfoldEqnFn := Name → MetaM (Option Name)
+
+private builtin_initialize getUnfoldEqnFnsRef : IO.Ref (List GetUnfoldEqnFn) ← IO.mkRef []
+
+/--
+  Register a new function for retrieving a "unfold" equation theorem.
+
+  We generate this kind of equation theorem on demand, and it is generated by more than one module.
+  For example, the structural and well-founded recursion modules generate it.
+  Most recent getters are tried first.
+
+  A getter returns an `Option Name`. The result is `none` if the getter failed.
+  Otherwise, it is a theorem name. Example: the definition
+
+  ```
+  def f (xs : List Nat) : List Nat :=
+    match xs with
+    | [] => []
+    | x::xs => (x+1)::f xs
+  ```
+  should have the theorem
+  ```
+  (xs : Nat) →
+    f xs =
+      match xs with
+      | [] => []
+      | x::xs => (x+1)::f xs
+  ```
+-/
+def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
+  getUnfoldEqnFnsRef.modify (f :: ·)
+
+def getUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
+  for f in (← getUnfoldEqnFnsRef.get) do
+    if let some r ← f declName then
+      return some r
+  return none
+
+end Lean.Meta