max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
29848 commits 1 branch 0 tags 5.3 GiB
Commit graph

535 commits

Author SHA1 Message Date
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
ebdbdc1043 chore: temporarily disable extendJoinPointContext 
see #1686
 2022-10-04 17:41:41 -07:00
Leonardo de Moura
adeab12beb feat: add support for Iff.rec and Iff.casesOn to new code generator 
closes #1684
 2022-10-04 06:32:49 -07:00
Sebastian Ullrich
8ed831101e chore: benchmark new compiler 2022-10-04 05:03:54 -07:00
Leonardo de Moura
c4db085ac1 fix: missing dependency check at simpJpCases? 2022-10-03 19:39:10 -07:00
Leonardo de Moura
b3aff375f0 feat: add CodeDecl.dependsOn 2022-10-03 19:36:26 -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
Henrik Böving
eaab29712d feat: extend join point context pass 2022-10-03 17:03:22 -07:00
Leonardo de Moura
fed7ff27e8 fix: issue reported on Zulip 
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/302056742
 2022-10-03 09:51:32 -07:00
Leonardo de Moura
dc6f635f41 refactor: add LCNF/Internalize.lean 2022-10-03 09:18:11 -07:00
Leonardo de Moura
31d59e337b fix: LCNF any type issue 
This fixes an issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/301935406
 2022-10-02 08:09:13 -07:00
Leonardo de Moura
190a1331bd feat: add toMonoType 2022-10-01 20:44:31 -07:00
Leonardo de Moura
1ce9e30403 refactor: extension for storing LCNF types for declarations that do not have code associated with them 2022-10-01 20:44:31 -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
18b5ff9e78 chore: propagate recursive flag during code specialization 2022-09-30 20:01:18 -07:00
Leonardo de Moura
9fda3d973d feat: add trace option trace.Compiler.saveBase 2022-09-30 19:50:33 -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
4c2c6931f4 feat: add flag at LCNF Decl indicating whether the original Lean declaration was declared using partial or unsafe 2022-09-30 19:28:05 -07:00
Leonardo de Moura
fb1a603e60 feat: add another CSE pass before saveBase 2022-09-29 18:56:20 -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
b4454902c1 feat: LCNF Code.forEachExpr and Decl.forEachExpr 2022-09-29 15:50:49 -07:00
Leonardo de Moura
13edf0e9cc feat: add forEachModuleDecl and forEachMainModuleDecl 2022-09-29 14:16:10 -07:00
Leonardo de Moura
bb1e94de82 feat: normalize free variable ids before saving LCNF code in the environment 2022-09-29 12:48:21 -07:00
Leonardo de Moura
8cca2ea24e fix: refresh LCNF parameter binder names 2022-09-29 12:46:53 -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
73ebaf8499 feat: improve visitLambda at toLCNF 2022-09-28 19:17:28 -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
970331de05 chore: avoid a.getAppFn.isAnyType idiom 2022-09-28 15:34:09 -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
002c7d2f22 feat: configuration options for the code generator 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
Leonardo de Moura
24e584cf00 feat: add Renaming.lean 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
73d5e12ac5 fix: baseExt must not use SimplePersistentEnvExtension 
We invoke `Decl.saveBase` more than once when we update a declaration.
 2022-09-26 08:15:47 -07:00
Leonardo de Moura
ba619be393 fix: apply macroInline again after inlineMatchers 2022-09-26 07:31:27 -07:00
Leonardo de Moura
837ce4374c feat: use reduceJpArity after successful simpJpCases? 2022-09-26 07:25:29 -07:00
Leonardo de Moura
35ca2b203c refactor: split Simp.lean 2022-09-26 07:04:20 -07:00
Mario Carneiro
85119ba9d1 chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Leonardo de Moura
fd1ae3118c feat: replace isCasesOnCases? with simpJpCases? 
It addresses the code explosion issue with the old optimization.
For example, the resulting size for `Lean.Json.Parser.escapedChar`
went from 31593 to 361.
 2022-09-25 20:57:24 -07:00
Leonardo de Moura
bbac49e925 feat: add collectJpCasesInfo 
Collect statistics for implementing new optimization that will replace `isCasesOnCases?`
 2022-09-25 20:57:24 -07:00