max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
14749 commits 1 branch 0 tags 5.3 GiB
Commit graph

70 commits

Author SHA1 Message Date
Leonardo de Moura
4f53e505b0 fix(library/compiler): we need to unfold auxiliary nested _match applications eagerly 2018-09-18 14:17:37 -07:00
Leonardo de Moura
8e1a6dc81b chore(library/compiler/preprocess): add trace.compiler.state1 option 2018-09-18 08:23:53 -07:00
Leonardo de Moura
c23411e1ca chore(library/compiler/preprocess): display function name 2018-09-17 19:58:54 -07:00
Leonardo de Moura
5d455bf10a chore(library/compiler): skip type checking for _cstage1 declarations 
This is a temporary hack for speeding up build time.
 2018-09-17 14:45:04 -07:00
Leonardo de Moura
faf4561723 feat(library/compiler/lcnf): expand nested f._match_<idx> applications at to_lcnf 2018-09-17 13:41:03 -07:00
Leonardo de Moura
ca176259f4 feat(library/compiler): treat f._meta_rec applications as f applications in the new compiler stack 2018-09-17 09:56:06 -07:00
Leonardo de Moura
3ebf1db2dc feat(library/compiler): treat f._meta_rec applications as f applications 2018-09-17 09:48:14 -07:00
Leonardo de Moura
33821f399c chore(library/compiler): lc_util.* ==> util.* 2018-09-17 08:50:50 -07:00
Leonardo de Moura
81067d355d chore(library/compiler): util.* ==> old_util.* 2018-09-17 08:44:45 -07:00
Leonardo de Moura
499ab0baa3 feat(library/compiler/preprocess): save declarations after csimp 
We inline functions using these auxiliary declarations.
 2018-09-16 14:07:42 -07:00
Leonardo de Moura
52d1abf0bc feat(library/compiler): add cse to new compiler stack 2018-09-14 17:48:18 -07:00
Leonardo de Moura
8571430a34 chore(library/compiler): cse ==> old_cse 2018-09-14 16:58:37 -07:00
Leonardo de Moura
3cf0d0f77a chore(library/compiler): lcsimp ==> csimp 2018-09-14 09:07:35 -07:00
Leonardo de Moura
1c0a6367c8 feat(library/compiler): new dead let removal 2018-09-14 08:41:55 -07:00
Leonardo de Moura
960eab96b3 chore(library/compiler): minor changes 2018-09-13 18:13:53 -07:00
Leonardo de Moura
31d98caa0f feat(library/compiler): add compiler simplifier skeleton 2018-09-13 18:13:53 -07:00
Leonardo de Moura
d5d926b0ef feat(library/compiler/lcnf): eliminate no_confusion 2018-09-12 10:40:09 -07:00
Leonardo de Moura
9b21287a3e feat(library/compiler/lcnf): add lean compiler normal form 2018-09-11 18:10:10 -07:00
Leonardo de Moura
6914d35062 chore(library/compiler/preprocess): dead trace option 2018-09-11 13:55:25 -07:00
Leonardo de Moura
aa3292eb36 feat(kernel/type_checker): remove m_memoize 
It is always `true`
 2018-09-07 20:50:53 -07:00
Leonardo de Moura
5d00936a8f chore(*): remove some old_type_checker dependencies 2018-09-07 08:48:21 -07:00
Leonardo de Moura
9ac56cd2a9 fix(library/compiler/preprocess): prevent auxiliary recursors from being expanded accidentally 2018-09-06 18:09:32 -07:00
Leonardo de Moura
d325a4dd1d feat(library/type_context, kernel/type_checker): use inductive_reduce_rec 2018-09-03 16:52:53 -07:00
Leonardo de Moura
dd03747d22 chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
Leonardo de Moura
ae18cee0ea chore(library/module): remove pos_info tracking 
We will use a completely different approach in Lean4
 2018-08-27 15:55:57 -07:00
Leonardo de Moura
22ba0a1155 chore(library): remove inverse.cpp 
We used this module to implement inductive_compiler pack/unpack functions
 2018-08-23 13:16:27 -07:00
Leonardo de Moura
82095cc018 refactor(kernel): split declaration into declaration and constant_info 
This is just another step towards the design described at commit 16598391a07d4a
 2018-08-22 17:53:11 -07:00
Leonardo de Moura
ec1aa2553c refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object 
TODO: inductive, constructor, recursor
 2018-06-25 10:05:45 -07:00
