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

246 commits

Author SHA1 Message Date
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
4cca030251 chore(library/compiler/lcnf): do not beta reduce at to_lcnf 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
b8dceda9b7 chore(kernel): type_checker::context ==> type_checker::state 2018-09-13 14:06:57 -07:00
Leonardo de Moura
c02e2d3b56 feat(library/compiler/lcnf): split cases followed by application 2018-09-13 12:57:08 -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
7f496f43f1 fix(library/compiler/lcnf): it was not erasing proofs that start with Pi 2018-09-12 18:26:23 -07:00
Leonardo de Moura
379c06faf4 fix(library/compiler/lcnf): avoid trivial let-decls 2018-09-12 18:24:12 -07:00
Leonardo de Moura
bfb3ffbc79 feat(library/compiler/lcnf): safe beta reduction 2018-09-12 14:51:19 -07:00
Leonardo de Moura
112f183be4 feat(library/compiler/lcnf): eliminate false.cases_on and eq.cases_on 2018-09-12 14:27:01 -07:00
Leonardo de Moura
1e5f0a91f1 feat(library/compiler/lcnf): eliminate and.rec and and.cases_on 2018-09-12 14:21:28 -07:00
Leonardo de Moura
b1fb4416f3 feat(library/compiler/lcnf): make sure constructor applications are fully applied 2018-09-12 14:04:24 -07:00
Leonardo de Moura
4058276a82 feat(library/compiler/lcnf): eliminate false.rec 2018-09-12 13:55:32 -07:00
Leonardo de Moura
cfdc331ecb feat(library/compiler/lcnf): replace eq.rec and eq.ndrec applications with lc_cast 2018-09-12 11:00:34 -07:00
Leonardo de Moura
c526670e6f feat(library/compiler/lcnf): eliminate id_rhs even if it is partially applied 2018-09-12 10:45:23 -07:00
Leonardo de Moura
2d6582e67c fix(library/compiler/lcnf): dumb mistake, Pi case is not reachable 2018-09-12 10:40:09 -07:00
Leonardo de Moura
ec1809de74 fix(library/compiler/lcnf): restore cache 2018-09-12 10:40:09 -07:00
Leonardo de Moura
ec92653d93 feat(library/compiler/lcnf): do not create aux let-decl for lc_proof-applications 2018-09-12 10:40:09 -07:00
Leonardo de Moura
d5d926b0ef feat(library/compiler/lcnf): eliminate no_confusion 2018-09-12 10:40:09 -07:00
Leonardo de Moura
de2abf5d8c fix(library/compiler/lc_util): missing file 2018-09-11 18:11:27 -07:00
Leonardo de Moura
8ee10e202f chore(library/compiler/lcnf): use _x_<idx> instead of _x.<idx> 
This is a temporary change while we debug the new compiler.
 2018-09-11 18:10:10 -07:00
Leonardo de Moura
72e99ea3ee fix(library/compiler/lcnf): apply_beta takes arguments in reverse order 2018-09-11 18:10:10 -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
3e5f59d6df chore(kernel): remove expr.quote constructor 
In Lean4, we will reify expressions.
 2018-09-07 22:08:08 -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
85465885f3 chore(library/type_context): remove "frozen local instances" 
We will re-implement the type class resolution algorithm, and the new
implementation will not rely on a persistent cache. We will improve
performance by:
1) Using better indexing data-structures.
2) Using a local cache during the search.
 2018-09-07 13:17:37 -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
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
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
Sebastian Ullrich
6009279ab3 fix(library/compiler/cse): deactivate CSE for constructor applications 
Fixes 1968
 2018-08-22 14:32:03 -07:00
Leonardo de Moura
f3e99286bb chore(kernel): remove certified_declaration 2018-08-22 12:11:34 -07:00
Leonardo de Moura
9d35d31529 refactor(kernel): merge constant_assumption and axiom 2018-08-01 09:57:47 -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
e9f843ddf6 refactor(kernel/expr): remove mlocal_* functions 
The constructors `mvar` and `fvar` have different memory layouts.
 2018-06-22 14:25:31 -07:00
Leonardo de Moura
b24ba6b93d chore(library/compiler/simp_inductive): fix bogus g++ 4.9 warning 2018-06-21 16:52:27 -07:00
Leonardo de Moura
01ea596aea refactor(kernel/expr): implement expr using runtime/object 2018-06-21 16:05:33 -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
9e7e600ad7 feat(kernel): add expr.proj constructor 
TODO: implement infer_proj and reduce_proj
 2018-06-19 15:45:49 -07:00
Leonardo de Moura
b84090aaca feat(library/annotation): remove annonation macro 
We now use the new `expr.mdata` constructor.
 2018-06-18 13:39:02 -07:00
Leonardo de Moura
0847571ea6 feat(kernel): add mdata constructor 2018-06-18 13:36:22 -07:00
Leonardo de Moura
13c532d0d4 fix(*): truncation bugs 
- Lean strings (like std::string) may contain null characters. The
  codebase was ignoring this issue.

- We now have a wrapper `string_ref` for wrapping Lean string objects in
  C++. This wrapper also implements correctly the coercions std::string <-> string_ref.
  Remark: I also found a few places where the code relies on the
  following property which is not true
  Forall s : std::string, std::string(s.c_str()) == s

- `name` object wrapper was assuming that all numerals were small
  `nat` values. This is true in most cases, but the system would
  crash when processing if it is a big number.

- The commit tries to make sure runtime/util/kernel are correct.
  Modules that will be deleted contain many `TODO` comments
  indicating they may crash and/or produce incorrect results
  when strings contain null characters and numerals are big.

cc @kha

@kha: I thought about using `string` instead of `string_ref`.
We consistently use `std::string`. So, it should be fine, but I
was concerned about code readability.

After we bootstrap Lean4, we will be able to delete `lean::list`
template, and rename `lean::list_ref` to `lean::list`.

I am going to add `pair_ref` for wrapping Lean pair objects.
If we use `lean::string` instead of `lean::string_ref`, then
we should also use `lean::pair` instead of `lean::pair_ref`.
But, there is a problem in this case since we have
https://github.com/leanprover/lean4/blob/master/src/util/pair.h#L13
:(
 2018-06-15 16:05:11 -07:00