From fb175ccab73a8019371db0bad66722963426d65f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Dec 2020 16:08:50 -0800
Subject: [PATCH] feat: add `Deriving.lean`

---
 src/Lean/Elab.lean                |  1 +
 src/Lean/Elab/Deriving.lean       |  6 ++++++
 src/Lean/Elab/Deriving/Basic.lean | 35 +++++++++++++++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 src/Lean/Elab/Deriving.lean
 create mode 100644 src/Lean/Elab/Deriving/Basic.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index f53a128296..537b9c061b 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -25,3 +25,4 @@ import Lean.Elab.Structure
 import Lean.Elab.Print
 import Lean.Elab.MutualDef
 import Lean.Elab.PreDefinition
+import Lean.Elab.Deriving
diff --git a/src/Lean/Elab/Deriving.lean b/src/Lean/Elab/Deriving.lean
new file mode 100644
index 0000000000..79cfa2577c
--- /dev/null
+++ b/src/Lean/Elab/Deriving.lean
@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Deriving.Basic
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
new file mode 100644
index 0000000000..1b30af33c7
--- /dev/null
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Command
+
+namespace Lean
+namespace Elab
+open Command
+
+def DerivingHandler := (typeNames : List Name) → CommandElabM Bool
+
+builtin_initialize derivingHandlersRef : IO.Ref (NameMap DerivingHandler) ← IO.mkRef {}
+
+def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
+  let initializing ← IO.initializing
+  unless initializing do
+    throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
+  if (← derivingHandlersRef.get).contains className then
+    throw (IO.userError s!"failed to register deriving handler, a handler has already been registered for '{className}'")
+  derivingHandlersRef.modify fun m => m.insert className handler
+
+def defaultHandler (className : Name) (typeNames : List Name) : CommandElabM Unit := do
+  throwError! "default handlers have not been implemented yet"
+
+def applyDerivingHandlers (className : Name) (typeNames : List Name) : CommandElabM Unit := do
+  match (← derivingHandlersRef.get).find? className with
+  | some handler =>
+    unless (← handler typeNames) do
+      defaultHandler className typeNames
+  | none => defaultHandler className typeNames
+
+end Elab
+end Lean