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

350 commits

Author SHA1 Message Date
Leonardo de Moura
135a8d7508 chore(library/compiler): remove old compiler steps that have already been replaced 2018-10-05 17:30:27 -07:00
Leonardo de Moura
13f0a7cd81 chore(frontends/lean, library/vm): save some debugging help code 2018-10-03 13:20:24 -07:00
Leonardo de Moura
b4c2861939 refactor(library/compiler): rename "erasure normal form" functions 2018-10-01 14:17:11 -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
c746783c0d fix(frontends/lean/pp): bug when pretty printing kernel projections 2018-09-27 17:09:02 -07:00
Sebastian Ullrich
f0a983fe30 fix(frontends/lean/pp): function with implicits in structure instance 2018-09-24 09:53:28 -07:00
Leonardo de Moura
0ff1f16bf0 feat(frontends/lean/pp): add pp.compact_let option 
It helps to debug the new compiler stack.
 2018-09-20 12:05:48 -07:00
Leonardo de Moura
3ba777e709 fix(frontends/lean/pp): do not pp let type when m_binder_types == false 2018-09-11 18:10:10 -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
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Sebastian Ullrich
39cdae50ee feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms 2018-09-02 18:08:41 -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
bc57c66ae3 refactor(kernel/level): naming consistency 2018-06-22 10:29:56 -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
fd5bfc7dfe refactor(kernel): simplify binder_info 
Now, it is an enumeration type like its Lean counterpart.
 2018-06-20 15:31:40 -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
d87dfbfb03 chore(library/equations_compiler): remove equations macro 2018-06-19 13:41:08 -07:00
Leonardo de Moura
b4f4924be4 chore(library/equations_compiler): remove as_pattern macro 2018-06-19 13:41:07 -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
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
1a18bb265d chore(frontends/lean): remove a few old_type_checker occurrences 2018-06-14 14:05:04 -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
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
fc8aa30f0f chore(library/pp_options): remove dead option 2018-06-05 14:27:04 -07:00
Leonardo de Moura
6472cb0579 chore(kernel/abstract_type_context): rename has_local_pp_name 2018-06-05 14:26:31 -07:00
Leonardo de Moura
9a671d7c7d chore(library/compiler): delete rec_fn_macro 2018-05-31 17:11:25 -07:00
Leonardo de Moura
2ddb9d1598 refactor(library): remove delayed_abstraction macro 
We replace them with a new kind of (delayed) assignment at `metavar_context`
```
mvar := (lctx, locals, v)
```
where `lctx` is a local context, `locals` is a list of local
constants, and `v` is an expression.
When all metavariables in `v` are assigned, this assignment is replaced with
```
mvar := Fun(locals, v)
```
 2018-05-30 10:04:04 -07:00
Leonardo de Moura
2ebf8ab8f1 chore(*): unnecessary #includes 2018-05-18 13:19:22 -07:00
Leonardo de Moura
8ee2f4fea1 feat(*): basic runtime string support 2018-05-14 16:52:55 -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
a2f0bf7c1b chore(*): disable SMT tactic framework and backward chaining 2018-04-10 12:05:51 -07:00
Leonardo de Moura
c08a3bc557 refactor(library/typed_expr): move typed_expr to frontends/lean 2018-04-09 15:25:40 -07:00
Sebastian Ullrich
d6d44a1994 fix(frontends/lean/pp): fix #1922 
Fixes #1922
 2018-03-02 13:02:48 -08:00
Leonardo de Moura
11e87545be chore(frontends/lean): remove dead variables 2018-02-21 15:04:19 -08:00
Leonardo de Moura
058520d6e4 feat(frontends/lean/pp,library/local_context): use sanitize_name_generator_name 
Remark: we should remove `sanitize_if_fresh` as soon as we delete `::lean::mk_fresh_name`
 2018-02-21 15:04:19 -08:00
Nuno Lopes
7b45d28e77 chore(unicode): use utf8 chars directly in strings 2018-02-13 10:42:08 -08:00
Nuno Lopes
c43ebd8bf7 fix(msvc): remove another \uXX char that was causing an infinite loop 2018-02-13 10:42:08 -08:00
Nuno Lopes
977e11f9be fix(warnings): fix warnings on VS. its now /W2 clean 2018-02-13 10:42:08 -08:00
Sebastian Ullrich
be61ab4213 chore(frontends/lean/pp): document binding power intricacies 2018-02-02 08:58:52 -08:00
Sebastian Ullrich
e427068081 fix(frontends/lean/pp): missing parentheses around notation 2018-02-02 08:58:52 -08:00
Leonardo de Moura
fa6697ffa8 feat(frontends/lean/pp): add option pp.annotations for debugging purposes 2018-01-30 12:48:48 -08:00
Sebastian Ullrich
e7e05a3ad0 feat(frontends/lean): add aliasing patterns id@pat 2017-11-17 16:35:21 -08:00
Leonardo de Moura
1f757ba84e fix(frontends/lean/pp): fixes #1817 2017-09-07 15:23:58 -07:00
Gabriel Ebner
2804a0ea27 fix(util/name): escape empty name components using french quotes 2017-07-31 16:01:46 +01:00