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

refactor: split term/command quotations

Browse source
This commit is contained in:
Sebastian Ullrich 2022-04-15 14:40:16 +02:00 • committed by Leonardo de Moura
parent ca8fdcaa0c
commit a2baf2cb96
3 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/Quotation.lean
View file

@ -194,6 +194,7 @@ elab_stx_quot Parser.Term.attr.quot
elab_stx_quot Parser.Term.prio.quot
elab_stx_quot Parser.Term.doElem.quot
elab_stx_quot Parser.Term.dynamicQuot
elab_stx_quot Parser.Command.quot
/- match -/

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

@ -9,17 +9,19 @@ import Lean.Parser.Do
namespace Lean
namespace Parser
/--
Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like
`` `($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). -/
-- TODO: use two separate quotation parsers with parser priorities instead
@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth (termParser <|> many1Unbox commandParser) >> ")"
/-- Syntax quotation for terms. -/
@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth termParser >> ")"
@[builtinTermParser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
namespace Command
/--
Syntax quotation for (sequences of) commands. The identical syntax for term quotations takes priority, so ambiguous quotations like
`` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.
Multiple commands 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 low] def quot := leading_parser "`(" >> incQuotDepth (many1Unbox commandParser) >> ")"
/--
A mutual block may be broken in different cliques, we identify them using an `ident` (an element of the clique)
We provide two kinds of hints to the termination checker:

2
tests/lean/StxQuot.lean.expected.out
View file

@ -1,4 +1,4 @@
StxQuot.lean:8:12: error: expected command, identifier or term
StxQuot.lean:8:12: error: expected identifier or term
"`Nat.one._@.UnhygienicMain._hyg.1"
"<missing>"
"<missing>"