Leonardo de Moura
0a126b7702
perf: better support for "inlineable" instances
2022-10-14 08:42:50 -07:00
Leonardo de Moura
1bb67918f8
chore: cleanup eagerLambdaLifting and add notes
2022-10-14 08:42:50 -07:00
Leonardo de Moura
31f2acd97a
chore: cleanup trace messages
2022-10-13 18:56:17 -07:00
Leonardo de Moura
19301c09c6
chore: remove unnecessary match
2022-10-13 18:56:17 -07:00
Leonardo de Moura
6ed89a4ceb
chore: revert cross module lambda lifting cache
...
It adds almost 50Mb to the .olean files.
2022-10-13 18:42:52 -07:00
Leonardo de Moura
ac9d65b17b
feat: cache lambda lifting
2022-10-13 11:24:14 -07:00
Leonardo de Moura
518123b191
feat: more conservative SpecParamInfo inference
2022-10-13 08:20:55 -07:00
Leonardo de Moura
407c744ae5
chore: add workarounds for old code generator
...
It is a bit ironic that the new code generator should contain
workarounds for the old one.
2022-10-13 07:09:19 -07:00
Leonardo de Moura
886ed9b2e3
fix: remove function expected error at LCNF
2022-10-13 06:16:25 -07:00
Leonardo de Moura
c33b5b6588
chore: remove unnecessary eqvTypes
2022-10-13 06:08:51 -07:00
Leonardo de Moura
bc2b891e7e
refactor: remove type compatibility sanity checks at LCNF Check.lean
...
See new note at `Check.lean` for details.
2022-10-13 06:01:41 -07:00
Leonardo de Moura
1f54c0126c
doc: add note at Decl.simp
2022-10-13 04:26:05 -07:00
Leonardo de Moura
2563fda777
feat: enable eager lambda lifting
2022-10-13 04:22:19 -07:00
Leonardo de Moura
0966f14233
fix: local function declarations size may be 0
2022-10-13 03:34:14 -07:00
Leonardo de Moura
2675c0647b
feat: detect unreachable cases alternatives at LCNF simp
2022-10-13 02:49:55 -07:00
Leonardo de Moura
af99715a58
feat: store inline attribute at LCNF declarations
...
This commit also adds support for inheriting the inline attribute when
the compiler lambda lifts local functions from instances.
2022-10-13 02:06:35 -07:00
Leonardo de Moura
b9f174604d
feat: check new alwaysInline attribute
2022-10-12 16:55:16 -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
Leonardo de Moura
8fe4b75c48
feat: do not inline definitions occurring in instances at the base phase
2022-10-12 16:24:16 -07:00
Leonardo de Moura
5606b4e59e
feat: add [alwaysInline] attribute
...
We are planning to ignore the `[inline]` attribute when the "inlining
quota" has been exhausted in the new code generator.
2022-10-12 16:08:37 -07:00
Gabriel Ebner
fb6cb05465
feat: support let_fun in new compiler
2022-10-12 11:52:28 -07:00
Leonardo de Moura
aa845dee98
feat: cache lambda lifted functions
2022-10-11 21:28:03 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Leonardo de Moura
02a3dcb1dd
feat: hash for LCNF.Code
2022-10-10 20:34:12 -07:00
Leonardo de Moura
3f24ce71ab
feat: add another floatLetIn pass at mono phase
2022-10-10 17:19:40 -07:00
Henrik Böving
dd3c0f77f1
feat: FloatLetIn compiler pass
2022-10-10 23:56:20 +02:00
Henrik Böving
d132551829
feat: extend FVarUtil framework
2022-10-10 23:32:36 +02:00
Henrik Böving
e15e6bfaee
chore: address PR comments
2022-10-10 23:32:36 +02:00
Leonardo de Moura
b20e208867
chore: pretty print LCNF cases result type
2022-10-09 20:13:17 -07:00
Leonardo de Moura
6f023a44ad
fix: let _x.i := _x.j simplification at LCNF simp
2022-10-09 18:38:28 -07:00
Leonardo de Moura
72d3840f0c
feat: add simpCast?
2022-10-09 18:29:12 -07:00
Leonardo de Moura
6c5475725e
feat: (lcCast _ _ g) a_1 ... a_n => g a_1 ... a_n if type correct
2022-10-09 17:45:15 -07:00
Leonardo de Moura
30bd019a7f
chore: simplify SimpValue.lean
2022-10-09 17:35:13 -07:00
Leonardo de Moura
54944819a0
feat: add simpCastCast?
2022-10-09 16:43:33 -07:00
Leonardo de Moura
cd303cd8e5
fix: do not apply simpAppApp? over cast
2022-10-09 16:43:10 -07:00
Leonardo de Moura
cf313d2101
chore: improve eqvTypes
2022-10-09 16:42:55 -07:00
Leonardo de Moura
43fe67c41a
chore: helper pass for debugging purposes
2022-10-09 16:41:54 -07:00
Leonardo de Moura
9feb4d8ab7
fix: do not generate code for [extern] functions
2022-10-09 15:35:29 -07:00
Leonardo de Moura
11fcdb7bf4
feat: add cast at exit points if necessary when inlining code
2022-10-09 13:01:10 -07:00
Leonardo de Moura
ef2d17120c
chore: fix note
2022-10-09 12:25:45 -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
f61ec4929f
chore: add low-level normExprCore
2022-10-09 12:10:11 -07:00
Leonardo de Moura
e81673366a
chore: remove leftover
2022-10-09 12:10:11 -07:00
Leonardo de Moura
613c8027d7
fix: missing instantiateParamsLevelParams
2022-10-09 12:10:11 -07:00
Leonardo de Moura
827ef94486
feat: add eqvTypes
2022-10-09 12:10:11 -07:00
Leonardo de Moura
c14d07fe2e
feat: include def/fun/jp resulting type in the LCNF pretty printer
2022-10-09 12:10:11 -07:00
Leonardo de Moura
eeb98d9cf4
refactor: rename FixedArgs => FixedParams
2022-10-09 12:10:11 -07:00
Leonardo de Moura
37a61568bc
feat: improve fixed parameter analyzer
2022-10-09 12:10:11 -07:00
Leonardo de Moura
8e6cb25cbf
chore: temporarily disable eager lambda lifting
...
We need a better heuristic for deciding which functions in instances
should be eagerly lambda lifted. Otherwise, it will have to keep
chasing which instances we have to annotate with `[inline]`.
2022-10-08 19:51:19 -07:00
