Leonardo de Moura
8fe1c495eb
chore: update stage0
2020-01-24 12:38:53 -08:00
Leonardo de Moura
364bb7bdf7
fix: proper Name literals
...
cc @kha
2020-01-24 12:38:15 -08:00
Leonardo de Moura
4425feaebb
chore: fix tests
2020-01-23 16:08:52 -08:00
Simon Hudon
95f951bdf2
fix: test files
2020-01-23 16:07:29 -08:00
Leonardo de Moura
addbb8dd67
fix: redirect
...
@cipher1024 I modified your fix. It would produce memory leaks if the
code executed by #eval modifies the stdout.
Here is the problem.
- Your replaces the handler with some new handler `H` and stores the
old handler `O` in a `flet`.
- Code is executed and replaces the stdout handler with `H'`. The `H`s RC is
decremented and `H'`s RC is incremeneted. So far, so good.
- Now, the destructor of your `flet` is executed, and it replaces `H'`
with `O`, but `H'` RC is not decremented.
2020-01-23 15:58:34 -08:00
Simon Hudon
123577126c
fix: #eval redirection of stdout
2020-01-23 15:44:49 -08:00
Leonardo de Moura
35179809a2
feat: hide macro scopes encoding when displaying errors
2020-01-23 15:33:02 -08:00
Leonardo de Moura
3cb1d01130
chore: update stage0
2020-01-23 15:01:09 -08:00
Leonardo de Moura
060a68d73f
feat: remove addMacroScope approximation
2020-01-23 14:59:31 -08:00
Leonardo de Moura
ed6cb007d0
refactor: ExtractMacroScopesResult => MacroScopesView, add MacroScopesView.review
2020-01-23 14:11:32 -08:00
Leonardo de Moura
7662548517
chore: update stage0
2020-01-23 13:06:34 -08:00
Leonardo de Moura
c309f1dccd
chore: remove unnecessary field
2020-01-23 13:05:27 -08:00
Leonardo de Moura
b47caaa0a5
refactor: notation and macro commands are now just macros
2020-01-23 13:04:21 -08:00
Leonardo de Moura
0abf1f04a7
chore: update stage0
2020-01-23 12:54:45 -08:00
Leonardo de Moura
9359a6569a
feat: add [builtinMacro]
2020-01-23 12:54:04 -08:00
Leonardo de Moura
954c69de35
feat: use macroscopes for creating fresh kinds
2020-01-23 12:38:31 -08:00
Leonardo de Moura
d99ef11447
fix: nested addMacroScope
2020-01-23 12:36:37 -08:00
Leonardo de Moura
09a482a2b4
chore: update stage0
2020-01-23 12:23:22 -08:00
Leonardo de Moura
e681bd71d9
feat: simplify MacroM
2020-01-23 12:22:33 -08:00
Leonardo de Moura
8e9b18396d
chore: udpate stage0
2020-01-23 12:13:43 -08:00
Leonardo de Moura
0228f9c9b7
chore: remove addMacroScopeExt
2020-01-23 12:08:20 -08:00
Leonardo de Moura
0a59e53265
chore: update stage0
2020-01-23 12:03:20 -08:00
Leonardo de Moura
6fdcb1c192
chore: prepare to remove addMacroScopeExt
2020-01-23 12:02:45 -08:00
Leonardo de Moura
0c1c4ea9cc
chore: update expected output
2020-01-23 11:52:03 -08:00
Leonardo de Moura
aef998af72
chore: update stage0
2020-01-23 11:47:07 -08:00
Leonardo de Moura
4ef8aa347a
feat: missing case
2020-01-23 11:46:29 -08:00
Leonardo de Moura
981d4733f3
chore: update stage0
2020-01-23 11:33:36 -08:00
Leonardo de Moura
fab256d4cc
feat: improve macroscope encoding
2020-01-23 11:33:35 -08:00
Leonardo de Moura
87d002bb43
feat: extend MacroM
...
It now has access to `mainModule` and a name generator.
2020-01-23 09:48:37 -08:00
Leonardo de Moura
98ee6e9734
refactor: move NameGenerator to LeanInit
2020-01-23 08:49:58 -08:00
Leonardo de Moura
670243400b
chore: update stage0
2020-01-22 20:15:29 -08:00
Leonardo de Moura
67535441ad
fix: macroTail issue
...
cc @Kha
2020-01-22 20:14:09 -08:00
Leonardo de Moura
083999d337
chore: update stage0
2020-01-22 17:33:25 -08:00
Leonardo de Moura
764b854742
fix: bug at longestMatchStep
...
@Kha I found the bug by accident when I was playing with the
bigop.lean
2020-01-22 17:31:54 -08:00
Leonardo de Moura
3f24b31286
chore: remove leftover
2020-01-22 16:50:05 -08:00
Leonardo de Moura
1ff7950a77
feat: use truncateTrailing at error messages
2020-01-22 16:19:07 -08:00
Leonardo de Moura
ae84270226
feat: include result of sequence of macro expansions
...
@Kha I added this feature to help debugging macros.
I was using `set_option trace.Elab true` as a workaround, but it is
too verbose.
For example, in the following buggy code
```
new_frontend
macro "foo" x:term : term => `(x + 1)
macro "bla" x:term : term => `(foo $x)
```
We get the error message
```
<input>:6:11: error: unknown identifier 'x.15'
with resulting expansion
x + 1
while expanding
foo 1
while expanding
bla 1
```
Perhaps we should preserve the macroscopes at "with resulting
expansion". Anyway, I think it is better than the previous error.
```
<input>:6:11: error: unknown identifier 'x.15'
while expanding
foo 1
while expanding
bla 1
```
2020-01-22 16:08:07 -08:00
Leonardo de Moura
4c53dfa8a7
chore: typo
2020-01-22 14:24:32 -08:00
Leonardo de Moura
c9e9208ea2
feat: cleanup bigop example
2020-01-22 14:22:34 -08:00
Leonardo de Moura
c9474c1883
feat: add more examples
...
cc @Kha
2020-01-22 14:09:45 -08:00
Leonardo de Moura
37e83651f0
fix: postpone synthesizeUsingDefault
2020-01-22 14:09:05 -08:00
Leonardo de Moura
e57289f98e
feat: handle new HasOfNat.ofNat at evalNat
2020-01-22 13:55:13 -08:00
Leonardo de Moura
c1861765aa
fix: workaround for new_frontend keyword
2020-01-22 13:34:02 -08:00
Leonardo de Moura
53e64e4e44
test: bigop test
2020-01-22 13:22:29 -08:00
Leonardo de Moura
a7a36f80bb
feat: add termIdToAntiquot
2020-01-22 13:18:09 -08:00
Leonardo de Moura
ff43704411
chore: update stage0
2020-01-22 12:59:33 -08:00
Leonardo de Moura
5193ce45e4
refactor: move Syntax helper functions to LeanInit
2020-01-22 12:58:06 -08:00
Leonardo de Moura
a5bcebb07f
feat: add antiquotation support for strLit, numLit and charLit
2020-01-22 12:57:28 -08:00
Leonardo de Moura
0be31c14ec
fix: workaround for term parser antiquotation issue
...
@Kha this is a temporary workaround. We should discuss how to cleanup
in the next Dev meeting.
2020-01-22 12:05:12 -08:00
Leonardo de Moura
642850efb2
fix: antiquotation for all categories
2020-01-22 11:52:08 -08:00
