Gabriel Ebner
7356840cbc
feat: use sepBy1Indent for tactic blocks
2022-09-18 16:43:23 -07:00
Leonardo de Moura
90b9b0b7e9
chore: move compiler tests to run folder
2022-09-18 15:08:52 -07:00
Leonardo de Moura
05145577fd
feat: cache specialization results
2022-09-18 14:53:18 -07:00
Leonardo de Moura
db6ee72aed
chore: typo
2022-09-17 09:55:46 -07:00
Leonardo de Moura
50fe9ceeaa
test: more tests for new compiler
2022-09-16 18:00:27 -07:00
Leonardo de Moura
3c6dee8048
fix: LCNF eta expansion bug at Simp.lean
2022-09-16 18:00:27 -07:00
Leonardo de Moura
c16d4fb926
chore: fix test suite
2022-09-15 18:59:51 -07:00
Leonardo de Moura
d3b0b49c43
feat: improve elabBinRelCore
...
See new test and comments at `elaBinRelCore`
2022-09-15 15:17:57 -07:00
Mario Carneiro
eac410db4e
fix: fix tests
2022-09-15 14:02:38 -07:00
Yuri de Wit
bbc70c4cf0
fix: fixes #1599 by adding correct indentation
2022-09-15 13:11:51 -07:00
Leonardo de Moura
10a56bf4a1
fix: fixes #1571
...
The previous implementation was using the following heuristic
```lean
-- heuristic: use non-dependent arrows only if possible for whole group to avoid
-- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
let dependent := curNames.any fun n => hasIdent n.getId stxBody
```
The result produced by this heuristic was **not** producing an
accidental name capture, but I agree
it was confusing to have `∀ (a : True), ∃ a, a = a : Prop` instead of
`True → ∃ a, a = a : Prop` since there is no dependency.
AFAICT, all examples affected by this commit have a better output now.
cc @digma0 @kha
2022-09-15 11:16:16 -07:00
Leonardo de Moura
9e5a818de5
fix: bug at LCNF toDecl
2022-09-14 15:23:34 -07:00
Leonardo de Moura
00e269c93c
fix: throw error at ⟨..⟩ notation if constructor is private
2022-09-14 15:02:38 -07:00
Gabriel Ebner
f1b5fa53f0
chore: use new comment syntax
2022-09-14 08:26:17 -07:00
Leonardo de Moura
fccb60fb69
feat: support for [inlineIfReduce] at new compiler
2022-09-13 18:23:42 -07:00
Leonardo de Moura
e8246e026d
fix: bug at compatibleTypes
...
Many thanks to @hargoniX
2022-09-13 15:58:06 -07:00
Leonardo de Moura
8f2ab82408
fix: bug at bindCases
...
Many thanks to @hargoniX
2022-09-13 15:36:46 -07:00
Leonardo de Moura
7535c12bc5
test: add frontend meeting examples to test suite
2022-09-13 09:08:38 -07:00
Gabriel Ebner
b4af14d44a
fix: deindent docstrings with empty lines
2022-09-13 07:16:12 -07:00
Mario Carneiro
a0fcb660c5
feat: allow multiple source + no expected type
2022-09-13 07:09:08 -07:00
Mario Carneiro
adc215dab9
feat: support {s with ..}
2022-09-13 07:09:08 -07:00
Gabriel Ebner
d67546e388
chore: add test
2022-09-13 06:19:40 -07:00
Gabriel Ebner
ca28b0462c
feat: show all missing fields in structure instance
2022-09-13 06:19:40 -07:00
Mario Carneiro
3bb3efdedc
feat: allow optional type in example
2022-09-13 03:11:04 -07:00
Leonardo de Moura
b2d6caca0a
fix: inferProjType at LCNF
2022-09-12 18:27:14 -07:00
Leonardo de Moura
506cf01d94
fix: bug at simpCasesOnCtor?
2022-09-12 16:02:19 -07:00
Leonardo de Moura
59b4d977b5
chore: fix tests
2022-09-10 15:06:03 -07:00
Henrik Böving
a03ea65d73
refactor: monadic compiler test framework style + new pass manager
2022-09-10 15:00:05 -07:00
Leonardo de Moura
ca098d3769
feat: inline applications of the form inline (f ...)
...
The `inline` identity function is a directive for the compiler.
2022-09-10 13:28:49 -07:00
Leonardo de Moura
f1c150228b
fix: fixes #1558
2022-09-09 15:27:51 -07:00
Leonardo de Moura
353eb0dd27
fix: disable auto implicit feature when running tactics
...
fixes #1569
2022-09-09 15:17:50 -07:00
Leonardo de Moura
abf514378b
fix: fixes #1575
2022-09-09 15:05:21 -07:00
Leonardo de Moura
7c3826d3e9
fix: fixes #1576
2022-09-09 14:29:48 -07:00
Leonardo de Moura
16534bacc9
chore: re-activate test
2022-09-08 15:23:18 -07:00
Henrik Böving
5514339ffd
fix: visit jp bodies in join point finder
2022-09-08 15:21:53 -07:00
Leonardo de Moura
2ec7f14ca8
chore: temporarily disable test to fix build
2022-09-08 14:53:48 -07:00
Gabriel Ebner
fb259f95db
feat: remove description argument from register_simp_attr
2022-09-08 14:49:43 -07:00
Henrik Böving
576a4ec2c5
test: basic compiler tests for findJoinPoints
2022-09-08 14:09:14 -07:00
Henrik Böving
d2f7e724ac
feat: findJoinPoints pass
2022-09-08 14:09:14 -07:00
Leonardo de Moura
5c00708b7f
test: specialize attribute tests
2022-09-07 16:32:25 -07:00
Leonardo de Moura
f4fbf92313
fix: make privateToUserNameAux more robust
2022-09-06 17:15:56 -07:00
Leonardo de Moura
bf44e9fb2f
fix: bug at inferProjType for LCNF
2022-09-05 19:23:35 -07:00
Gabriel Ebner
213cb322be
chore: add test
2022-09-05 08:52:46 -07:00
Leonardo de Moura
34f3fcdee5
chore: fix test
2022-09-05 06:58:32 -07:00
Leonardo de Moura
d0600b3750
fix: incorrect binder name being used
...
cc @hargoniX
2022-09-04 16:56:42 -07:00
Leonardo de Moura
01ca711859
feat: add PullFunDecls.lean
2022-09-04 16:44:45 -07:00
Henrik Böving
4ee9080a9b
feat: basic compiler pass tests
2022-09-03 19:55:53 -07:00
Mario Carneiro
37252e5fa7
chore: remove Bootstrap package
2022-09-02 16:39:03 -07:00
Mario Carneiro
158e182b8b
chore: move Bootstrap.Dynamic -> Init.Dynamic
2022-09-02 04:36:54 -07:00
Leonardo de Moura
d96bf8a633
chore: restore accidentally deleted test
...
25447af13c
2022-09-01 06:06:03 -07:00
