Commit graph

20218 commits

Author SHA1 Message Date
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
Leonardo de Moura
e0197b4e09 feat: add bindCases
It is similar to `Code.bind` but has special support for `inlineMatcher`
2022-09-04 19:04:21 -07:00
Leonardo de Moura
d0600b3750 fix: incorrect binder name being used
cc @hargoniX
2022-09-04 16:56:42 -07:00
Leonardo de Moura
abd37d8fd1 feat: check binder names at LCNF/Check.lean 2022-09-04 16:55:42 -07:00
Leonardo de Moura
01ca711859 feat: add PullFunDecls.lean 2022-09-04 16:44:45 -07:00
Leonardo de Moura
df16c5a0e7 feat: add Code.collectUsed and FunDecl.collectUsed 2022-09-04 13:05:48 -07:00
Leonardo de Moura
b3c5184772 chore: remove dead code 2022-09-04 07:14:01 -07:00
Henrik Böving
32157f0e42 feat: Basic compiler testing framework 2022-09-03 19:55:53 -07:00
E.W.Ayers
30b44c03b4 fix: map fn should have explict args 2022-09-03 19:45:08 -07:00
E.W.Ayers
37745b5174 feat: intersectBy 2022-09-03 19:45:08 -07:00
E.W.Ayers
9cd24caee6 feat: utils for RBMap 2022-09-03 19:45:08 -07:00
Leonardo de Moura
56ea3af6e2 doc: Compiler/LCNF/Simp.lean 2022-09-03 19:44:10 -07:00
Leonardo de Moura
9f44e9c858 feat: simplify nested cases on the same discriminant 2022-09-03 19:44:10 -07:00
Leonardo de Moura
5478485de1 feat: allow "small prefix" at cases on cases optimization 2022-09-03 08:21:11 -07:00
Leonardo de Moura
bc88b0307e feat: cases on cases for new LCNF simplifier 2022-09-03 07:54:19 -07:00
Mario Carneiro
37252e5fa7 chore: remove Bootstrap package 2022-09-02 16:39:03 -07:00
Leonardo de Moura
196c9537f2 feat: eta reduction at toLCNF 2022-09-02 06:31:06 -07:00
Leonardo de Moura
d5dcd5e856 feat: eta-expand local function declarations that are not being inlined 2022-09-02 05:22:41 -07:00
Mario Carneiro
158e182b8b chore: move Bootstrap.Dynamic -> Init.Dynamic 2022-09-02 04:36:54 -07:00
Mario Carneiro
060290619e chore: move Bootstrap.Dynamic -> Init.Dynamic (part 1) 2022-09-02 04:36:54 -07:00
Leonardo de Moura
e3a8574e15 perf: workaround for issue #316 2022-09-02 04:15:02 -07:00
Leonardo de Moura
dfdbec51ad fix: typo 2022-09-02 03:41:49 -07:00