From d0062691de9ff628f26d634a0a9ea97c4ee73a64 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Jan 2019 15:06:51 +0100
Subject: [PATCH] feat(library/init/lean): implement `init_quot`

---
 library/init/lean/elaborator.lean     | 6 +++++-
 library/init/lean/parser/command.lean | 6 +++++-
 src/frontends/lean/vm_elaborator.cpp  | 3 +++
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 359c205eb1..613869324e 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -750,6 +750,9 @@ def export.elaborate : elaborator :=
   -- TODO: do eager sanity checks (namespace does not exist, etc.)
   modify $ λ st, {st with export_decls := st.export_decls ++ v.spec.map (λ spec, ⟨ns, spec⟩)}
 
+def init_quot.elaborate : elaborator :=
+λ stx, old_elab_command stx $ expr.mdata (kvmap.set_name {} `command `init_quot) dummy
+
 /-- List of commands: recursively elaborate each command. -/
 def no_kind.elaborate : coelaborator := do
   stx ← current_command,
@@ -821,7 +824,8 @@ def elaborators : rbmap name coelaborator (<) := rbmap.from_list [
   (attribute.name, attribute.elaborate),
   (open.name, open.elaborate),
   (export.name, export.elaborate),
-  (check.name, check.elaborate)
+  (check.name, check.elaborate),
+  (init_quot.name, init_quot.elaborate)
 ] _
 
 def resolve_global : name → elaborator_m (list name)
diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index 65bcfa8d19..d954f6ee26 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -93,12 +93,16 @@ node! «attribute» [
   ids: ident.parser*
 ]
 
+@[derive parser.has_tokens parser.has_view]
+def init_quot.parser : command_parser :=
+node! «init_quot» ["init_quot"]
+
 @[derive has_tokens]
 def builtin_command_parsers : list command_parser := [
   declaration.parser, variable.parser, variables.parser, namespace.parser, end.parser,
   open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser,
   mixfix.parser, reserve_mixfix.parser, check.parser, attribute.parser,
-  export.parser, include.parser, omit.parser]
+  export.parser, include.parser, omit.parser, init_quot.parser]
 end «command»
 
 def command_parser.run (commands : list command_parser) (p : command_parser)
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index c838a9a286..9d8cfe31b5 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -318,6 +318,9 @@ static void elaborate_command(parser & p, expr const & cmd) {
         } else if (*cmd_name == "structure") {
             elab_structure_cmd(p, cmd);
             return;
+        } else if (*cmd_name == "init_quot") {
+            p.set_env(module::add(p.env(), mk_quot_decl()));
+            return;
         }
     }
     throw elaborator_exception(cmd, "unexpected input to 'elaborate_command'");