Leonardo de Moura
6c038626f8
fix(library/blast/simple_strategy): tracing
2015-11-13 15:22:09 -08:00
Leonardo de Moura
ca4c078089
feat(library/blast): add "subst" action
2015-11-13 15:21:26 -08:00
Leonardo de Moura
cc4608a392
feat(library/blast): add "revert" auxiliary action
2015-11-13 14:15:48 -08:00
Leonardo de Moura
0dd6d6b140
feat(library/blast): avoid default name when creating hypotheses
2015-11-13 13:13:48 -08:00
Leonardo de Moura
bc8c5a3f68
feat(library/blast): basic tracing for blast
2015-11-13 13:05:20 -08:00
Leonardo de Moura
2889ec5870
feat(library/blast/state): add methods for deleting hypotheses
2015-11-13 11:59:34 -08:00
Leonardo de Moura
0a25652885
feat(library/blast/intros): intros is now a silent step.
2015-11-13 10:55:15 -08:00
Leonardo de Moura
4aa20fcff0
feat(library/blast/state): add support for "silent" proof steps.
2015-11-13 10:54:10 -08:00
Leonardo de Moura
2e32cf51f9
feat(library/blast/state): do not track dependecies to values
2015-11-13 10:38:25 -08:00
Leonardo de Moura
a7fdf5cc73
fix(library/blast/blast): avoid unnecessary calls to set_local_instances
...
This was producing a performance problem since the cache is invalidated/flushed
whenever we call this method.
2015-11-13 10:08:29 -08:00
Daniel Selsam
1276f2f050
feat(library/blast/simplifier): struct for cache key
2015-11-12 21:21:52 -08:00
Daniel Selsam
4e85d59785
style(library/abstract_expr_manager): whitespace
2015-11-12 21:21:52 -08:00
Daniel Selsam
031979cb49
feat(library/blast/simplifier): take simp_rule_sets as argument
2015-11-12 21:20:16 -08:00
Leonardo de Moura
8f378db661
feat(library/blast): add normalize procedure to blast API
2015-11-12 20:42:58 -08:00
Leonardo de Moura
1e436b8b3e
fix(library/blast/state): incorrect assertions
2015-11-12 16:28:09 -08:00
Leonardo de Moura
98f91931bf
fix(library/blast/state): compilation errors
2015-11-12 16:25:59 -08:00
Leonardo de Moura
6eef52196e
feat(library/blast): add gexpr "generalized expressions"
2015-11-11 16:11:51 -08:00
Leonardo de Moura
fee0cff295
feat(library/blast): add simple indexing data-structure for active hypotheses
2015-11-11 00:02:47 -08:00
Leonardo de Moura
bd06bf9fb1
doc(library/blast): document action_result
2015-11-10 17:49:41 -08:00
Leonardo de Moura
48eb6cb138
refactor(library/blast/state): simplify state
2015-11-10 17:27:39 -08:00
Leonardo de Moura
511337a4e9
fix(library/blast): missing file
2015-11-10 17:00:26 -08:00
Leonardo de Moura
f8f3f9402e
feat(library/blast): major reorg and basic backward chaining action
2015-11-10 17:00:16 -08:00
Leonardo de Moura
5be1893d98
fix(library/blast/state): bug at instantiate_urefs_mrefs
2015-11-10 16:38:44 -08:00
Leonardo de Moura
6f01a7339a
refactor(library/blast): move simple search strategy to separate module
2015-11-10 11:44:18 -08:00
Leonardo de Moura
6ac2bf9c6c
refactor(library/blast): add choice_point object
2015-11-10 11:28:59 -08:00
Leonardo de Moura
b76cdb1c68
refactor(library/blast): move blast options to separate module
2015-11-10 11:03:54 -08:00
Leonardo de Moura
f1c2a88e17
feat(library/blast): add proof_expr thin layer for creating proof terms at blast
2015-11-10 10:50:58 -08:00
Leonardo de Moura
5304f62f54
feat(library/blast/hypothesis): track proof depth in hypotheses
2015-11-10 09:54:28 -08:00
Leonardo de Moura
409ad18f9b
refactor(library/blast/state): cleanup state interface
2015-11-10 09:20:44 -08:00
Daniel Selsam
fc5dba4cd1
fix(library/simplifier/simp_rule_set): use lists instead of vectors
2015-11-10 08:58:46 -08:00
Leonardo de Moura
b59dd2305c
refactor(library/blast): rename state::get ==> state::get_hypothesis_decl
2015-11-09 14:52:21 -08:00
Leonardo de Moura
fb7a47cf2b
refactor(library/blast): avoid auxiliary local when creating hypothesis for intros
2015-11-09 14:40:39 -08:00
Leonardo de Moura
a14bb86148
feat(library/blast/state): add mk_lambda/mk_pi for abstracting hrefs
2015-11-09 14:20:19 -08:00
Leonardo de Moura
973a5c4812
feat(library/blast): improve blast type_context push/pop operations
2015-11-09 13:36:49 -08:00
Leonardo de Moura
9c364b410e
refactor(library/blast): hypothesis m_depth ==> m_dep_depth
2015-11-09 13:29:07 -08:00
Leonardo de Moura
9a557958f4
refactor(library/blast): merge state and branch classes
...
We will keep only one active branch in blast.
All other branches are implicit.
2015-11-09 13:24:30 -08:00
Leonardo de Moura
9bdf3a0d33
refactor(library/blast): we should reuse uref/mref/href in idxs
...
Motivation: avoid nasty bugs when caching results
2015-11-09 12:41:52 -08:00
Leonardo de Moura
d952a1d299
refactor(library/blast/expr): remove unnecessary complexity
2015-11-09 12:27:33 -08:00
Leonardo de Moura
c5117785a8
feat(library/blast): add intros action
2015-11-08 19:18:40 -08:00
Leonardo de Moura
78f1679b03
feat(library/blast): add basic assumption action
2015-11-08 18:16:34 -08:00
Leonardo de Moura
6340b1ae5b
feat(library/blast): very basic search procedure and iterative deepening
2015-11-08 17:57:37 -08:00
Leonardo de Moura
8308e87a6c
feat(library/blast/blast): initialize local instances at type_context objects
2015-11-08 15:20:05 -08:00
Leonardo de Moura
39019b6873
refactor(library/blast/simplifier): use app_builder mk_congr, mk_congr_arg and mk_congr_fun
2015-11-08 14:05:03 -08:00
Leonardo de Moura
1374f8cba1
fix(library/blast/simplifier): compilation warnings
2015-11-08 14:05:03 -08:00
Leonardo de Moura
b8857b078b
feat(library/blast): add get_app_builder to blast API
2015-11-08 14:05:03 -08:00
Leonardo de Moura
1d1f043192
refactor(library/app_builder): throw exception instead of returning none_expr
2015-11-08 14:05:03 -08:00
Daniel Selsam
0061d595d0
feat(library/blast/simplifier): use generated congruence lemmas
2015-11-08 14:05:03 -08:00
Daniel Selsam
b2368ba81b
style(library/blast/simplifier): whitespace
2015-11-08 14:05:03 -08:00
Daniel Selsam
f1d5cc5d5b
test(library/blast/simplifier): add asserts
2015-11-08 14:05:03 -08:00
Leonardo de Moura
afc7a2af84
feat(library/blast): expose mk_congr_lemma_for_simp and get_fun_info
2015-11-08 14:05:03 -08:00
Daniel Selsam
f3caeb77cd
style(library/blast/simplifier): whitespace
2015-11-08 14:05:03 -08:00
Daniel Selsam
6c2c82f47c
feat(library/blast/simplifier): conditional rewriting
2015-11-08 14:05:03 -08:00
Daniel Selsam
d4e410162b
feat(library/blast/simplifier): expand macros
2015-11-08 14:05:02 -08:00
Daniel Selsam
b727d5810a
feat(library/blast/simplifier): rewrite with tmp locals
2015-11-08 14:05:02 -08:00
Daniel Selsam
3f331a261a
fix(library/blast/simplifier): stack of caches for local context
2015-11-08 14:05:02 -08:00
Daniel Selsam
b81aa35221
feat(library/blast/simplifier): more informative tracing
2015-11-08 14:05:02 -08:00
Daniel Selsam
0ad41173bb
fix(library/blast/simplifier): caches for each relation
2015-11-08 14:05:02 -08:00
Daniel Selsam
a304f6a9df
fix(library/blast/simplifier): loop rewrite rules
2015-11-08 14:05:02 -08:00
Daniel Selsam
a73e4e30a3
feat(library/blast/simplifier): use new blast_tmp_type_context constructor
2015-11-08 14:05:02 -08:00
Daniel Selsam
8e5e8e6540
feat(library/blast/simplifier): basic infrastructure
2015-11-08 14:05:02 -08:00
Leonardo de Moura
78b1d4279b
fix(library/blast/state): compilation problems in debug mode
2015-11-08 14:05:01 -08:00
Leonardo de Moura
8d9d84f33c
refactor(library/blast): we don't require maximally shared terms anymore in blast
...
This commit also removes the blast::mk_* expr and level functions.
They were just noops.
I kept only mk_uref, mk_href and mk_mref
2015-11-08 14:05:01 -08:00
Leonardo de Moura
45c02cb65c
feat(library/blast/blast): add extra constructor
2015-11-08 14:05:01 -08:00
Leonardo de Moura
980eb95e0c
fix(library/type_context,library/blast/blast): blast uses multiple type_context objects, this commit makes sure all of them use the same local name generator
2015-11-08 14:05:01 -08:00
Leonardo de Moura
98b79373cc
feat(library/blast/blast): add blast::internalize
2015-11-08 14:05:01 -08:00
Leonardo de Moura
43efc11f36
feat(library/blast/blast): automatically clear tmp_type_context at recycling time
2015-11-08 14:05:01 -08:00
Leonardo de Moura
3517a3dfa9
feat(library/blast): add blast_tmp_type_context
2015-11-08 14:05:01 -08:00
Leonardo de Moura
aa697206e8
refactor(library/type_context): rename set_context to set_local_instances
2015-11-08 14:05:01 -08:00
Leonardo de Moura
fb7efa9337
feat(library/type_context): new tmp local_constant policy
2015-11-08 14:05:01 -08:00
Leonardo de Moura
333ba83087
feat(library/type_context): add mk_tmp_local that allows us to specify the pretty printing name
...
We also modify the type inference procedure to preserve the binder names.
2015-11-08 14:05:01 -08:00
Leonardo de Moura
5b71025b07
fix(library/blast/blast): temporary type_context for blast must handle external meta-variables.
2015-11-08 14:05:01 -08:00
Leonardo de Moura
f8916ed411
feat(library/blast/blast): create tmp_type_context that is compatible with blast
2015-11-08 14:05:00 -08:00
Leonardo de Moura
18d9272f22
refactor(library/type_context): revise get_assignment
...
It is safer to return optional.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
27904787fe
refactor(library/type_inference): rename type_inference module to type_context
2015-11-08 14:05:00 -08:00
Leonardo de Moura
914f3b4e34
chore(library/blast/blast): fix style
2015-11-08 14:05:00 -08:00
Leonardo de Moura
0e4f97792e
feat(library/blast): add blast::scope_debug auxiliary class for testing blast related procedures
2015-11-08 14:05:00 -08:00
Leonardo de Moura
fd917effad
feat(library/blast): use new type_inference module in blast
2015-11-08 14:05:00 -08:00
Leonardo de Moura
ee924e4842
fix(library/blast/infer_type): typos
2015-11-08 14:04:56 -08:00
Leonardo de Moura
2c7d245bbe
fix(library/blast/blast): bug when translating goal metavariables into
...
blast mref's
2015-10-08 13:10:41 -07:00
Leonardo de Moura
5d3ed8a634
fix(library/blast/hypothesis): hypotheses are initially inactive
2015-10-08 13:10:41 -07:00
Leonardo de Moura
3bb09e9959
fix(library/blast): typos
2015-10-06 08:35:24 -07:00
Leonardo de Moura
c626e2e3c6
refactor(library/blast): divide hypotheses in: assumption, active and todo
...
The sets active and todo are disjoint.
A metavariable declaration can only depend on assumptions.
2015-10-04 21:59:37 -07:00
Leonardo de Moura
44881552b4
refactor(library/blast): refactor hypothesis object: merge m_value and m_justification fields
2015-10-04 21:27:39 -07:00
Leonardo de Moura
7b883cae8f
feat(library/blast): simplify metavar_decl
2015-10-04 18:24:21 -07:00
Leonardo de Moura
4ab14e709e
feat(library/blast): finish is_def_eq/unifier for blast tactic
2015-10-03 18:19:05 -07:00
Leonardo de Moura
cd48114c47
fix(library/blast/infer_type): type of mref's
2015-10-02 15:53:22 -07:00
Leonardo de Moura
0a3fbda050
feat(library/blast): convert universe metavariables into uref's
2015-10-02 15:50:41 -07:00
Leonardo de Moura
442cbff578
feat(library/blast): add blast tactic is_def_eq procedure (aka unification)
...
We still have to implement subst_mref, assign_mref, and occurs check.
2015-10-02 15:21:28 -07:00
Leonardo de Moura
aadac02bec
feat(library/blast): add infer_type for blast tactic
2015-10-02 13:11:17 -07:00
Leonardo de Moura
ad51339a28
feat(library/blast): add whnf for blast tactic
2015-10-01 16:21:17 -07:00
Leonardo de Moura
57035d3162
feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more
2015-09-30 13:31:42 -07:00
Leonardo de Moura
ac7c0fffd8
refactor(library/blast): simplify blast/expr
2015-09-30 12:54:03 -07:00
Leonardo de Moura
63c8966816
refactor(library/blast): change how we mark fixed/frozen hypothesis
2015-09-29 14:08:14 -07:00
Leonardo de Moura
eff60d835a
fix(library/blast/expr): typo
2015-09-29 12:44:56 -07:00
Leonardo de Moura
bce193ed2d
feat(library/blast/state): make sure the type/value of hypotheses and target is a closed term.
2015-09-29 12:42:20 -07:00
Leonardo de Moura
352d81e56a
feat(library/blast/state): add assertion to make sure blast state does not contain local constants.
2015-09-29 12:32:42 -07:00
Leonardo de Moura
c652eeeac6
feat(library/data/expr): add support for regular local constants in blast tactic
...
We need them when inferring types and checking whether two expressions
are definitionally equal or not.
Remark: they are temporary objects, and should never be included in the
blast state object.
2015-09-29 12:29:33 -07:00
Leonardo de Moura
21193156ef
refactor(library/blast): rename lref to href (hypothesis reference)
2015-09-29 12:13:20 -07:00
Leonardo de Moura
be76512756
feat(library/blast/blast): normalize hypotheses and unfold reducible constants when converting goal into blast state
2015-09-29 10:42:35 -07:00
Leonardo de Moura
ca059107cf
fix(library/blast/state): incorrect 'replace'
2015-09-29 10:42:00 -07:00
