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
2a89bcd931
feat: use Coe in the new frontend
2020-01-28 15:51:36 -08:00
Leonardo de Moura
d3cb5b832c
fix: handle delayed assignments at isDefEqQuick
2020-01-28 15:09:16 -08:00
Leonardo de Moura
2df230e7a8
feat: missing instance
2020-01-28 14:09:04 -08:00
Leonardo de Moura
a9c06230b2
chore: update stage0
2020-01-28 13:11: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
2efdeda903
fix: bug at preprocessArgs
2020-01-28 12:56:01 -08:00
Leonardo de Moura
9eb1723680
fix: outParam support
2020-01-28 11:13:32 -08:00
Leonardo de Moura
ef51d6c2ab
chore: improve error message
2020-01-28 10:56: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
7809274c3a
chore: Coe.lean ==> HasCoe.lean
2020-01-28 08:55:22 -08:00
Leonardo de Moura
ef105ba49d
chore: remove coe functions
...
They will be used in the new `Coe` file
2020-01-28 08:49:02 -08:00
Leonardo de Moura
5083ecffcc
chore: update stage0
2020-01-28 08:46:50 -08:00
Leonardo de Moura
5ca71f48ca
chore: make sure Quotation.lean does not depend on old coe
2020-01-28 08:39:36 -08:00
Leonardo de Moura
22c42ec1d8
chore: remove unnecessary method
2020-01-28 08:24:35 -08:00
Leonardo de Moura
f0f522a6d6
chore: prepare to rename old coe primitives
2020-01-28 08:18:56 -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
244382f49c
chore: reintroduce accidentally dropped withMacroExpansion
2020-01-27 16:43:18 +01:00
Sebastian Ullrich
88b09315f1
chore: better error message on missing import
...
The macOS CI build rarely, randomly fails with a "failed to lock file" message.
This commit will not fix this error, but at least should make it clearer whether
the file actually cannot be locked or is just missing.
/cc @leodemoura
2020-01-27 13:09:01 +01:00
Sebastian Ullrich
9065ce55a8
chore: ignore test output files
2020-01-27 13:08:57 +01:00
Sebastian Ullrich
c805eb87e6
refactor: elabAnoymousCtor: align more closely to the paper
2020-01-27 10:35:16 +01:00
Leonardo de Moura
254d29b4b7
chore: update stage0
2020-01-26 15:15:20 -08:00
Leonardo de Moura
145bd50903
feat: disallow patterns with choice nodes
...
@Kha Patterns with nested "choice" nodes produce counterintuitive
behavior, and hard to understand errors. They only work when we have
the exact same overloads at macro definition and application time.
Here is a funky example
```
syntax [myAdd] term "++":65 term:65 : term -- overloads "++"
/- The following `macro_rules` manages to eliminate "choice" node by using the
explicitly provided node kind. -/
macro_rules [myAdd] `($a ++ $b) => `($a + $b)
check (1:Nat) ++ 2 -- works as expected
syntax "FOO!" term : term
/- Before this commit, the following pattern was accepted,
and it contained a "choice" node for `++`. It is a `myAdd` or
`HasAppend.append`.
Now, this kind of pattern is rejected since it contains a nested
"choice" -/
macro_rules `(FOO! $a ++ $b) => `($a ++ $b)
/- Before this commit, the following command worked because
it contained a "choice" node similar to the one at macro definition
time. -/
check FOO! [1, 2] ++ [2, 3]
-- Now, we have 3 overloads for "++".
syntax [myAppend] term "++":65 term:65 : term
-- The `macro_rules` fails here.
```
This commit fixes this weird behavior by disallowing "choice" nodes in
patterns.
2020-01-26 15:13:14 -08:00
Leonardo de Moura
4e580e78bc
chore: update stage0
2020-01-26 15:13:14 -08:00
Leonardo de Moura
8525584a78
refactor: naming consistency ensure List and Array have similar find* methods
...
`find?` -> takes predicate
`findSome?` -> takes a function (A -> Option B)
2020-01-26 15:13:05 -08:00
Leonardo de Moura
ac5eaa4d7d
test: overload builtin notation
2020-01-26 14:00:41 -08:00
Leonardo de Moura
5ff63c2bc6
choice: better error message
2020-01-26 13:58:51 -08:00
Leonardo de Moura
cde1399a01
test: overloaded syntax
2020-01-26 13:57:13 -08:00
Leonardo de Moura
17d5453827
fix: elabTerm must be part of observing
2020-01-26 13:55:21 -08:00
Leonardo de Moura
7133d3fc84
feat: handle explicit node kinds in macro_rules, and handle choice kind
2020-01-26 09:39:46 -08:00
Leonardo de Moura
6a1712717f
chore: update stage0
2020-01-26 08:43:43 -08:00
Leonardo de Moura
02d31fb619
feat: allow user to specify intended syntax node kind at macro_rules
2020-01-26 08:43:05 -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
6a0208630e
feat: add sanity checking at macro_rules
2020-01-25 20:31:58 -08:00
Leonardo de Moura
43df63e594
chore: remove unnecessary |s from test
2020-01-25 20:24:22 -08:00
Leonardo de Moura
b0bcc1c2bb
chore: update stage0
2020-01-25 20:18:03 -08:00
Leonardo de Moura
f5630ae054
chore: remove let_core
2020-01-25 20:17:25 -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
ba16094e63
chore: update stage0
2020-01-25 20:01:01 -08:00
Leonardo de Moura
74bac15c6f
chore: make sure letDecl is a node
...
This is useful when defining notation such as `where`.
Moreover, it allows us to write `$d:letDecl`, but `$d` never matches
a `letDecl`
2020-01-25 19:56:53 -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
9f816277fc
feat: make sure letSimpleDecl and letPatDecl have the same #args
2020-01-25 19:08:16 -08:00
Leonardo de Moura
051fd530e0
chore: handle new let at toPreterm
2020-01-25 18:33:36 -08:00
