Leonardo de Moura
c33cd11be1
feat: add CoeHead and CoeTail to minimize nontermination
...
The adventure continues.
cc @Kha @dselsam
2020-01-28 18:20:58 -08:00
Leonardo de Moura
a7de10a74a
feat: add support for CoeFun in the new elaborator
...
cc @kha
2020-01-28 16:50:53 -08:00
Leonardo de Moura
4aa710d4a6
feat: add bridge Coe + HasNat transitivity instance
...
cc @kha @dselsam
2020-01-28 16:17:14 -08:00
Leonardo de Moura
8c7aade7b6
feat: add coercion tests
2020-01-28 15:52:04 -08:00
Leonardo de Moura
e9e4dfe1ff
feat: add new Coe.lean
2020-01-28 13:10:30 -08:00
Leonardo de Moura
07bfeab6be
feat: add CoeFun and CoeSort to new Coe prototype
2020-01-28 12:57:14 -08:00
Leonardo de Moura
bb1a90b24d
chore: fix tests
2020-01-28 10:34:27 -08:00
Leonardo de Moura
642509229f
feat: split Coe and CoeDep
...
Motivation: control term size.
```lean
synth CoeT Nat 0 (Option (Option (Option (Option (Option Nat)))))
```
is much smaller with the new encoding
2020-01-28 09:48:18 -08:00
Leonardo de Moura
a272670ead
test: new instances
2020-01-27 21:23:14 -08:00
Leonardo de Moura
9b6dfa71a2
test: new Coe prototype
2020-01-27 20:33:10 -08:00
Sebastian Ullrich
9065ce55a8
chore: ignore test output files
2020-01-27 13:08:57 +01:00
Leonardo de Moura
ac5eaa4d7d
test: overload builtin notation
2020-01-26 14:00:41 -08:00
Leonardo de Moura
cde1399a01
test: overloaded syntax
2020-01-26 13:57:13 -08:00
Leonardo de Moura
e52c4291cc
feat: allow macro_rules block with different syntax node kinds
2020-01-26 08:39:40 -08:00
Leonardo de Moura
43df63e594
chore: remove unnecessary |s from test
2020-01-25 20:24:22 -08:00
Leonardo de Moura
d0d3e24975
chore: fix tests
2020-01-25 20:14:50 -08:00
Leonardo de Moura
1512ccfdc8
chore: reacticate where elaboration
2020-01-25 20:11:42 -08:00
Leonardo de Moura
5b8e713150
chore: minor
2020-01-25 19:35:18 -08:00
Leonardo de Moura
901fcddf89
chore: first | is now optional at macro_rules
...
cc @Kha
2020-01-25 19:34:44 -08:00
Leonardo de Moura
19e4c30542
feat: elaborate new let decl
...
We can now write
```lean
syntax "case!" ident ":" term "with" term "," term : term
macro_rules
| `(case! $h : $c with $t, $e) => `(let $h := $c; cond $h $t $e)
```
Before the series of commits to change `let` syntax, the
quasiquotation `(let $h := $c; cond $h $t $e)
produced the weird error message "`;` expected" at ":=".
The problem was that $h was matching the now deleted "nonterminal"
```lean
def letIdDecl := parser! try (letIdLhs >> " := ") >> termParser
```
This was not a bug, but a side-effect on how the `let` syntax was
declared.
cc @kha
2020-01-25 16:32:21 -08:00
Leonardo de Moura
993ae96fb7
chore: elaborate let_core
2020-01-25 15:21:47 -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
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
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
a4858bf9f9
Revert "feat: MonadIO now extends MonadExcept IO.Error"
...
This reverts commit c0a7495495
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
Leonardo de Moura
850729ba1b
chore: fix tests
2020-01-24 17:32:21 -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
060a68d73f
feat: remove addMacroScope approximation
2020-01-23 14:59:31 -08:00
Leonardo de Moura
0c1c4ea9cc
chore: update expected output
2020-01-23 11:52:03 -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
53e64e4e44
test: bigop test
2020-01-22 13:22:29 -08:00
Leonardo de Moura
e8c54ad1bf
fix: use nonReservedSymbol when defining tactic new syntax
2020-01-21 14:37:29 -08:00
Leonardo de Moura
4f0dc252ae
test: add extensible macro example
2020-01-21 14:05:21 -08:00
Leonardo de Moura
2b63aa27d3
chore: use new_frontend in the whole test
2020-01-21 09:16:38 -08:00
Leonardo de Moura
7e61315e6d
chore: fix tests
2020-01-20 22:26:07 -08:00
Leonardo de Moura
47c85cc351
fix: bug at ParserDescr.ident
2020-01-20 21:55:16 -08:00
Leonardo de Moura
1dbfc4b337
fix: add checkNoWsBefore before option * in mkAntiquot
...
@kha we need it, otherwise we can't process rules such as
```
| `(FOO $t >>> $r) => `($t * $r)
```
without adding parenthesis at `(($t) * $r)
2020-01-20 21:48:40 -08:00
Leonardo de Moura
98033f298f
feat: add support for simple category
2020-01-20 20:55:54 -08:00
Leonardo de Moura
c89972b6e2
chore: test
2020-01-20 18:53:54 -08:00
Sebastian Ullrich
129442a76a
fix: syntax: do not qualify fresh kinds
2020-01-20 14:58:58 -08:00
Leonardo de Moura
481665422f
chore: fix test
2020-01-20 14:55:27 -08:00
Leonardo de Moura
4d57790cc5
fix: add workaround for setting correct LBP for $ in antiquotations
2020-01-20 10:42:58 -08:00
Leonardo de Moura
b5fc9c19fe
feat add evalIntros
2020-01-19 17:48:19 -08:00
Simon Hudon
c0a7495495
feat: MonadIO now extends MonadExcept IO.Error
2020-01-19 17:23:37 -08:00
