Leonardo de Moura
|
de9df69ef6
|
refactor(src): move compiler folder to library
|
2016-05-09 13:28:00 -07:00 |
|
Leonardo de Moura
|
bc81d0957f
|
feat(compiler): add preprocessing step for reducing the arity of auxiliary declarations
|
2016-05-09 11:46:22 -07:00 |
|
Leonardo de Moura
|
49ff96ae8c
|
fix(compiler/preprocess_rec): do not type check after erase_irrelevant
|
2016-05-07 16:39:34 -07:00 |
|
Leonardo de Moura
|
4f5e55bcbf
|
refactor(compiler): rename lambda_lifting to elim_recursors
Moreover, we do not apply lambda lifting anymore at this step.
We will do it later after irrelevant terms have been erased.
|
2016-05-07 16:00:57 -07:00 |
|
Leonardo de Moura
|
a322f5fe60
|
feat(compiler): start erase_irrelevant
|
2016-05-07 15:27:24 -07:00 |
|
Leonardo de Moura
|
2e970d67ba
|
fix(compiler/preprocess_rec): add extra comp_irrelevant step
|
2016-05-04 17:17:45 -07:00 |
|
Leonardo de Moura
|
8c9cf4b0a8
|
feat(compiler/preprocess_rec): simplify cases_on applications
|
2016-05-03 17:37:27 -07:00 |
|
Leonardo de Moura
|
156068609f
|
feat(compiler/preprocess_rec): do not unfold cases_on
|
2016-05-03 15:42:20 -07:00 |
|
Leonardo de Moura
|
ea3fae060f
|
chore(compiler/preprocess_rec): use tout
|
2016-05-02 18:18:53 -07:00 |
|
Leonardo de Moura
|
85e7003524
|
refactor(compiler): expose primitive for marking computationally irrelevant terms
|
2016-05-02 17:33:49 -07:00 |
|
Leonardo de Moura
|
007d82107d
|
feat(compiler): add basic function inliner
|
2016-05-02 17:24:13 -07:00 |
|
Leonardo de Moura
|
da8f37d7cc
|
feat(compiler): mark computationally irrelevant terms
|
2016-05-02 16:23:54 -07:00 |
|
Leonardo de Moura
|
5d770f9575
|
feat(compiler): add lambda lifting
|
2016-05-01 19:33:51 -07:00 |
|
Leonardo de Moura
|
f2c10b0cee
|
feat(compiler): add compiler_step_visitor helper class
|
2016-05-01 12:02:42 -07:00 |
|
Leonardo de Moura
|
92325f9295
|
fix(compiler/preprocess_rec): fix expand_aux_recursors_fn
|
2016-04-28 17:41:08 -07:00 |
|
Leonardo de Moura
|
0b3e23892b
|
refactor(library/replace_visitor): add replace_visitor_closed
|
2016-04-28 17:09:02 -07:00 |
|
Leonardo de Moura
|
836b3bfe95
|
refactor(compiler/preprocess_rec): make sure expand_aux_recursors does not depend on old code
|
2016-04-28 16:40:24 -07:00 |
|
Leonardo de Moura
|
8dde1489f9
|
refactor(library/util): isolate util procedures that depend on old_type_checker
|
2016-03-21 13:36:08 -07:00 |
|
Leonardo de Moura
|
e7f1f409c4
|
refactor(kernel): simplify kernel type_checker
TODO: cleanup, move justification/metavar/constraints to library
|
2016-03-18 16:28:42 -07:00 |
|
Leonardo de Moura
|
c9e9fee76a
|
refactor(*): remove name_generator and use simpler mk_fresh_name
|
2016-02-11 18:05:57 -08:00 |
|
Leonardo de Moura
|
f482e09cc2
|
fix(compiler/preprocess_rec): warning when compiling using clang on OSX
|
2015-11-16 18:38:41 -08:00 |
|
Leonardo de Moura
|
49a574dbbf
|
refactor(compiler): rename elim_rec to preprocess_rec
|
2015-09-11 17:12:32 -07:00 |
|