michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
7861 commits 3 branches 0 tags 28 MiB
Commit graph

75 commits

Author SHA1 Message Date
Daniel Selsam
606e28ca99 refactor(library/blast/imp_extension): buffer instead of list 2015-12-04 08:22:46 -08:00
Daniel Selsam
601dc544b6 feat(library/blast/imp_extension): imperative branch extensions 2015-12-04 08:22:46 -08:00
Leonardo de Moura
83b9769225 fix(library/blast): init_classical_flag 
The procedure get_namespaces does not return the set of opened
namespaces. I added a comment there to clarify that.
 2015-12-04 08:13:19 -08:00
Daniel Selsam
0dfac6d07e feat(library/blast): classical flag 2015-12-04 07:53:05 -08:00
Leonardo de Moura
87995b96e3 fix(library/blast/congruence_closure): is_relation_app ==> is_equivalence_relation_app 2015-12-02 23:28:57 -08:00
Daniel Selsam
139536896c feat(library/light_lt_manager): light wrappers for ordered rewriting 2015-12-02 22:56:54 -08:00
Leonardo de Moura
f84c6a6cfa fix(library/blast,frontends/lean): handling pattern hints after unfolding 2015-12-02 22:52:55 -08:00
Leonardo de Moura
562d7b3e4a feat(library/blast/blast): add support in blast for controlling whether macros are unfolded or not at whnf/normalize 2015-12-02 22:52:55 -08:00
Leonardo de Moura
56282a11f6 feat(library/blast/blast): use type_context normalizer 2015-11-22 17:04:04 -08:00
Leonardo de Moura
028a2ab785 feat(library/blast): add get_config() 2015-11-20 10:39:26 -08:00
Leonardo de Moura
2d93fe4b76 feat(library/blast/congruence_closure): implement congruence closure 
Proof extraction is still missing
 2015-11-19 19:37:11 -08:00
Leonardo de Moura
193c446fc4 fix(library/blast/blast): metavariable assignment validation 2015-11-19 10:52:18 -08:00
Leonardo de Moura
f8a20341cb refactor(library/blast): get_hypothesis_decl return a reference 2015-11-18 18:20:02 -08:00
Leonardo de Moura
bf5fe8d180 feat(library/blast): add trace module 2015-11-18 12:59:53 -08:00
Leonardo de Moura
3de9a89d93 feat(library/blast/congruence_closure): congruence_closure basics 2015-11-17 18:45:22 -08:00
Leonardo de Moura
60945e95b4 feat(library/blast): add 'discard' action for detecting irrelevant hypotheses 2015-11-16 11:43:51 -08:00
Daniel Selsam
5e8068b2b2 feat(library/blast/simplifier): draft of fusion 2015-11-16 09:13:07 -08:00
Leonardo de Moura
db59c6829c feat(library/blast): add basic support for non-recursive recursors/eliminators in the simple_strategy, fix bug at recursor_action 2015-11-15 18:39:12 -08:00
Leonardo de Moura
24ed427c2f feat(library/blast): add "recursor" (aka elimination/induction) action 2015-11-15 18:00:32 -08:00
Leonardo de Moura
4cd5e18bd0 refactor(library/blast): add strategy abstract object 2015-11-15 13:12:21 -08:00
Leonardo de Moura
b5db77961d feat(library/blast): add "trivial" action 2015-11-14 15:02:14 -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
Leonardo de Moura
8f378db661 feat(library/blast): add normalize procedure to blast API 2015-11-12 20:42:58 -08:00
Leonardo de Moura
6eef52196e feat(library/blast): add gexpr "generalized expressions" 2015-11-11 16:11:51 -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
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
973a5c4812 feat(library/blast): improve blast type_context push/pop operations 2015-11-09 13:36:49 -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
b8857b078b feat(library/blast): add get_app_builder to blast API 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
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