feat: support syntax abbreviations in dynamic quotations
This commit is contained in:
Gabriel Ebner
Sebastian Ullrich
parent
a3250dc44b
commit
7e483d3a0a
3 changed files with 93 additions and 92 deletions
|
|
@ -1817,54 +1817,6 @@ def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
|
|||
def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
|
||||
{ fn := fun c s => categoryParserOfStackFn offset { c with prec := prec } s }
|
||||
|
||||
unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s =>
|
||||
match ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.Parser declName <|>
|
||||
ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.TrailingParser declName with
|
||||
| Except.ok p => p.fn ctx s
|
||||
| Except.error e => s.mkUnexpectedError s!"error running parser {declName}: {e}"
|
||||
|
||||
@[implementedBy evalParserConstUnsafe]
|
||||
constant evalParserConst (declName : Name) : ParserFn
|
||||
|
||||
unsafe def parserOfStackFnUnsafe (offset : Nat) : ParserFn := fun ctx s =>
|
||||
let stack := s.stxStack
|
||||
if stack.size < offset + 1 then
|
||||
s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
|
||||
else
|
||||
match stack.get! (stack.size - offset - 1) with
|
||||
| Syntax.ident (val := parserName) .. =>
|
||||
match ctx.resolveName parserName with
|
||||
| [(parserName, [])] =>
|
||||
let iniSz := s.stackSize
|
||||
let s := evalParserConst parserName ctx s
|
||||
if !s.hasError && s.stackSize != iniSz + 1 then
|
||||
s.mkUnexpectedError "expected parser to return exactly one syntax object"
|
||||
else
|
||||
s
|
||||
| _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
|
||||
| _ => s.mkUnexpectedError s!"unknown parser {parserName}"
|
||||
| _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
|
||||
|
||||
@[implementedBy parserOfStackFnUnsafe]
|
||||
constant parserOfStackFn (offset : Nat) : ParserFn
|
||||
|
||||
def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
|
||||
{ fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
|
||||
|
||||
register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
|
||||
defValue := false
|
||||
group := "internal"
|
||||
descr := "(Lean bootstrapping) use parsers from the current stage inside quotations"
|
||||
}
|
||||
|
||||
/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
|
||||
def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
|
||||
fn := fun c s =>
|
||||
if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
|
||||
evalParserConst declName c s
|
||||
else
|
||||
p.fn c s }
|
||||
|
||||
private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
|
||||
if s.stackSize == iniSz + 1 then s
|
||||
else s.mkNode nullKind iniSz -- throw error instead?
|
||||
|
|
|
|||
|
|
@ -147,20 +147,6 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit
|
|||
| Except.ok tokenTable => builtinTokenTable.set tokenTable
|
||||
| Except.error msg => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}")
|
||||
|
||||
def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
|
||||
let p := evalInsideQuot declName p
|
||||
let categories ← builtinParserCategoriesRef.get
|
||||
let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
|
||||
builtinParserCategoriesRef.set categories
|
||||
builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
|
||||
updateBuiltinTokens p.info declName
|
||||
|
||||
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
|
||||
addBuiltinParser catName declName true p prio
|
||||
|
||||
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
|
||||
addBuiltinParser catName declName false p prio
|
||||
|
||||
def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
|
||||
match e with
|
||||
| Entry.token tk =>
|
||||
|
|
@ -178,34 +164,6 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
|
|||
| Except.ok categories => { s with categories := categories }
|
||||
| _ => unreachable!
|
||||
|
||||
unsafe def mkParserOfConstantUnsafe
|
||||
(categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do
|
||||
let env := (← read).env
|
||||
let opts := (← read).opts
|
||||
match env.find? constName with
|
||||
| none => throw ↑s!"unknow constant '{constName}'"
|
||||
| some info =>
|
||||
match info.type with
|
||||
| Expr.const `Lean.Parser.TrailingParser _ _ =>
|
||||
let p ← IO.ofExcept $ env.evalConst Parser opts constName
|
||||
pure ⟨false, p⟩
|
||||
| Expr.const `Lean.Parser.Parser _ _ =>
|
||||
let p ← IO.ofExcept $ env.evalConst Parser opts constName
|
||||
pure ⟨true, p⟩
|
||||
| Expr.const `Lean.ParserDescr _ _ =>
|
||||
let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName
|
||||
let p ← compileParserDescr d
|
||||
pure ⟨true, p⟩
|
||||
| Expr.const `Lean.TrailingParserDescr _ _ =>
|
||||
let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName
|
||||
let p ← compileParserDescr d
|
||||
pure ⟨false, p⟩
|
||||
| _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"
|
||||
|
||||
@[implementedBy mkParserOfConstantUnsafe]
|
||||
constant mkParserOfConstantAux
|
||||
(categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
|
||||
|
||||
/- Parser aliases for making `ParserDescr` extensible -/
|
||||
inductive AliasValue (α : Type) where
|
||||
| const (p : α)
|
||||
|
|
@ -268,6 +226,32 @@ def ensureBinaryParserAlias (aliasName : Name) : IO Unit :=
|
|||
def ensureConstantParserAlias (aliasName : Name) : IO Unit :=
|
||||
discard $ getConstAlias parserAliasesRef aliasName
|
||||
|
||||
unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do
|
||||
let env := (← read).env
|
||||
let opts := (← read).opts
|
||||
match env.find? constName with
|
||||
| none => throw ↑s!"unknow constant '{constName}'"
|
||||
| some info =>
|
||||
match info.type with
|
||||
| Expr.const `Lean.Parser.TrailingParser _ _ =>
|
||||
let p ← IO.ofExcept $ env.evalConst Parser opts constName
|
||||
pure ⟨false, p⟩
|
||||
| Expr.const `Lean.Parser.Parser _ _ =>
|
||||
let p ← IO.ofExcept $ env.evalConst Parser opts constName
|
||||
pure ⟨true, p⟩
|
||||
| Expr.const `Lean.ParserDescr _ _ =>
|
||||
let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName
|
||||
let p ← compileParserDescr d
|
||||
pure ⟨true, p⟩
|
||||
| Expr.const `Lean.TrailingParserDescr _ _ =>
|
||||
let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName
|
||||
let p ← compileParserDescr d
|
||||
pure ⟨false, p⟩
|
||||
| _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"
|
||||
|
||||
@[implementedBy mkParserOfConstantUnsafe]
|
||||
constant mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
|
||||
|
||||
partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser :=
|
||||
let rec visit : ParserDescr → ImportM Parser
|
||||
| ParserDescr.const n => getConstAlias parserAliasesRef n
|
||||
|
|
@ -281,7 +265,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr)
|
|||
| ParserDescr.symbol tk => return symbol tk
|
||||
| ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol tk includeIdent
|
||||
| ParserDescr.parser constName => do
|
||||
let (_, p) ← mkParserOfConstantAux categories constName visit;
|
||||
let (_, p) ← mkParserOfConstantAux constName visit;
|
||||
pure p
|
||||
| ParserDescr.cat catName prec =>
|
||||
match getCategory categories catName with
|
||||
|
|
@ -290,7 +274,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr)
|
|||
visit d
|
||||
|
||||
def mkParserOfConstant (categories : ParserCategories) (constName : Name) : ImportM (Bool × Parser) :=
|
||||
mkParserOfConstantAux categories constName (compileParserDescr categories)
|
||||
mkParserOfConstantAux constName (compileParserDescr categories)
|
||||
|
||||
structure ParserAttributeHook where
|
||||
/- Called after a parser attribute is applied to a declaration. -/
|
||||
|
|
@ -354,6 +338,43 @@ def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBeha
|
|||
| none => LeadingIdentBehavior.default
|
||||
| some cat => cat.behavior
|
||||
|
||||
unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
|
||||
let categories := (parserExtension.getState ctx.env).categories
|
||||
match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
|
||||
| Except.ok (bool, p) => p.fn ctx s
|
||||
| Except.error e => s.mkUnexpectedError e.toString
|
||||
|
||||
@[implementedBy evalParserConstUnsafe]
|
||||
constant evalParserConst (declName : Name) : ParserFn
|
||||
|
||||
register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
|
||||
defValue := false
|
||||
group := "internal"
|
||||
descr := "(Lean bootstrapping) use parsers from the current stage inside quotations"
|
||||
}
|
||||
|
||||
/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
|
||||
def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
|
||||
fn := fun c s =>
|
||||
if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
|
||||
evalParserConst declName c s
|
||||
else
|
||||
p.fn c s }
|
||||
|
||||
def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
|
||||
let p := evalInsideQuot declName p
|
||||
let categories ← builtinParserCategoriesRef.get
|
||||
let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
|
||||
builtinParserCategoriesRef.set categories
|
||||
builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
|
||||
updateBuiltinTokens p.info declName
|
||||
|
||||
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
|
||||
addBuiltinParser catName declName true p prio
|
||||
|
||||
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
|
||||
addBuiltinParser catName declName false p prio
|
||||
|
||||
def mkCategoryAntiquotParser (kind : Name) : Parser :=
|
||||
mkAntiquot kind.toString none
|
||||
|
||||
|
|
@ -606,5 +627,27 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
|
|||
fn := withOpenDeclFn p.fn
|
||||
}
|
||||
|
||||
def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
|
||||
let stack := s.stxStack
|
||||
if stack.size < offset + 1 then
|
||||
s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
|
||||
else
|
||||
match stack.get! (stack.size - offset - 1) with
|
||||
| Syntax.ident (val := parserName) .. =>
|
||||
match ctx.resolveName parserName with
|
||||
| [(parserName, [])] =>
|
||||
let iniSz := s.stackSize
|
||||
let s := evalParserConst parserName ctx s
|
||||
if !s.hasError && s.stackSize != iniSz + 1 then
|
||||
s.mkUnexpectedError "expected parser to return exactly one syntax object"
|
||||
else
|
||||
s
|
||||
| _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
|
||||
| _ => s.mkUnexpectedError s!"unknown parser {parserName}"
|
||||
| _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
|
||||
|
||||
def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
|
||||
{ fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
|
|||
6
tests/lean/run/syntaxAbbrevQuot.lean
Normal file
6
tests/lean/run/syntaxAbbrevQuot.lean
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
syntax foo := "a" <|> "b"
|
||||
|
||||
syntax "bla" foo : term -- TODO: necessary to declare a and b as keywords
|
||||
|
||||
#check `(foo| a)
|
||||
#check (· matches `(foo| a))
|
||||
Loading…
Add table
Reference in a new issue