Leonardo de Moura
dcf0ae2a33
chore: update stage0
2020-01-25 16:23:39 -08:00
Leonardo de Moura
eb8e7b9f3d
feat: add new let syntax
...
It avoids hidden nonterminals, and store the equation case as a
separate rule. It would be great if we could have 3 independent rules,
but this is not possible because `longestMatch` would return a choice
for terms as simple as `let x := v; ...` The problem is that it is
both a `letSimpleDecl` and a `letPatDecl`. We resolve the ambiguity at
the parsing level using `<|>`.
cc @Kha
2020-01-25 16:15:30 -08:00
Leonardo de Moura
31f8b281c2
chore: update stage0
...
We are now ready to change `let` syntax
2020-01-25 15:38:49 -08:00
Leonardo de Moura
b708407b7b
chore: implement Quotation.lean using let_core, disable let syntax
2020-01-25 15:34:24 -08:00
Leonardo de Moura
618d0d0ce3
chore: update stage0
2020-01-25 15:25:22 -08:00
Leonardo de Moura
993ae96fb7
chore: elaborate let_core
2020-01-25 15:21:47 -08:00
Leonardo de Moura
2ae231cc65
chore: update stage0
2020-01-25 15:15:05 -08:00
Leonardo de Moura
5796eba368
chore: add elabLetDeclAux
2020-01-25 15:14:28 -08:00
Leonardo de Moura
58833e6f79
chore: add let_core
...
We want to change the representation of `let` terms.
`let_core` is a temporary syntax for helping us with the translation.
2020-01-25 15:08:36 -08:00
Leonardo de Moura
bdb9f4c86e
feat: allow raw identifiers to be used where terms are expected
...
@Kha this commit fix another example of weird error message I have
experienced in the last few days.
The macro
```lean
syntax "case!" ident ":" term "with" term "," term : term
macro_rules
| `(case! $h : $cond with $t, $e) =>
`((fun $h => cond $h $t $e) $cond)
```
is accepted, but as in `fun` binders, we get a weird error when
trying to elaborate an instance of the macro.
Example:
```lean
check case! h : 0 == 0 with h, not h
```
2020-01-25 14:55:32 -08:00
Leonardo de Moura
0d0f2f7c96
chore: update stage0
2020-01-25 14:55:32 -08:00
Leonardo de Moura
7b6caba457
feat: add `ident as a valid elaboration kind
2020-01-25 14:55:32 -08:00
Leonardo de Moura
6d5de9f965
feat: handle raw identifiers as binders in fun
...
@Kha I am adding this kind of feature to improve the user experience.
For example, the macro
```
syntax "[" ident "↦" term "]" : term
macro_rules
| `([$x ↦ $v]) => `(fun $x => $v)
```
is accepted and looks perfectly reasonable.
However, before this commit, we would get a nasty error when
elaborating
```lean
check [x ↦ x + 1]
```
2020-01-25 14:55:21 -08:00
Sebastian Ullrich
1bf63f18ec
chore: update stage0
2020-01-25 16:42:16 +01:00
Sebastian Ullrich
2509b3913a
Revert "feat: add std streams"
...
This reverts commit 7575a32035
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
0be2424910
Revert "feat: override standard streams"
...
This reverts commit bd87ea5d5e
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
b760692a26
Revert "fix: thread local storage of std streams"
...
This reverts commit 961861ceab
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
a4858bf9f9
Revert "feat: MonadIO now extends MonadExcept IO.Error"
...
This reverts commit c0a7495495
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
58313a050a
Revert "fix: #eval redirection of stdout"
...
This reverts commit 123577126c
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
ad29568051
Revert "fix: redirect"
...
This reverts commit addbb8dd67
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
e82add884f
Revert "fix: test files"
...
This reverts commit 95f951bdf2
2020-01-25 16:32:06 +01:00
Sebastian Ullrich
88fe0de284
fix: default LEAN_PATH for installed Lean
2020-01-25 15:58:06 +01:00
Sebastian Ullrich
5c0fa84af5
feat: barely implement do elaboration
2020-01-25 15:57:41 +01:00
Sebastian Ullrich
df3fc8c147
chore: fix nix-build by disabling ccache for now
2020-01-25 15:26:59 +01:00
Sebastian Ullrich
02c773bc70
refactor: further Quotation cleanup
2020-01-25 13:47:27 +01:00
Sebastian Ullrich
093518725c
refactor: minor cleanups for standalone expander
2020-01-25 11:58:29 +01:00
Leonardo de Moura
850729ba1b
chore: fix tests
2020-01-24 17:32:21 -08:00
Leonardo de Moura
26d8874607
chore: update stage0
2020-01-24 17:24:02 -08:00
Leonardo de Moura
aa045f3b07
feat: safer mkCIdentFrom
...
cc @Kha
2020-01-24 17:23:21 -08:00
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
