Leonardo de Moura
4cca030251
chore(library/compiler/lcnf): do not beta reduce at to_lcnf
2018-09-13 18:13:53 -07:00
Leonardo de Moura
31d98caa0f
feat(library/compiler): add compiler simplifier skeleton
2018-09-13 18:13:53 -07:00
Sebastian Ullrich
647f40763c
feat(library/message_builder): pretty-print kernel_exceptions
2018-09-13 16:38:40 -07:00
Sebastian Ullrich
98e09c274f
feat(library/init/lean/parser/{pratt,level}): factor out pratt combinator, implement level parsers
2018-09-13 16:38:40 -07:00
Sebastian Ullrich
b7c3f517a9
feat(frontends/lean/builtin_exprs): support for precedence annotations in node!/node_choice!
2018-09-13 16:38:40 -07:00
Leonardo de Moura
b8dceda9b7
chore(kernel): type_checker::context ==> type_checker::state
2018-09-13 14:06:57 -07:00
Leonardo de Moura
c02e2d3b56
feat(library/compiler/lcnf): split cases followed by application
2018-09-13 12:57:08 -07:00
Leonardo de Moura
23e5136ea2
fix(library/equations_compiler/wf_rec): do not generate code for auxiliary *._pack functions added by equation compiler
...
In the new equation compiler, we should not generate code in the
equation compiler.
2018-09-12 22:05:52 -07:00
Leonardo de Moura
20f31c85bf
chore(kernel/type_checker): we don't use the kernel type checker for elaboration anymore
2018-09-12 20:36:32 -07:00
Leonardo de Moura
c49ad19736
refactor(kernel/type_checker): type_checker::cache ==> type_checker::context
...
We also move `environment` and `name_generator` to
`type_checker::context`. Reason: the cache assumes the environment did
not change. The (cache) correctness relies on the fact that we don't
reuse free variable identifiers.
2018-09-12 20:34:30 -07:00
Leonardo de Moura
7f496f43f1
fix(library/compiler/lcnf): it was not erasing proofs that start with Pi
2018-09-12 18:26:23 -07:00
Leonardo de Moura
379c06faf4
fix(library/compiler/lcnf): avoid trivial let-decls
2018-09-12 18:24:12 -07:00
Leonardo de Moura
3ec73b7156
fix(library/equations_compiler/compiler): avoid pull_nested_rec_fn by unfolding auxiliary declarations
...
The idea is to mimic the behavior of meta definitions.
This is a temporary fix. The new equation compiler will have to provide
a better solution for this problem.
2018-09-12 18:17:50 -07:00
Leonardo de Moura
1be71cf725
chore(shell/lean): fix unused variable warning
2018-09-12 16:51:59 -07:00
Leonardo de Moura
df9d0b2211
fix(frontends/lean/elaborator): avoid internal identifiers leaking as "user names" in equations
2018-09-12 15:09:44 -07:00
Leonardo de Moura
bfb3ffbc79
feat(library/compiler/lcnf): safe beta reduction
2018-09-12 14:51:19 -07:00
Leonardo de Moura
112f183be4
feat(library/compiler/lcnf): eliminate false.cases_on and eq.cases_on
2018-09-12 14:27:01 -07:00
Leonardo de Moura
1e5f0a91f1
feat(library/compiler/lcnf): eliminate and.rec and and.cases_on
2018-09-12 14:21:28 -07:00
Leonardo de Moura
b1fb4416f3
feat(library/compiler/lcnf): make sure constructor applications are fully applied
2018-09-12 14:04:24 -07:00
Leonardo de Moura
4058276a82
feat(library/compiler/lcnf): eliminate false.rec
2018-09-12 13:55:32 -07:00
Leonardo de Moura
cfdc331ecb
feat(library/compiler/lcnf): replace eq.rec and eq.ndrec applications with lc_cast
2018-09-12 11:00:34 -07:00
Leonardo de Moura
c526670e6f
feat(library/compiler/lcnf): eliminate id_rhs even if it is partially applied
2018-09-12 10:45:23 -07:00
Leonardo de Moura
2d6582e67c
fix(library/compiler/lcnf): dumb mistake, Pi case is not reachable
2018-09-12 10:40:09 -07:00
Leonardo de Moura
ec1809de74
fix(library/compiler/lcnf): restore cache
2018-09-12 10:40:09 -07:00
Leonardo de Moura
70f057bee7
chore(library/type_context): add infer_proj to type_context_old
...
We need it to pp the new compiler intermediate results.
2018-09-12 10:40:09 -07:00
Leonardo de Moura
ec92653d93
feat(library/compiler/lcnf): do not create aux let-decl for lc_proof-applications
2018-09-12 10:40:09 -07:00
Leonardo de Moura
d5d926b0ef
feat(library/compiler/lcnf): eliminate no_confusion
2018-09-12 10:40:09 -07:00
Sebastian Ullrich
c5bc567a16
chore(library/module_mgr): fix warning
2018-09-12 10:38:25 -07:00
Sebastian Ullrich
f738e51ae1
fix(library/module_mgr): go back to storing transitive mtime in module_info
...
It was being discarded when the module_mgr was called multiple times from the
outside, i.e. in the loop in lean.cpp
2018-09-12 09:31:48 -07:00
Sebastian Ullrich
75b2b09c08
feat(library/module_mgr): 'trace.import' trace class
2018-09-12 09:14:58 -07:00
Sebastian Ullrich
62671c8b6f
fix(shell/lean): Flycheck doesn't ignore stderr
2018-09-12 08:29:21 -07:00
Leonardo de Moura
de2abf5d8c
fix(library/compiler/lc_util): missing file
2018-09-11 18:11:27 -07:00
Leonardo de Moura
8ee10e202f
chore(library/compiler/lcnf): use _x_<idx> instead of _x.<idx>
...
This is a temporary change while we debug the new compiler.
2018-09-11 18:10:10 -07:00
Leonardo de Moura
72e99ea3ee
fix(library/compiler/lcnf): apply_beta takes arguments in reverse order
2018-09-11 18:10:10 -07:00
Leonardo de Moura
3ba777e709
fix(frontends/lean/pp): do not pp let type when m_binder_types == false
2018-09-11 18:10:10 -07:00
Leonardo de Moura
d814ee612a
chore(kernel/local_ctx): typo
2018-09-11 18:10:10 -07:00
Leonardo de Moura
9b21287a3e
feat(library/compiler/lcnf): add lean compiler normal form
2018-09-11 18:10:10 -07:00
Sebastian Ullrich
52d4cc10ad
feat(shell/lean,lean4-mode/lean4-flycheck): use stdin for communication
...
no more `flycheck_` files
2018-09-11 16:35:25 -07:00
Leonardo de Moura
81545c12f2
chore(runtime/object): fix comment
2018-09-11 14:31:14 -07:00
Leonardo de Moura
46d6f7bfb5
chore(runtime/object): store function pointer as void * inside closure
2018-09-11 14:27:45 -07:00
Leonardo de Moura
e8fa692611
chore(runtime/object): change default object_memory_kind to STHeap
2018-09-11 13:57:55 -07:00
Leonardo de Moura
3feae112bc
chore(frontends/lean/parser): unused var warning
2018-09-11 13:55:44 -07:00
Leonardo de Moura
6914d35062
chore(library/compiler/preprocess): dead trace option
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
78ced9ffcf
refactor(library/module_mgr): minimize parser interface
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
43e57358af
refactor(library/module_mgr): minor refactorings
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af99f153f8
refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
716de48078
chore(library/module): remove loaded_module.m_env
...
It was used by `--run` only, which I guess will change quite a bit anyway
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
904d7c4a88
chore(*): remove old task API and task queues
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af55cb13e7
fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
38208802c6
refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous
2018-09-11 13:55:25 -07:00
