Leonardo de Moura
613c8027d7
fix: missing instantiateParamsLevelParams
2022-10-09 12:10:11 -07:00
Mario Carneiro
391aef5cd7
feat: automatic extension names
2022-10-06 17:19:30 -07:00
Leonardo de Moura
913ca41129
refactor: merge lcAny and lcErased
...
`lcErased` is a superset of `lcAny` anyway, and we didn't find ways of
using the distinction to generate better code.
2022-10-05 04:46:52 -07:00
Leonardo de Moura
c4db085ac1
fix: missing dependency check at simpJpCases?
2022-10-03 19:39:10 -07:00
Leonardo de Moura
da4812659c
feat: use DiscrM to implement simpJpCases?
2022-10-03 19:13:31 -07:00
Leonardo de Moura
ddbf4c01eb
refactor: add DiscrM.lean
2022-10-03 19:00:30 -07:00
Leonardo de Moura
f0be5439e6
feat: JpCases for join points with multiple parameters
2022-10-03 18:35:16 -07:00
Leonardo de Moura
dc6f635f41
refactor: add LCNF/Internalize.lean
2022-10-03 09:18:11 -07:00
Leonardo de Moura
15909f209f
feat: inline small declarations not tagged with [noinline]
2022-09-30 20:51:37 -07:00
Leonardo de Moura
72506c81ea
chore: trace.Compiler.simp.inline
2022-09-30 20:21:34 -07:00
Leonardo de Moura
0e18b4318c
feat: online inline recursive functions if they are tagged with [inlineIfReduce]
2022-09-30 19:39:12 -07:00
Leonardo de Moura
595734b936
chore: remove workaround
...
It is now implemented at `Quote (Array _)`
2022-09-29 17:12:48 -07:00
Leonardo de Moura
e5494e7a49
fix: eta-expansion at compatibleTypes
...
It fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301424293
2022-09-29 11:02:06 -07:00
Leonardo de Moura
5c925f9345
feat: add functions to create small arrays and use them in the constant folder
...
It reduces the code generated for functions using a bunch
of quotations. For example, the size of
`Lean.Elab.Term.Do.ToTerm.matchNestedTermResult` went from 2348 to 1507
2022-09-28 22:00:50 -07:00
Leonardo de Moura
6bc6522d86
feat: constructor => discriminant optimization
2022-09-28 21:14:19 -07:00
Leonardo de Moura
94c2ec38d5
feat: implement cast TODO
...
fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301269857
2022-09-28 15:40:53 -07:00
Leonardo de Moura
fd5f3a5bad
feat: track recursively inlining
...
closes #1657
see #1646
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/inline.20codegen.20crash/near/301099703
2022-09-27 16:26:49 -07:00
Leonardo de Moura
135790f41a
fix: missing eraseCode at inlineProjInst?
...
Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/LCNF.20local.20context.20contains.20unused.20local.20variable.20declaratio/near/301102923
2022-09-27 16:26:49 -07:00
Leonardo de Moura
65c307a7b7
feat: add environment extension for constant folder
...
TODO: add command/attribute for conveniently installing folders
2022-09-27 16:26:49 -07:00
Leonardo de Moura
8596e4af88
fix: mark code as simplified
2022-09-26 21:27:45 -07:00
Leonardo de Moura
193e3fd184
feat: add basic String folding
2022-09-26 21:23:08 -07:00
Leonardo de Moura
e6f5b3758c
feat: precompute folders
2022-09-26 21:10:38 -07:00
Leonardo de Moura
1e75001405
feat: preserve user provided names at LCNF Simp
...
It helps preserving let-declaration names in pure code, but it is not
very useful for monadic let-decls (e.g., `let x <- act`). The binder
names are often lost we eliminating the abstraction layers.
2022-09-26 21:04:13 -07:00
Henrik Böving
2958b8a7f5
feat: basic constant folder
...
supports:
- arithmetic operations:
- folding full constants
- folding neutral elements
- folding annihilators
- List.toArray
2022-09-26 21:03:47 -07:00
Leonardo de Moura
35ca2b203c
refactor: split Simp.lean
2022-09-26 07:04:20 -07:00
