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

1431 commits

Author SHA1 Message Date
Sebastian Ullrich
25ffbdda57 chore(src/*): fix style 2019-02-07 15:41:12 +01:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08:00
Leonardo de Moura
c097f1c1e0 fix(kernel/builtin): add extern 2019-02-01 17:58:55 -08:00
Leonardo de Moura
ac53080ced fix(kernel/builtin): incorrect signature 2019-02-01 15:06:57 -08:00
Leonardo de Moura
4fa06e38b2 chore(*): add skeleton for new builtin primitives, update src/boot 2019-02-01 14:03:03 -08:00
Leonardo de Moura
9e7d1d5bd2 chore(kernel/expr): remove leftover 2018-11-09 11:55:02 -08:00
Leonardo de Moura
43ceb6bfbe refactor(kernel/local_ctx): simplify local_ctx 
Remark: we still need to revise the classes: `type_context` and `local_context`.
 2018-10-24 10:02:38 -07:00
Leonardo de Moura
83abbcb9a6 fix(library/compiler/erase_irrelevant): preserve builtin runtime types 
`uint32` is a definition, and `type_checker::whnf` unfolds it.
To preserve the information at `erase_irrelevant`, we use a custom
`whnf_type` method that stops reduction as soon as a builtin runtime
type is found.
 2018-10-22 13:58:08 -07:00
Leonardo de Moura
db647139a2 feat(kernel): use cheap_beta_reduce at infer_lambda too 2018-10-20 17:28:45 -07:00
Leonardo de Moura
0b38547e97 feat(kernel): move cheap_beta_reduce to kernel and use it at infer_let 2018-10-20 17:13:41 -07:00
Leonardo de Moura
a40c526e48 feat(library/compiler/csimp): add basic constant folding for nat operations 2018-10-17 08:38:30 -07:00
Leonardo de Moura
611f6ae780 feat(library/compiler/specialize): code specialization 
TODO:
- Cache results at `specialize_ext`
- Cleanup

It is not feasible to run code specializer without cache: code explosion.
 2018-10-16 15:50:42 -07:00
Leonardo de Moura
8837217a2e chore(kernel/expr): dead decls 2018-10-15 11:10:11 -07:00
Leonardo de Moura
c74f4c16ca feat(library/kernel,library/compiler/csimp): make sure nat.rec and nat.cases_on reduce when major premise is a nat literal 2018-10-10 18:35:15 -07:00
Leonardo de Moura
9f161e6968 fix(library,kernel): the new proj_sname field must be taken into account during comparisons 
`proj_sname` is not just for enabling better pretty printing. It is
necessary in the compiler when type information is lost, and we can't
infer the type of a `proj`-term argument (field `proj_expr`).
 2018-10-03 13:11:46 -07:00
Leonardo de Moura
c3569dc72d feat(kernel): store structure name in proj-expressions 2018-10-02 09:23:11 -07:00
Leonardo de Moura
2c4139d5e5 feat(library/compiler): eta expand quot primitives, add support for eq.rec_on 2018-09-30 08:24:18 -07:00
Leonardo de Moura
751cdd7c42 feat(kernel/type_checker): avoid unnecessary lambdas 2018-09-29 17:24:49 -07:00
Leonardo de Moura
6e9e9c0012 feat(library/compiler): eta expand definitions 2018-09-23 19:27:06 -07:00
Leonardo de Moura
1534f17a89 feat(library/compiler/lcnf): add better support for complete-transition used in the equation compiler and x@ patterns 2018-09-20 21:38:57 -07:00
Leonardo de Moura
9b29572604 feat(kernel/type_checker): improve infer_let 
Before this commit, given a term `let x : t := v in b`, `infer_type`
would return `let x : t := v in T` where `T` is the type of `b` in
the local context extended with declaration `x : t := v`.
This is correct, but it produces unnecessarily large terms
in the new compiler stack which makes a heavy use of let-expressions.
We noticed the problem when the size of some .olean files were 100x
bigger. For example, `repr.olean` increased from 136Kb to
13Mb after we started saving the `._cstage1` (code after after
simplification) in the `.olean` files.

The new implementation relies on the fact that `T` seldom depends on
`x`. So, in most cases, the result is just `T` instead of `let x : t := v in T`

After this change, the new .olean files are at most 56% bigger than
.olean files not containing `._cstate1` code. This seems reasonable
since most of our .olean files only contain code and we are storing a
copy of each function.

@kha The new lcnf format keeps exposing problems :)
 2018-09-17 18:25:27 -07:00
Leonardo de Moura
f0e24e73f4 feat(kernel/expr): missing constructor 2018-09-16 14:30:43 -07:00
Leonardo de Moura
59652e885a fix(kernel/type_checker): whnf_fvar 2018-09-16 13:49:35 -07:00
Leonardo de Moura
000db32e40 chore(kernel/type_checker): remove dead branch 2018-09-16 12:22:28 -07:00
Leonardo de Moura
4874e25715 feat(kernel): save constructor idx and nfields at constructor_val 2018-09-14 13:45:58 -07:00
Sebastian Ullrich
647f40763c feat(library/message_builder): pretty-print kernel_exceptions 2018-09-13 16:38:40 -07:00
Leonardo de Moura
b8dceda9b7 chore(kernel): type_checker::context ==> type_checker::state 2018-09-13 14:06:57 -07:00
Leonardo de Moura
20f31c85bf chore(kernel/type_checker): we don't use the kernel type checker for elaboration anymore 2018-09-12 20:36:32 -07:00
Leonardo de Moura
c49ad19736 refactor(kernel/type_checker): type_checker::cache ==> type_checker::context 
We also move `environment` and `name_generator` to
`type_checker::context`. Reason: the cache assumes the environment did
not change. The (cache) correctness relies on the fact that we don't
reuse free variable identifiers.
 2018-09-12 20:34:30 -07:00
Leonardo de Moura
d814ee612a chore(kernel/local_ctx): typo 2018-09-11 18:10:10 -07:00
Sebastian Ullrich
904d7c4a88 chore(*): remove old task API and task queues 2018-09-11 13:55:25 -07:00
Leonardo de Moura
4863ca071a chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
Leonardo de Moura
03a99986bb feat(kernel): implement local_decl using runtime 2018-09-08 16:25:43 -07:00
Leonardo de Moura
3b07eeec47 fix(kernel/inductive): name generator was not being consistenly used 2018-09-08 16:21:33 -07:00
Leonardo de Moura
5503bd113b chore(kernel/type_checker): assume m_cache != nullptr will continue to hold in future versions 2018-09-08 09:13:08 -07:00
Leonardo de Moura
7479d6e55b refactor(kernel/type_checker): allow type_checker::cache to be reused 2018-09-08 08:43:19 -07:00
Leonardo de Moura
dacc4c9cd6 chore(kernel): move abstract_type_context to library 2018-09-08 08:29:51 -07:00
Leonardo de Moura
3e5f59d6df chore(kernel): remove expr.quote constructor 
In Lean4, we will reify expressions.
 2018-09-07 22:08:08 -07:00
Leonardo de Moura
4ddd915886 chore(kernel): remove dummy file 2018-09-07 21:43:15 -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
88d4a1b0cd feat(kernel/inductive): inductive_reduce_rec should not throw exception when it finds an unknown constant 
It should just fail to reduce. This is important when using it in the elaborator.
 2018-09-07 17:34:54 -07:00
Leonardo de Moura
1b81577d8b fix(kernel/inductive): remove unnecessary whnf 
The frontend is responsible for unfolding reducible definitions before
sending inductive declarations to the kernel.
 2018-09-07 17:27:08 -07:00
Leonardo de Moura
6b673d1ca9 chore(util,kernel): consistent constructors for object_ref-like wrappers 2018-09-07 17:06:41 -07:00
Leonardo de Moura
2946174c1e chore(kernel): remove old_type_checker 2018-09-07 08:55:37 -07:00
Leonardo de Moura
a3d886f1e8 chore(kernel/type_checker): remove leftover 2018-09-07 08:51:21 -07:00
Leonardo de Moura
81bf600973 chore(kernel/type_checker): fix style 2018-09-06 18:12:20 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
afb9584a63 feat(kernel): store at inductive_val whether the type is reflexive or not 2018-09-05 14:46:03 -07:00
Leonardo de Moura
9970019f76 fix(kernel/inductive): incorrect assertion 
It fails on non parametric datatypes with nullary constructors.
 2018-09-05 09:52:25 -07:00
Leonardo de Moura
176e0a3ed3 fix(kernel/inductive): typo 2018-09-04 17:32:18 -07:00