Leonardo de Moura
774fa01b1a
chore(library/pp_options): reduce pp default limits
2016-02-04 14:55:21 -08:00
Leonardo de Moura
42fbc63bb6
fix(library/tc_multigraph): avoid name collisions
...
@avigad, @fpvandoorn, @rlewis1988, @dselsam
I changed how transitive instances are named.
The motivation is to avoid a naming collision problem found by Daniel.
Before this commit, we were getting an error on the following file
tests/lean/run/collision_bug.lean.
Now, transitive instances contain the prefix "_trans_".
It makes it clear this is an internal definition and it should not be used
by users.
This change also demonstrates (again) how the `rewrite` tactic is
fragile. The problem is that the matching procedure used by it has
very little support for solving matching constraints that involving type
class instances. Eventually, we will need to reimplement `rewrite`
using the new unification procedure used in blast.
In the meantime, the workaround is to use `krewrite` (as usual).
2016-02-04 13:15:42 -08:00
Leonardo de Moura
9d88db3941
perf(library/type_context): add cache for minimizing the access to is_opaque and environment::find
2016-02-02 19:47:58 -08:00
Leonardo de Moura
701d6b5016
perf(library/blast/forward/pattern): simplify is_higher_order test
2016-02-02 18:56:48 -08:00
Leonardo de Moura
a7b3dcbc09
perf(library/blast/state): do not add hypotheses that are Pi-expressions into discrimination trees
2016-02-02 18:50:23 -08:00
Leonardo de Moura
c55b10af1b
perf(library/type_context): move check_system to strategic places
2016-02-02 16:12:53 -08:00
Leonardo de Moura
b508cf813c
perf(library/type_context): small optimization
2016-02-02 15:36:53 -08:00
Leonardo de Moura
bc86e9f179
perf(library/type_context): add caching for type_context::infer
2016-02-02 15:24:57 -08:00
Leonardo de Moura
a7b37d0e09
perf(library/type_context): cache type class resolution failures too
2016-01-29 14:06:47 -08:00
Leonardo de Moura
6b137b7dd3
chore(library/blast/forward/ematch): improve comment
2016-01-29 11:55:51 -08:00
Leonardo de Moura
587c263c28
feat(library/blast/forward/ematch): improve support for casts in the e-matcher
2016-01-29 11:38:43 -08:00
Daniel Selsam
6ed6306c3f
fix(library/blast/unit/unit_propagate): use ppb when tracing
2016-01-27 15:23:52 -08:00
Leonardo de Moura
684995640a
fix(library/blast/unit/unit_propagate): memory access violation
2016-01-27 15:22:34 -08:00
Leonardo de Moura
fb95b71a5e
fix(library/blast/forward/pattern): bug in the pattern inference code
2016-01-27 13:39:19 -08:00
Leonardo de Moura
a713ca9686
feat(library/type_context): add helper method get_num_choice_points
2016-01-26 22:02:25 -08:00
Daniel Selsam
12e148c7b6
feat(library/blast/forward/ematch): even more tracing
2016-01-26 21:40:46 -08:00
Daniel Selsam
2868ec9c43
fix(library/blast/trace): missing pragma
2016-01-26 20:41:01 -08:00
Daniel Selsam
eca079a4fc
feat(library/blast/unit/unit_propagate): basic tracing
2016-01-26 20:40:42 -08:00
Leonardo de Moura
810ee9759c
fix(library/blast/backward/backward_action): add missing normalize at backward_action, and remove incorrect fix at discrimination tree
2016-01-26 20:35:57 -08:00
Leonardo de Moura
6f6672eaaa
fix(library/blast/discr_tree): ignore annotations in discrimination trees
2016-01-26 18:46:40 -08:00
Daniel Selsam
568b3bbeeb
feat(library/blast/forward/ematch): trace match-ss
2016-01-24 16:24:24 -08:00
Daniel Selsam
98fb43e991
fix(library/blast/forward/ematch): advance iterator before continuing
2016-01-24 16:23:44 -08:00
Daniel Selsam
753d5d0689
fix(library/blast/grind/intro_elim_lemmas): need to copy expr
2016-01-24 16:23:27 -08:00
Leonardo de Moura
d12067193b
fix(library/blast/forward/pattern): residue computation in the ematching module
2016-01-24 16:15:33 -08:00
Leonardo de Moura
38ab1cae9e
feat(library/blast/unit/unit_propagate): basic support for "dependent lemmas" at unit propagate
...
New test contains examples of "dependent lemmas"
2016-01-24 16:02:08 -08:00
Leonardo de Moura
297ef10611
fix(library/blast/congruence_closure): subsingleton propagation in the congruence closure module
...
We must normalize inferred type.
2016-01-24 14:55:28 -08:00
Leonardo de Moura
3d0ea4c9d1
feat(library/type_context): improve find_unsynth_metavar
2016-01-24 13:39:25 -08:00
Daniel Selsam
b2554dcb8f
fix(library/blast/congruence_closure): cannot assume all subterms have been internalized
2016-01-16 20:10:21 -08:00
Leonardo de Moura
19bfbe2df8
fix(library/blast/congruence_closure): uselist initialization (aka add_occurrence)
...
Make sure it matches the description in the paper.
2016-01-16 19:53:36 -08:00
Leonardo de Moura
1d04160a9b
fix(library/blast/congruence_closure): bug at eq_congr_key_cmp::operator()(eq_congr_key const & k1, eq_congr_key const & k2)
...
It was not implementing the condition described in our paper.
2016-01-16 19:33:24 -08:00
Leonardo de Moura
98319139d9
fix(library/blast/forward/ematch): bug in match_leaf
2016-01-16 10:51:00 -08:00
Daniel Selsam
a883101a3b
feat(library/blast/forward/ematch): basic support for heq classes
2016-01-15 21:38:16 -08:00
Daniel Selsam
abbffc7436
feat(library/blast/forward/ematch): more tracing
2016-01-13 22:04:12 -08:00
Leonardo de Moura
8d49e42ec2
fix(library/blast/congruence_closure): user-defined congruence lemmas for equality and relation congruences
2016-01-13 21:59:38 -08:00
Leonardo de Moura
3f7122ce07
feat(library/blast/congruence_closure): more general congruence lemmas
2016-01-13 21:44:32 -08:00
Leonardo de Moura
f0cc98ebb5
chore(library/blast/recursor/recursor_action): disable spurious warning
2016-01-13 17:28:13 -08:00
Leonardo de Moura
b1d32bbaf6
chore(library/blast/forward/ematch): more tracing
2016-01-13 16:28:09 -08:00
Daniel Selsam
ba16d188e6
feat(library/blast/forward/ematch): basic debug tracing
2016-01-13 15:15:15 -08:00
Daniel Selsam
58d41e486c
feat(library/trace): register debug trace class
2016-01-13 15:15:15 -08:00
Leonardo de Moura
599ec08c70
feat(library/blast/congruence_closure): add support for eq.rec and cast in the congruence closure module
2016-01-13 14:18:38 -08:00
Leonardo de Moura
c19be9d9e7
feat(library/util): add is_app_of helper function
2016-01-13 13:33:30 -08:00
Leonardo de Moura
8fded5224b
chore(library/blast/congruence_closure): improve comment
2016-01-13 13:06:09 -08:00
Leonardo de Moura
3643e79cb3
feat(library/blast/congruence_closure): improve the suppoer for subsingletons in the ematching procedure
2016-01-13 11:17:42 -08:00
Leonardo de Moura
8f7b533ca1
refactor(library): move 'cast' to init folder
2016-01-13 11:17:42 -08:00
Leonardo de Moura
12876ccc20
fix(library/blast/forward/ematch): ematch + subsingleton
2016-01-12 22:31:09 -08:00
Leonardo de Moura
c2b6e3c29c
fix(library/blast/recursor/recursor_strategy): deactivate hypotheses before invoking nested strategy
2016-01-12 18:41:14 -08:00
Leonardo de Moura
b40f0ffe8b
fix(library/blast/forward/ematch): keep using ematching on implicit arguments
...
Ematching module should only ignore type classes (i.e., instance
implicit) and subsingletons (which includes propositions).
2016-01-11 15:40:51 -08:00
Leonardo de Moura
bb759b1a90
feat(library/blast/congruence_closure): use blast.cc.heq by default
2016-01-11 11:59:54 -08:00
Leonardo de Moura
5edcccaeb0
feat(library/blast/forward/ematch): add support for the new hcongr lemmas in the ematching module
2016-01-11 11:56:36 -08:00
Leonardo de Moura
32268b71d2
feat(library/app_builder): avoid redundant heq_of_eq(eq_of_heq(H)) proofs
2016-01-10 19:29:34 -08:00
