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

9723 commits

Author SHA1 Message Date
Leonardo de Moura
8ff6ac9e0f refactor(kernel/environment): intro_rule ==> constructor 
Lean is a programming language
 2018-06-01 15:35:02 -07:00
Leonardo de Moura
909284dd74 refactor(runtime): normlize object names 2018-06-01 15:34:42 -07:00
Leonardo de Moura
de48d49b53 feat(kernel): preparing for adding new inductive datatype module 2018-06-01 14:47:49 -07:00
Leonardo de Moura
ac0352b584 refactor(kernel): remove quotitent normalizer extension 
The `quot` type is now implemented in the kernel.
We will do the same thing for inductives.
We will not support normalizer extensions anymore in Lean4.
It doesn't make sense since we settled with 2 extensions: quotients and
inductives. Moreover, any new extension would require substantial
changes (e.g., code generator).
The normalizer_extension feature was useful when we were experimenting
with different kernel flavors.
 2018-06-01 10:52:17 -07:00
Leonardo de Moura
722974e8c7 feat(kernel): add option to skip type checking at add_meta 2018-05-31 17:27:55 -07:00
Leonardo de Moura
9a671d7c7d chore(library/compiler): delete rec_fn_macro 2018-05-31 17:11:25 -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
eab962bbc6 feat(kernel): add add_meta 2018-05-31 15:40:50 -07:00
Leonardo de Moura
cab6b39c76 refactor(library): remove sorry checking 
We have to revise how we do this.
 2018-05-31 15:20:39 -07:00
Leonardo de Moura
8a918a2a14 fix(checker/text_import): commit 3c1ccc9 broke it 2018-05-31 14:59:36 -07:00
Leonardo de Moura
112d1da8d0 refactor(library/module): no need to store trust lvl in declarations 
We are going to delete macros. So, we don't need to store trust_lvl information.
 2018-05-31 14:55:18 -07:00
Leonardo de Moura
3c1ccc9b74 refactor(kernel): use m_meta instead of m_trusted 2018-05-31 11:18:00 -07:00
Leonardo de Moura
e80765daca fix(library/export_decl): bug at export_decl_modification::perform 
The `perform` method was adding the modification to the environment
where it was being applied.
 2018-05-31 09:16:46 -07:00
Leonardo de Moura
80545832f4 chore(library): remove user attributes 2018-05-31 09:10:41 -07:00
Leonardo de Moura
f507b882e2 chore(frontends/lean): remove support for user commands from old front end 2018-05-31 09:06:07 -07:00
Leonardo de Moura
0947abaee4 chore(frontends/lean): remove broken declare_trace command 
This command is broken, and we will have a new tracing infrastructure in Lean4.
 2018-05-31 09:02:25 -07:00
Leonardo de Moura
2e8967adf1 doc(kernel/environment): document why we need is_descendant 2018-05-31 08:14:54 -07:00
Leonardo de Moura
12a03f7784 chore(frontends/lean/definition_cmds): remove dependency 2018-05-30 14:46:54 -07:00
Leonardo de Moura
d3272ca1c5 refactor(frontends/lean,library/tactic/kabstract): remove add_key_equivalence command 
This command was never used in the Lean3 corelib and mathlib.
It is safe to assume it is not needed.
 2018-05-30 14:10:03 -07:00
Leonardo de Moura
d707a27c2b chore(library/class): unnecessary dependency 2018-05-30 14:05:21 -07:00
Leonardo de Moura
843cd9bacb chore(library/compiler/rec_fn_macro): remove dead code 2018-05-30 13:16:34 -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
c9a6f98454 chore(library/sorry): style 2018-05-29 22:27:03 -07:00
Leonardo de Moura
f7b6645b60 fix(frontends/lean/elaborator): add missing synthesize 
We added for the following reasons:
1- It should mimic the behavior of `visit_lambda` and `visit_pi`.
2- It minimizes the number of auxiliary metavariables that need to be
   created when we execute `locals.mk_lambda(new_body)`. In Lean3,
   it would minimize the number of delayed abstractions.
 2018-05-29 16:40:13 -07:00
