From 1ad5b5984a8ed066db0791eae496e664e3460b33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jun 2020 12:44:13 -0700
Subject: [PATCH] feat: add `Inductive.lean`

---
 src/Lean/Elab.lean             |  1 +
 src/Lean/Elab/Declaration.lean | 14 +++++++++++--
 src/Lean/Elab/Inductive.lean   | 38 ++++++++++++++++++++++++++++++++++
 3 files changed, 51 insertions(+), 2 deletions(-)
 create mode 100644 src/Lean/Elab/Inductive.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 9107c285ec..07e3eda9b5 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -19,3 +19,4 @@ import Lean.Elab.Syntax
 import Lean.Elab.Match
 import Lean.Elab.DoNotation
 import Lean.Elab.StructInst
+import Lean.Elab.Inductive
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 1ff8d6cb5e..51cf60c91b 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Util.CollectLevelParams
 import Lean.Elab.Definition
+import Lean.Elab.Inductive
 
 namespace Lean
 namespace Elab
@@ -116,11 +117,20 @@ withDeclId declId $ fun name => do
   applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
   applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
+/-
+parser! "inductive " >> declId >> optDeclSig >> many introRule
+-/
 def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
-pure () -- TODO
+let (binders, type?) := expandOptDeclSig (stx.getArg 2);
+elabInductiveCore stx modifiers (stx.getArg 1) binders type? (stx.getArg 3).getArgs
 
+/-
+parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many introRule
+-/
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
-pure () -- TODO
+let (binders, type?) := expandOptDeclSig (stx.getArg 3);
+let modifiers        := modifiers.addAttribute { name := `class };
+elabInductiveCore stx modifiers (stx.getArg 2) binders type? (stx.getArg 4).getArgs
 
 def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
 pure () -- TODO
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
new file mode 100644
index 0000000000..9484b9e7be
--- /dev/null
+++ b/src/Lean/Elab/Inductive.lean
@@ -0,0 +1,38 @@
+/-
+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
+import Lean.Elab.Definition
+
+namespace Lean
+namespace Elab
+namespace Command
+
+def mkInductive (ref : Syntax) (declName : Name) (explictLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (intros : Array Syntax)
+    : TermElabM Declaration := do
+Term.throwError ref ref
+
+def elabInductiveCore
+    (ref           : Syntax)
+    (modifiers     : Modifiers)
+    (declId        : Syntax)
+    (binders       : Syntax)
+    (type?         : Option Syntax)
+    (introRules    : Array Syntax) : CommandElabM Unit := do
+withDeclId declId $ fun name => do
+  declName          ← mkDeclName modifiers name;
+  checkNotAlreadyDeclared ref declName;
+  applyAttributes ref declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
+  explictLevelNames ← getLevelNames;
+  decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
+    -- TODO
+    pure ()
+  };
+
+  throwError ref (ref ++ "\n" ++ toString explictLevelNames)
+
+end Command
+end Elab
+end Lean