Leonardo de Moura
|
6b8de16ede
|
feat: simplify notation command and allow strLit
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
6ff732f698
|
refactor: move notation comands to Syntax.lean
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
d9c6624a0a
|
feat: add support for trailing syntax
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
42642a2890
|
fix: new_frontend command issue
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
ef4f50d6d5
|
fix: include macroStack and use getBetterRef when reporting IO errors
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
8963090142
|
chore: reduce code duplication
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
b9c161b30c
|
feat: elaborate macro command
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
c5ab63a92b
|
refactor: move MonadQuotation to LeanInit, add MacroM
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
99aca85ac7
|
refactor: move declarations used at macro command to LeanInit
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
f280ad401a
|
chore: add trace class `Elab.definition
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
e0bcd9ac13
|
refactor: LeanExt => LeanInit
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
b2b22fbe42
|
chore: fix bogus "too many explicit universe levels" error message
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
14310f4d5b
|
chore: improve error message
|
2020-01-15 20:53:23 -08:00 |
|
Leonardo de Moura
|
6835070447
|
feat: add macro parser
|
2020-01-15 20:53:23 -08:00 |
|
Sebastian Ullrich
|
b1a59bb1cf
|
refactor: simplify quoteSyntax
|
2020-01-15 17:47:08 +01:00 |
|
Leonardo de Moura
|
b14c7cb69b
|
feat: allow user to set nodeKind at syntax command
|
2020-01-14 18:51:31 -08:00 |
|
Leonardo de Moura
|
9f14a45cef
|
fix: Level parser
|
2020-01-14 18:43:42 -08:00 |
|
Leonardo de Moura
|
664172d266
|
feat: elaborate syntax command
|
2020-01-14 18:18:43 -08:00 |
|
Leonardo de Moura
|
570ae2ff0e
|
feat: add mkFreshKind
|
2020-01-14 18:07:14 -08:00 |
|
Leonardo de Moura
|
c889d0ce48
|
fix: infixR helper only works for termParsers
|
2020-01-14 18:06:57 -08:00 |
|
Leonardo de Moura
|
e7db119948
|
feat: add HasQuote for Option
|
2020-01-14 18:03:33 -08:00 |
|
Leonardo de Moura
|
35213b63ae
|
fix: bootstrapping issues
We need `Name` `mkNameStr` available in the environment to define
`syntax` command.
|
2020-01-14 18:02:39 -08:00 |
|
Leonardo de Moura
|
5eebbc7bda
|
chore: remove unnecessary attributes
If one day we add elaboration functions for level and syntax, then we
can add them back.
|
2020-01-14 14:34:30 -08:00 |
|
Leonardo de Moura
|
2d83d49341
|
refactor: add Elab/Syntax.lean
|
2020-01-14 14:22:55 -08:00 |
|
Leonardo de Moura
|
abc6bc1447
|
chore: use try to fix : overload
|
2020-01-14 14:19:44 -08:00 |
|
Leonardo de Moura
|
ab8cbdc7e0
|
feat: improve syntax rules
|
2020-01-14 14:15:48 -08:00 |
|
Leonardo de Moura
|
b057f55e52
|
chore: add missing rules
|
2020-01-14 14:01:40 -08:00 |
|
Leonardo de Moura
|
17811a9286
|
feat: add syntax parsers
|
2020-01-14 13:50:06 -08:00 |
|
Leonardo de Moura
|
dd2936d28e
|
chore: move helper functions to Parser.lean
|
2020-01-14 13:33:20 -08:00 |
|
Leonardo de Moura
|
15a2d7d8ca
|
chore: tacticSymbol ==> nonReservedSymbol
|
2020-01-14 13:08:38 -08:00 |
|
Leonardo de Moura
|
ad0792f6c9
|
feat: add syntax category
|
2020-01-14 12:34:45 -08:00 |
|
Leonardo de Moura
|
a88dca17bc
|
chore: style
|
2020-01-14 08:51:50 -08:00 |
|
Daniel Selsam
|
4a0d8b475c
|
doc: try naming result type
|
2020-01-14 08:49:41 -08:00 |
|
Leonardo de Moura
|
e9d1014d63
|
feat: add ParserDescrCore.tacticSymbol constructor
|
2020-01-13 16:54:52 -08:00 |
|
Leonardo de Moura
|
aedd59258b
|
fix: missing file
|
2020-01-13 16:52:12 -08:00 |
|
Leonardo de Moura
|
2f5f00ed4f
|
feat: improve leadingIdentAsSymbol trick
|
2020-01-13 16:42:49 -08:00 |
|
Leonardo de Moura
|
397addb958
|
doc: leadingIdentAsSymbol trick
|
2020-01-13 16:38:12 -08:00 |
|
Leonardo de Moura
|
983579c0cf
|
feat: enable leadingIdentAsSymbol for tactic category
|
2020-01-13 16:20:34 -08:00 |
|
Leonardo de Moura
|
e98507023e
|
feat: basic tactic parser
|
2020-01-13 16:07:48 -08:00 |
|
Leonardo de Moura
|
b8146cc235
|
feat: add leadingIdentAsSymbol to ParserCategory
|
2020-01-13 16:07:21 -08:00 |
|
Leonardo de Moura
|
340d5f01f5
|
chore: symbolOrIdent ==> nonReservedSymbol
|
2020-01-13 14:32:34 -08:00 |
|
Leonardo de Moura
|
2b1869790c
|
feat: add tactic parser attributes
|
2020-01-13 13:00:19 -08:00 |
|
Simon Hudon
|
dd6e95c718
|
fix: lowercase error messages
|
2020-01-12 11:05:48 -08:00 |
|
Sebastian Ullrich
|
2e5f62d44f
|
test: parser/macro macros
|
2020-01-12 10:32:27 -08:00 |
|
Sebastian Ullrich
|
586f515470
|
fix: global name resolution of macro-introduced idents
|
2020-01-12 10:32:27 -08:00 |
|
Sebastian Ullrich
|
3f63635388
|
refactor: use adaptExpander in Elab.Quotation
|
2020-01-12 10:32:27 -08:00 |
|
Sebastian Ullrich
|
05d216beb0
|
feat: command elaboration step trace
|
2020-01-12 10:32:27 -08:00 |
|
Sebastian Ullrich
|
8d021e0cec
|
fix: fresh macro scope per command
|
2020-01-12 10:32:27 -08:00 |
|
Sebastian Ullrich
|
82078fba84
|
chore: make Syntax.reprint output without source info more readable
|
2020-01-12 10:32:27 -08:00 |
|
Sebastian Ullrich
|
c08fcdb662
|
chore: ad-hoc match_syntax support in the new frontend
|
2020-01-12 10:32:27 -08:00 |
|