Leonardo de Moura
7842036aba feat(library/type_context): avoid delayed_abstractions when creating binders lambda/pi/let 
This is the first step to eliminate the delayed_abstraction macro.
 2018-05-29 16:37:33 -07:00
Leonardo de Moura
73f83216c1 fix(frontends/lean/elaborator): bug at invoke_tactic 
The `is_def_eq` must be performed using the local context associated
with the metavariable.
 2018-05-29 16:34:43 -07:00
Leonardo de Moura
3615073faf fix(frontends/lean/elaborator): visit_expr_quote bug 2018-05-29 16:21:52 -07:00
Leonardo de Moura
0b1525b58e fix(library/type_context): is_quick_class bug 
It was returning false for expressions such as `let x := 10 in has_add nat`.
 2018-05-29 15:12:44 -07:00
Leonardo de Moura
978ef203b9 fix(frontends/lean/elaborator): the is_def_eq test must be performed in the right local context 2018-05-29 13:35:01 -07:00
Leonardo de Moura
14d62ab12d chore(runtime/serializer): compilation warning 2018-05-29 08:04:42 -07:00
Leonardo de Moura
1332fbabd6 feat(library,frontends): remove sorry macro 
Lean4 will not have macros.
 2018-05-24 14:00:30 -07:00
Leonardo de Moura
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
Leonardo de Moura
a1b9ae0e67 feat(util/obj_list): add map_reuse and cleanup code 2018-05-23 15:05:08 -07:00
Leonardo de Moura
4af1f31877 feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels 2018-05-23 14:48:22 -07:00
Leonardo de Moura
ef8bbccf9f chore(util/object_ref): disable automatic coercion from object_ref to object * 2018-05-23 13:12:40 -07:00
Leonardo de Moura
e7ac7cb542 chore(cmake/Modules/cpplint.py): disable bogus cpplint check 2018-05-23 10:10:37 -07:00
Leonardo de Moura
306c300226 refactor(kernel/level): implement level on top of object 2018-05-23 09:54:46 -07:00
Leonardo de Moura
b66a088b52 fix(runtime/serializer): memory leak 2018-05-23 09:52:20 -07:00
Leonardo de Moura
3d46684d2a chore(util/name): minor change 2018-05-23 09:41:44 -07:00
Leonardo de Moura
e2a7d78dd6 chore(util/name): remove dead code 2018-05-22 17:57:33 -07:00
Leonardo de Moura
480d999e63 fix(runtime/object): bugs at string_append and string_push 2018-05-22 17:51:51 -07:00
Leonardo de Moura
7afa418e13 chore(runtime/serializer): style 2018-05-22 17:43:23 -07:00
Leonardo de Moura
339764bf6a refactor(runtime): add string_object 
The idea is to avoid the hack for storing the string unicode length.
It also reduces the amount of space used to serialize strings.
 2018-05-22 17:28:04 -07:00
Leonardo de Moura
fb00f9a780 fix(runtime/object): missing free 2018-05-22 16:50:07 -07:00
Leonardo de Moura
b2f3d3f456 chore(*): remove redundant code 2018-05-22 16:46:04 -07:00
Leonardo de Moura
5b17a30203 feat(runtime): add object serializer 
Any type implemented on top of `object` gets the serializer/deserializer for free
 2018-05-22 16:34:41 -07:00
Leonardo de Moura
67b59a0a3c fix(util): memory leaks 2018-05-22 11:05:51 -07:00
Leonardo de Moura
914e702356 chore(kernel/level): remove unnecessary friend annotation 2018-05-22 09:46:17 -07:00
Leonardo de Moura
eb54a4f551 chore(kernel/cache_stack): compilation warning 2018-05-22 09:46:00 -07:00
Leonardo de Moura
160b7e8847 refactor(library/init/meta/expr): local_const will have only one field 
In Lean3, we supported two kinds of local constant:
context-less (inherited from Lean2) and context-based (type,
binder-info and pretty printing name are stored in the context).
The context-less was used in the kernel and a few modules we kept when
we moved from Lean2 to Lean3. Even if we keep the hybrind
representation, we should not expose the context-less to users.
 2018-05-21 15:36:09 -07:00