max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: count quotation depth in parser correctly

Browse source
This commit is contained in:
Sebastian Ullrich 2021-04-29 13:02:56 +02:00
parent be1a929dc7
commit 73cf3533a1
10 changed files with 36 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
nix/bootstrap.nix
View file

@ -72,7 +72,7 @@ rec {
src = ../src;
fullSrc = ../.;
inherit debug;
leanFlags = [ "-Dinterpreter.prefer_native=false" ];
leanFlags = [ "-Dinterpreter.prefer_native=true" ];
});
in (all: all // all.lean) rec {
Init = build { name = "Init"; deps = []; };

22
src/Lean/Parser/Basic.lean
View file

@ -132,7 +132,7 @@ structure ParserModuleContext where
structure ParserContext extends InputContext, ParserModuleContext where
prec : Nat
tokens : TokenTable
insideQuot : Bool := false
quotDepth : Nat := 0
suppressInsideQuot : Bool := false
savedPos? : Option String.Pos := none
forbiddenTk? : Option Token := none
@ -447,7 +447,7 @@ def setLhsPrecFn (prec : Nat) : ParserFn := fun c s =>
}
def checkInsideQuotFn : ParserFn := fun c s =>
if c.insideQuot then s
if c.quotDepth > 0 && !c.suppressInsideQuot then s
else s.mkUnexpectedError "unexpected syntax outside syntax quotation"
@[inline] def checkInsideQuot : Parser := {
@ -456,7 +456,7 @@ def checkInsideQuotFn : ParserFn := fun c s =>
}
def checkOutsideQuotFn : ParserFn := fun c s =>
if !c.insideQuot then s
if !c.quotDepth == 0 || c.suppressInsideQuot then s
else s.mkUnexpectedError "unexpected syntax inside syntax quotation"
@[inline] def checkOutsideQuot : Parser := {
@ -464,13 +464,17 @@ def checkOutsideQuotFn : ParserFn := fun c s =>
fn := checkOutsideQuotFn
}
def toggleInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
if c.suppressInsideQuot then p c s
else p { c with insideQuot := !c.insideQuot } s
def addQuotDepthFn (i : Int) (p : ParserFn) : ParserFn := fun c s =>
p { c with quotDepth := c.quotDepth + i |>.toNat } s
@[inline] def toggleInsideQuot (p : Parser) : Parser := {
@[inline] def incQuotDepth (p : Parser) : Parser := {
info := p.info,
fn := toggleInsideQuotFn p.fn
fn := addQuotDepthFn 1 p.fn
}
@[inline] def decQuotDepth (p : Parser) : Parser := {
info := p.info,
fn := addQuotDepthFn (-1) p.fn
}
def suppressInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
@ -1687,7 +1691,7 @@ def pushNone : Parser :=
{ fn := fun c s => s.pushSyntax mkNullNode }
-- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> toggleInsideQuot termParser >> symbolNoAntiquot ")")
def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
def antiquotExpr : Parser := identNoAntiquot <|> antiquotNestedExpr
@[inline] def tokenWithAntiquotFn (p : ParserFn) : ParserFn := fun c s => do

2
src/Lean/Parser/Command.lean
View file

@ -15,7 +15,7 @@ namespace Parser
Multiple command will be put in a `null node, but a single command will not (so that you can directly
match against a quotation in a command kind's elaborator). -/
-- TODO: use two separate quotation parsers with parser priorities instead
@[builtinTermParser] def Term.quot := leading_parser "`(" >> toggleInsideQuot (termParser <|> many1Unbox commandParser) >> ")"
@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth (termParser <|> many1Unbox commandParser) >> ")"
@[builtinTermParser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
namespace Command

2
src/Lean/Parser/Do.lean
View file

@ -125,7 +125,7 @@ The second `notFollowedBy` prevents this problem.
@[builtinTermParser] def «do» := leading_parser:argPrec "do " >> doSeq
@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> toggleInsideQuot doElemParser >> ")"
@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> incQuotDepth doElemParser >> ")"
/- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/
@[builtinTermParser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq

2
src/Lean/Parser/Extension.lean
View file

@ -536,7 +536,7 @@ def notFollowedByCategoryTokenFn (catName : Name) : ParserFn := fun ctx s =>
let (s, stx) := peekToken ctx s
match stx with
| Except.ok (Syntax.atom _ sym) =>
if ctx.insideQuot && sym == "$" then s
if ctx.quotDepth > 0 && sym == "$" then s
else match cat.tables.leadingTable.find? (Name.mkSimple sym) with
| some _ => s.mkUnexpectedError (toString catName)
| _ => s

12
src/Lean/Parser/Syntax.lean
View file

@ -42,9 +42,9 @@ end Syntax
namespace Term
@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|" >> toggleInsideQuot syntaxParser >> ")"
@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|" >> toggleInsideQuot precedenceParser >> ")"
@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|" >> toggleInsideQuot priorityParser >> ")"
@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|" >> incQuotDepth syntaxParser >> ")"
@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|" >> incQuotDepth precedenceParser >> ")"
@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|" >> incQuotDepth priorityParser >> ")"
end Term
@ -76,9 +76,9 @@ def macroArgSimple := leading_parser ident >> checkNoWsBefore "no space before '
def macroArgSymbol := leading_parser strLit >> optional (atomic <| checkNoWsBefore >> "%" >> checkNoWsBefore >> ident)
def macroArg := macroArgSymbol <|> atomic macroArgSimple
def macroHead := macroArg
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> incQuotDepth Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> incQuotDepth (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> incQuotDepth (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
@[builtinCommandParser] def «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)

16
src/Lean/Parser/Term.lean
View file

@ -226,11 +226,11 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|" >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|" >> incQuotDepth (evalInsideQuot ``funBinder funBinder) >> ")"
def bracketedBinderF := bracketedBinder -- no default arg
@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|" >> toggleInsideQuot (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> toggleInsideQuot attrParser >> ")"
@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|" >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> incQuotDepth attrParser >> ")"
@[builtinTermParser] def panic := leading_parser:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
@ -245,14 +245,14 @@ def macroLastArg := macroDollarArg <|> macroArg
-- Macro for avoiding exponentially big terms when using `STWorld`
@[builtinTermParser] def stateRefT := leading_parser "StateRefT" >> macroArg >> macroLastArg
@[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> toggleInsideQuot (parserOfStack 1) >> ")"
@[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
end Term
@[builtinTermParser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
@[builtinTermParser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> incQuotDepth Tactic.seq1 >> ")"
@[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> toggleInsideQuot levelParser >> ")"
@[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> incQuotDepth levelParser >> ")"
builtin_initialize
register_parser_alias "letDecl" Term.letDecl

3
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -412,7 +412,8 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
@[combinatorFormatter Lean.Parser.setExpected]
def setExpected.formatter (expected : List String) (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.toggleInsideQuot] def toggleInsideQuot.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (declName : Name) (p : Formatter) : Formatter := p

3
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -465,7 +465,8 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
@[combinatorParenthesizer Lean.Parser.setExpected]
def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.toggleInsideQuot] def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (declName : Name) (p : Parenthesizer) : Parenthesizer := p

2
src/stdlib.make.in
View file

@ -14,7 +14,7 @@ LEANMAKE_OPTS=\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=true"\
LEANC_OPTS+="${LEANC_OPTS}"\
LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\