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

69 commits

Author SHA1 Message Date
Leonardo de Moura
69a446c8d1 feat: add field all to DefinitionVal and TheoremVal 
Remark: we need an update stage0, and the field is not being updated
correctly set yet.
 2022-06-23 16:13:26 -07:00
Leonardo de Moura
57b4b8ad1b chore: disable the kernel "tryHeuristic" for abbreviations 2021-07-23 12:10:16 -07:00
Leonardo de Moura
ae61f2ac67 chore: remove dead code 2021-01-05 18:36:27 -08:00
Leonardo de Moura
f0ac477d2e feat: add sanity checks 2021-01-01 18:31:28 -08:00
Leonardo de Moura
612ef66bb4 feat: store whether inductive type is nested or not 2020-12-10 14:25:23 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
1480b39d86 chore: no Task in Theorem 2020-09-03 08:47:55 -07:00
Leonardo de Moura
6ada62a3ee feat: export helper functions 
Motivation: prevent changes in the scalar fields layout from breaking
C++ code.
Ideally, we should do that for all constructors, and implement a tool
that creates the C++ functions automatically for us.
We don't do it because we will delete most of this code after we
finish the Lean4 transition.
 2020-02-25 13:00:22 -08:00
Leonardo de Moura
c7d96a6522 fix: theorem values are tasks 2020-01-16 17:20:36 -08:00
Leonardo de Moura
c650e11d6b fix: missing isUnsafe fieldat OpaqueVal 2019-12-30 11:53:08 -08:00
Leonardo de Moura
08cdb757b4 feat(library/init/lean/environment): add Environment.addAndCompile 
To fix `BuiltinParserAttribute`, we need to be able to add auxiliary declarations programmatically.
 2019-06-18 18:20:17 -07:00
Leonardo de Moura
edb4d76ecd feat(kernel/environment): environment as a Lean object 2019-05-13 12:41:33 -07:00
Leonardo de Moura
5f54b5887b chore(kernel/declaration): fix compilation warnings 2019-03-19 11:25:55 -07:00
Leonardo de Moura
aa56578a29 fix(library/compiler/compiler): assertion violations 2019-03-19 11:25:55 -07:00
Leonardo de Moura
20ba4c4b04 feat(kernel): opaque constants 
They are very similar to `theorems`, but they are never ever unfolded.
 2019-03-15 15:45:06 -07:00
Leonardo de Moura
0888dee25e chore(*): meta ==> unsafe 2019-03-15 15:04:40 -07:00
Leonardo de Moura
818f2f2d4a chore(kernel): remove old #include 2019-03-06 06:56:16 -08:00
Leonardo de Moura
2c4139d5e5 feat(library/compiler): eta expand quot primitives, add support for eq.rec_on 2018-09-30 08:24:18 -07:00
Leonardo de Moura
4874e25715 feat(kernel): save constructor idx and nfields at constructor_val 2018-09-14 13:45:58 -07:00
Leonardo de Moura
4863ca071a chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
Leonardo de Moura
6b673d1ca9 chore(util,kernel): consistent constructors for object_ref-like wrappers 2018-09-07 17:06:41 -07:00
Leonardo de Moura
afb9584a63 feat(kernel): store at inductive_val whether the type is reflexive or not 2018-09-05 14:46:03 -07:00
Leonardo de Moura
59fa70616a feat(kernel/inductive): add reduce 2018-09-03 15:22:15 -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
7928dbb239 chore(kernel): get_constructor ==> get_cnstr 2018-09-03 12:30:49 -07:00
Leonardo de Moura
47bc71f4fa feat(kernel/inductive): postprocess recursors and their rules 2018-09-02 21:06:51 -07:00
Leonardo de Moura
517923d362 feat(kernel/inductive): generate recursors in the new inductive datatype module 2018-08-31 17:47:22 -07:00
Leonardo de Moura
863355c6a0 feat(kernel/inductive): continue new inductive datatype module 
Add more validation, and create new inductive_val and constant_val objects.
 2018-08-29 09:27:06 -07:00
Leonardo de Moura
101886ffae feat(kernel): proper constant_info and declaration objects for quot type 2018-08-28 13:46:31 -07:00
Leonardo de Moura
161431e995 feat(kernel): implement new mutual_definition declaration object 
This commit also removes the old `environment::add_meta` hackish method.
 2018-08-28 10:30:44 -07:00
Leonardo de Moura
776c977742 refactor(kernel): continue constant_info/declaration refactoring 2018-08-27 17:23:26 -07:00
Leonardo de Moura
27ef29a50f refactor(kernel/declaration): continue constant_info/declaration refactoring 2018-08-27 13:22:10 -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
Leonardo de Moura
47d74e1a5a chore(kernel/declaration): minor cleanup 2018-08-21 10:11:23 -07:00
Leonardo de Moura
9d35d31529 refactor(kernel): merge constant_assumption and axiom 2018-08-01 09:57:47 -07:00
Leonardo de Moura
bda46cc9ac feat(kernel): add inductive_decl type on top of runtime/object, and ajust kernel/inductive.cpp 2018-06-26 12:16:33 -07:00
Leonardo de Moura
bb0b43798c feat(kernel/declaration): add wrappers for accessing inductive/constructor/recursor declarations 2018-06-25 15:01:02 -07:00
Leonardo de Moura
7684860aec feat(kernel): add C++ wrappers for creating inductive declarations 2018-06-25 14:24:48 -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
9c6238e1ac refactor(kernel/declaration): reducibility hints as runtime/object 2018-06-25 08:04:44 -07:00
Leonardo de Moura
ede1a51d60 refactor(kernel/declaration): remove self_opt flag from reducibility hints 
This flag was used by the kernel to decide whether the following
heuristic should be used to avoid unfolding `f` at `is_def_eq`.

       f a =?= f b
       -----------
         a =?= b

This heuristic was introduced at Lean1 after a discussion with
Georges Gontier. Since this discussion, we added support for
caching failures of this heuristic. This proved to be much more
effective to attack the performance problems.
Moreover, we do not even use this flag in the `type_context::is_def_eq`
used during elaboration.

The current codebase contains only one place where this flag was set to
`false`: coercions generated at structure_cmd. This change was
made at commit
1c70514231
in the Lean2 codebase when we were not caching failures and
the kernel type checker was also used during elaboration.
 2018-06-22 09:02:50 -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
1bc7c0812c chore(kernel,library): remove task from the kernel and library 2018-05-18 09:06:03 -07:00
Gabriel Ebner
595cbb8fe9 refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
Gabriel Ebner
a972c13ce9 refactor(library/task_queue): move task queue to util 2016-12-12 10:01:34 -05:00
Leonardo de Moura
f96d35dc1c fix(library/aux_definition,frontends/lean/definition_cmds): unfold macros at trust level 0 2016-12-05 13:08:12 -08:00
Gabriel Ebner
3ecfddcbd5 fix(*): fix build 2016-11-29 11:12:43 -08:00
Gabriel Ebner
385ea13688 feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
Leonardo de Moura
db3ad3156b chore(src/kernel/declaration): move cell inside declaration 2016-11-07 14:59:37 -08:00
Gabriel Ebner
8eb4bbd0cb fix(kernel/declaration): allow introspection of declarations in GDB 
If the declaration::cell struct is not defined in the same header file
as declaration, GDB will show the cells as <incomplete type>.
 2016-11-07 14:55:32 -08:00