Leonardo de Moura
335c58f8a7 feat(kernel): add expr_kind::Quote 
This is a temporary expr constructor. We need it to be able to eliminate
expr_macro, and then define expr using runtime/object
 2018-06-12 17:40:00 -07:00
Leonardo de Moura
2a79da1ab6 refactor(kernel): move formatting stuff out of the kernel 2018-06-07 16:28:54 -07:00
Leonardo de Moura
2d7b6ed12c chore(library/compiler): remove copy_tag from old compiler 2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
b95e710e8c feat(library/compiler, library/equations_compiler): avoid rec_fn_macro in the equation and bytecode compilers 2018-05-31 17:08:12 -07:00
Leonardo de Moura
3c1ccc9b74 refactor(kernel): use m_meta instead of m_trusted 2018-05-31 11:18:00 -07:00
Leonardo de Moura
bdea7d420d chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
Leonardo de Moura
ada4932507 feat(library/compiler): add new cache support to compiler 2018-02-21 15:04:20 -08:00
Leonardo de Moura
96fab5172f perf(library/compiler): apply lambda lifting after erase trivial structures 
cc @kha
 2018-02-15 16:55:27 -08:00
Leonardo de Moura
884e5a6d2c chore(library/compiler): remove obsolete optimization step 
This optimization became obsolete after commit cd8c154bcd
 2018-02-02 08:39:39 -08:00
Leonardo de Moura
e0bdb10ab4 fix(library/type_context): clenaup whnf_head_pred 
The code had a few leftovers from the old `whnf_pred` method.
We don't use `whnf_pred` anymore.
 2018-01-08 11:31:03 -08:00
Leonardo de Moura
fabf7f6380 perf(library/equations_compiler, library/compiler): expand auxiliary _match_idx definitions when generating byte code 
We use the auxiliary procedure pull_nested_rec_fn to pull recursive
application in nested match expressions. This is needed because the
nested match expression is compiled before we process the recursive
procedure that contains it. This transformation may produce
performance problems if the recursive application does not depend on
the data being matched. Here is an example from the new test:

```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) :=
  match f v with
  | tt := tst l
  | ff := tst r
  end
```

pull_nested_rec_fn will convert it into

```
def tst : tree → nat
| (tree.leaf v)     := v
| (tree.node v l r) := tst._match_1 (f v) (tst l) (tst r)
```

Since our interpreter uses eager evaluation, both `(tst l)` and `(tst r)`
are executed. This commit fixes this issue by expanding `tst._match_1`
during code generation.
 2017-11-09 11:14:57 -08:00
Leonardo de Moura
482e06427b feat(library/equations_compiler): meta mutual definitions 
closes #1622
 2017-10-30 15:06:12 -07:00
Gabriel Ebner
89e1b196db fix(library/compiler/preprocess): do not unfold noncomputable definitions 
This happened in Johannes' real number formalization.  We tried to
unfold a noncomputable definition even though it would have been erased
afterwards, and failed.

The check_computable check was introduced in order to fix the error
message in #1401, the error message is still intelligible in that
example.
 2017-08-01 08:37:18 +01:00
Leonardo de Moura
9d5b69ad5c fix(library/compiler/preprocess): compile_lemma => compile_irrelevant 
We can also ignore functions that return types at compile_lemma (now
called compile_irrelevant).

fixes #1658
 2017-06-12 20:33:31 -07:00
Sebastian Ullrich
0ca6e2c96f refactor(library/{type_context,compiler/preprocess},frontends/lean/elaborator): use opaque, general type class instead of special app elaboration for eval_expr 2017-04-27 16:04:59 -07:00
Sebastian Ullrich
5d68938a9c feat(frontends/lean): expr literals ```(...) 2017-03-05 08:37:16 -08:00
Leonardo de Moura
22988bb95d feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator 
TODO: make sure the user is not manually using cases_on for the
auxiliary datatype generated by the inductive_compiler to
destruct nested inductives.
 2017-03-04 13:54:44 -08:00
Leonardo de Moura
184d505d51 fix(library/compiler/preprocess): do not unfold noncomputable definitions in the compiler 
see #1401
 2017-02-26 22:05:16 -08:00
Leonardo de Moura
622e9a6035 feat(library/type_context): use m_unfold_pred to decide whether macros should be unfolded or not 
see #1394
 2017-02-21 18:07:39 -08:00
Sebastian Ullrich
9d8c84713c refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
Sebastian Ullrich
5ed1ac924c feat(frontends/lean/elaborator): support partially applied eval_expr 2017-02-17 13:03:47 +01:00