Commit graph

20239 commits

Author SHA1 Message Date
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
Henrik Böving
5514339ffd fix: visit jp bodies in join point finder 2022-09-08 15:21:53 -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
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
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
19f5fe6f42 feat: add getSpecializationArgs? 2022-09-07 16:08:45 -07:00
Leonardo de Moura
55171a893a feat: elaborate specialization arguments 2022-09-07 15:22:56 -07:00
Leonardo de Moura
f611a6e52f feat: add specialize attribute parser 2022-09-07 14:50:29 -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
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
Leonardo de Moura
7113d71cd2 doc: LCNF/Simp.lean docstrings 2022-09-05 17:36:35 -07:00
Leonardo de Moura
1207e5e285 feat: erase cases when all alternatives are the same 2022-09-05 17:22:54 -07:00
Leonardo de Moura
58d8224d9e feat: add LCNF cases default 2022-09-05 14:08:14 -07:00
Gabriel Ebner
8e7e58fc38 feat: synchronous operations for Channel 2022-09-05 08:52:46 -07:00
Gabriel Ebner
c4d421b3de feat: Channel 2022-09-05 08:52:46 -07:00
Gabriel Ebner
7c552380da feat: Mutex, Condvar 2022-09-05 08:52:46 -07:00
Gabriel Ebner
c2f1e01b3b feat: Promise 2022-09-05 08:52:46 -07:00
Gabriel Ebner
451f6df5df fix: IO.waitAny requires nonempty list 2022-09-05 08:52:46 -07:00
Gabriel Ebner
20f41deea7 feat: add Eval instance for BaseIO 2022-09-05 08:52:46 -07:00
Gabriel Ebner
b80775df6f chore: add nonempty instance for monads 2022-09-05 08:52:46 -07:00
Gabriel Ebner
3bd0379993 chore: add nonempty instance for Task 2022-09-05 08:52:46 -07:00
Gabriel Ebner
f7bae54b09 chore: resurrect Std.Queue 2022-09-05 08:52:46 -07:00
Gabriel Ebner
22c3ec3996 chore: generalize IO.sleep to BaseIO 2022-09-05 08:52:46 -07:00
Leonardo de Moura
553addc078 feat: alpha equivalence for LCNF code 2022-09-05 08:06:05 -07:00
Leonardo de Moura
fde8d35bbb refactor: declare passes when declaring transformations 2022-09-05 06:58:32 -07:00
Leonardo de Moura
1c41a750ed feat: add ReduceJpArity compiler pass 2022-09-05 06:58:32 -07:00
Mario Carneiro
a73e02e5fc doc: fix typo 2022-09-05 10:24:57 +02:00