fix(library/init/lean/parser/parser): new registerBuiltinParserAttribute

It is still broken since we apply attributes before we compile code.

Recall that attributes such as `@[export]` and `@[extern]` must be applied before we
compile code.

On the other hand, any attribute `attrName`
```
@[attrName] def foo := ...
```
which creates auxiliary definitions that depend on `foo` must be applied
AFTER we generate code for `foo`. Otherwise, we will fail to compile the
auxiliary definition since we don't have code for `foo` yet.

I will fix the issue above by allowing attributes to specify when they
should be applied. I will start with only two options: before and after
code compilation. In the future, we may need more options (e.g., before
elaboration), but I don't see the need yet.

cc @kha

library/init/io.lean

@@ -61,12 +61,12 @@ constant IO.initializing : IO Bool := default _
 
 abbrev monadIO (m : Type → Type) := HasMonadLiftT IO m
 
-def ioOfExcept {ε α : Type} [HasToString ε] (e : Except ε α) : IO α :=
+namespace IO
+
+def ofExcept {ε α : Type} [HasToString ε] (e : Except ε α) : IO α :=
 match e with
 | Except.ok a    := pure a
-| Except.error e := throw $ toString e
+| Except.error e := throw (IO.userError (toString e))
-
-namespace IO
 
 def lazyPure {α : Type} (fn : Unit → α) : IO α :=
 pure (fn ())

library/init/lean/compiler/initattr.lean

@@ -60,4 +60,7 @@ match initAttr.getParam env fn with
 def hasInitAttr (env : Environment) (fn : Name) : Bool :=
 (getInitFnNameFor env fn).isSome
 
+def setInitAttr (env : Environment) (declName : Name) (initFnName : Name := Name.anonymous) : Except String Environment :=
+initAttr.setParam env declName initFnName
+
 end Lean

library/init/lean/expr.lean

@@ -68,13 +68,13 @@ attribute [extern "lean_expr_mk_lit"]    Expr.lit
 attribute [extern "lean_expr_mk_mdata"]  Expr.mdata
 attribute [extern "lean_expr_mk_proj"]   Expr.proj
 
-namespace Expr
 def mkApp (fn : Expr) (args : List Expr) : Expr :=
 args.foldl Expr.app fn
 
-def mkCapp (fn : Name) (args : List Expr) : Expr :=
+def mkCApp (fn : Name) (args : List Expr) : Expr :=
 mkApp (Expr.const fn []) args
 
+namespace Expr
 @[extern "lean_expr_hash"]
 constant hash (n : @& Expr) : USize := default USize
 
@@ -96,6 +96,9 @@ instance : HasBeq Expr := ⟨Expr.eqv⟩
 
 end Expr
 
+def mkConst (n : Name) (ls : List Level := []) : Expr :=
+Expr.const n ls
+
 def getAppFn : Expr → Expr
 | (Expr.app f a) := getAppFn f
 | e              := e
@@ -103,6 +106,9 @@ def getAppFn : Expr → Expr
 def mkBinApp (f a b : Expr) :=
 Expr.app (Expr.app f a) b
 
