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

116 commits

Author SHA1 Message Date
Arthur Adjedj
ff20a14c69
fix : make mk_no_confusion_type handle delta-reduction when generating telescope (#2501) 
* fix : make `mk_no_confusion_type` handle delta-reduction when checking the inductive type.

* tests: extend `2500.lean`
 2023-10-14 17:18:37 +11:00
Gabriel Ebner
4544443d98 feat: reorder tc subgoals according to out-params 2023-04-10 13:00:04 -07:00
Leonardo de Moura
ffb0f42aae fix: fixes #1901 2022-12-01 08:39:06 -08:00
Leonardo de Moura
081dff288f fix: debug build 2022-04-13 13:12:53 -07:00
Leonardo de Moura
efb859013e chore: ignore {} annotations at mk_projections 2022-04-13 10:16:41 -07:00
Leonardo de Moura
1afee372f7 refactor: move consume_type_annotations declaration to expr.h 2022-03-10 08:00:39 -08:00
Leonardo de Moura
33883e9d2a fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam) 2022-03-10 07:47:38 -08:00
Leonardo de Moura
80a73dd903 feat: basic support for definitions at inductive declarations 2021-10-25 12:44:35 -07:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Leonardo de Moura
d26aa5e1ab feat: black list other auxiliary constructions 2021-04-02 16:21:54 -07:00
Leonardo de Moura
b575087859 fix: unfold class projections when using TransparencyMode.instances 2021-01-25 12:30:26 -08:00
Leonardo de Moura
8c2cb44ac0 fix: error message produced by lean_mk_projections 2020-12-22 17:40:32 -08:00
Leonardo de Moura
de568b1268 chore: remove dead code 2020-10-28 09:33:19 -07:00
Leonardo de Moura
3f0cc1d2ec fix: library/constructions primitives crash at kernel_exception 2020-10-24 18:52:01 -07:00
Leonardo de Moura
f36f7592e6 chore: move to new frontend 2020-10-15 16:18:42 -07:00
Sebastian Ullrich
7718795178 fix: mark Lean objects in C++ globals reachable from the new frontend as persistent 
sed -Ei 's/(g_\w+)\s*= new (name|expr|format|level|string_ref)\W.*;/\0\n    mark_persistent(\1->raw());/' src/kernel/**/*.cpp src/util/**/*.cpp src/library/**/*.cpp
 2020-10-11 17:43:28 +02:00
Leonardo de Moura
7f43d01703 fix: assertion violation 2020-07-24 14:54:20 -07:00
Leonardo de Moura
ca2e82f39b feat: add projections 2020-07-23 16:42:34 -07:00
Leonardo de Moura
8fd25ec326 feat: export "constructions" 
@Kha Maybe one day I will reimplement them in Lean. Note that they do
not depend on the old type_context.
 2020-07-15 16:32:23 -07:00
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Leonardo de Moura
a124461dca chore: rename projection function major field to self 
This is useful for projection function for classes + named arguments.
 2019-12-12 08:55:55 -08:00
Leonardo de Moura
4a6d0a8082 feat: projections of classes should not be reducible 2019-11-23 09:25:49 -08:00
Leonardo de Moura
85092412c7 refactor: remove Expr.FVar hack 
@Kha @dselsam:
This hack was preventing us from making `Expr` a "real" Lean type.
This was bad for a few reasons:
- It was hard to extend/modify `Expr` in Lean since we would also have
to modify the C++ code that creates the `Expr` objects with the hidden
fields.
- `Expr.lam` and `Expr.forallE` were not following the Lean layout
standard where we sort fields by size. @Kha: recall we used that to
avoid a UB. The issue with `Expr.lam` and `Expr.forallE` is that they
have a "visible" field (`BinderInfo`), which is smaller than
hidden fields such as hash code.
- `Expr.fvar` had only one field at `Expr.lean,` but four behind the
scenes.

I added a new constructor `Local` that is only accessible from C++.
It is only used in legacy code we inherited from Lean2.
We will eventually delete it.

This refactoring was quite painful since many parts of the codebase
were mixing the new `Expr.fvar` with the old `Expr.local`.
I doubt I would be able to do it without the new staging framework
@Kha built.

BTW, some of the patches are horrible. I didn't care much since we
are going to deleted the super ugly files. That being said,
you should expect new weird bevaior due to `Expr.fvar` vs `Expr.local`.

Next step: use the new `ExprCachedData` to make all `Expr` hidden visibles
accessible from Lean.

checkpoint
 2019-11-15 14:04:26 -08:00
Leonardo de Moura
1bf1290570 feat: use kernel projections in constructions 
Motivation: auxiliary recursors such as `brecOn` do not depend on
user-facing projection definitions anymore.
Thus, we can simplify `whnfCore` at `TypeUtil`.
 2019-11-04 03:38:57 -08:00
Leonardo de Moura
edeae776da chore(library/module): module::add for declarations is not needed anymore 2019-05-14 11:23:35 -07:00
Leonardo de Moura
2b76d79791 chore(library/init/core): remove more nonsense 2019-03-22 13:14:20 -07:00
Leonardo de Moura
039e7fab48 refactor(library): add suffixes.h with commonly used suffixes such as brec_on 2019-03-21 15:06:43 -07:00
Leonardo de Moura
0888dee25e chore(*): meta ==> unsafe 2019-03-15 15:04:40 -07:00
Leonardo de Moura
c3569dc72d feat(kernel): store structure name in proj-expressions 2018-10-02 09:23:11 -07:00
Leonardo de Moura
fabfe32ca5 chore(*): remove unnecessary scoped_ext dependencies 2018-09-08 15:42:48 -07:00
Leonardo de Moura
dacc4c9cd6 chore(kernel): move abstract_type_context to library 2018-09-08 08:29:51 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
208b932583 feat(library/constructions/brec_on): add brec_on and binduction_on for new inductive datatype module 
We don't support these constructions for nested inductive types, but we
do for mutual inductives.
 2018-09-05 14:46:03 -07:00
Leonardo de Moura
f335623530 feat(library/constructions/brec_on): add below and ibelow for new inductive datatype module 2018-09-05 14:46:03 -07:00
Leonardo de Moura
4964ad660f feat(library/constructions/no_confusion): add no_confusion for new inductive datatype module 2018-09-05 10:27:49 -07:00
Leonardo de Moura
4773a3be5f feat(library/constructions/no_confusion): add no_confusion_type for new inductive datatype module 2018-09-05 09:55:13 -07:00
Leonardo de Moura
d8e7941116 feat(library/constructions/rec_on): add rec_on for new inductive datatype module 2018-09-04 17:22:16 -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
a0283bf2a0 fix(library/constructions/cases_on): bugs 2018-09-04 10:33:56 -07:00
Leonardo de Moura
10a7eccecd feat(library/constructions/cases_on): add cases_on for new inductive datatype module 2018-09-04 09:26:16 -07:00
Leonardo de Moura
b1fb1b069e chore(library/constructions): remove constructor (dead code) 2018-09-03 17:41:19 -07:00
Leonardo de Moura
af8f3c7bb4 chore(library/constructions): remove injective 
It was mainly used to perform dependent elimination with nested
inductive datatypes produced by the inductive compiler.
 2018-09-03 17:38:13 -07:00
Leonardo de Moura
cc748c0b17 chore(library/constructions): remove drec (dead code) 2018-09-03 17:32:16 -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
fc96c335fb chore(library/constructions): remove has_sizeof 
This will be implemented in Lean in the future.
 2018-08-23 11:57:38 -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
f3e99286bb chore(kernel): remove certified_declaration 2018-08-22 12:11:34 -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