From baadfca817ad38fb1f29c5fc561ffdbd76696e66 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 13 Aug 2020 17:39:43 +0200
Subject: [PATCH] fix: commit missing file...

---
 src/Lean/ParserCompiler.lean | 51 ++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 src/Lean/ParserCompiler.lean

diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
new file mode 100644
index 0000000000..4bbf24e57a
--- /dev/null
+++ b/src/Lean/ParserCompiler.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+import Lean.Attributes
+import Lean.Compiler.InitAttr
+import Lean.ToExpr
+import Lean.Meta.Message
+
+/-!
+Gadgets for compiling parser declarations into other programs, such as pretty printers.
+-/
+
+namespace Lean
+
+structure CombinatorCompilerAttribute :=
+(attr : AttributeImpl)
+(ext  : SimplePersistentEnvExtension (Name × Name) (NameMap Name))
+
+-- TODO(Sebastian): We'll probably want priority support here at some point
+
+def registerCombinatorCompilerAttribute (name : Name) (descr : String)
+    : IO CombinatorCompilerAttribute := do
+ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name) ← registerSimplePersistentEnvExtension {
+  name            := name,
+  addImportedFn   := mkStateFromImportedEntries (fun s p => s.insert p.1 p.2) {},
+  addEntryFn      := fun (s : NameMap Name) (p : Name × Name) => s.insert p.1 p.2,
+};
+let attrImpl : AttributeImpl := {
+  name  := name,
+  descr := descr,
+  add   := fun env decl args _ => match attrParamSyntaxToIdentifier args with
+    | some parserDecl => pure $ ext.addEntry env (parserDecl, decl)
+    | none            => throw $ IO.userError "invalid attribute argument, expected identifier"
+};
+registerBuiltinAttribute attrImpl;
+pure { attr := attrImpl, ext := ext }
+
+namespace CombinatorCompilerAttribute
+
+instance : Inhabited CombinatorCompilerAttribute := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
+
+def getDeclFor (attr : CombinatorCompilerAttribute) (env : Environment) (parserDecl : Name) : Option Name :=
+(attr.ext.getState env).find? parserDecl
+
+def setDeclFor (attr : CombinatorCompilerAttribute) (env : Environment) (parserDecl : Name) (decl : Name) : Environment :=
+attr.ext.addEntry env (parserDecl, decl)
+
+end CombinatorCompilerAttribute
+end Lean