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
This commit is contained in:
Leonardo de Moura
parent
766467d095
commit
697f69020f
5 changed files with 95 additions and 130 deletions
|
|
@ -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
|
||||
|
||||
namespace IO
|
||||
| Except.error e := throw (IO.userError (toString e))
|
||||
|
||||
def lazyPure {α : Type} (fn : Unit → α) : IO α :=
|
||||
pure (fn ())
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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 := {})
|
||||
(ledTable : TokenMap TrailingParser := {})
|
||||
(ledParsers : List TrailingParser := []) -- for supporting parsers such as function application
|
||||
(tokens : Trie TokenConfig := {})
|
||||
(leadingTable : TokenMap Parser := {})
|
||||
(trailingTable : TokenMap TrailingParser := {})
|
||||
(trailingParsers : List TrailingParser := []) -- for supporting parsers such as function application
|
||||
(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 := orelseFn (longestMatchFn ps) (anyOfFn tables.ledParsers) a c s in
|
||||
let (s, ps) := indexed tables.trailingTable 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 :=
|
||||
(tables : IO.Ref (Option ParsingTables))
|
||||
(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 _ }⟩
|
||||
def mkBultinParsingTablesRef : IO (IO.Ref ParsingTables) :=
|
||||
IO.mkRef {}
|
||||
|
||||
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 :=
|
||||
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 :=
|
||||
def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit :=
|
||||
do tables ← tablesRef.get,
|
||||
tablesRef.reset,
|
||||
match info.updateTokens tables.tokens with
|
||||
| Except.ok newTokens := tablesRef.set { tokens := newTokens, .. tables }
|
||||
| Except.error msg := throw (IO.userError msg)
|
||||
tables ← updateTokens tables p.info,
|
||||
match p.info.firstTokens with
|
||||
| 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 :=
|
||||
match env.find declName with
|
||||
| none := throw "unknown declaration"
|
||||
| some decl :=
|
||||
match decl.type with
|
||||
| Expr.const `Lean.Parser.TrailingParser _ := do
|
||||
def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit :=
|
||||
do tables ← tablesRef.get,
|
||||
tablesRef.reset,
|
||||
tables ← updateTokens tables p.info,
|
||||
match p.info.firstTokens with
|
||||
| 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,
|
||||
updateTokens p.info tablesRef,
|
||||
match p.info.firstTokens with
|
||||
| FirstTokens.tokens tks := tablesRef.modify $ λ tables, tks.foldl (λ tables tk, { ledTable := tables.ledTable.insert tk.val p, .. tables }) tables
|
||||
| _ := tablesRef.modify $ λ tables, { ledParsers := p :: tables.ledParsers, .. tables }
|
||||
| Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.nud _) := do
|
||||
p ← evalConst Parser declName,
|
||||
updateTokens p.info tablesRef,
|
||||
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
|
||||
def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment :=
|
||||
let name := `_regBuiltinParser ++ declName in
|
||||
let type := Expr.app (mkConst `IO) (mkConst `Unit) in
|
||||
let val := mkCApp addFnName [mkConst refDeclName, toExpr declName, mkConst declName] in
|
||||
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false } in
|
||||
match env.addAndCompile {} decl with
|
||||
| none := throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
|
||||
| some env := IO.ofExcept (setInitAttr env name)
|
||||
|
||||
@[implementedBy addBuiltinParserUnsafe]
|
||||
private constant addBuiltinParser (env : Environment) (declName : Name) (tables : IO.Ref ParsingTables) : IO Unit := default _
|
||||
def declareLeadingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment :=
|
||||
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 :=
|
||||
do tables ← IO.mkRef (none : Option ParsingTables),
|
||||
ledParsers ← IO.mkRef ([] : List Name),
|
||||
nudParsers ← IO.mkRef ([] : List Name),
|
||||
let attr : AttributeImpl := {
|
||||
name := name,
|
||||
descr := "Builtin parser",
|
||||
add := λ env declName args persistent, do
|
||||
unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument")),
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent")),
|
||||
match env.find declName with
|
||||
| none := throw "unknown declaration"
|
||||
| some decl :=
|
||||
match decl.type with
|
||||
| Expr.const `Lean.Parser.TrailingParser _ :=
|
||||
ledParsers.modify $ λ ns, declName :: ns
|
||||
| Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.nud _) :=
|
||||
nudParsers.modify $ λ ns, declName :: ns
|
||||
| _ := throwUnexpectedParserType declName,
|
||||
pure env
|
||||
},
|
||||
registerAttribute attr,
|
||||
pure { tables := tables, attr := attr, ledParsers := ledParsers, nudParsers := nudParsers }
|
||||
def registerBuiltinParserAttribute (attrName : Name) (refDeclName : Name) : IO Unit :=
|
||||
registerAttribute {
|
||||
name := attrName,
|
||||
descr := "Builtin parser",
|
||||
add := λ env declName args persistent, do
|
||||
unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument")),
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent")),
|
||||
match env.find declName with
|
||||
| none := throw "unknown declaration"
|
||||
| some decl :=
|
||||
match decl.type with
|
||||
| Expr.const `Lean.Parser.TrailingParser _ :=
|
||||
declareTrailingBuiltinParser env refDeclName declName
|
||||
| Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.nud _) :=
|
||||
declareLeadingBuiltinParser env refDeclName declName
|
||||
| _ :=
|
||||
throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
|
||||
}
|
||||
|
||||
/- 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
|
||||
def mkBuiltinTermParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinTermParser
|
||||
def mkBuiltinLevelParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinLevelParser
|
||||
@[init] def regBuiltinCommandParserAttr : IO Unit :=
|
||||
registerBuiltinParserAttribute `builtinCommandParser `Lean.Parser.builtinCommandParsingTable
|
||||
@[init] def regBuiltinTermParserAttr : IO Unit :=
|
||||
registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable
|
||||
@[init] def regBuiltinLevelParserAttr : IO Unit :=
|
||||
registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
|
||||
|
||||
@[init mkBuiltinCommandParserAttr]
|
||||
constant builtinCommandParserAttr : BuiltinParserAttribute := default _
|
||||
@[init mkBuiltinTermParserAttr]
|
||||
constant builtinTermParserAttr : BuiltinParserAttribute := default _
|
||||
@[init mkBuiltinLevelParserAttr]
|
||||
constant builtinLevelParserAttr : BuiltinParserAttribute := default _
|
||||
|
||||
/- builting test parsing tables. TODO: delete -/
|
||||
def mkBuiltinTestParserAttr : IO BuiltinParserAttribute := registerBuiltinParserAttribute `builtinTestParser
|
||||
@[init mkBuiltinTestParserAttr]
|
||||
constant builtinTestParserAttr : BuiltinParserAttribute := default _
|
||||
/- TODO(Leo): delete -/
|
||||
@[init mkBultinParsingTablesRef]
|
||||
constant builtinTestParsingTable : IO.Ref ParsingTables := default _
|
||||
@[init] def regBuiltinTestParserAttr : IO Unit :=
|
||||
registerBuiltinParserAttribute `builtinTestParser `Lean.Parser.builtinTestParsingTable
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue