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
Leonardo de Moura
2a79da1ab6
refactor(kernel): move formatting stuff out of the kernel
2018-06-07 16:28:54 -07:00
Leonardo de Moura
3d38923e07
feat(frontends/lean/inductive_cmds): add option for invoking future inductive module
2018-06-01 16:25:21 -07:00
Leonardo de Moura
de48d49b53
feat(kernel): preparing for adding new inductive datatype module
2018-06-01 14:47:49 -07:00
