Mario Carneiro
|
19a50a32ec
|
chore: remove List.init
|
2022-09-11 07:21:24 -07:00 |
|
Mario Carneiro
|
2886174dd0
|
chore: remove map₂, [specialize] zipWith
|
2022-09-11 07:21:24 -07:00 |
|
Mario Carneiro
|
8017aa1706
|
fix: use Type u universes in List.foldl
|
2022-09-11 07:19:30 -07:00 |
|
Chris Lovett
|
1749210a4b
|
doc: fix typos and do some polish on wording (#1568)
|
2022-09-10 15:13:43 -07:00 |
|
Leonardo de Moura
|
59b4d977b5
|
chore: fix tests
|
2022-09-10 15:06:03 -07:00 |
|
Henrik Böving
|
a03ea65d73
|
refactor: monadic compiler test framework style + new pass manager
|
2022-09-10 15:00:05 -07:00 |
|
Henrik Böving
|
c6db1099d0
|
feat: add occurences and phases to PassManager
|
2022-09-10 14:58:49 -07:00 |
|
Leonardo de Moura
|
ca098d3769
|
feat: inline applications of the form inline (f ...)
The `inline` identity function is a directive for the compiler.
|
2022-09-10 13:28:49 -07:00 |
|
Leonardo de Moura
|
1953f5953f
|
chore: dangling file
|
2022-09-10 13:23:14 -07:00 |
|
Leonardo de Moura
|
f1c150228b
|
fix: fixes #1558
|
2022-09-09 15:27:51 -07:00 |
|
Leonardo de Moura
|
353eb0dd27
|
fix: disable auto implicit feature when running tactics
fixes #1569
|
2022-09-09 15:17:50 -07:00 |
|
Leonardo de Moura
|
9f134cad8e
|
chore: remove leftover
7c3826d3e9
|
2022-09-09 15:06:47 -07:00 |
|
Leonardo de Moura
|
abf514378b
|
fix: fixes #1575
|
2022-09-09 15:05:21 -07:00 |
|
Leonardo de Moura
|
7c3826d3e9
|
fix: fixes #1576
|
2022-09-09 14:29:48 -07:00 |
|
Leonardo de Moura
|
16534bacc9
|
chore: re-activate test
|
2022-09-08 15:23:18 -07:00 |
|
Henrik Böving
|
5514339ffd
|
fix: visit jp bodies in join point finder
|
2022-09-08 15:21:53 -07:00 |
|
Leonardo de Moura
|
2ec7f14ca8
|
chore: temporarily disable test to fix build
|
2022-09-08 14:53:48 -07:00 |
|
Leonardo de Moura
|
e39c3af5bb
|
chore: remove [inline] from parser combinators
|
2022-09-08 14:50:27 -07:00 |
|
Leonardo de Moura
|
a40118c79d
|
chore: disable eager applyCasesOnImplementedBy
It must be performed at phase 2.
We still want to perform the regular `[implementedBy]` replacements at
phase 1 since they affect code specialization.
|
2022-09-08 14:50:27 -07:00 |
|
Leonardo de Moura
|
1c188b62cd
|
chore: typo
|
2022-09-08 14:50:27 -07:00 |
|
Gabriel Ebner
|
fb259f95db
|
feat: remove description argument from register_simp_attr
|
2022-09-08 14:49:43 -07:00 |
|
Leonardo de Moura
|
5b969b75bd
|
chore: fix build
|
2022-09-08 14:23:18 -07:00 |
|
Henrik Böving
|
576a4ec2c5
|
test: basic compiler tests for findJoinPoints
|
2022-09-08 14:09:14 -07:00 |
|
Henrik Böving
|
f912349a29
|
fix: compiler test framework style
|
2022-09-08 14:09:14 -07:00 |
|
Henrik Böving
|
d2f7e724ac
|
feat: findJoinPoints pass
|
2022-09-08 14:09:14 -07:00 |
|
Mario Carneiro
|
f2254088d1
|
feat: deriving Repr for TSyntax
|
2022-09-08 13:14:06 +02:00 |
|
Leonardo de Moura
|
26e304261f
|
fix: PullFunDecls.lean
Use topological sort.
|
2022-09-07 22:41:05 -07:00 |
|
Leonardo de Moura
|
46b85ec297
|
chore: update stage0
|
2022-09-07 20:39:33 -07:00 |
|
Leonardo de Moura
|
0a21603cdc
|
feat: apply implementedBy replacements at second simp pass
|
2022-09-07 20:38:16 -07:00 |
|
Leonardo de Moura
|
07bdab45d2
|
feat: apply casesOn implementedBy replacements
|
2022-09-07 20:37:09 -07:00 |
|
Leonardo de Moura
|
bd21583d4b
|
fix: ComputedFields.lean
`all` fields was not being set correctly.
TODO: check `all` fields in the kernel.
|
2022-09-07 20:35:59 -07:00 |
|
Leonardo de Moura
|
ea3235c551
|
fix: skip casesOn recursors at code generation
|
2022-09-07 18:46:48 -07:00 |
|
Leonardo de Moura
|
5c00708b7f
|
test: specialize attribute tests
|
2022-09-07 16:32:25 -07:00 |
|
Leonardo de Moura
|
19f5fe6f42
|
feat: add getSpecializationArgs?
|
2022-09-07 16:08:45 -07:00 |
|
Leonardo de Moura
|
de0be1d820
|
chore: update stage0
|
2022-09-07 15:46:17 -07:00 |
|
Leonardo de Moura
|
55171a893a
|
feat: elaborate specialization arguments
|
2022-09-07 15:22:56 -07:00 |
|
Leonardo de Moura
|
d0d98bef25
|
chore: update stage0
|
2022-09-07 14:53:01 -07:00 |
|
Leonardo de Moura
|
f611a6e52f
|
feat: add specialize attribute parser
|
2022-09-07 14:50:29 -07:00 |
|
Leonardo de Moura
|
1e135e58a1
|
chore: update stage0
|
2022-09-07 13:24:19 -07:00 |
|
Leonardo de Moura
|
735dabdb3f
|
refactor: use ParametricAttribute to implement [specialize]
|
2022-09-07 13:17:24 -07:00 |
|
Leonardo de Moura
|
04b32eb140
|
chore: remove noinline and nospecialize from runEval
|
2022-09-07 13:08:01 -07:00 |
|
Leonardo de Moura
|
661eb39bc8
|
feat: add inlinePartial config option
|
2022-09-06 20:46:17 -07:00 |
|
Leonardo de Moura
|
f4fbf92313
|
fix: make privateToUserNameAux more robust
|
2022-09-06 17:15:56 -07:00 |
|
Leonardo de Moura
|
85851d0c43
|
fix: bug at PullFunDecls
|
2022-09-06 17:15:56 -07:00 |
|
Sebastian Ullrich
|
bb1c5a7a49
|
doc: ink all .lean files in doc/
|
2022-09-06 21:12:19 +02:00 |
|
Leonardo de Moura
|
56f0d6c183
|
feat: specialize partial applications of local functions
|
2022-09-06 06:44:33 -07:00 |
|
Leonardo de Moura
|
c769808a4e
|
chore: add TODO
|
2022-09-05 19:35:17 -07:00 |
|
Leonardo de Moura
|
1812e86c7f
|
feat: eta expand partial applications of functions that take local instances as arguments
|
2022-09-05 19:33:22 -07:00 |
|
Leonardo de Moura
|
bf44e9fb2f
|
fix: bug at inferProjType for LCNF
|
2022-09-05 19:23:35 -07:00 |
|
Leonardo de Moura
|
3e210d9f26
|
chore: helper functions, missing instance
|
2022-09-05 19:20:31 -07:00 |
|