feat: add Inductive.lean

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

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

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