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

1543 commits

Author SHA1 Message Date
Leonardo de Moura
d044e9f47e chore: remove instance cache 
If the missing cache generates perf problems in the future, we should
add the cache at `MetaM`.

cc @Kha
 2020-07-08 09:40:34 -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
f4e06664c6 chore: fix debug build 2020-03-18 21:02:00 -07:00
Leonardo de Moura
72ec0ec3ad feat: string literal support on recursors and kernel isDefEq 2020-03-17 17:23:33 -07:00
Leonardo de Moura
0ef54ae74c chore: remove TODO 2020-03-17 17:13:32 -07:00
Leonardo de Moura
ea10c5c6fc feat: add support for reducing Nat basic functions in the kernel 2020-03-17 13:31:57 -07:00
Leonardo de Moura
2e6fac2853 feat: add support for reduceBool and reduceNat in the kernel type_checker 2020-03-14 12:13:22 -07:00
Leonardo de Moura
3e4196a8df feat: expose kernel is_def_eq 2020-03-14 08:15:58 -07:00
Leonardo de Moura
174771cdb3 fix: nat lit support 2020-03-13 06:54:33 -07:00
Leonardo de Moura
16d88b04ea chore: avoid cnstr_set_scalar and cnstr_get_scalar 2020-02-25 13:27:30 -08: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
b9dc76df35 feat: name minor premises using ctor names 2020-02-23 18:45:53 -08:00
Leonardo de Moura
c7d96a6522 fix: theorem values are tasks 2020-01-16 17:20:36 -08:00
Leonardo de Moura
e2ad834a2c fix: weird bug that only occurs in debug mode 2020-01-09 16:11:33 -08:00
Leonardo de Moura
56d6961529 fix: old constant names 2020-01-09 15:40:55 -08:00
Leonardo de Moura
bba9cdd8ff feat: improve support for nat literals 2020-01-09 15:36:46 -08:00
Leonardo de Moura
bccaaa7af0 fix: bug at lit_type binding 
cc @kha
 2020-01-06 15:44:38 -08:00
Leonardo de Moura
769debf970 fix: is_unsafe 2019-12-30 12:05:28 -08:00
Leonardo de Moura
c650e11d6b fix: missing isUnsafe fieldat OpaqueVal 2019-12-30 11:53:08 -08:00
Leonardo de Moura
61191f9921 chore: use b_obj_arg annotation 2019-12-22 15:14:36 -08:00
Sebastian Ullrich
3b37737c8a fix: leaks 2019-12-22 15:09:19 -08:00
Leonardo de Moura
fdfff29bb1 feat: expose liftLooseBVars and lowerLooseBVars 2019-12-21 08:57:11 -08:00
Leonardo de Moura
6ae510cea4 fix: reject inductive datatypes with duplicate constructor names 2019-12-14 09:11:39 -08:00
Leonardo de Moura
8192828b9c fix: lean_expr_update_* functions 2019-12-11 10:15:21 -08:00
Leonardo de Moura
427df087e8 feat: instantiateLevelParams in Lean 2019-12-01 18:32:48 -08:00
Sebastian Ullrich
3980194fbf chore: more assertions and old code 2019-11-19 12:55:02 +01:00
Sebastian Ullrich
11809d23a9 chore: remove outdated assertion 
/cc @leodemoura
 2019-11-19 10:56:35 +01:00
Leonardo de Moura
b78ac59523 refactor: Level fully implemented in Lean 2019-11-17 08:24:09 -08:00
Leonardo de Moura
a3ccbe66cf refactor: Expr fully implemented in Lean 
No hidden fields.
 2019-11-16 12:10:49 -08:00
Leonardo de Moura
3ae5c2f2e4 chore: remove old comment 2019-11-15 14:11:50 -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
aea02eb1f8 chore: fix MVar refactoring issues 2019-11-15 10:04:42 -08:00
Leonardo de Moura
d9f3b4bf63 refactor: remove Expr.mvar hidden field 2019-11-15 10:04:42 -08:00
Leonardo de Moura
017554fbb6 chore: minor optimization 2019-11-11 17:23:59 -08:00
Leonardo de Moura
1e065d495b feat: expose hasLooseBVar 2019-11-09 12:29:50 -08:00
Leonardo de Moura
54ce57fe26 feat: add instantiateRevRange 2019-11-08 08:28:31 -08:00
Leonardo de Moura
146aa71886 feat: reduce auxiliary recursors 2019-11-02 14:38:24 -07:00
Leonardo de Moura
8c7f514a9d feat: expose instantiateLevelParams 2019-10-31 20:12:08 -07:00
Leonardo de Moura
7c99d58b83 chore: update stage0 and fix local_ctx.cpp 2019-10-26 09:55:31 -07:00
Leonardo de Moura
f46db3cc01 feat: add Expr helper functions 2019-10-25 16:47:07 -07:00
Leonardo de Moura
966882b85c feat: add Expr.updateMData 2019-10-25 10:57:17 -07:00
Leonardo de Moura
14afe50384 chore: fix extern Level primitive names 2019-10-24 19:09:37 -07:00
Leonardo de Moura
025e9d32ef feat: update functions for universe levels, use C version of Level.hasParam and Level.hasMVar 2019-10-24 19:04:01 -07:00
Leonardo de Moura
ba286dee8e chore: update stage0 2019-10-24 17:44:41 -07:00
Leonardo de Moura
cb210b0adc feat: expose Expr.hasExprMVar and Expr.hasLevelMVar 2019-10-24 17:32:47 -07:00
Leonardo de Moura
563da4522d chore: udpate stage0 2019-10-24 15:12:09 -07:00
Leonardo de Moura
d1c9a440d8 feat: add missing Expr.update* functions 2019-10-24 15:10:03 -07:00
Leonardo de Moura
93c6ab8eee feat: add Expr.updateApp test of concept 2019-10-23 15:19:34 -07:00
Leonardo de Moura
0032c02247 feat: expose Expr.equal (structural equality) and adding Expr mappings aliases 2019-10-23 10:49:51 -07:00