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

236 commits

Author SHA1 Message Date
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
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
78192972e9 chore(kernel): expr_kind::Meta ==> expr_kind::MVar 2018-06-14 15:13:45 -07:00
Leonardo de Moura
73e067d361 feat(kernel): add expression literals 2018-06-14 14:55:14 -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
1612aca0b2 chore(kernel): rename expr kinds 2018-06-09 06:50:14 -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
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
6333043adf refactor(kernel): abstract_local(s) ==> abstract 2018-06-07 16:28:54 -07:00