+def mkBinCApp (f : Name) (a b : Expr) :=
+mkBinApp (mkConst f) a b
+
 def mkDecIsTrue (pred proof : Expr) :=
 mkBinApp (Expr.const `Decidable.isTrue []) pred proof
 

library/init/lean/parser/parser.lean

@@ -6,11 +6,13 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import init.lean.position
 import init.lean.syntax
+import init.lean.toexpr
 import init.lean.environment
 import init.lean.attributes
 import init.lean.evalconst
 import init.lean.parser.trie
 import init.lean.parser.identifier
+import init.lean.compiler.initattr
 
 namespace Lean
 namespace Parser
@@ -861,10 +863,10 @@ instance {α : Type} : HasEmptyc (TokenMap α) := ⟨RBMap.empty⟩
 end TokenMap
 
 structure ParsingTables :=
-(nudTable   : TokenMap Parser := {})
+(leadingTable    : TokenMap Parser := {})
-(ledTable   : TokenMap TrailingParser := {})
+(trailingTable   : TokenMap TrailingParser := {})
-(ledParsers : List TrailingParser := []) -- for supporting parsers such as function application
+(trailingParsers : List TrailingParser := []) -- for supporting parsers such as function application
-(tokens     : Trie TokenConfig := {})
+(tokens          : Trie TokenConfig := {})
 
 def currLbp (c : ParserContext) (s : ParserState) : ParserState × Nat :=
 let (s, stx) := peekToken c s in
@@ -894,15 +896,15 @@ else s.mkNode nullKind iniSz -- throw error instead?
 def leadingParser (tables : ParsingTables) : ParserFn nud :=
 λ a c s,
   let iniSz   := s.stackSize in
-  let (s, ps) := indexed tables.nudTable c s in
+  let (s, ps) := indexed tables.leadingTable c s in
   let s       := longestMatchFn ps a c s in
   mkResult s iniSz
 
 def trailingParser (tables : ParsingTables) : ParserFn led :=
 λ a c s,
   let iniSz   := s.stackSize in
-  let (s, ps) := indexed tables.ledTable c s in
+  let (s, ps) := indexed tables.trailingTable c s in
-  let s       := orelseFn (longestMatchFn ps) (anyOfFn tables.ledParsers) a c s in
+  let s       := orelseFn (longestMatchFn ps) (anyOfFn tables.trailingParsers) a c s in
   mkResult s iniSz
 
 partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext) : Syntax → ParserState → ParserState
@@ -942,140 +944,93 @@ if s.hasError then
 else
   Except.ok s.stxStack.back
 
-structure BuiltinParserAttribute :=
+def mkBultinParsingTablesRef : IO (IO.Ref ParsingTables) :=
-(tables     : IO.Ref (Option ParsingTables))
+IO.mkRef {}
-(ledParsers : IO.Ref (List Name))
-(nudParsers : IO.Ref (List Name))
-(attr       : AttributeImpl)
-
-namespace BuiltinParserAttribute
-
-instance : Inhabited BuiltinParserAttribute :=
-⟨{ tables := default _, attr := default _, ledParsers := default _, nudParsers := default _ }⟩
 
 private def updateTokens (tables : ParsingTables) (info : ParserInfo) : IO ParsingTables :=
 match info.updateTokens tables.tokens with
 | Except.ok newTokens := pure { tokens := newTokens, .. tables }
 | Except.error msg    := throw (IO.userError msg)
 
-unsafe def getTablesUnsafe (attr : BuiltinParserAttribute) : IO ParsingTables :=
+def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit :=
-do tables ← attr.tables.get,
-   match tables with
-   | some tables := pure tables
-   | none := do
-     ledParsers ← attr.ledParsers.get,
-     nudParsers ← attr.nudParsers.get,
-     let ledParsers := ledParsers.reverse,
-     let nudParsers := nudParsers.reverse,
-     let tables : ParsingTables := {},
-     tables ← nudParsers.mfoldl
-       (λ tables declName, do
-         p ← evalConst Parser declName,
-         tables ← updateTokens tables p.info,
-         match p.info.firstTokens with
-         | FirstTokens.tokens tks := pure $ tks.foldl (λ tables tk, { nudTable := tables.nudTable.insert tk.val p, .. tables }) tables
-         | _                      := throw (IO.userError ("invalid parser '" ++ toString declName ++ "', initial token is not statically known")))
-       tables,
-     ledParsers.mfoldl
-       (λ tables declName, do
-         p ← evalConst TrailingParser declName,
-         tables ← updateTokens tables p.info,
-         match p.info.firstTokens with
-         | FirstTokens.tokens tks := pure $ tks.foldl (λ tables tk, { ledTable := tables.ledTable.insert tk.val p, .. tables }) tables
-         | _                      := pure $ { ledParsers := p :: tables.ledParsers, .. tables })
-       tables
-
-@[implementedBy getTablesUnsafe]
-constant getTables (attr : BuiltinParserAttribute) : IO ParsingTables := default _
-
-def runParser (attr : BuiltinParserAttribute) (env : Environment) (input : String) (fileName := "<input>") : IO Syntax :=
-do tables ← attr.getTables,
-   match runParser env tables input fileName with
-   | Except.error err := throw (IO.userError err)
-   | Except.ok stx    := pure stx
-
-end BuiltinParserAttribute
-
-private def throwUnexpectedParserType (declName : Name) : IO Unit :=
-throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
-
-private def updateTokens (info : ParserInfo) (tablesRef : IO.Ref ParsingTables) : IO Unit :=
 do tables ← tablesRef.get,
    tablesRef.reset,
-   match info.updateTokens tables.tokens with
+   tables ← updateTokens tables p.info,
-   | Except.ok newTokens := tablesRef.set { tokens := newTokens, .. tables }
+   match p.info.firstTokens with
-   | Except.error msg    := throw (IO.userError msg)
+   | FirstTokens.tokens tks :=
+     let tables := tks.foldl (λ (tables : ParsingTables) tk, { leadingTable := tables.leadingTable.insert tk.val p, .. tables }) tables in
+     tablesRef.set tables
+   | _ :=
+     throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', initial token is not statically known"))
 
-private unsafe def addBuiltinParserUnsafe (env : Environment) (declName : Name) (tablesRef : IO.Ref ParsingTables) : IO Unit :=
+def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit :=
-match env.find declName with
+do tables ← tablesRef.get,
-| none      := throw "unknown declaration"
+   tablesRef.reset,
-| some decl :=
+   tables ← updateTokens tables p.info,
-  match decl.type with
+   match p.info.firstTokens with
-  | Expr.const `Lean.Parser.TrailingParser _ := do
+   | FirstTokens.tokens tks :=
+     let tables := tks.foldl (λ (tables : ParsingTables) tk, { trailingTable := tables.trailingTable.insert tk.val p, .. tables }) tables in
+     tablesRef.set tables
+   | _ :=
+     let tables := { trailingParsers := p :: tables.trailingParsers, .. tables } in
+     tablesRef.set tables
 
-    p ← evalConst TrailingParser declName,
+def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment :=
-    updateTokens p.info tablesRef,
+let name := `_regBuiltinParser ++ declName in
-    match p.info.firstTokens with
+let type := Expr.app (mkConst `IO) (mkConst `Unit) in
-    | FirstTokens.tokens tks := tablesRef.modify $ λ tables, tks.foldl (λ tables tk, { ledTable := tables.ledTable.insert tk.val p, .. tables }) tables
+let val  := mkCApp addFnName [mkConst refDeclName, toExpr declName, mkConst declName] in
-    | _                      := tablesRef.modify $ λ tables, { ledParsers := p :: tables.ledParsers, .. tables }
+let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } in
-  | Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.nud _) := do
+match env.addAndCompile {} decl with
-    p ← evalConst Parser declName,
+| none     := throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
-    updateTokens p.info tablesRef,
+| some env := IO.ofExcept (setInitAttr env name)
-    match p.info.firstTokens with
-    | FirstTokens.tokens tks := tablesRef.modify $ λ tables, tks.foldl (λ tables tk, { nudTable := tables.nudTable.insert tk.val p, .. tables }) tables
-    | _                      := throw (IO.userError ("invalid parser '" ++ toString declName ++ "', initial token is not statically known"))
-  | _ := throwUnexpectedParserType declName
 
-@[implementedBy addBuiltinParserUnsafe]
+def declareLeadingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment :=
-private constant addBuiltinParser (env : Environment) (declName : Name) (tables : IO.Ref ParsingTables) : IO Unit := default _
+declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser refDeclName declName
+
+def declareTrailingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment :=
+declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser refDeclName declName
 
 /-
 The parsing tables for builtin parsers are "stored" in the extracted source code.
-This is needed for bootstrapping reasons.
-For example, we use the attribute `[builtinTermParser]` to compute the initial state for the
-attribute `[termParser]`.
 -/
-def registerBuiltinParserAttribute (name : Name) : IO BuiltinParserAttribute :=
+def registerBuiltinParserAttribute (attrName : Name) (refDeclName : Name) : IO Unit :=
-do tables ← IO.mkRef (none : Option ParsingTables),
+registerAttribute {
-   ledParsers ← IO.mkRef ([] : List Name),
+ name  := attrName,
-   nudParsers ← IO.mkRef ([] : List Name),
+ descr := "Builtin parser",
-   let attr : AttributeImpl := {
+ add   := λ env declName args persistent, do
-     name  := name,
+   unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument")),
-     descr := "Builtin parser",
+   unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent")),
-     add   := λ env declName args persistent, do
+   match env.find declName with
-      unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument")),
+   | none  := throw "unknown declaration"
-      unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent")),
+   | some decl :=
-      match env.find declName with
+     match decl.type with
-      | none  := throw "unknown declaration"
+     | Expr.const `Lean.Parser.TrailingParser _ :=
-      | some decl :=
+       declareTrailingBuiltinParser env refDeclName declName
-        match decl.type with
+     | Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.nud _) :=
-        | Expr.const `Lean.Parser.TrailingParser _ :=
+       declareLeadingBuiltinParser env refDeclName declName
-          ledParsers.modify $ λ ns, declName :: ns
+     | _ :=
-        | Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.nud _) :=
+       throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
-          nudParsers.modify $ λ ns, declName :: ns
+}
-        | _ := throwUnexpectedParserType declName,
-        pure env
-   },
-   registerAttribute attr,
-   pure { tables := tables, attr := attr, ledParsers := ledParsers, nudParsers := nudParsers }
 
-/- Register builtin parsing tables -/
+@[init mkBultinParsingTablesRef]
+constant builtinCommandParsingTable : IO.Ref ParsingTables := default _
+@[init mkBultinParsingTablesRef]
+constant builtinTermParsingTable : IO.Ref ParsingTables := default _
+@[init mkBultinParsingTablesRef]
+constant builtinLevelParsingTable : IO.Ref ParsingTables := default _
 
-def mkBuiltinCommandParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinCommandParser
+@[init] def regBuiltinCommandParserAttr : IO Unit :=
-def mkBuiltinTermParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinTermParser
+registerBuiltinParserAttribute `builtinCommandParser `Lean.Parser.builtinCommandParsingTable
-def mkBuiltinLevelParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinLevelParser
+@[init] def regBuiltinTermParserAttr : IO Unit :=
+registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable
+@[init] def regBuiltinLevelParserAttr : IO Unit :=
+registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
 
-@[init mkBuiltinCommandParserAttr]
+/- TODO(Leo): delete -/
-constant builtinCommandParserAttr : BuiltinParserAttribute := default _
+@[init mkBultinParsingTablesRef]
-@[init mkBuiltinTermParserAttr]
+constant builtinTestParsingTable : IO.Ref ParsingTables := default _
-constant builtinTermParserAttr : BuiltinParserAttribute := default _
+@[init] def regBuiltinTestParserAttr : IO Unit :=
-@[init mkBuiltinLevelParserAttr]
+registerBuiltinParserAttribute `builtinTestParser `Lean.Parser.builtinTestParsingTable
-constant builtinLevelParserAttr : BuiltinParserAttribute := default _
-
-/- builting test parsing tables. TODO: delete -/
-def mkBuiltinTestParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinTestParser
-@[init mkBuiltinTestParserAttr]
-constant builtinTestParserAttr : BuiltinParserAttribute := default _
 
 end Parser
 end Lean

src/library/compiler/compiler.cpp

@@ -253,7 +253,8 @@ extern "C" object * lean_add_and_compile(object * env, object * opts, object * d
     try {
         environment new_env = add_and_compile(environment(env, true), options(opts, true), declaration(decl, true));
         return mk_cnstr(1, new_env).steal();
-    } catch (exception &) {
+    } catch (exception & ex) {
+        // throw;
         return box(0);
     }
 }