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
244b72befd
feat: simpArrow
2021-01-01 17:15:15 -08:00
Leonardo de Moura
17114cc3e8
feat: make sure kernel generates KernelException.declHasMVars instead of KernelException.other
...
... when a declaration contains metavariables.
2020-12-24 06:56:22 -08:00
Leonardo de Moura
c71eebde8c
chore: remove util/buffer.h dependency from runtime
2020-12-14 18:07: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
b4012fdd71
chore: remove old comment that is not true anymore
2020-11-23 08:44:50 -08:00
Leonardo de Moura
17fb995348
feat: improve mkLevelMax'
2020-11-14 08:36:23 -08:00
Leonardo de Moura
438494ae3f
chore: fix assertion
2020-11-02 06:22:46 -08:00
Leonardo de Moura
7b5f283507
chore: remove Expr.localE constructor
...
It was used by the old frontend
2020-11-01 09:37:48 -08:00
Leonardo de Moura
de568b1268
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
16f7bef88f
chore: remove old frontend leftovers
2020-10-26 09:08:07 -07:00
Leonardo de Moura
ec17fcbc1a
feat: use motive to name the kernel generated recursor
...
Motivation: users can use named arguments to provide them.
2020-10-23 05:31:28 -07:00
Sebastian Ullrich
438b3351dd
feat: add interpreter.prefer_native option
2020-10-21 11:21:56 +02:00
Sebastian Ullrich
f5565d1d92
fix: mark a few more things as persistent
2020-10-11 17:43:28 +02:00
Sebastian Ullrich
c3c037b4de
fix: fixup a few automatic fixes
2020-10-11 17:43:28 +02: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
8383177c96
fix: nonoptimal specialization
...
@Kha Here is the fix for the problem I told you this morning.
Please, take a look at `specialize.cpp` and see whether it makes sense.
2020-09-24 12:40:28 -07:00
Leonardo de Moura
1480b39d86
chore: no Task in Theorem
2020-09-03 08:47:55 -07:00
Leonardo de Moura
b64e44fc44
fix: allow kernel projections to be used in inductive families containing only one constructor
2020-08-05 12:56:04 -07:00
Leonardo de Moura
fb5440a074
fix: new frontend does not eagerly simplify universe level expressions
...
Remark: even if we change the new frontend to simplify all universe
level expressions, we should not rely on this property in the kernel.
Reason: users may still create terms without this property.
Remark: this bug was preventing the kernel from accepting valid declarations.
2020-07-24 15:45:01 -07:00
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
