Leonardo de Moura
4432629eb0
feat(util/nat): add C++ wrapper for manipulating runtime nat values
2018-06-13 09:29:52 -07:00
Leonardo de Moura
a3e5dd31b3
chore(library/locals): style
2018-06-12 17:58:25 -07:00
Leonardo de Moura
ba598ada1a
fix(library/init/meta/expr): expose quote constructor
2018-06-12 17:55:27 -07:00
Leonardo de Moura
1c6350b0f1
fix(frontends/lean/elaborator): quote case
2018-06-12 17:55:00 -07:00
Leonardo de Moura
335c58f8a7
feat(kernel): add expr_kind::Quote
...
This is a temporary expr constructor. We need it to be able to eliminate
expr_macro, and then define expr using runtime/object
2018-06-12 17:40:00 -07:00
Leonardo de Moura
e590ebf54d
feat(kernel/inductive): initialize m_elim_level
2018-06-12 15:17:52 -07:00
Leonardo de Moura
e41a2ef3d8
chore(tests/lean): fix tests
2018-06-12 13:06:33 -07:00
Leonardo de Moura
a7d08d2f3d
feat(kernel/inductive/inductive): dependent elimination for inductive predicates
...
In Lean4, we will not generate non dependent recursors for inductive
predicates. The main goal is to make the shape of the automatically
generated recursors more uniform. The non uniform representation is
leftover from Lean2. In Lean2, we wanted to support different kernels
with different features. For example: we could create proof relevant
kernels, no impredicative universe, etc.
Recall that, in a kernel with an impredicative Prop and no proof
irrelevance, inductive predicates without dependent elimination are
weaker that inductive predicates with dependent elimination.
When proof irrelevance is enabled, we can generate the dependent
recursor from the non dependent one. Actually, the module drec.cpp
generates the dependent recursor.
Now, we only support one kind of kernel, and it doesn't make sense
anymore to generate non dependent recursors for inductive predicates.
This would only produce an unnecessary asymmetry on the inductive
datatype module.
Remark: we had to create non dependent recursors to help the elaborator.
This can be avoid if we improve the elaborator. I will do that in the
new elaborator implemented in Lean.
Remark: equation lemmas are broken for definitions that pattern match on
nested inductive datatypes. The problem is the super messy
`prove_eq_rec_invertible_aux` function. This function will not be needed
after I finish the new inductive datatype support in the kernel.
cc @kha
2018-06-12 13:03:26 -07:00
Leonardo de Moura
effefb8b03
chore(kernel/inductive): style
2018-06-12 13:03:25 -07:00
Leonardo de Moura
e9b4b811de
chore(library/equations_compiler/util): disable generation of equational lemmas
...
@kha, `eqn_compiler.lemmas` is false by default.
I will keep them disabled until I remove the inductive compiler.
I'm building the new inductive datatype module (to replace the inductive
compiler), and the lemmas will fail to be proved in the next commits
until the transition is complete.
2018-06-12 13:03:25 -07:00
Leonardo de Moura
cf91139c37
refactor(library/inductive_compiler): remove sizeof lemma generation
...
Remark: we are in the process of deleting the inductive_compiler
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
b2bebbf75d
chore(kernel): check_no_mlocal ==> check_no_metavar_no_fvar
2018-06-12 13:03:25 -07:00
Sebastian Ullrich
42d58580e6
chore(script/prepare-commit-msg): remove file extension, guess change type
2018-06-12 17:39:59 +02:00
Sebastian Ullrich
b01288e118
chore(tests/lean/lisp): speed up test
2018-06-12 17:39:59 +02: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
7655d5f328
refactor(kernel): has_local ==> has_fvar
2018-06-11 10:46:05 -07:00
Leonardo de Moura
4ff710b709
fix(kernel/old_type_checker): assertion violation
2018-06-11 10:40:09 -07:00
Leonardo de Moura
d2efeca70c
chore(kernel/instantiate): use new function names
2018-06-11 10:18:01 -07:00
Leonardo de Moura
50e50408eb
feat(kernel): type checker with local_ctx
2018-06-11 09:59:49 -07:00
Leonardo de Moura
26b47c2852
chore(kernel/old_type_checker): cleanup
2018-06-11 08:57:22 -07:00
Leonardo de Moura
bf165e0f51
fix(kernel/quot): assertion violation
2018-06-09 08:50:32 -07:00
Leonardo de Moura
06337d04e5
chore(library/tactic/simplify): fix compilation error
2018-06-09 08:11:51 -07:00
Leonardo de Moura
c632123fd1
chore(kernel/quot): avoid legacy code
2018-06-09 07:54:45 -07:00
Leonardo de Moura
d5c24806e7
feat(kernel/local_ctx): add methods for replacing legacy Pi/Fun
2018-06-09 07:45:16 -07:00
Leonardo de Moura
a6250840d5
chore(kernel): rename some expr functions
2018-06-09 07:18:24 -07:00
Leonardo de Moura
1612aca0b2
chore(kernel): rename expr kinds
2018-06-09 06:50:14 -07:00
Leonardo de Moura
9626ad919c
chore(library/export): remove text export module
...
This can be implemented in Lean.
2018-06-08 13:36:36 -07:00
Leonardo de Moura
62788a9ca3
refactor(kernel): fix terminology: "free_var" is actually a loose bound variable
...
We represent free variables uisng local constants.
We will fix this terminology too.
2018-06-08 13:25:36 -07:00
Leonardo de Moura
bd91d08bcd
chore(library/replace_visitor): add copy_pos
2018-06-08 11:25:07 -07:00
Leonardo de Moura
03391006dc
chore(tests/lean/revert): fix test
2018-06-08 11:21:01 -07:00
Leonardo de Moura
7057f69923
chore(library/pos_info_provider): style
2018-06-08 11:15:30 -07:00
Leonardo de Moura
4836dd55b5
chore(frontends/lean): propogate position information
...
This is a huge HACK to get some position information.
2018-06-08 11:12:01 -07:00
Leonardo de Moura
ad892ca97c
feat(library/pos_info_provider): store raw pointers at pos_info table
...
This is imprecise, but we avoid memory retention issue.
2018-06-08 10:44:16 -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
6a84b9378a
chore(library/inductive_compiler/util): fix assertion
2018-06-07 16:28:54 -07:00
Leonardo de Moura
45da5872e6
chore(checker): remove leanchecker
2018-06-07 16:28:54 -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
8ae1e51b6d
feat(kernel): distinguish kernel_exceptions using different classes
2018-06-07 16:28:54 -07:00
Leonardo de Moura
e90585737f
refactor(*): use C++11 std::current_exception and std::rethrow_exception
...
With these new C++11 APIs, we can delete the `clone` and `rethrow`
methods from our exception classes.
2018-06-07 16:28:54 -07:00
Leonardo de Moura
c697cf4c29
chore(tests/util): remove exception test
2018-06-07 16:28:54 -07:00
Leonardo de Moura
2d7b6ed12c
chore(library/compiler): remove copy_tag from old compiler
2018-06-07 16:28:54 -07:00
Leonardo de Moura
c73e628e50
chore(kernel/abstract): add LEGACY comment
2018-06-07 16:28:54 -07:00
Leonardo de Moura
ddf1c89e76
chore(kernel/abstract): remove mk_binding cache
2018-06-07 16:28:54 -07:00
Leonardo de Moura
3d1faee826
chore(kernel/abstract_type_context): remove dead method abstract_type_context::abstract
...
We needed this method when we were using delayed abstractions
2018-06-07 16:28:54 -07:00
Leonardo de Moura
6333043adf
refactor(kernel): abstract_local(s) ==> abstract
2018-06-07 16:28:54 -07:00
Leonardo de Moura
de82517d80
refactor(kernel): remove abstract since we only use abstract_locals
2018-06-07 16:28:54 -07:00
Sebastian Ullrich
3304221aa2
chore(tests/lean/lisp.lean): update test output
2018-06-07 18:00:24 +02:00
Sebastian Ullrich
cdb1f22156
test(tests/lean/lisp.lean): add or and if macros
2018-06-07 17:39:51 +02:00
