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

71 commits

Author SHA1 Message Date
Leonardo de Moura
2fa938220b chore(library/init/data/string): cleanup 2018-11-14 14:09:45 -08:00
Leonardo de Moura
835b3a10cc chore(library/init): consistent names 2018-11-14 13:08:57 -08:00
Leonardo de Moura
1191dd4deb refactor(library/compiler): move mk_runtime_type to util 2018-11-07 15:19:24 -08:00
Leonardo de Moura
c285d48c96 feat(library/compiler/erase_irrelevant): simplify mk_runtime_type 2018-11-07 15:10:41 -08:00
Leonardo de Moura
8af0c85d4f feat(library/compiler/erase_irrelevant): convert enumeration types into uint* types 2018-11-06 16:55:02 -08:00
Leonardo de Moura
9f3544aaa4 feat(library/compiler/erase_irrelevant): preserve enumeration types 2018-11-06 16:55:02 -08:00
Leonardo de Moura
6f03df871b chore(library/compiler): remove whnf_upto_runtime_type 
It is not needed anymore.
 2018-11-06 16:55:02 -08:00
Leonardo de Moura
74b92cd419 feat(library/compiler/llnf): collect constructor info 2018-10-27 16:58:51 -07:00
Leonardo de Moura
571be8616a refactor(library/compiler/erase_irrelevant): postpone simplification 
Remove transformations such as
```
prod.cases_on M (\fun a b, t)
```
==>
```
let a := M.0 in
let b := M.1 in
t
```

We will perform this kind of transformation in a later stage.
 2018-10-26 15:59:04 -07:00
Leonardo de Moura
3ee863da68 feat(library/compiler/erase_irrelevant): eliminate cases_on for builtin types 2018-10-23 14:58: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
6b8008a222 feat(library/compiler): new compiler entry point (skeleton) 2018-10-05 17:30:27 -07:00
Leonardo de Moura
adfc0e28ea feat(library/compiler/erase_irrelevant): missing is_irrelevant checks, missing terms being visited, mixing erased with non-erased terms 2018-10-03 16:22:44 -07:00
Leonardo de Moura
cd8dc8670d fix(library/compiler/erase_irrelevant): visit_constant 2018-10-02 18:56:13 -07:00
Leonardo de Moura
49425aa80c fix(library/compiler/erase_irrelevant): assertion violation 2018-10-02 18:56:13 -07:00
Leonardo de Moura
24bd5782e0 fix(library/compiler/erase_irrelevant): make sure lambda that return irrelevant data is marked as irrelevant 2018-10-02 18:56:13 -07:00
Leonardo de Moura
fd46adb7b3 fix(library/compiler/erase_irrelevant): minor issues 2018-10-02 13:36:48 -07:00
Leonardo de Moura
20e7edd4ac feat(library/compiler): erase trivial structures and flat cases on structures 2018-10-02 11:05:15 -07:00
Leonardo de Moura
c05e7a31a3 chore(library/compiler): add is_runtime_scalar_type and is_runtime_builtin_type 2018-10-02 09:03:53 -07:00
Leonardo de Moura
25b45d6f9e feat(library/compiler): add erase_irrelevant transformation to new compiler stack 2018-10-01 17:06:56 -07:00
Leonardo de Moura
81e9e95570 chore(library/compiler): erase_irrelevant ==> old_erase_irrelevant 2018-10-01 14:17:11 -07:00
Leonardo de Moura
a17b95acc7 feat(library/compiler/erase_irrelevant): add support for lc_unreachable 2018-09-30 08:25:06 -07:00
Leonardo de Moura
81067d355d chore(library/compiler): util.* ==> old_util.* 2018-09-17 08:44:45 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
8ed89c6ac3 chore(library): remove normalize.cpp 
The command `#reduce` was also temporarily removed.
 2018-09-04 10:51:14 -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
c5714c2fac chore(kernel): remove expr.macro constructor 
We are now ready to implement `expr` using `runtime/object`.
 2018-06-19 17:54:43 -07:00
Leonardo de Moura
8101b9df6e refactor(library/string): remove string_macro 
We now use expr_lit.
 2018-06-14 16:26:39 -07:00
Leonardo de Moura
91a65f692f refactor(library/compiler): remove nat_value macro 2018-06-14 15:26:32 -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
62788a9ca3 refactor(kernel): fix terminology: "free_var" is actually a loose bound variable 
We represent free variables uisng local constants.
We will fix this terminology too.
 2018-06-08 13:25:36 -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
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
0556412f8d refactor(*): add runtime folder 
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
 2018-05-14 14:23:56 -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
dbfcc65c60 fix(library/compiler/erase_irrelevant): erase_type 2018-02-19 07:55:43 -08:00
Sebastian Ullrich
283d8ade1a fix(library/quote): use opaque macro for elaborated expr quotations 2017-06-07 10:00:17 -07:00
Sebastian Ullrich
8c0394b294 refactor(library,frontends/lean): separate expr and pexpr macros 2017-05-09 16:02:41 -07:00
Leonardo de Moura
0d97700c60 feat(library/compiler): add support for and.rec in the code generator 2017-04-16 13:31:37 -07:00
Leonardo de Moura
60dd85719c feat(library/system/io): system.io without axioms 2017-03-22 23:36:05 -07:00
Sebastian Ullrich
16558bf082 refactor(library,library): rename pre_monad to has_bind 2017-03-09 20:32:25 -08:00
Sebastian Ullrich
763097dbd2 refactor(library): revise the monadic hierarchy 2017-03-09 20:30:03 -08:00
Leonardo de Moura
4ab0a6d8d2 fix(library): problems with the subtype constructor and field renaming 
The problem was not detected by the test suite because of issue #1446
 2017-03-08 19:42:12 -08:00
Leonardo de Moura
ceeb77ec8c fix(library/compiler/erase_irrelevant): erase types of irrelevant lambdas 
This modification makes sure we do not create unnecessary closures,
and avoid artificial dependencies that may prevent destructive updates.
 2017-03-08 14:48:45 -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
2c0a5a5120 fix(library/compiler/erase_irrelevant): remove broken io monad optimization 
It doesn't work when combined with inlining and common-subexpression-elimination
 2017-02-07 21:24:31 -08:00
Leonardo de Moura
a516d384ae fix(library/compiler/erase_irrelevant): make sure io monad actions are not erased by dead code elimination optimization 2017-01-02 01:42:36 -08:00
Leonardo de Moura
bd2f9bce05 fix(library/compiler/erase_irrelevant): issue created by elim_unused_lets optimization 2016-12-14 18:51:53 -08:00
Leonardo de Moura
6577cc87a3 feat(library): add pre_monad 
closes #1235
 2016-12-08 12:48:55 -08:00