Leonardo de Moura
ec59bbe15c
chore: ensure LCNF pretty printer result supports Format.group
2022-10-16 16:06:08 -07:00
Leonardo de Moura
72c576f62a
feat: complete reduceArity pass
2022-10-16 16:00:33 -07:00
Leonardo de Moura
1a02c326e5
chore: fix test
2022-10-16 14:54:07 -07:00
Leonardo de Moura
9244a7a8a5
fix: ensure old and new compiler auxiliary declaration names do not collide
2022-10-16 14:49:55 -07:00
Leonardo de Moura
79ed382492
chore: fix test
2022-10-16 09:00:25 -07:00
Leonardo de Moura
c20febff31
feat: add helper Syntax.node* functions
2022-10-16 08:40:01 -07:00
Leonardo de Moura
b4d850502d
fix: avoid join point that takes closure at seqToCode
2022-10-15 15:48:02 -07:00
Leonardo de Moura
61813d60c6
test: for join point taking closure as parameter
2022-10-15 12:05:53 -07:00
Leonardo de Moura
376c541e9a
feat: do not generate code for declarations that will be specialized
2022-10-15 08:54:46 -07:00
Leonardo de Moura
6378283fa8
feat: add Probe.toString
2022-10-14 19:21:56 -07:00
Henrik Böving
38788a72be
feat: basic compiler probing framework with examples
2022-10-14 19:09:35 -07:00
Gabriel Ebner
1c561c39a8
feat: function coercions with unification
2022-10-14 12:08:10 -07:00
Mario Carneiro
0acdaddcf2
feat: unexpander for mkArray0
2022-10-14 08:51:45 -07:00
Rishikesh Vaishnav
76c4693c95
fix: improve fuzzy-matching heuristics ( #1710 )
2022-10-14 16:17:14 +02:00
Leonardo de Moura
dfd95c712e
chore: fix tests
2022-10-13 06:16:56 -07:00
Leonardo de Moura
4ac802dd9a
chore: fix test
2022-10-13 04:31:46 -07:00
Leonardo de Moura
2675c0647b
feat: detect unreachable cases alternatives at LCNF simp
2022-10-13 02:49:55 -07:00
Sebastian Ullrich
e7b90b489a
fix: stabilize unused variables linter output
2022-10-13 10:46:53 +02:00
Gabriel Ebner
38d3e37c75
perf: improve Unhygienic.run code
2022-10-12 19:36:05 -07:00
Leonardo de Moura
49a6f8c105
chore: add horrible hack for Decidable in the new code generator
...
cc @gebner
2022-10-12 16:53:29 -07:00
Leonardo de Moura
7308fa0e7d
feat: ensure lambda lifter is creating unused names
2022-10-12 16:35:55 -07:00
Gabriel Ebner
79569c9003
chore: replace let by have in stx matches
2022-10-12 11:52:28 -07:00
Mario Carneiro
8dfae9eb38
feat: import command stub
2022-10-12 11:11:31 -07:00
Leonardo de Moura
aa845dee98
feat: cache lambda lifted functions
2022-10-11 21:28:03 -07:00
Gabriel Ebner
15d7744cca
chore: fix tests
2022-10-11 17:24:35 -07:00
Gabriel Ebner
6593bd98b3
chore: add test for 1692
2022-10-11 17:24:35 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Mario Carneiro
f4b04216eb
feat: go to duplicate definition
2022-10-11 10:07:49 +02:00
Leonardo de Moura
525b4f761c
chore: fix tests
2022-10-10 17:48:32 -07:00
Henrik Böving
dd3c0f77f1
feat: FloatLetIn compiler pass
2022-10-10 23:56:20 +02:00
Leonardo de Moura
7b3709e28a
chore: simplify proof in test for #1711
...
TODO: improve support for instance implicit arguments at `congr`
2022-10-10 07:29:53 -07:00
Leonardo de Moura
0041de5d1d
fix: congr tactic should not try to synthesize instance implicit arguments that have been inferred when applying congr theorem
...
see #1711
2022-10-10 07:24:27 -07:00
Leonardo de Moura
fb4200e633
chore: fix tests
2022-10-09 21:51:51 -07:00
Leonardo de Moura
cc09afc5e1
fix: type error introducing when inlining LCNF functions
...
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/303142516
2022-10-09 12:10:11 -07:00
Leonardo de Moura
263be54dcf
chore: fix tests
2022-10-09 12:10:11 -07:00
Mario Carneiro
d4219c9d70
fix: List.Mem should have two parameters
2022-10-09 05:46:52 -07:00
Leonardo de Moura
56002e1b33
fix: fixes #1707
2022-10-08 07:58:56 -07:00
Leonardo de Moura
6bc4144409
fix: fixes #1549
2022-10-08 07:41:49 -07:00
Leonardo de Moura
e3ec468e3b
fix: fixes #1650
2022-10-07 19:00:23 -07:00
Leonardo de Moura
cf2ea445fe
fix: fixes #1681
2022-10-07 18:36:25 -07:00
Chris Lovett
3eeb064d83
fix: Clear Diagnostics when file is closed ( #1591 )
2022-10-07 17:28:15 -07:00
Leonardo de Moura
45974229d2
feat: reactivate extendJoinPointContext at mono phase
...
closes #1686
cc @hargoniX
2022-10-07 16:27:44 -07:00
Leonardo de Moura
1b8e310ada
fix: fixes #1674
2022-10-07 13:33:41 -07:00
Leonardo de Moura
5c74bc1324
fix: fixes #1705
2022-10-07 13:11:26 -07:00
Leonardo de Moura
5b1aac7b8f
fix: avoid nontermination on non-utf8 input
...
This is not a perfect solution, but ensures the non-termination does
not happen. The changes also make it easier to prove termination in
the future.
TODO: validate UTF8 input?
closes #1690
2022-10-06 17:45:21 -07:00
Ed Ayers
7fabdf95d6
refactor: diffTag → diffStatus
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-10-06 13:06:31 -07:00
E.W.Ayers
506abff532
fix: replace highlight with diffTag
2022-10-06 13:06:31 -07:00
Leonardo de Moura
0577993d61
chore: fix tests
2022-10-06 07:41:48 -07:00
Leonardo de Moura
c6b3ebdd85
feat: detect trivial structures and add extension for storing mono phase types
2022-10-05 08:55:44 -07:00
Leonardo de Moura
ee59048bfb
chore: remove dead declaration
...
We have merged `lcErased` and `lcAny` in the new code generator.
2022-10-05 05:17:31 -07:00
