Leonardo de Moura
b14d69b1d7
chore(*): remove converter, ac_tactics, hole_commands, rbtree/rbmap proofs, bitvec
2018-04-10 12:25:51 -07:00
Leonardo de Moura
a2f0bf7c1b
chore(*): disable SMT tactic framework and backward chaining
2018-04-10 12:05:51 -07:00
Leonardo de Moura
c08a3bc557
refactor(library/typed_expr): move typed_expr to frontends/lean
2018-04-09 15:25:40 -07:00
Leonardo de Moura
bcaa0b2ad3
refactor(library/typed_expr): do not use macros for implementing typed_expr
...
Remark: in Lean4, we will not have macro_defs.
2018-04-09 15:16:46 -07:00
Leonardo de Moura
8dd53cd94f
chore(*): rename expr_struct_* to expr_*
...
We don't need to modifier `_struct` anymore since we don't use the
pointer equality based hashtables anymore.
2018-04-09 12:55:48 -07:00
Leonardo de Moura
faf8e025e7
chore(kernel): remove m_hash_alloc field from expressions
...
This field was originally added to create hashtables based on pointer
equality. We don't use them anymore, and the caches based on
m_hash_alloc can be implemented using m_hash without any performance
impact. This commit also fixes two places where `expr_set` was used
instead of `expr_struct_set`.
This commit is also important for the Lean4 plans where `expr` will
be implemented in Lean, and fields like `m_hash_alloc` would require us
to track state.
2018-04-09 10:05:56 -07:00
Leonardo de Moura
bdea7d420d
chore(*): type_context ==> type_context_old
2018-03-05 12:38:24 -08:00
Sebastian Ullrich
d6d44a1994
fix(frontends/lean/pp): fix #1922
...
Fixes #1922
2018-03-02 13:02:48 -08:00
Sebastian Ullrich
48147646bc
refactor(library): mk_result/get_result_* ~> mk_success/get_success_*
2018-03-01 14:56:01 +01:00
Sebastian Ullrich
f72a700e34
fix(frontends/lean/decl_cmds): attribute cmd: save info for first ident
2018-02-28 17:42:19 +01:00
Sebastian Ullrich
76843717c4
chore(frontends/lean/elaborator): style
2018-02-28 12:49:22 +01:00
Sebastian Ullrich
1abf8738fc
feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration
2018-02-28 12:49:22 +01:00
Sebastian Ullrich
f3ca420b64
feat(frontends/lean/elaborator): hide opt/auto param types when elaborating structure field values
2018-02-28 12:49:22 +01:00
Sebastian Ullrich
cf8dd9e75e
feat(fronteds/lean/builtin_exprs): do notation: use overloadable bind instead of has_bind.bind
2018-02-28 12:49:22 +01:00
Leonardo de Moura
902445c56f
chore(frontends/lean): remove parser_state object
...
This is dead code. We have decided to implement the new parser in Lean.
2018-02-27 14:05:02 -08:00
Leonardo de Moura
3895fd8511
chore(library): use type_context to update metavar_context
2018-02-27 12:23:26 -08:00
Leonardo de Moura
173eb1c6b7
refactor(util/fresh_name): implement fresh_name using unique thread id
...
@kha This commit is retracting the experiment using
`mk_fresh_name_generator_child` when creating new tasks.
The names get too long.
I'm still refactoring the code and trying to eliminate all occurrences
of `mk_fresh_name`. I still have a long way to go, but I am merging
this branch into master since it has many other fixes.
2018-02-23 10:35:04 -08:00
Leonardo de Moura
5607884787
feat(library/tactic): use new cache
...
Remark: so far, caching, in the tactic framework, only makes a difference for the `simp` tactic.
This is not surprising since the simplifier tries to apply rewriting
lemmas over and over again.
2018-02-21 15:04:20 -08:00
Leonardo de Moura
8a93d2770e
feat(library/equations_compiler): add new cache support to equation compiler
2018-02-21 15:04:20 -08:00
Leonardo de Moura
9d9ac16e7a
feat(library): add implementation of abstract_context_cache
2018-02-21 15:04:20 -08:00
Leonardo de Moura
7762dc381a
feat(library/type_context): use context_cache interface
2018-02-21 15:04:20 -08:00
Leonardo de Moura
11e87545be
chore(frontends/lean): remove dead variables
2018-02-21 15:04:19 -08:00
Leonardo de Moura
f8e0916c64
feat(library/tactic, frontends/lean): replace a few mk_tagged_fresh_name with mk_unused_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
058520d6e4
feat(frontends/lean/pp,library/local_context): use sanitize_name_generator_name
...
Remark: we should remove `sanitize_if_fresh` as soon as we delete `::lean::mk_fresh_name`
2018-02-21 15:04:19 -08:00
Leonardo de Moura
b16f641179
feat(util/name_generator): name generator prefix bookkeeping
2018-02-21 15:04:19 -08:00
Leonardo de Moura
ce028d651d
refactor(kernel): abstract_type_context::mk_fresh_name ==> abstract_type_context::next_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
28d6326228
refactor(frontends/lean/parser): add name_generator
2018-02-21 15:04:19 -08:00
Leonardo de Moura
2e5b66a5f1
refactor(kernel): make sure kernel does not use global ::lean::mk_fresh_name
2018-02-21 15:04:19 -08:00
Leonardo de Moura
8eb34a39cb
feat(frontends/lean): save/restore fresh name_generator state in parser snapshots
2018-02-21 15:04:19 -08:00
Leonardo de Moura
78d8ff8031
feat(*): add reset_thread_local
2018-02-21 15:04:19 -08:00
Sebastian Ullrich
f247363305
feat(library/time_task): print cumulative times on --profile
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
782af7e5d6
chore(library/vm/interaction_state): do not profile calls into Lean other than tactic execution
...
Otherwise, we produce a message for e.g. every single interactive tactic parameter
2018-02-19 09:13:24 -08:00
Sebastian Ullrich
9c5df7875a
perf(frontends/lean/elaborator): visit_structure_instance_fn: delay building error message
2018-02-19 09:13:24 -08:00
Leonardo de Moura
56dba5b98a
fix(frontends/lean/elaborator): fixes #1930
...
@kha the following idiom is not safe
```
while (is_pi(t)) {
t = whnf(binding_body(t));
}
```
`whnf(e)` assumes that `e` does not have dangling deBruijn variables.
We should use (the more expensive):
```
while (is_pi(t)) {
t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
}
```
BTW, this problem is not related to the assertion violation at #1930
I just stumbled on it when fixing the violation.
2018-02-19 08:51:26 -08:00
Nuno Lopes
7b45d28e77
chore(unicode): use utf8 chars directly in strings
2018-02-13 10:42:08 -08:00
Nuno Lopes
c43ebd8bf7
fix(msvc): remove another \uXX char that was causing an infinite loop
2018-02-13 10:42:08 -08:00
Nuno Lopes
977e11f9be
fix(warnings): fix warnings on VS. its now /W2 clean
2018-02-13 10:42:08 -08:00
Sebastian Ullrich
affe3463ab
fix(frontends/lean/elaborator): fix assertion error: accidental mutation of a variable
2018-02-08 14:07:08 +01:00
Sebastian Ullrich
5736fda1ee
chore(frontends/lean/elaborator): do not name mvars from { .. } catchall
...
We already use the same names for the field mvars, which can be confusing during debugging
2018-02-08 14:04:33 +01:00
Nuno Lopes
c1a768b7a7
fix(msvc): further work on MSVC port
...
only 7 files left
2018-02-06 10:11:10 -08:00
Sebastian Ullrich
4d5bd6d03c
fix(frontends/lean/elaborator): fix build
2018-02-02 20:53:24 +01:00
Sebastian Ullrich
703d12d594
feat(frontends/lean/elaborator): do not execute tactics after error recovery
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
b3262d53b4
feat(frontends/lean/elaborator): structure notation: fall back to inferring superclasses
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
86e231e6c9
feat(frontends/lean/structure_cmd): make superclass fields inst implicit
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
9f25cf665e
feat(frontends/lean/elaborator): structure instance notation: allow implicit fields
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
6eeb90c8fb
chore(frontends/lean/elaborator): remove confusing assign_mvar method
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
040748419f
refactor(frontends/lean/elaborator): refactor and document structure instance notation code
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
6ab13a433d
chore(library/type_context): should not have an implicit constructor, copy constructor, or assignment operator
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
3f497b8d8e
fix(library/constructions/projection): out_params should always be implicit in projections
2018-02-02 08:58:52 -08:00
Sebastian Ullrich
33936cc4ad
feat(frontends/lean/decl_cmds): save ident infos after attribute cmd
2018-02-02 08:58:52 -08:00
