Leonardo de Moura
74f48414f1
feat: add option --exitOnPanic (short version -e)
...
Lean does not exit on panic anymore.
The old behavior (`std::exit(1)`) produces a horrible debugging
experience for the elaborator since all trace messages are lost.
The new command line option restores the old behavior.
cc @Kha @dselsam
2019-12-19 09:24:37 -08:00
Leonardo de Moura
49bdbf7eb2
chore: style
2019-12-19 08:43:17 -08:00
Leonardo de Moura
76d351d830
refactor: split Elab/Term.lean into smaller files
2019-12-19 07:26:54 -08:00
Leonardo de Moura
f334e7e89c
chore: cleanup and remove Array.getA
2019-12-19 07:09:51 -08:00
Leonardo de Moura
1c459a6fb0
refactor: use match_syntax to implement expandCDot
2019-12-19 06:34:52 -08:00
Sebastian Ullrich
a2e0f1e6b1
refactor: simplify quotations
2019-12-19 10:59:20 +01:00
Sebastian Ullrich
88a924b728
feat: support (almost) proper name resolution in quotations in the old frontend
2019-12-18 20:11:45 -08:00
Sebastian Ullrich
c07b7e7958
fix: lookup of locals with numeric name parts
2019-12-18 20:11:14 -08:00
Sebastian Ullrich
eac0c3e168
fix: use new literal representations in HasQuote
2019-12-18 20:11:14 -08:00
Leonardo de Moura
6cc928d180
test: add postpone test
2019-12-18 20:04:38 -08:00
Leonardo de Moura
a2d38a7ef3
doc: Elab/Term.lean
2019-12-18 19:42:05 -08:00
Leonardo de Moura
00cc28096c
feat: add support for postponing elabTerm
2019-12-18 11:05:02 -08:00
Leonardo de Moura
a3ae2aabb2
chore: use new antiquotation notation
2019-12-17 15:30:17 -08:00
Leonardo de Moura
37b2393479
chore: change antiquotation symbol
2019-12-17 15:24:12 -08:00
Leonardo de Moura
f09e2ab069
feat: elabParen using match_syntax
2019-12-17 14:55:40 -08:00
Leonardo de Moura
a1373d68c9
fix: fun (_ : A) => ... notation
2019-12-17 14:28:48 -08:00
Leonardo de Moura
35aa0faec5
chore: style
2019-12-17 14:16:40 -08:00
Leonardo de Moura
60b5810a10
feat: elaborate fun with patterns
2019-12-17 14:11:44 -08:00
Leonardo de Moura
f6d9f4029e
feat: elaborate cdot
2019-12-17 13:41:46 -08:00
Leonardo de Moura
1b6319788e
feat: elaborate parenSpecial
2019-12-17 13:32:46 -08:00
Leonardo de Moura
746782a99b
chore: add withMacro
2019-12-17 13:19:39 -08:00
Sebastian Ullrich
1c566a86f0
doc: comment on scp
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
5de274781b
refactor: remove broken support for nested antiquotations
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
f7a12ab132
doc: Hygiene.lean
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
0e3f6fa3aa
doc: add comments on syntax quotation elab
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
e54d96ad5b
chore: avoid let-bindings match_syntax RHSs for now because of elaboration issues
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
71f569e9b9
feat: implement antiquotation kinds %%e:k and splices %%e*
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
086bcae041
refactor: quoteSyntax: use TermElabM
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
6a2dbad53f
feat: match_syntax support in the old parser
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
e8944fcf9d
feat: implement match_syntax
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
53276e99dc
feat: implement proper macro scope handling for TermElabM
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
de091d1eef
feat: use addMacroScope in syntax quotation terms
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
2310ec2413
chore: separate C++ calls for parsing & expansion
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
76eb7ad205
feat: handle nested quotation-antiquotations
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
6dac30d8c3
feat: extend MonadQuotation and make Unhygienic at least a locally correct implementation
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
5db6ebed32
refactor: add HasQuote class
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
88bbae29fe
refactor: use TermElab in quotation expander, polish Unhygienic story
2019-12-17 12:16:34 -08:00
Sebastian Ullrich
027b3921b3
fix: don't panic on unsupported antiquotation content
2019-12-17 12:16:13 -08:00
Sebastian Ullrich
b5e5a02c8d
refactor: use quotation terms in quotation term elaborator
2019-12-17 12:16:13 -08:00
Leonardo de Moura
2e8b7b2461
feat: expanding cdot notation
2019-12-17 12:09:41 -08:00
Leonardo de Moura
3d6146756f
feat: elaborate lambda abstractions
2019-12-17 11:44:40 -08:00
Leonardo de Moura
d9d1c67d86
feat: add cdot notation detection
...
We need `fun` elaboration.
2019-12-17 10:21:39 -08:00
Leonardo de Moura
d3da0abc8a
chore: style
2019-12-17 10:21:20 -08:00
Leonardo de Moura
9760ddfd92
feat: add new kind
2019-12-17 10:21:03 -08:00
Leonardo de Moura
1b9fb2f726
fix: elabNum
2019-12-16 17:51:29 -08:00
Leonardo de Moura
c5d2b06037
feat: add decLevel?
2019-12-16 17:32:35 -08:00
Leonardo de Moura
e922f8a46c
feat: split synthetic into synthetic and syntheticOpaque
2019-12-16 17:06:45 -08:00
Leonardo de Moura
827c0c3294
doc: update synthetic metavariable comment
2019-12-16 11:50:27 -08:00
Leonardo de Moura
4eb6f67e7a
chore: style
2019-12-16 10:48:54 -08:00
Leonardo de Moura
0ca5239de9
chore: Field ==> LVal
2019-12-16 10:47:31 -08:00
