Leonardo de Moura
|
766afdd0bc
|
feat: store FunDecls at LCNF local context
|
2022-08-22 21:46:37 -07:00 |
|
Leonardo de Moura
|
82acc2b39c
|
feat: improve Code.bind
Add `joinTypes`.
|
2022-08-22 21:07:36 -07:00 |
|
Leonardo de Moura
|
1f57155eb9
|
feat: add Code.bind concatenating LCNF code blocks
|
2022-08-22 20:17:52 -07:00 |
|
Leonardo de Moura
|
a2fabc6d49
|
feat: inferType for new LCNF
|
2022-08-22 19:51:17 -07:00 |
|
Leonardo de Moura
|
bd1186536f
|
feat: LCNF to Expr translator
|
2022-08-22 17:59:27 -07:00 |
|
Leonardo de Moura
|
b2c2d49bae
|
feat: new CompilerM for LCNF
|
2022-08-22 17:52:04 -07:00 |
|
Leonardo de Moura
|
92d157f705
|
feat: local context for LCNF
|
2022-08-22 16:57:12 -07:00 |
|
Leonardo de Moura
|
e1ae11a708
|
refactor: copy LCNFTypes.lean to LCNF/Types.lean
The old file is going to be deleted after we complete the refactor.
|
2022-08-22 16:56:15 -07:00 |
|
Leonardo de Moura
|
9ed83e23ae
|
feat: dead code eliminator for the new LCNF structure
|
2022-08-22 16:30:37 -07:00 |
|
Leonardo de Moura
|
18f3af302b
|
feat: new datastructure for representing LCNF code
|
2022-08-22 16:25:11 -07:00 |
|
Leonardo de Moura
|
f8c7de5a64
|
feat: add new performance counters
|
2022-08-21 19:48:30 -07:00 |
|
Leonardo de Moura
|
bc5b6272d8
|
fix: use _mustInline in lambdas only
|
2022-08-21 16:41:18 -07:00 |
|
Leonardo de Moura
|
d11947abc0
|
perf: optimize mkLetUsingScope
Avoid overhead of `hasLooseBVars` at `LocalContext.mkBinding`
|
2022-08-21 16:07:29 -07:00 |
|
Leonardo de Moura
|
eaa384bd81
|
perf: remove unnecessary calls to ensureUniqueLetVarNames
`instantiateRevInternalize` is already ensuring we have unique names.
|
2022-08-21 14:15:42 -07:00 |
|
Leonardo de Moura
|
9700b58114
|
fix: mustInline at Compiler.simp
|
2022-08-21 13:57:56 -07:00 |
|
Leonardo de Moura
|
df89717ae3
|
perf: custom isTypeFormerType for toLCNF translation
|
2022-08-21 12:45:37 -07:00 |
|
Leonardo de Moura
|
cae7b7443d
|
chore: remove trace leftovers
|
2022-08-21 11:42:50 -07:00 |
|
Leonardo de Moura
|
7c0bb0a6dc
|
feat: add compiler.check option
|
2022-08-21 11:15:07 -07:00 |
|
Leonardo de Moura
|
faabf14c1b
|
perf: improve PullLocalDecls.dependsOn
|
2022-08-21 11:15:07 -07:00 |
|
Leonardo de Moura
|
778f9aa08f
|
feat: eta expand local function declarations that are not being inlined
|
2022-08-21 06:38:42 -07:00 |
|
Leonardo de Moura
|
fa7769260a
|
perf: combine instantiateRev and internalize in a single traversal
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
b2a99e1b68
|
chore: minor optimization at mkFlatLet
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
776a9b0dcb
|
feat: don't eagerly simplify local functions that will be inlined
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
571a839416
|
chore: doc strings and add .mustInline case
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
d2d0a745d5
|
feat: use eta-reduction when reducing projection instances
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
a5034d6700
|
feat: add performance counter to Compiler.Simp
|
2022-08-20 20:03:05 -07:00 |
|
Leonardo de Moura
|
3788145a56
|
perf: minimize instantiateRev number of calls
|
2022-08-20 08:36:27 -07:00 |
|
Leonardo de Moura
|
6c1e9d9b28
|
perf: use [specialize] at withNewScope
|
2022-08-19 18:56:15 -07:00 |
|
Leonardo de Moura
|
36cca3ebdd
|
perf: add toLCNFType cache
|
2022-08-19 18:49:33 -07:00 |
|
Leonardo de Moura
|
b37178d547
|
perf: improve toLCNFType
|
2022-08-19 18:40:44 -07:00 |
|
Henrik Böving
|
d0aa234c78
|
feat: handle out of scope join points in join point finder
|
2022-08-19 17:44:54 -07:00 |
|
Leonardo de Moura
|
8aa9d2cdbf
|
feat: add "cases on cases" simplification
|
2022-08-19 17:39:10 -07:00 |
|
Leonardo de Moura
|
49823c28c4
|
fix: inlining heuristic
|
2022-08-19 16:23:37 -07:00 |
|
Leonardo de Moura
|
15f0e26368
|
feat: replace cases alternative with unreachable if one of the fields is the empty type
|
2022-08-19 12:25:46 -07:00 |
|
Leonardo de Moura
|
a29a61b728
|
chore: remove dead code
|
2022-08-19 11:56:22 -07:00 |
|
Leonardo de Moura
|
a7c96142ea
|
feat: improve code inliner
and fix bugs at the `onlyOneExitPoint` case.
|
2022-08-19 11:33:34 -07:00 |
|
Leonardo de Moura
|
6d11dc9b62
|
feat: add mkAuxDeclName
|
2022-08-19 11:31:56 -07:00 |
|
Leonardo de Moura
|
b1e292e238
|
feat: add option for disabling join point scope checking
|
2022-08-19 11:31:18 -07:00 |
|
Leonardo de Moura
|
d0c8ad1d22
|
feat: reduce number of simp steps
|
2022-08-19 05:54:50 -07:00 |
|
Leonardo de Moura
|
88c4d5c340
|
perf: simplify and optimize inlineProjInst?
|
2022-08-19 04:49:31 -07:00 |
|
Leonardo de Moura
|
4cbe67954b
|
feat: improve inlineProjInst?
|
2022-08-18 18:25:55 -07:00 |
|
Leonardo de Moura
|
9a04193e73
|
fix: getStage1Decl? minor issue
|
2022-08-18 17:40:05 -07:00 |
|
Leonardo de Moura
|
0b2d013beb
|
chore: remove leftover
|
2022-08-18 17:39:29 -07:00 |
|
Leonardo de Moura
|
9ae2b83ac0
|
feat: add Compiler.Decl.pullInstances
|
2022-08-18 15:09:22 -07:00 |
|
Leonardo de Moura
|
bf2c0bf5b7
|
feat: avoid generation of auxliary join points when inlining functions that have only one exit point
|
2022-08-18 00:12:24 -07:00 |
|
Leonardo de Moura
|
23be59b747
|
chore: add Compiler.stat trace option
|
2022-08-18 00:10:56 -07:00 |
|
Leonardo de Moura
|
c780d390d6
|
fix: bug at InferType.lean
|
2022-08-18 00:10:35 -07:00 |
|
Leonardo de Moura
|
651d4044b3
|
fix: bug at attachJp
|
2022-08-17 19:22:53 -07:00 |
|
Leonardo de Moura
|
ff53e9cc56
|
chore: remove leftover
|
2022-08-17 19:04:12 -07:00 |
|
Leonardo de Moura
|
3a898802f7
|
feat: inline type class instances
|
2022-08-17 19:01:49 -07:00 |
|