Leonardo de Moura
106952622a
chore: modify induction hypotheses generated names
2021-05-01 16:21:12 -07: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
b4012fdd71
chore: remove old comment that is not true anymore
2020-11-23 08:44:50 -08: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
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
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
b9dc76df35
feat: name minor premises using ctor names
2020-02-23 18:45:53 -08:00
Leonardo de Moura
56d6961529
fix: old constant names
2020-01-09 15:40:55 -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
0d5ac5288a
feat(runtime): increase small nat size
...
In 64-bit machines, the max small nat value should now be (2^63 - 1), and on 32-bit
machines (2^32 - 1).
The main motivation for this modification are the array indexing
operations. With the new representation, if a Nat index is not small,
then it must not be a valid index. This was not true in 64-bit
machines. Example: an array of size 2^33 would fit in memory, and but
an index `i` > 2^32 - 1 would not be a small nat value.
2019-03-26 14:21:03 -07:00
Leonardo de Moura
0888dee25e
chore(*): meta ==> unsafe
2019-03-15 15:04:40 -07:00
Leonardo de Moura
c74f4c16ca
feat(library/kernel,library/compiler/csimp): make sure nat.rec and nat.cases_on reduce when major premise is a nat literal
2018-10-10 18:35:15 -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
3b07eeec47
fix(kernel/inductive): name generator was not being consistenly used
2018-09-08 16:21:33 -07:00
Leonardo de Moura
aa3292eb36
feat(kernel/type_checker): remove m_memoize
...
It is always `true`
2018-09-07 20:50:53 -07:00
Leonardo de Moura
1b81577d8b
fix(kernel/inductive): remove unnecessary whnf
...
The frontend is responsible for unfolding reducible definitions before
sending inductive declarations to the kernel.
2018-09-07 17:27:08 -07:00
Leonardo de Moura
58e91559d0
feat(*): use new inductive datatype module
2018-09-06 18:09:22 -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
9970019f76
fix(kernel/inductive): incorrect assertion
...
It fails on non parametric datatypes with nullary constructors.
2018-09-05 09:52:25 -07:00
Leonardo de Moura
176e0a3ed3
fix(kernel/inductive): typo
2018-09-04 17:32:18 -07:00
Leonardo de Moura
ccfcd8279f
fix(kernel/inductive): bug
2018-09-03 16:41:51 -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
f9d87e7a98
feat(kernel/inductive): add inductive postprocessor
...
We still need to restore recursors and their rules
2018-09-02 17:44:19 -07:00
Leonardo de Moura
41a87f6856
feat(kernel/inductive): normalize parameter names
2018-09-02 16:40:31 -07:00
Leonardo de Moura
7d4097818b
feat(kernel/inductive): add recursor rules
2018-09-02 15:55:29 -07:00
Leonardo de Moura
f30cb0635f
chore(kernel/inductive): cleanup
2018-09-02 09:26:58 -07:00
Leonardo de Moura
98f035088c
chore(kernel/inductive): cleanup
2018-08-31 18:01:26 -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
2fb677f1d0
feat(kernel/inductive): add positivity check to new inductive datatype module
2018-08-31 09:52:38 -07:00
Leonardo de Moura
706d7045c3
feat(kernel/inductive): add nested => mutual preprocessor
2018-08-30 18:05:43 -07:00
Leonardo de Moura
f1105e108a
fix(kernel/inductive): bug at check_inductive_types
2018-08-30 18:05:43 -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
d1d56776ad
feat(kernel): invoke add_inductive for inductive datatype declarations
2018-08-28 15:54:46 -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
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
bc57c66ae3
refactor(kernel/level): naming consistency
2018-06-22 10:29:56 -07:00
Leonardo de Moura
e590ebf54d
feat(kernel/inductive): initialize m_elim_level
2018-06-12 15:17:52 -07:00
Leonardo de Moura
effefb8b03
chore(kernel/inductive): style
2018-06-12 13:03:25 -07:00
Leonardo de Moura
5088252aa8
feat(kernel): add proper constructor struct
2018-06-12 13:03:25 -07:00
Leonardo de Moura
c3c6c4afc3
feat(kernel/inductive): add check_inductive_types
2018-06-12 13:03:25 -07:00
Leonardo de Moura
a632df3211
refactor(kernel/inductive): do not use ginductive inductive declaration format
...
The format used by ginductive is more compact, but it forces the kernel
to implement the `infer_implicit_params`. It would also create problems
when we make inductive_decls a special case of declaration
2018-06-11 12:52:44 -07:00
Leonardo de Moura
818170d780
refactor(kernel): remove tag from kernel expressions
...
We are temporarily storing position information in a global table.
2018-06-08 10:29:22 -07:00
