chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
dd1aa2f271
commit
e525a8d7c3
18 changed files with 21950 additions and 21440 deletions
|
|
@ -148,16 +148,17 @@ inductive ParserDescr
|
|||
| sepBy1 : ParserDescr → ParserDescr → ParserDescr
|
||||
| node : Name → ParserDescr → ParserDescr
|
||||
| trailingNode : Name → ParserDescr → ParserDescr
|
||||
| symbol : String → Nat → ParserDescr
|
||||
| symbol : String → ParserDescr
|
||||
| nonReservedSymbol : String → Bool → ParserDescr
|
||||
| numLit : ParserDescr
|
||||
| strLit : ParserDescr
|
||||
| charLit : ParserDescr
|
||||
| nameLit : ParserDescr
|
||||
| ident : ParserDescr
|
||||
| rbpLt : Nat → ParserDescr
|
||||
| parser : Name → Nat → ParserDescr
|
||||
|
||||
instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol "" 0⟩
|
||||
instance ParserDescr.inhabited : Inhabited ParserDescr := ⟨ParserDescr.symbol ""⟩
|
||||
abbrev TrailingParserDescr := ParserDescr
|
||||
|
||||
/- Syntax -/
|
||||
|
|
|
|||
|
|
@ -102,13 +102,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
|
|||
if ctx.leadingIdentAsSymbol && rbp?.isNone then
|
||||
`(ParserDescr.nonReservedSymbol $(quote atom) false)
|
||||
else
|
||||
match rbp? with
|
||||
| some rbp => `(ParserDescr.symbol $(quote atom) $(quote rbp))
|
||||
| none => do
|
||||
env ← liftM getEnv;
|
||||
match Parser.getTokenLbp? env atom with
|
||||
| some lbp => `(ParserDescr.symbol $(quote atom) $(quote lbp))
|
||||
| none => `(ParserDescr.symbol $(quote atom) 0)
|
||||
`(ParserDescr.symbol $(quote atom))
|
||||
| none => liftM throwUnsupportedSyntax
|
||||
else if kind == `Lean.Parser.Syntax.num then
|
||||
`(ParserDescr.numLit)
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ categoryParser `command rbp
|
|||
`($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead.
|
||||
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). -/
|
||||
@[builtinTermParser] def Term.stxQuot := parser! symbol "`(" appPrec >> (termParser <|> many1 commandParser true) >> ")"
|
||||
@[builtinTermParser] def Term.stxQuot := parser! [appPrec] "`(" >> (termParser <|> many1 commandParser true) >> ")"
|
||||
|
||||
namespace Command
|
||||
def commentBody : Parser :=
|
||||
|
|
@ -54,15 +54,15 @@ def «constant» := parser! "constant " >> declId >> declSig >> optional d
|
|||
def «instance» := parser! "instance " >> optional declId >> declSig >> declVal
|
||||
def «axiom» := parser! "axiom " >> declId >> declSig
|
||||
def «example» := parser! "example " >> declSig >> declVal
|
||||
def inferMod := parser! try (symbol "{" appPrec >> "}")
|
||||
def inferMod := parser! try ("{" >> "}")
|
||||
def introRule := parser! " | " >> ident >> optional inferMod >> optDeclSig
|
||||
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many introRule
|
||||
def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many introRule
|
||||
def structExplicitBinder := parser! symbol "(" appPrec >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
|
||||
def structImplicitBinder := parser! symbol "{" appPrec >> many ident >> optional inferMod >> optDeclSig >> "}"
|
||||
def structInstBinder := parser! symbol "[" appPrec >> many ident >> optional inferMod >> optDeclSig >> "]"
|
||||
def structExplicitBinder := parser! "(" >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
|
||||
def structImplicitBinder := parser! "{" >> many ident >> optional inferMod >> optDeclSig >> "}"
|
||||
def structInstBinder := parser! "[" >> many ident >> optional inferMod >> optDeclSig >> "]"
|
||||
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
|
||||
def structCtor := parser! ident >> optional inferMod >> symbol " :: " 67
|
||||
def structCtor := parser! ident >> optional inferMod >> " :: "
|
||||
def structureTk := parser! "structure "
|
||||
def classTk := parser! "class "
|
||||
def «extends» := parser! " extends " >> sepBy1 termParser ", "
|
||||
|
|
@ -85,12 +85,12 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
|
|||
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
|
||||
@[builtinCommandParser] def «init_quot» := parser! "init_quot"
|
||||
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
|
||||
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> symbol "[" appPrec >> sepBy1 attrInstance ", " >> "]" >> many1 ident
|
||||
@[builtinCommandParser] def «export» := parser! "export " >> ident >> symbol "(" appPrec >> many1 ident >> ")"
|
||||
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident
|
||||
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
|
||||
def openHiding := parser! try (ident >> "hiding") >> many1 ident
|
||||
def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident
|
||||
def openRenaming := parser! try (ident >> "renaming") >> sepBy1 openRenamingItem ", "
|
||||
def openOnly := parser! try (ident >> symbol "(" appPrec) >> many1 ident >> ")"
|
||||
def openOnly := parser! try (ident >> "(") >> many1 ident >> ")"
|
||||
def openSimple := parser! many1 ident
|
||||
@[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
|
||||
|
||||
|
|
|
|||
|
|
@ -17,13 +17,13 @@ categoryParser `level rbp
|
|||
|
||||
namespace Level
|
||||
|
||||
@[builtinLevelParser] def paren := parser! symbol "(" appPrec >> levelParser >> ")"
|
||||
@[builtinLevelParser] def max := parser! nonReservedSymbol "max " true >> many1 (levelParser appPrec)
|
||||
@[builtinLevelParser] def imax := parser! nonReservedSymbol "imax " true >> many1 (levelParser appPrec)
|
||||
@[builtinLevelParser] def hole := parser! symbol "_" appPrec
|
||||
@[builtinLevelParser] def num := parser! numLit
|
||||
@[builtinLevelParser] def ident := parser! ident
|
||||
@[builtinLevelParser] def addLit := tparser! symbol "+" (65:Nat) >> numLit
|
||||
@[builtinLevelParser] def paren := parser! [appPrec] "(" >> levelParser >> ")"
|
||||
@[builtinLevelParser] def max := parser! [appPrec] nonReservedSymbol "max " true >> many1 (levelParser appPrec)
|
||||
@[builtinLevelParser] def imax := parser! [appPrec] nonReservedSymbol "imax " true >> many1 (levelParser appPrec)
|
||||
@[builtinLevelParser] def hole := parser! [appPrec] "_"
|
||||
@[builtinLevelParser] def num := parser! [appPrec] numLit
|
||||
@[builtinLevelParser] def ident := parser! [appPrec] ident
|
||||
@[builtinLevelParser] def addLit := tparser! [65] "+" >> numLit
|
||||
|
||||
end Level
|
||||
|
||||
|
|
|
|||
|
|
@ -92,28 +92,7 @@ input.get (input.next pos)
|
|||
(e.g., a list). -/
|
||||
def appPrec : Nat := 1024
|
||||
|
||||
structure TokenConfig :=
|
||||
(val : String)
|
||||
(lbp : Option Nat := none)
|
||||
(lbpNoWs : Option Nat := none) -- optional left-binding power when there is not whitespace before the token.
|
||||
|
||||
namespace TokenConfig
|
||||
|
||||
def beq : TokenConfig → TokenConfig → Bool
|
||||
| ⟨val₁, lbp₁, lbpnws₁⟩, ⟨val₂, lbp₂, lbpnws₂⟩ => val₁ == val₂ && lbp₁ == lbp₂ && lbpnws₁ == lbpnws₂
|
||||
|
||||
instance : HasBeq TokenConfig :=
|
||||
⟨beq⟩
|
||||
|
||||
def toStr : TokenConfig → String
|
||||
| ⟨val, some lbp, some lbpnws⟩ => val ++ ":" ++ toString lbp ++ ":" ++ toString lbpnws
|
||||
| ⟨val, some lbp, none⟩ => val ++ ":" ++ toString lbp
|
||||
| ⟨val, none, some lbpnws⟩ => val ++ ":none:" ++ toString lbpnws
|
||||
| ⟨val, none, none⟩ => val
|
||||
|
||||
instance : HasToString TokenConfig := ⟨toStr⟩
|
||||
|
||||
end TokenConfig
|
||||
abbrev Token := String
|
||||
|
||||
structure TokenCacheEntry :=
|
||||
(startPos stopPos : String.Pos := 0)
|
||||
|
|
@ -125,7 +104,7 @@ structure ParserCache :=
|
|||
def initCacheForInput (input : String) : ParserCache :=
|
||||
{ tokenCache := { startPos := input.bsize + 1 /- make sure it is not a valid position -/} }
|
||||
|
||||
abbrev TokenTable := Trie TokenConfig
|
||||
abbrev TokenTable := Trie Token
|
||||
|
||||
abbrev SyntaxNodeKindSet := PersistentHashMap SyntaxNodeKind Unit
|
||||
|
||||
|
|
@ -276,8 +255,8 @@ instance ParserFn.inhabited : Inhabited ParserFn := ⟨fun _ => id⟩
|
|||
inductive FirstTokens
|
||||
| epsilon : FirstTokens
|
||||
| unknown : FirstTokens
|
||||
| tokens : List TokenConfig → FirstTokens
|
||||
| optTokens : List TokenConfig → FirstTokens
|
||||
| tokens : List Token → FirstTokens
|
||||
| optTokens : List Token → FirstTokens
|
||||
|
||||
namespace FirstTokens
|
||||
|
||||
|
|
@ -311,7 +290,7 @@ instance : HasToString FirstTokens := ⟨toStr⟩
|
|||
end FirstTokens
|
||||
|
||||
structure ParserInfo :=
|
||||
(collectTokens : List TokenConfig → List TokenConfig := id)
|
||||
(collectTokens : List Token → List Token := id)
|
||||
(collectKinds : SyntaxNodeKindSet → SyntaxNodeKindSet := id)
|
||||
(firstTokens : FirstTokens := FirstTokens.unknown)
|
||||
|
||||
|
|
@ -793,31 +772,30 @@ def isIdCont : String → ParserState → Bool
|
|||
else
|
||||
false
|
||||
|
||||
private def isToken (idStartPos idStopPos : Nat) (tk : Option TokenConfig) : Bool :=
|
||||
private def isToken (idStartPos idStopPos : Nat) (tk : Option Token) : Bool :=
|
||||
match tk with
|
||||
| none => false
|
||||
| some tk =>
|
||||
-- if a token is both a symbol and a valid identifier (i.e. a keyword),
|
||||
-- we want it to be recognized as a symbol
|
||||
tk.val.bsize ≥ idStopPos - idStartPos
|
||||
tk.bsize ≥ idStopPos - idStartPos
|
||||
|
||||
def mkTokenAndFixPos (startPos : Nat) (tk : Option TokenConfig) : ParserFn :=
|
||||
def mkTokenAndFixPos (startPos : Nat) (tk : Option Token) : ParserFn :=
|
||||
fun c s =>
|
||||
match tk with
|
||||
| none => s.mkErrorAt "token" startPos
|
||||
| some tk =>
|
||||
let input := c.input;
|
||||
let leading := mkEmptySubstringAt input startPos;
|
||||
let val := tk.val;
|
||||
let stopPos := startPos + val.bsize;
|
||||
let stopPos := startPos + tk.bsize;
|
||||
let s := s.setPos stopPos;
|
||||
let s := whitespace c s;
|
||||
let wsStopPos := s.pos;
|
||||
let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring };
|
||||
let atom := mkAtom { leading := leading, pos := startPos, trailing := trailing } val;
|
||||
let atom := mkAtom { leading := leading, pos := startPos, trailing := trailing } tk;
|
||||
s.pushSyntax atom
|
||||
|
||||
def mkIdResult (startPos : Nat) (tk : Option TokenConfig) (val : Name) : ParserFn :=
|
||||
def mkIdResult (startPos : Nat) (tk : Option Token) (val : Name) : ParserFn :=
|
||||
fun c s =>
|
||||
let stopPos := s.pos;
|
||||
if isToken startPos stopPos tk then
|
||||
|
|
@ -833,7 +811,7 @@ else
|
|||
let atom := mkIdent info rawVal val;
|
||||
s.pushSyntax atom
|
||||
|
||||
partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → ParserFn
|
||||
partial def identFnAux (startPos : Nat) (tk : Option Token) : Name → ParserFn
|
||||
| r, c, s =>
|
||||
let input := c.input;
|
||||
let i := s.pos;
|
||||
|
|
@ -961,20 +939,20 @@ fun c s =>
|
|||
@[inline] def symbolFnAux (sym : String) (errorMsg : String) : ParserFn :=
|
||||
satisfySymbolFn (fun s => s == sym) [errorMsg]
|
||||
|
||||
def symbolInfo (sym : String) (lbp : Option Nat) : ParserInfo :=
|
||||
{ collectTokens := fun tks => { val := sym, lbp := lbp } :: tks,
|
||||
firstTokens := FirstTokens.tokens [ { val := sym, lbp := lbp } ] }
|
||||
def symbolInfo (sym : String) : ParserInfo :=
|
||||
{ collectTokens := fun tks => sym :: tks,
|
||||
firstTokens := FirstTokens.tokens [ sym ] }
|
||||
|
||||
@[inline] def symbolFn (sym : String) : ParserFn :=
|
||||
symbolFnAux sym ("'" ++ sym ++ "'")
|
||||
|
||||
@[inline] def symbolAux (sym : String) (lbp : Option Nat := none) : Parser :=
|
||||
@[inline] def symbolAux (sym : String) : Parser :=
|
||||
let sym := sym.trim;
|
||||
{ info := symbolInfo sym lbp,
|
||||
{ info := symbolInfo sym,
|
||||
fn := symbolFn sym }
|
||||
|
||||
@[inline] def symbol (sym : String) (lbp : Nat) : Parser :=
|
||||
symbolAux sym lbp
|
||||
@[inline] def symbol (sym : String) : Parser :=
|
||||
symbolAux sym
|
||||
|
||||
/-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
|
||||
parsing local tokens that have not been added to the token table (but may have
|
||||
|
|
@ -1006,9 +984,9 @@ nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")
|
|||
def nonReservedSymbolInfo (sym : String) (includeIdent : Bool) : ParserInfo :=
|
||||
{ firstTokens :=
|
||||
if includeIdent then
|
||||
FirstTokens.tokens [ { val := sym }, { val := "ident" } ]
|
||||
FirstTokens.tokens [ sym, "ident" ]
|
||||
else
|
||||
FirstTokens.tokens [ { val := sym } ] }
|
||||
FirstTokens.tokens [ sym ] }
|
||||
|
||||
@[inline] def nonReservedSymbol (sym : String) (includeIdent := false) : Parser :=
|
||||
let sym := sym.trim;
|
||||
|
|
@ -1057,9 +1035,9 @@ def checkNoWsBefore (errorMsg : String) : Parser :=
|
|||
{ info := epsilonInfo,
|
||||
fn := checkNoWsBeforeFn errorMsg }
|
||||
|
||||
def symbolNoWsInfo (sym : String) (lbpNoWs : Option Nat) : ParserInfo :=
|
||||
{ collectTokens := fun tks => { val := sym, lbpNoWs := lbpNoWs } :: tks,
|
||||
firstTokens := FirstTokens.tokens [ { val := sym, lbpNoWs := lbpNoWs } ] }
|
||||
def symbolNoWsInfo (sym : String) : ParserInfo :=
|
||||
{ collectTokens := fun tks => sym :: tks,
|
||||
firstTokens := FirstTokens.tokens [ sym ] }
|
||||
|
||||
@[inline] def symbolNoWsFnAux (sym : String) (errorMsg : String) : ParserFn :=
|
||||
fun c s =>
|
||||
|
|
@ -1082,28 +1060,28 @@ fun c s =>
|
|||
symbolNoWsFnAux sym ("'" ++ sym ++ "' without whitespace around it")
|
||||
|
||||
/- Similar to `symbol`, but succeeds only if there is no space whitespace after leading term and after `sym`. -/
|
||||
@[inline] def symbolNoWsAux (sym : String) (lbp : Option Nat) : Parser :=
|
||||
@[inline] def symbolNoWsAux (sym : String) : Parser :=
|
||||
let sym := sym.trim;
|
||||
{ info := symbolNoWsInfo sym lbp,
|
||||
{ info := symbolNoWsInfo sym,
|
||||
fn := symbolNoWsFn sym }
|
||||
|
||||
@[inline] def symbolNoWs (sym : String) (lbp : Nat) : Parser :=
|
||||
symbolNoWsAux sym lbp
|
||||
@[inline] def symbolNoWs (sym : String) : Parser :=
|
||||
symbolNoWsAux sym
|
||||
|
||||
def unicodeSymbolFnAux (sym asciiSym : String) (expected : List String) : ParserFn :=
|
||||
satisfySymbolFn (fun s => s == sym || s == asciiSym) expected
|
||||
|
||||
def unicodeSymbolInfo (sym asciiSym : String) (lbp : Option Nat) : ParserInfo :=
|
||||
{ collectTokens := fun tks => { val := sym, lbp := lbp } :: { val := asciiSym, lbp := lbp } :: tks,
|
||||
firstTokens := FirstTokens.tokens [ { val := sym, lbp := lbp }, { val := asciiSym, lbp := lbp } ] }
|
||||
def unicodeSymbolInfo (sym asciiSym : String) : ParserInfo :=
|
||||
{ collectTokens := fun tks => sym :: asciiSym :: tks,
|
||||
firstTokens := FirstTokens.tokens [ sym, asciiSym ] }
|
||||
|
||||
@[inline] def unicodeSymbolFn (sym asciiSym : String) : ParserFn :=
|
||||
unicodeSymbolFnAux sym asciiSym ["'" ++ sym ++ "', '" ++ asciiSym ++ "'"]
|
||||
|
||||
@[inline] def unicodeSymbol (sym asciiSym : String) (lbp : Option Nat := none) : Parser :=
|
||||
@[inline] def unicodeSymbol (sym asciiSym : String) : Parser :=
|
||||
let sym := sym.trim;
|
||||
let asciiSym := asciiSym.trim;
|
||||
{ info := unicodeSymbolInfo sym asciiSym lbp,
|
||||
{ info := unicodeSymbolInfo sym asciiSym,
|
||||
fn := unicodeSymbolFn sym asciiSym }
|
||||
|
||||
/- Succeeds if RBP < upper -/
|
||||
|
|
@ -1112,12 +1090,14 @@ fun c s =>
|
|||
if c.rbp < upper then s
|
||||
else s.mkUnexpectedError errorMsg
|
||||
|
||||
def checkRbpLt (lower : Nat) (errorMsg : String := "unexpected RBP") : Parser :=
|
||||
private def precErrorMsg := "unexpected token at this precedence level; consider parenthesizing the term"
|
||||
|
||||
@[inline] def checkRbpLt (upper : Nat) (errorMsg : String := precErrorMsg) : Parser :=
|
||||
{ info := epsilonInfo,
|
||||
fn := checkRbpLtFn lower errorMsg }
|
||||
fn := checkRbpLtFn upper errorMsg }
|
||||
|
||||
/- Succeeds if RBP <= upper -/
|
||||
def checkRbpLe (upper : Nat) (errorMsg : String := "unexpected RBP") : Parser :=
|
||||
@[inline] def checkRbpLe (upper : Nat) (errorMsg : String := precErrorMsg) : Parser :=
|
||||
checkRbpLt (upper + 1) errorMsg
|
||||
|
||||
/- Version of `leadingNode` which uses `checkRbpLe` -/
|
||||
|
|
@ -1126,11 +1106,11 @@ checkRbpLt (upper + 1) errorMsg
|
|||
checkRbpLe prec >> leadingNode n p
|
||||
|
||||
/- Version of `trailingNode` which uses `checkRbpLt` -/
|
||||
@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
|
||||
@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : TrailingParser :=
|
||||
checkRbpLt prec >> trailingNode n p
|
||||
|
||||
def mkAtomicInfo (k : String) : ParserInfo :=
|
||||
{ firstTokens := FirstTokens.tokens [ { val := k } ] }
|
||||
{ firstTokens := FirstTokens.tokens [ k ] }
|
||||
|
||||
def numLitFn : ParserFn :=
|
||||
fun c s =>
|
||||
|
|
@ -1219,7 +1199,7 @@ def unquotedSymbol : Parser :=
|
|||
{ fn := unquotedSymbolFn }
|
||||
|
||||
instance stringToParserCoe : HasCoe String Parser :=
|
||||
⟨fun s => symbol s 0⟩
|
||||
⟨fun s => symbol s ⟩
|
||||
|
||||
namespace ParserState
|
||||
|
||||
|
|
@ -1390,27 +1370,6 @@ instance ParserCategory.inhabited : Inhabited ParserCategory := ⟨{ tables := {
|
|||
|
||||
abbrev ParserCategories := PersistentHashMap Name ParserCategory
|
||||
|
||||
def currLbp (left : Syntax) (c : ParserContext) (s : ParserState) : ParserState × Nat :=
|
||||
let (s, stx?) := peekToken c s;
|
||||
match stx? with
|
||||
| some stx@(Syntax.atom _ sym) =>
|
||||
if sym == "$" && checkTailNoWs stx then (s, appPrec) -- TODO: split `lbpNoWs` into "before" and "after", and set right lbp for '$' in antiquotations
|
||||
else match c.tokens.matchPrefix sym 0 with
|
||||
| (_, some tk) => match tk.lbp, tk.lbpNoWs with
|
||||
| some lbp, none => (s, lbp)
|
||||
| none, some lbpNoWs => (s, lbpNoWs)
|
||||
| some lbp, some lbpNoWs => if checkTailNoWs left then (s, lbpNoWs) else (s, lbp)
|
||||
| none, none => (s, 0)
|
||||
| _ => (s, 0)
|
||||
| some (Syntax.ident _ _ _ _) => (s, appPrec)
|
||||
-- TODO(Leo): add support for associating lbp with syntax node kinds.
|
||||
| some (Syntax.node k _) =>
|
||||
if isLitKind k || k == fieldIdxKind then
|
||||
(s, appPrec)
|
||||
else
|
||||
(s, 0)
|
||||
| _ => (s, 0)
|
||||
|
||||
def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) (leadingIdentAsSymbol : Bool) : ParserState × List α :=
|
||||
let (s, stx) := peekToken c s;
|
||||
let find (n : Name) : ParserState × List α :=
|
||||
|
|
@ -1459,7 +1418,7 @@ categoryParser `term rbp
|
|||
/- Antiquotations -/
|
||||
/- ============== -/
|
||||
|
||||
def dollarSymbol : Parser := symbol "$" 1
|
||||
def dollarSymbol : Parser := symbol "$"
|
||||
|
||||
/-- Fail if previous token is immediately followed by ':'. -/
|
||||
private def noImmediateColon : Parser :=
|
||||
|
|
@ -1489,7 +1448,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 (symbol "(" appPrec >> termParser >> ")")
|
||||
def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbol "(" >> termParser >> ")")
|
||||
def antiquotExpr : Parser := identNoAntiquot <|> antiquotNestedExpr
|
||||
|
||||
/--
|
||||
|
|
@ -1500,7 +1459,7 @@ def antiquotExpr : Parser := identNoAntiquot <|> antiquotNestedExpr
|
|||
produces the syntax tree for `$e`. -/
|
||||
def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser :=
|
||||
let kind := (kind.getD Name.anonymous) ++ `antiquot;
|
||||
let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux ":" >> nonReservedSymbol name;
|
||||
let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name;
|
||||
-- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
|
||||
-- antiquotation kind via `noImmediateColon`
|
||||
let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
|
||||
|
|
@ -1510,7 +1469,7 @@ node kind $ try $
|
|||
many (checkNoWsBefore "" >> dollarSymbol) >>
|
||||
checkNoWsBefore "no space before spliced term" >> antiquotExpr >>
|
||||
nameP >>
|
||||
optional (checkNoWsBefore "" >> symbolAux "*" none)
|
||||
optional (checkNoWsBefore "" >> symbol "*")
|
||||
|
||||
def tryAnti (c : ParserContext) (s : ParserState) : Bool :=
|
||||
let (s, stx?) := peekToken c s;
|
||||
|
|
@ -1597,21 +1556,19 @@ s.pushSyntax result
|
|||
|
||||
partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : ParserState → ParserState
|
||||
| s =>
|
||||
let left := s.stxStack.back;
|
||||
let (s, lbp) := currLbp left c s;
|
||||
if c.rbp ≥ lbp then s
|
||||
let identAsSymbol := false;
|
||||
let (s, ps) := indexed tables.trailingTable c s identAsSymbol;
|
||||
if ps.isEmpty && tables.trailingParsers.isEmpty then
|
||||
s -- no available trailing parser
|
||||
else
|
||||
let iniSz := s.stackSize;
|
||||
let identAsSymbol := false;
|
||||
let (s, ps) := indexed tables.trailingTable c s identAsSymbol;
|
||||
if ps.isEmpty && tables.trailingParsers.isEmpty then
|
||||
s -- no available trailing parser
|
||||
let iniSz := s.stackSize;
|
||||
let iniPos := s.pos;
|
||||
let s := trailingLoopStep tables ps c s;
|
||||
if s.hasError then
|
||||
if s.pos == iniPos then s.restore iniSz iniPos else s
|
||||
else
|
||||
let s := trailingLoopStep tables ps c s;
|
||||
if s.hasError then s
|
||||
else
|
||||
let s := mkTrailingResult s iniSz;
|
||||
trailingLoop s
|
||||
let s := mkTrailingResult s iniSz;
|
||||
trailingLoop s
|
||||
|
||||
/--
|
||||
|
||||
|
|
@ -1636,14 +1593,13 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par
|
|||
overlap with antiquotation parsers nested inside them. -/
|
||||
@[inline] def prattParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) (antiquotParser : ParserFn) : ParserFn :=
|
||||
fun c s =>
|
||||
let left := s.stxStack.back;
|
||||
let (s, lbp) := currLbp left c s;
|
||||
if c.rbp > lbp then s.mkUnexpectedError "unexpected token"
|
||||
let iniSz := s.stackSize;
|
||||
let iniPos := s.pos;
|
||||
let s := leadingParser kind tables leadingIdentAsSymbol antiquotParser c s;
|
||||
if s.hasError then
|
||||
s
|
||||
else
|
||||
let s := leadingParser kind tables leadingIdentAsSymbol antiquotParser c s;
|
||||
if s.hasError then s
|
||||
else
|
||||
trailingLoop tables c s
|
||||
trailingLoop tables c s
|
||||
|
||||
def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {}
|
||||
@[init mkBuiltinTokenTable] constant builtinTokenTable : IO.Ref TokenTable := arbitrary _
|
||||
|
|
@ -1671,13 +1627,13 @@ categories ← IO.ofExcept $ addParserCategoryCore categories catName { tables :
|
|||
builtinParserCategoriesRef.set categories
|
||||
|
||||
inductive ParserExtensionOleanEntry
|
||||
| token (val : TokenConfig) : ParserExtensionOleanEntry
|
||||
| token (val : Token) : ParserExtensionOleanEntry
|
||||
| kind (val : SyntaxNodeKind) : ParserExtensionOleanEntry
|
||||
| category (catName : Name) (leadingIdentAsSymbol : Bool)
|
||||
| parser (catName : Name) (declName : Name) : ParserExtensionOleanEntry
|
||||
|
||||
inductive ParserExtensionEntry
|
||||
| token (val : TokenConfig) : ParserExtensionEntry
|
||||
| token (val : Token) : ParserExtensionEntry
|
||||
| kind (val : SyntaxNodeKind) : ParserExtensionEntry
|
||||
| category (catName : Name) (leadingIdentAsSymbol : Bool)
|
||||
| parser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) : ParserExtensionEntry
|
||||
|
|
@ -1706,14 +1662,11 @@ private def mergePrecendences (msgPreamble : String) (sym : String) : Option Nat
|
|||
else
|
||||
throw $ msgPreamble ++ "precedence mismatch for '" ++ toString sym ++ "', previous: " ++ toString a ++ ", new: " ++ toString b
|
||||
|
||||
private def addTokenConfig (tokens : TokenTable) (tk : TokenConfig) : Except String TokenTable := do
|
||||
if tk.val == "" then throw "invalid empty symbol"
|
||||
else match tokens.find? tk.val with
|
||||
| none => pure $ tokens.insert tk.val tk
|
||||
| some oldTk => do
|
||||
lbp ← mergePrecendences "" tk.val oldTk.lbp tk.lbp;
|
||||
lbpNoWs ← mergePrecendences "(no whitespace) " tk.val oldTk.lbpNoWs tk.lbpNoWs;
|
||||
pure $ tokens.insert tk.val { tk with lbp := lbp, lbpNoWs := lbpNoWs }
|
||||
private def addTokenConfig (tokens : TokenTable) (tk : Token) : Except String TokenTable := do
|
||||
if tk == "" then throw "invalid empty symbol"
|
||||
else match tokens.find? tk with
|
||||
| none => pure $ tokens.insert tk tk
|
||||
| some _ => pure tokens
|
||||
|
||||
def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
|
||||
throw ("unknown parser category '" ++ toString catName ++ "'")
|
||||
|
|
@ -1723,8 +1676,8 @@ match categories.find? catName with
|
|||
| none =>
|
||||
throwUnknownParserCategory catName
|
||||
| some cat =>
|
||||
let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
|
||||
let tks := tks.map $ fun tk => mkNameSimple tk.val;
|
||||
let addTokens (tks : List Token) : Except String ParserCategories :=
|
||||
let tks := tks.map $ fun tk => mkNameSimple tk;
|
||||
let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with leadingTable := tables.leadingTable.insert tk p }) cat.tables;
|
||||
pure $ categories.insert catName { cat with tables := tables };
|
||||
match p.info.firstTokens with
|
||||
|
|
@ -1735,8 +1688,8 @@ match categories.find? catName with
|
|||
pure $ categories.insert catName { cat with tables := tables }
|
||||
|
||||
private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) : PrattParsingTables :=
|
||||
let addTokens (tks : List TokenConfig) : PrattParsingTables :=
|
||||
let tks := tks.map $ fun tk => mkNameSimple tk.val;
|
||||
let addTokens (tks : List Token) : PrattParsingTables :=
|
||||
let tks := tks.map $ fun tk => mkNameSimple tk;
|
||||
tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with trailingTable := tables.trailingTable.insert tk p }) tables;
|
||||
match p.info.firstTokens with
|
||||
| FirstTokens.tokens tks => addTokens tks
|
||||
|
|
@ -1806,12 +1759,13 @@ def compileParserDescr (categories : ParserCategories) : ParserDescr → Except
|
|||
| ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
|
||||
| ParserDescr.node k d => node k <$> compileParserDescr d
|
||||
| ParserDescr.trailingNode k d => trailingNode k <$> compileParserDescr d
|
||||
| ParserDescr.symbol tk lbp => pure $ symbol tk lbp
|
||||
| ParserDescr.symbol tk => pure $ symbol tk
|
||||
| ParserDescr.numLit => pure $ numLit
|
||||
| ParserDescr.strLit => pure $ strLit
|
||||
| ParserDescr.charLit => pure $ charLit
|
||||
| ParserDescr.nameLit => pure $ nameLit
|
||||
| ParserDescr.ident => pure $ ident
|
||||
| ParserDescr.rbpLt prec => pure $ checkRbpLt prec
|
||||
| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol tk includeIdent
|
||||
| ParserDescr.parser catName rbp =>
|
||||
match categories.find? catName with
|
||||
|
|
@ -1916,7 +1870,7 @@ fun ctx s =>
|
|||
@[init] def setCategoryParserFnRef : IO Unit :=
|
||||
categoryParserFnRef.set categoryParserFnImpl
|
||||
|
||||
def addToken (env : Environment) (tk : TokenConfig) : Except String Environment := do
|
||||
def addToken (env : Environment) (tk : Token) : Except String Environment := do
|
||||
-- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
|
||||
-- So, we must run it here to handle exception.
|
||||
_ ← addTokenConfig (parserExtension.getState env).tokens tk;
|
||||
|
|
@ -1936,11 +1890,6 @@ kinds.foldl (fun ks k _ => k::ks) []
|
|||
def getTokenTable (env : Environment) : TokenTable :=
|
||||
(parserExtension.getState env).tokens
|
||||
|
||||
def getTokenLbp? (env : Environment) (sym : String) : Option Nat := do
|
||||
let tokens := getTokenTable env;
|
||||
tk ← tokens.find? sym;
|
||||
tk.lbp
|
||||
|
||||
def mkInputContext (input : String) (fileName : String) : InputContext :=
|
||||
{ input := input,
|
||||
fileName := fileName,
|
||||
|
|
|
|||
|
|
@ -23,9 +23,9 @@ def «precedence» := parser! ":" >> precedenceLit
|
|||
def optPrecedence := optional (try «precedence»)
|
||||
|
||||
namespace Syntax
|
||||
@[builtinSyntaxParser] def paren := parser! symbol "(" appPrec >> many1 syntaxParser >> ")"
|
||||
@[builtinSyntaxParser] def cat := parser! ident >> optPrecedence
|
||||
@[builtinSyntaxParser] def atom := parser! strLit >> optPrecedence
|
||||
@[builtinSyntaxParser] def paren := parser! [appPrec] "(" >> many1 syntaxParser >> ")"
|
||||
@[builtinSyntaxParser] def cat := parser! [appPrec] ident >> optPrecedence
|
||||
@[builtinSyntaxParser] def atom := parser! [appPrec] strLit >> optPrecedence
|
||||
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
|
||||
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
|
||||
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"
|
||||
|
|
@ -35,10 +35,10 @@ namespace Syntax
|
|||
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser appPrec >> syntaxParser appPrec
|
||||
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser appPrec >> syntaxParser appPrec
|
||||
|
||||
@[builtinSyntaxParser] def optional := tparser! symbolAux "?" none
|
||||
@[builtinSyntaxParser] def many := tparser! symbolAux "*" none
|
||||
@[builtinSyntaxParser] def many1 := tparser! symbolAux "+" none
|
||||
@[builtinSyntaxParser] def orelse := tparser! symbol " <|> " 2 >> syntaxParser 1
|
||||
@[builtinSyntaxParser] def optional := tparser! "?"
|
||||
@[builtinSyntaxParser] def many := tparser! "*"
|
||||
@[builtinSyntaxParser] def many1 := tparser! "+"
|
||||
@[builtinSyntaxParser] def orelse := tparser! [2] " <|> " >> syntaxParser 1
|
||||
|
||||
end Syntax
|
||||
|
||||
|
|
@ -59,7 +59,7 @@ def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol
|
|||
def strLitPrec := parser! strLit >> optPrecedence
|
||||
def identPrec := parser! ident >> optPrecedence
|
||||
|
||||
def optKind : Parser := optional (symbol "[" appPrec >> ident >> "]")
|
||||
def optKind : Parser := optional ("[" >> ident >> "]")
|
||||
-- TODO: remove " := " after old frontend is gone
|
||||
@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser
|
||||
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts
|
||||
|
|
@ -69,9 +69,9 @@ def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|>
|
|||
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
|
||||
def macroArg := try strLitPrec <|> try macroArgSimple
|
||||
def macroHead := macroArg <|> try identPrec
|
||||
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> symbol "`(" appPrec >> sepBy1 tacticParser "; " true true >> ")"
|
||||
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> symbol "`(" appPrec >> many1 commandParser true >> ")"
|
||||
def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> ((symbol "`(" appPrec >> categoryParserOfStack 2 >> ")") <|> termParser)
|
||||
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
|
||||
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"
|
||||
def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> (("`(" >> categoryParserOfStack 2 >> ")") <|> termParser)
|
||||
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
|
||||
@[builtinCommandParser] def «macro» := parser! "macro " >> macroHead >> many macroArg >> macroTail
|
||||
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ def ident' : Parser := ident <|> underscore
|
|||
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
|
||||
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
|
||||
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticParser
|
||||
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> symbol " = " 50 >> ident
|
||||
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident
|
||||
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
|
||||
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> (Term.hole <|> Term.namedHole <|> tacticParser)
|
||||
def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
|
||||
|
|
@ -48,10 +48,10 @@ def generalizingVars := optional (" generalizing " >> many1 ident)
|
|||
@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
|
||||
def withIds : Parser := optional (" with " >> many1 ident')
|
||||
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
|
||||
@[builtinTacticParser] def paren := parser! symbol "(" appPrec >> nonEmptySeq >> ")"
|
||||
@[builtinTacticParser] def nestedTacticBlock := parser! symbol "begin " appPrec >> seq >> "end"
|
||||
@[builtinTacticParser] def nestedTacticBlockCurly := parser! symbol "{" appPrec >> seq >> "}"
|
||||
@[builtinTacticParser] def orelse := tparser! symbol " <|> " 2 >> tacticParser 1
|
||||
@[builtinTacticParser] def paren := parser! [appPrec] "(" >> nonEmptySeq >> ")"
|
||||
@[builtinTacticParser] def nestedTacticBlock := parser! [appPrec] "begin " >> seq >> "end"
|
||||
@[builtinTacticParser] def nestedTacticBlockCurly := parser! [appPrec] "{" >> seq >> "}"
|
||||
@[builtinTacticParser] def orelse := tparser! [2] " <|> " >> tacticParser 1
|
||||
|
||||
end Tactic
|
||||
end Parser
|
||||
|
|
|
|||
|
|
@ -30,16 +30,16 @@ namespace Term
|
|||
/- Helper functions for defining simple parsers -/
|
||||
|
||||
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
|
||||
unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
|
||||
checkRbpLt lbp >> unicodeSymbol sym asciiSym >> termParser (lbp - 1)
|
||||
|
||||
def infixR (sym : String) (lbp : Nat) : TrailingParser :=
|
||||
symbol sym lbp >> termParser (lbp - 1)
|
||||
checkRbpLt lbp >> symbol sym >> termParser (lbp - 1)
|
||||
|
||||
def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
|
||||
unicodeSymbol sym asciiSym lbp >> termParser lbp
|
||||
checkRbpLt lbp >> unicodeSymbol sym asciiSym >> termParser lbp
|
||||
|
||||
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
|
||||
symbol sym lbp >> termParser lbp
|
||||
checkRbpLt lbp >> symbol sym >> termParser lbp
|
||||
|
||||
def leadPrec := appPrec - 1
|
||||
|
||||
|
|
@ -47,56 +47,56 @@ def leadPrec := appPrec - 1
|
|||
-- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
|
||||
-- antiquotation.
|
||||
def explicitUniv := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}"
|
||||
def namedPattern := checkNoWsBefore "no space before '@'" >> parser! symbol "@" appPrec >> termParser appPrec
|
||||
@[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern)
|
||||
@[builtinTermParser] def num : Parser := parser! numLit
|
||||
@[builtinTermParser] def str : Parser := parser! strLit
|
||||
@[builtinTermParser] def char : Parser := parser! charLit
|
||||
@[builtinTermParser] def type := parser! symbol "Type" appPrec >> optional (checkRbpLt appPrec >> levelParser appPrec)
|
||||
@[builtinTermParser] def sort := parser! symbol "Sort" appPrec >> optional (checkRbpLt appPrec >> levelParser appPrec)
|
||||
@[builtinTermParser] def prop := parser! symbol "Prop" appPrec
|
||||
@[builtinTermParser] def hole := parser! symbol "_" appPrec
|
||||
@[builtinTermParser] def namedHole := parser! symbol "?" appPrec >> ident
|
||||
@[builtinTermParser] def «sorry» := parser! symbol "sorry" appPrec
|
||||
@[builtinTermParser] def cdot := parser! symbol "·" appPrec
|
||||
@[builtinTermParser] def emptyC := parser! symbol "∅" appPrec
|
||||
def namedPattern := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser appPrec
|
||||
@[builtinTermParser] def id := parser! [appPrec] ident >> optional (explicitUniv <|> namedPattern)
|
||||
@[builtinTermParser] def num : Parser := parser! [appPrec] numLit
|
||||
@[builtinTermParser] def str : Parser := parser! [appPrec] strLit
|
||||
@[builtinTermParser] def char : Parser := parser! [appPrec] charLit
|
||||
@[builtinTermParser] def type := parser! [appPrec] "Type" >> optional (checkRbpLt appPrec >> levelParser appPrec)
|
||||
@[builtinTermParser] def sort := parser! [appPrec] "Sort" >> optional (checkRbpLt appPrec >> levelParser appPrec)
|
||||
@[builtinTermParser] def prop := parser! [appPrec] "Prop"
|
||||
@[builtinTermParser] def hole := parser! [appPrec] "_"
|
||||
@[builtinTermParser] def namedHole := parser! [appPrec] "?" >> ident
|
||||
@[builtinTermParser] def «sorry» := parser! [appPrec] "sorry"
|
||||
@[builtinTermParser] def cdot := parser! [appPrec] "·"
|
||||
@[builtinTermParser] def emptyC := parser! [appPrec] "∅"
|
||||
def typeAscription := parser! " : " >> termParser
|
||||
def tupleTail := parser! ", " >> sepBy1 termParser ", "
|
||||
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
|
||||
@[builtinTermParser] def paren := parser! symbol "(" appPrec >> optional (termParser >> parenSpecial) >> ")"
|
||||
@[builtinTermParser] def anonymousCtor := parser! symbol "⟨" appPrec >> sepBy termParser ", " >> "⟩"
|
||||
@[builtinTermParser] def paren := parser! [appPrec] "(" >> optional (termParser >> parenSpecial) >> ")"
|
||||
@[builtinTermParser] def anonymousCtor := parser! [appPrec] "⟨" >> sepBy termParser ", " >> "⟩"
|
||||
def optIdent : Parser := optional (try (ident >> " : "))
|
||||
@[builtinTermParser] def «if» := parser! symbol "if " leadPrec >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
|
||||
@[builtinTermParser] def «if» := parser! [leadPrec] "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
|
||||
def fromTerm := parser! " from " >> termParser
|
||||
def haveAssign := parser! " := " >> termParser
|
||||
@[builtinTermParser] def «have» := parser! symbol "have " leadPrec >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
|
||||
@[builtinTermParser] def «suffices» := parser! symbol "suffices " leadPrec >> optIdent >> termParser >> fromTerm >> "; " >> termParser
|
||||
@[builtinTermParser] def «show» := parser! symbol "show " leadPrec >> termParser >> fromTerm
|
||||
def structInstArrayRef := parser! symbol "[" appPrec >> termParser >>"]"
|
||||
@[builtinTermParser] def «have» := parser! [leadPrec] "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
|
||||
@[builtinTermParser] def «suffices» := parser! [leadPrec] "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
|
||||
@[builtinTermParser] def «show» := parser! [leadPrec] "show " >> termParser >> fromTerm
|
||||
def structInstArrayRef := parser! "[" >> termParser >>"]"
|
||||
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
|
||||
def structInstField := parser! structInstLVal >> " := " >> termParser
|
||||
@[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}"
|
||||
@[builtinTermParser] def structInst := parser! [appPrec] "{" >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}"
|
||||
def typeSpec := parser! " : " >> termParser
|
||||
def optType : Parser := optional typeSpec
|
||||
@[builtinTermParser] def subtype := parser! symbol "{" appPrec >> ident >> optType >> " // " >> termParser >> "}"
|
||||
@[builtinTermParser] def listLit := parser! symbol "[" appPrec >> sepBy termParser "," true >> "]"
|
||||
@[builtinTermParser] def arrayLit := parser! symbol "#[" appPrec >> sepBy termParser "," true >> "]"
|
||||
@[builtinTermParser] def explicit := parser! symbol "@" appPrec >> termParser appPrec
|
||||
@[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")"
|
||||
@[builtinTermParser] def subtype := parser! [appPrec] "{" >> ident >> optType >> " // " >> termParser >> "}"
|
||||
@[builtinTermParser] def listLit := parser! [appPrec] "[" >> sepBy termParser "," true >> "]"
|
||||
@[builtinTermParser] def arrayLit := parser! [appPrec] "#[" >> sepBy termParser "," true >> "]"
|
||||
@[builtinTermParser] def explicit := parser! [appPrec] "@" >> termParser appPrec
|
||||
@[builtinTermParser] def inaccessible := parser! [appPrec] ".(" >> termParser >> ")"
|
||||
def binderIdent : Parser := ident <|> hole
|
||||
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
|
||||
def binderTactic := parser! try (" := " >> symbol " by " leadPrec) >> Tactic.nonEmptySeq
|
||||
def binderTactic := parser! try (" := " >> " by ") >> Tactic.nonEmptySeq
|
||||
def binderDefault := parser! " := " >> termParser
|
||||
def explicitBinder (requireType := false) := parser! symbol "(" appPrec >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
|
||||
def implicitBinder (requireType := false) := parser! symbol "{" appPrec >> many1 binderIdent >> binderType requireType >> "}"
|
||||
def instBinder := parser! symbol "[" appPrec >> optIdent >> termParser >> "]"
|
||||
def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
|
||||
def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
|
||||
def instBinder := parser! "[" >> optIdent >> termParser >> "]"
|
||||
def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
|
||||
@[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkRbpLe 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
|
||||
@[builtinTermParser] def depArrow := parser! [appPrec] bracketedBinder true >> checkRbpLe 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
|
||||
def simpleBinder := parser! many1 binderIdent
|
||||
@[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" leadPrec >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
|
||||
@[builtinTermParser] def «forall» := parser! [leadPrec] unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
|
||||
|
||||
def funBinder : Parser := implicitBinder <|> instBinder <|> termParser appPrec
|
||||
@[builtinTermParser] def «fun» := parser! unicodeSymbol "λ" "fun" leadPrec >> many1 funBinder >> darrow >> termParser
|
||||
@[builtinTermParser] def «fun» := parser! [leadPrec] unicodeSymbol "λ" "fun" >> many1 funBinder >> darrow >> termParser
|
||||
|
||||
def matchAlt : Parser :=
|
||||
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
|
||||
|
|
@ -107,14 +107,14 @@ withPosition $ fun pos =>
|
|||
(if optionalFirstBar then optional "|" else "|") >>
|
||||
sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
|
||||
|
||||
@[builtinTermParser] def «match» := parser! symbol "match " leadPrec >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
|
||||
@[builtinTermParser] def «nomatch» := parser! symbol "nomatch " leadPrec >> termParser
|
||||
@[builtinTermParser] def «parser!» := parser! symbol "parser! " leadPrec >> termParser
|
||||
@[builtinTermParser] def «tparser!» := parser! symbol "tparser! " leadPrec >> termParser
|
||||
@[builtinTermParser] def borrowed := parser! symbol "@&" appPrec >> termParser (appPrec - 1)
|
||||
@[builtinTermParser] def quotedName := parser! nameLit
|
||||
@[builtinTermParser] def «match» := parser! [leadPrec] "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
|
||||
@[builtinTermParser] def «nomatch» := parser! [leadPrec] "nomatch " >> termParser
|
||||
@[builtinTermParser] def «parser!» := parser! [leadPrec] "parser! " >> termParser -- TODO optional prec
|
||||
@[builtinTermParser] def «tparser!» := parser! [leadPrec] "tparser! " >> termParser
|
||||
@[builtinTermParser] def borrowed := parser! [appPrec] "@&" >> termParser (appPrec - 1)
|
||||
@[builtinTermParser] def quotedName := parser! [appPrec] nameLit
|
||||
-- NOTE: syntax quotations are defined in Init.Lean.Parser.Command
|
||||
@[builtinTermParser] def «match_syntax» := parser! symbol "match_syntax" leadPrec >> termParser >> " with " >> matchAlts
|
||||
@[builtinTermParser] def «match_syntax» := parser! [leadPrec] "match_syntax" >> termParser >> " with " >> matchAlts
|
||||
|
||||
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
|
||||
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracketedBinder >> optType
|
||||
|
|
@ -122,41 +122,41 @@ def letIdDecl : Parser := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl
|
|||
def letPatDecl : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser
|
||||
def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false
|
||||
def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl
|
||||
@[builtinTermParser] def «let» := parser! symbol "let " leadPrec >> letDecl >> "; " >> termParser
|
||||
@[builtinTermParser] def «let!» := parser! symbol "let! " leadPrec >> letDecl >> "; " >> termParser
|
||||
@[builtinTermParser] def «let» := parser! [leadPrec] "let " >> letDecl >> "; " >> termParser
|
||||
@[builtinTermParser] def «let!» := parser! [leadPrec] "let! " >> letDecl >> "; " >> termParser
|
||||
|
||||
def leftArrow : Parser := unicodeSymbol " ← " " <- "
|
||||
def doLet := parser! symbol "let " leadPrec >> letDecl
|
||||
def doLet := parser! "let ">> letDecl
|
||||
def doId := parser! try (ident >> optType >> leftArrow) >> termParser
|
||||
def doPat := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
|
||||
def doExpr := parser! termParser
|
||||
def doElem := doLet <|> doId <|> doPat <|> doExpr
|
||||
def doSeq := sepBy1 doElem "; "
|
||||
def bracketedDoSeq := parser! symbol "{" appPrec >> doSeq >> "}"
|
||||
@[builtinTermParser] def liftMethod := parser! leftArrow >> termParser
|
||||
@[builtinTermParser] def «do» := parser! symbol "do " leadPrec >> (bracketedDoSeq <|> doSeq)
|
||||
def bracketedDoSeq := parser! [appPrec] "{" >> doSeq >> "}"
|
||||
@[builtinTermParser] def liftMethod := parser! [0] leftArrow >> termParser
|
||||
@[builtinTermParser] def «do» := parser! [leadPrec] "do " >> (bracketedDoSeq <|> doSeq)
|
||||
|
||||
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec
|
||||
@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser appPrec
|
||||
@[builtinTermParser] def decide := parser! "decide! " >> termParser appPrec
|
||||
|
||||
@[builtinTermParser] def not := parser! symbol "¬" appPrec >> termParser 40
|
||||
@[builtinTermParser] def bnot := parser! symbol "!" appPrec >> termParser 40
|
||||
@[builtinTermParser] def not := parser! [appPrec] "¬" >> termParser 40
|
||||
@[builtinTermParser] def bnot := parser! [appPrec] "!" >> termParser 40
|
||||
-- symbol precedence should be higher, but must match the one of `sub` below
|
||||
@[builtinTermParser] def uminus := parser! symbol "-" 65 >> termParser 100
|
||||
@[builtinTermParser] def uminus := parser! [65] "-" >> termParser 100
|
||||
|
||||
def namedArgument := parser! try (symbol "(" appPrec >> ident >> " := ") >> termParser >> ")"
|
||||
@[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec)
|
||||
def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
|
||||
@[builtinTermParser] def app := tparser! [appPrec] many1 (namedArgument <|> termParser appPrec)
|
||||
|
||||
def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort)
|
||||
@[builtinTermParser] def proj := tparser! symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
|
||||
@[builtinTermParser] def proj := tparser! [appPrec+1] symbolNoWs "." >> (fieldIdx <|> ident)
|
||||
@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
|
||||
@[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" (appPrec+1) >> termParser >>"]"
|
||||
@[builtinTermParser] def arrayRef := tparser! [appPrec+1] symbolNoWs "[" >> termParser >>"]"
|
||||
|
||||
@[builtinTermParser] def dollar := tparser! try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
|
||||
@[builtinTermParser] def dollarProj := tparser! symbol "$." 1 >> (fieldIdx <|> ident)
|
||||
@[builtinTermParser] def dollar := tparser! [1] try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
|
||||
@[builtinTermParser] def dollarProj := tparser! [1] "$." >> (fieldIdx <|> ident)
|
||||
|
||||
@[builtinTermParser] def «where» := tparser! symbol " where " 1 >> sepBy1 letDecl (group ("; " >> symbol " where " 1))
|
||||
@[builtinTermParser] def «where» := tparser! [1] " where " >> sepBy1 letDecl (group ("; " >> symbol " where "))
|
||||
|
||||
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
|
||||
|
||||
|
|
@ -181,7 +181,7 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type
|
|||
@[builtinTermParser] def heq := tparser! unicodeInfixL " ≅ " " ~= " 50
|
||||
@[builtinTermParser] def equiv := tparser! infixL " ≈ " 50
|
||||
|
||||
@[builtinTermParser] def subst := tparser! symbol " ▸ " 75 >> sepBy1 (termParser 75) (symbol " ▸ " 75)
|
||||
@[builtinTermParser] def subst := tparser! [75] " ▸ " >> sepBy1 (termParser 75) " ▸ "
|
||||
|
||||
@[builtinTermParser] def and := tparser! unicodeInfixR " ∧ " " /\\ " 35
|
||||
@[builtinTermParser] def or := tparser! unicodeInfixR " ∨ " " \\/ " 30
|
||||
|
|
@ -206,12 +206,15 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type
|
|||
@[builtinTermParser] def mapConst := tparser! infixR " <$ " 100
|
||||
@[builtinTermParser] def mapConstRev := tparser! infixR " $> " 100
|
||||
|
||||
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
|
||||
@[builtinTermParser] def byTactic := parser! symbol "by " leadPrec >> Tactic.nonEmptySeq
|
||||
@[builtinTermParser] def tacticBlock := parser! [appPrec] "begin " >> Tactic.seq >> "end"
|
||||
@[builtinTermParser] def byTactic := parser! [leadPrec] "by " >> Tactic.nonEmptySeq
|
||||
-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
|
||||
@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> sepBy1 tacticParser "; " true true >> ")"
|
||||
@[builtinTermParser] def levelStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(level|" appPrec >> levelParser >> ")"
|
||||
@[builtinTermParser] def funBinderStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(funBinder|" appPrec >> funBinder >> ")"
|
||||
@[builtinTermParser] def tacticStxQuot : Parser :=
|
||||
checkRbpLe appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")")
|
||||
@[builtinTermParser] def levelStxQuot : Parser :=
|
||||
checkRbpLe appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(level|" >> levelParser >> ")")
|
||||
@[builtinTermParser] def funBinderStxQuot : Parser :=
|
||||
checkRbpLe appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(funBinder|" >> funBinder >> ")")
|
||||
|
||||
end Term
|
||||
end Parser
|
||||
|
|
|
|||
|
|
@ -1483,13 +1483,11 @@ return x_17;
|
|||
lean_object* _init_l_Lean_ParserDescr_inhabited___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_String_splitAux___main___closed__1;
|
||||
x_2 = lean_unsigned_to_nat(0u);
|
||||
x_3 = lean_alloc_ctor(11, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
x_2 = lean_alloc_ctor(11, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_ParserDescr_inhabited() {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -141,7 +141,7 @@ lean_object* l_Lean_Parser_Module_prelude___closed__1;
|
|||
lean_object* l___private_Lean_Parser_Module_2__mkEOI___closed__1;
|
||||
lean_object* l_Lean_Parser_Module_header___closed__7;
|
||||
lean_object* l_Lean_Parser_Module_import___closed__7;
|
||||
lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_symbolInfo(lean_object*);
|
||||
lean_object* l_IO_FS_Handle_getLine___at_Lean_Parser_parseFile___spec__3(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -168,7 +168,6 @@ uint8_t l_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_obj
|
|||
lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__9;
|
||||
extern lean_object* l_Lean_Syntax_decodeNatLitVal___closed__1;
|
||||
lean_object* l_PersistentArray_forM___at___private_Lean_Parser_Module_4__testModuleParserAux___main___spec__6(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_IO_FS_Handle_readToEndAux___main___at_Lean_Parser_parseFile___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_IO_FS_Handle_mk___at_IO_FS_withFile___spec__1(lean_object*, uint8_t, uint8_t, lean_object*);
|
||||
|
|
@ -493,11 +492,10 @@ return x_65;
|
|||
lean_object* _init_l_Lean_Parser_Module_prelude___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Module_prelude___elambda__1___closed__7;
|
||||
x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1;
|
||||
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
x_2 = l_Lean_Parser_symbolInfo(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Module_prelude___closed__2() {
|
||||
|
|
@ -1236,21 +1234,19 @@ return x_140;
|
|||
lean_object* _init_l_Lean_Parser_Module_import___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__6;
|
||||
x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1;
|
||||
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
x_2 = l_Lean_Parser_symbolInfo(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Module_import___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__8;
|
||||
x_2 = l_Lean_Syntax_decodeNatLitVal___closed__1;
|
||||
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
x_2 = l_Lean_Parser_symbolInfo(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Module_import___closed__3() {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -70,6 +70,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer___
|
|||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_strLitNoAntiquot_parenthesizer___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withPosition_parenthesizer___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_evalNat(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_Traverser_up(lean_object*);
|
||||
|
|
@ -262,8 +263,8 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_visit___main___closed__6;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_symbolAux_parenthesizer(lean_object*);
|
||||
extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
extern lean_object* l_Lean_choiceKind___closed__2;
|
||||
extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__2;
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_fieldIdx_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_getIdx(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_numLitNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -392,7 +393,6 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_numLitNoAntiquot_pa
|
|||
lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_visit___main___closed__9;
|
||||
extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3;
|
||||
uint8_t l_Lean_Elab_Term_Quotation_isAntiquot(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_many_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -453,6 +453,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__8;
|
|||
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__3;
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_nonReservedSymbol_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_unquotedSymbol_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_WHNF_whnfCore___main___at_Lean_Meta_whnfCore___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer(lean_object*);
|
||||
|
|
@ -595,7 +596,7 @@ lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, uint8_t, lean_objec
|
|||
extern lean_object* l_Nat_Inhabited;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGe_parenthesizer___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_unicodeSymbolInfo(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_unicodeSymbolInfo(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_PrettyPrinter_Parenthesizer_visit___main___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_ReaderT_lift___at_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
|
||||
|
|
@ -614,7 +615,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbolNoWsAux_parenthesizer___bo
|
|||
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6;
|
||||
lean_object* l_Nat_forMAux___main___at_Lean_PrettyPrinter_Parenthesizer_visit___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkRbpLt_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
extern lean_object* l___private_Lean_Meta_Tactic_Util_1__regTraceClasses___closed__1;
|
||||
extern lean_object* l_Lean_mkAppStx___closed__2;
|
||||
lean_object* l___private_Lean_PrettyPrinter_Parenthesizer_1__regTraceClasses(lean_object*);
|
||||
|
|
@ -3963,6 +3963,16 @@ lean_dec(x_2);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_appPrec;
|
||||
x_2 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -4021,7 +4031,7 @@ x_26 = lean_ctor_get(x_21, 2);
|
|||
lean_dec(x_26);
|
||||
x_27 = lean_ctor_get(x_21, 1);
|
||||
lean_dec(x_27);
|
||||
x_28 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_28 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
lean_ctor_set(x_21, 2, x_28);
|
||||
lean_ctor_set(x_21, 1, x_28);
|
||||
x_29 = lean_box(0);
|
||||
|
|
@ -4036,7 +4046,7 @@ x_31 = lean_ctor_get(x_21, 3);
|
|||
lean_inc(x_31);
|
||||
lean_inc(x_30);
|
||||
lean_dec(x_21);
|
||||
x_32 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_32 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
x_33 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_33, 0, x_30);
|
||||
lean_ctor_set(x_33, 1, x_32);
|
||||
|
|
@ -4068,7 +4078,7 @@ if (lean_is_exclusive(x_21)) {
|
|||
lean_dec_ref(x_21);
|
||||
x_38 = lean_box(0);
|
||||
}
|
||||
x_39 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_39 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
if (lean_is_scalar(x_38)) {
|
||||
x_40 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
|
|
@ -4117,7 +4127,7 @@ if (lean_is_exclusive(x_43)) {
|
|||
lean_dec_ref(x_43);
|
||||
x_48 = lean_box(0);
|
||||
}
|
||||
x_49 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_49 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
if (lean_is_scalar(x_48)) {
|
||||
x_50 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
|
|
@ -4929,7 +4939,7 @@ x_87 = lean_ctor_get(x_82, 2);
|
|||
lean_dec(x_87);
|
||||
x_88 = lean_ctor_get(x_82, 1);
|
||||
lean_dec(x_88);
|
||||
x_89 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_89 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
lean_ctor_set(x_82, 3, x_43);
|
||||
lean_ctor_set(x_82, 2, x_89);
|
||||
lean_ctor_set(x_82, 1, x_89);
|
||||
|
|
@ -4945,7 +4955,7 @@ lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94;
|
|||
x_91 = lean_ctor_get(x_82, 0);
|
||||
lean_inc(x_91);
|
||||
lean_dec(x_82);
|
||||
x_92 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_92 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
x_93 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_93, 0, x_91);
|
||||
lean_ctor_set(x_93, 1, x_92);
|
||||
|
|
@ -4980,7 +4990,7 @@ if (lean_is_exclusive(x_95)) {
|
|||
lean_dec_ref(x_95);
|
||||
x_98 = lean_box(0);
|
||||
}
|
||||
x_99 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_99 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
if (lean_is_scalar(x_98)) {
|
||||
x_100 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
|
|
@ -5049,7 +5059,7 @@ x_123 = lean_ctor_get(x_118, 2);
|
|||
lean_dec(x_123);
|
||||
x_124 = lean_ctor_get(x_118, 1);
|
||||
lean_dec(x_124);
|
||||
x_125 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_125 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
lean_ctor_set(x_118, 3, x_43);
|
||||
lean_ctor_set(x_118, 2, x_125);
|
||||
lean_ctor_set(x_118, 1, x_125);
|
||||
|
|
@ -5065,7 +5075,7 @@ lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130;
|
|||
x_127 = lean_ctor_get(x_118, 0);
|
||||
lean_inc(x_127);
|
||||
lean_dec(x_118);
|
||||
x_128 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_128 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
x_129 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_129, 0, x_127);
|
||||
lean_ctor_set(x_129, 1, x_128);
|
||||
|
|
@ -5100,7 +5110,7 @@ if (lean_is_exclusive(x_131)) {
|
|||
lean_dec_ref(x_131);
|
||||
x_134 = lean_box(0);
|
||||
}
|
||||
x_135 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_135 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
if (lean_is_scalar(x_134)) {
|
||||
x_136 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
|
|
@ -5206,7 +5216,7 @@ if (lean_is_exclusive(x_157)) {
|
|||
lean_dec_ref(x_157);
|
||||
x_161 = lean_box(0);
|
||||
}
|
||||
x_162 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_162 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
if (lean_is_scalar(x_161)) {
|
||||
x_163 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
|
|
@ -5283,7 +5293,7 @@ if (lean_is_exclusive(x_180)) {
|
|||
lean_dec_ref(x_180);
|
||||
x_184 = lean_box(0);
|
||||
}
|
||||
x_185 = l_Lean_Parser_antiquotNestedExpr___closed__1;
|
||||
x_185 = l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1;
|
||||
if (lean_is_scalar(x_184)) {
|
||||
x_186 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
|
|
@ -12588,7 +12598,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__3;
|
||||
x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -12634,7 +12644,7 @@ if (lean_obj_tag(x_8) == 0)
|
|||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_9 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__1;
|
||||
x_10 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
x_10 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
x_11 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__6;
|
||||
lean_inc(x_1);
|
||||
x_12 = l_Lean_Parser_unicodeSymbolFnAux(x_9, x_10, x_11, x_1, x_7);
|
||||
|
|
@ -12674,19 +12684,18 @@ return x_22;
|
|||
lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__1;
|
||||
x_3 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11;
|
||||
x_4 = l_Lean_Parser_unicodeSymbolInfo(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___elambda__1___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
|
||||
x_3 = l_Lean_Parser_unicodeSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_antiquotNestedExpr___closed__3;
|
||||
x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_PrettyPrinter_Parenthesizer_depArrow_x27___closed__1;
|
||||
|
|
@ -13322,6 +13331,8 @@ l_Lean_PrettyPrinter_Parenthesizer_monadQuotation___closed__4 = _init_l_Lean_Pre
|
|||
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_monadQuotation___closed__4);
|
||||
l_Lean_PrettyPrinter_Parenthesizer_monadQuotation = _init_l_Lean_PrettyPrinter_Parenthesizer_monadQuotation();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_monadQuotation);
|
||||
l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___lambda__1___closed__1);
|
||||
l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___closed__1();
|
||||
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___closed__1);
|
||||
l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_visitAntiquot___closed__2();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue