Leonardo de Moura
47bde4547d
feat(compiler/erase_irrelevant): erase type information from lambda and let expressions
2016-05-09 10:22:38 -07:00
Leonardo de Moura
94be486ade
fix(frontends/lean/builtin_cmds): generate error if declaration is not a definition
2016-05-07 18:39:40 -07:00
Leonardo de Moura
93aa264060
feat(frontends/lean/pp): pretty print neutral/unreachable terms
2016-05-07 18:30:19 -07:00
Leonardo de Moura
e5118a3a3a
feat(compiler/erase_irrelevant): replace irrelevant terms with "neutral" constant
2016-05-07 18:26:13 -07:00
Leonardo de Moura
c7b4e00bbf
refactor(compiler): move is_comp_irrelevant predicate to util
2016-05-07 18:19:19 -07:00
Leonardo de Moura
5f8c5cf2a4
feat(compiler/erase_irrelevant): distribute app arguments over cases_on minor premises
2016-05-07 18:12:28 -07:00
Leonardo de Moura
ca2de7126e
chore(compiler/erase_irrelevant): compilation warnings
2016-05-07 17:39:00 -07:00
Leonardo de Moura
255fe13929
feat(library/init/logic): make ite and dite as inline
2016-05-07 17:38:37 -07:00
Leonardo de Moura
2b7551501e
feat(compiler/erase_irrelevant): rec => cases_on
2016-05-07 17:32:27 -07:00
Leonardo de Moura
b54cd38b51
chore(compiler/elim_recursors): cleanup
2016-05-07 17:32:10 -07:00
Leonardo de Moura
50fd4eb7bd
feat(compiler/erase_irrelevant): eliminate subtype.tag, subtype.rec and subtype.elt_of
2016-05-07 16:57:26 -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
42af7c2a67
feat(compiler/erase_irrelevant): eliminate no_confusion applications
2016-05-07 16:30:23 -07:00
Leonardo de Moura
9f6d4e85b6
refactor(compiler): move get_constructor_arity to util
2016-05-07 16:21:56 -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
329a9723cb
feat(library): tag auxiliary no_confusion definitions
2016-05-07 15:26:49 -07:00
Leonardo de Moura
6b862d805d
fix(compiler/lambda_lifting): bug when creating auxiliary recursive definition
2016-05-07 13:18:47 -07:00
Leonardo de Moura
530f70e8f0
chore(compiler/lambda_lifting): cleanup
2016-05-06 15:34:36 -07:00
Leonardo de Moura
9b88dcca1b
feat(compiler/lambda_lifting): make sure auxiliary recursive functions are in eta-expanded normal form
2016-05-06 15:32:01 -07:00
Leonardo de Moura
de44321d6c
fix(compiler/lambda_lifting): consume nested lambdas when processing cases_on
2016-05-05 20:01:27 -07:00
Leonardo de Moura
e5e9bb388d
feat(compiler/lambda_lifting): add support for recursor applications of recursive datatypes
2016-05-05 19:50:19 -07:00
Leonardo de Moura
454ec00f17
feat(frontends/lean/pp): pretty print recursive calls
2016-05-05 18:10:55 -07:00
Leonardo de Moura
9a247d6ac4
feat(compiler): add auxiliary macro for compiling recursive functions
2016-05-05 17:21:45 -07:00
Leonardo de Moura
f5325f2e23
feat(compiler/lambda_lifting): try to reduce cases_on after major premise has been processed
2016-05-04 17:24:21 -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
37bc76ff09
feat(compiler/lambda_lifting): preprocess nonrecursive recusor applications using the same approach used for cases_on applications
2016-05-04 17:17:03 -07:00
Leonardo de Moura
a4ec6a3a17
feat(compiler, frontends/lean): add 'inline' definitions, and add compiler preprocessing step for unfolding them
2016-05-04 16:53:25 -07:00
Leonardo de Moura
7006c84214
feat(compiler/lambda_lifting): avoid unnecessary lambda lifting steps
...
It doesn't make sense to apply lambda lifting to lambda-expressions such as
(fun x, f x)
since we can reduce it to `f`
2016-05-03 18:48:31 -07:00
Leonardo de Moura
3dac0f6bb6
fix(compiler/simp_pr1_rec): make sure simplification support reflexive datatypes
...
Example:
inductive tree (A : Type) :=
| leaf : A → tree A
| node : (nat → tree A) → tree A
definition tree_fn : tree nat → nat
| (tree.leaf a) := a
| (tree.node f) := tree_fn (f 0)
2016-05-03 18:22:12 -07:00
Leonardo de Moura
19c87dd711
fix(compiler/simp_pr1_rec): make sure simplification is not affected by the comp_irrelevant annotation
2016-05-03 17:53:37 -07:00
Leonardo de Moura
79b8622ce5
feat(compiler/lambda_lifting): add support for cases_on recursor
...
We still have to implement support for the recursive case.
2016-05-03 17:37:56 -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
fd83b711b6
fix(library/type_context): make sure aux_recursors are not unfolded in whnf_pred IF the given predicate returns false for them.
2016-05-03 17:26:53 -07:00
Leonardo de Moura
8c878e8196
refactor(library/aux_recursors): make sure is_aux_recursor returns true for manually defined nat.cases_on
2016-05-03 17:26:11 -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
1c1ecdc3a9
feat(compiler/compiler_step_visitor): add visit_app
2016-05-03 15:41:50 -07:00
Leonardo de Moura
ea3fae060f
chore(compiler/preprocess_rec): use tout
2016-05-02 18:18:53 -07:00
Leonardo de Moura
da79cd7d95
feat(frontends/lean/pp): add option pp.hide_binder_types
2016-05-02 18:16:27 -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
2fca1ac2a4
feat(library/type_context): add method mk_let
...
It is identical to mk_lambda, but makes sure all locals are actually let-decls
2016-05-01 19:32:54 -07:00
Leonardo de Moura
889bdec2f7
feat(util/rb_tree): add unsigned_rev_cmp
2016-05-01 19:30:51 -07:00
Leonardo de Moura
048376d8fd
feat(library/locals): add auxiliary method
2016-05-01 19:01:47 -07:00
Leonardo de Moura
bd18516ddd
fix(library/local_context): typo
2016-05-01 19:01:30 -07:00
Leonardo de Moura
7bf3e2ffbb
fix(compiler/simp_pr1_rec): typo
2016-05-01 16:47:53 -07:00
Leonardo de Moura
d86772e986
fix(library/type_context): compilation errors in debug mode
2016-05-01 12:05:42 -07:00
Leonardo de Moura
d64a8d24f9
fix(library/replace_visitor): remove replace_visitor_closed, it does not handle nested let-expr correctly
2016-05-01 12:04:28 -07:00
