From 2ce2610c0a57d007fe3d77c43d3e7eac2c0d576b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Jan 2020 16:38:41 -0800
Subject: [PATCH] feat: add `compileDecl`

cc @kha
---
 src/Init/Lean/Elab/Command.lean    | 13 +++++++++----
 src/Init/Lean/Elab/Definition.lean |  2 +-
 tests/lean/run/frontend1.lean      |  4 ++++
 3 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 11cbe785e3..d7a0d6112c 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -561,10 +561,15 @@ result ++ remaining.toList
 def addDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
 env ← getEnv;
 match env.addDecl decl with
-| Except.ok    env => modify $ fun s => { env := env, .. s }
-| Except.error kex => do
-  opts ← getOptions;
-  throwError ref (kex.toMessageData opts)
+| Except.ok    env => setEnv env
+| Except.error kex => do opts ← getOptions; throwError ref (kex.toMessageData opts)
+
+def compileDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
+env  ← getEnv;
+opts ← getOptions;
+match env.compileDecl opts decl with
+| Except.ok env    => setEnv env
+| Except.error kex => throwError ref (kex.toMessageData opts)
 
 end Command
 end Elab
diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index b396238c27..fab75a1d68 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -150,7 +150,7 @@ withDeclId view.declId $ fun name => do
   | some decl => do
     addDecl ref decl;
     applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
-    -- TODO invoke compiler
+    compileDecl ref decl;
     applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
 
 end Command
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 5c5bee312e..7ee169cfd6 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -215,3 +215,7 @@ def three := 3
 #eval run "#check g (y := three)"
 #eval run "#check g (z := three)"
 #eval run "#check g three (z := zero)"
+
+#eval run "open Lean.Parser
+@[termParser] def myParser : Lean.Parser.Parser Lean.ParserKind.leading := parser! coe \"hi\"
+#check myParser"