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

5871 commits

Author SHA1 Message Date
Daniel Selsam
12e148c7b6 feat(library/blast/forward/ematch): even more tracing 2016-01-26 21:40:46 -08:00
Soonho Kong
30b5313118 feat(CMakeLists.txt): handle new/old ABIs issue for MSYS2 + g++ combination 
related issue: #930
 2016-01-26 20:41:20 -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
4821af8685 feat(frontends/lean/scanner): disallow superscripts in identifiers 
See new test for motivating example.
 2016-01-26 18:46:40 -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
Gabriel Ebner
7e11c5cf6e fix(src/util/file_lock): ignore failure to create locks on read-only file systems 
EACCES is already ignored when creating lock files.  In this case we
assume that the file to be locked is part of the system-wide
installation.  On NixOS however, the file system containing system
packages is mounted read-only, and open(2) returns EROFS.
 2016-01-16 11:00:44 -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
Syohei YOSHIDA
f2eef7aa1b feat(emacs): use s-join instead of string-join 
Because string-join was introduced at Emacs 24.4 and subr-x.el must be
loaded for using it.
 2016-01-14 09:36:52 -05:00
Syohei YOSHIDA
885c62648f fix(emacs/lean-option.el): don't use deprecated function, string-to-int 
string-to-int was deprecated since Emacs 22.
string-to-number should be used instead of string-to-int.
 2016-01-14 09:36:37 -05: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
d9294fc164 chore(kernel/expr): remove dead var 2016-01-13 17:36:33 -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
1048812e2e chore(frontends/lean/notation_cmd): cleanup weird coding pattern 2016-01-13 17:27:25 -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
723a9e227a chore(kernel/default_converter): remove dead code 2016-01-13 13:33:13 -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
Syohei YOSHIDA
f7494618ff fit(emacs/lean-input.el): fix loading cl.el at runtime 
This package uses only cl.el macro(lexical-let). So it is enough to
load cl.el at compile time.
 2016-01-13 11:19:53 -05:00
Syohei YOSHIDA
5903fe4287 feat(emacs): use cl-lib functions/macros instead of cl.el 2016-01-13 11:19:40 -05: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
Leonardo de Moura
ddff37dd0f fix(library/blast/congruence_closure): bug when using blast.cc.heq and handling relation congruences 2016-01-10 19:28:55 -08:00
Leonardo de Moura
2b38d0fe9b chore(library/app_builder): improve trace message 2016-01-10 18:31:54 -08:00
Leonardo de Moura
f22ba4e641 feat(library/type_context): cache mk_subsingleton_instance 2016-01-10 18:26:40 -08:00
Leonardo de Moura
799317c43e fix(library/blast/congruence_closure): add missing eq => heq lifting 2016-01-10 18:03:35 -08:00
Leonardo de Moura
cf8307ee20 feat(library/app_builder): use types in app_builder trace messages 2016-01-10 17:29:11 -08:00
Leonardo de Moura
3a846a28a3 feat(library/blast/congruence_closure): support for subsingleton propagation 2016-01-10 17:24:12 -08:00
Leonardo de Moura
c646c3cacc feat(library/init/logic): add subsingleton.helim with heterogeneous equality 2016-01-10 16:47:45 -08:00
Leonardo de Moura
6c015a4954 feat(library/blast/blast): use blast tmp_type_context to generate type class instances 2016-01-10 16:30:51 -08:00
Leonardo de Moura
912bccb3f9 fix(library/blast/congruence_closure): do not adjust proofs when blast.cc.heq == false 2016-01-10 15:28:16 -08:00
Leonardo de Moura
e9d24ec152 feat(library/blast/congruence_closure): create simpler congruence proofs when using blast.cc.heq 2016-01-10 15:11:31 -08:00
Leonardo de Moura
ea7da31bba feat(library/blast/congruence_closure): support for congruence lemmas that use heterogeneous equality 2016-01-10 13:45:40 -08:00
Leonardo de Moura
934f3b67ff feat(library/blast/congruence_closure): basic support for heterogeneous equality 
We still have to process the general congruence lemmas.
 2016-01-10 12:53:05 -08:00
Leonardo de Moura
22a6b7f1c3 feat(library/blast/congruence_closure): add blast.cc.heq option 2016-01-10 00:15:52 -08:00
Leonardo de Moura
437b0fb4ee feat(library/congr_lemma_manager): cache hcongr lemmas 2016-01-09 15:48:17 -08:00
Leonardo de Moura
42cdda227a feat(library/congr_lemma_manager): add heterogeneous equality congruence lemmas 2016-01-09 15:41:08 -08:00
Leonardo de Moura
403966792d feat(library/app_builder): add helper heq methods 2016-01-09 12:46:14 -08:00
Leonardo de Moura
d3242a2068 refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas 2016-01-09 12:32:18 -08:00
Soonho Kong
af42d3ff2d fix(emacs/load-lean.el): add seq to lean-required-packages 
fix #947

[skip ci]
 2016-01-08 03:35:23 +00:00
Leonardo de Moura
27eea05da9 fix(library/blast/discr_tree): bug in the discrimination tree module 2016-01-06 17:30:44 -08:00
Leonardo de Moura
3c22a9d4e1 feat(library/blast/recursor/recursor_strategy): add new options to control recursor/recursion strategy 2016-01-06 17:30:38 -08:00
Leonardo de Moura
76cebb45f9 feat(library/blast/congruence_closure): add support for 'no_confusion' in the congruence closure module 2016-01-06 17:30:25 -08:00
Leonardo de Moura
cb02d1deae feat(library/blast/congruence_closure): add support for specialized congr lemmas in the congruence closure module 2016-01-06 17:30:20 -08:00
Leonardo de Moura
ef691d6cf5 fix(library/abstract_expr_manager): bug introduced today 2016-01-06 17:30:14 -08:00
Leonardo de Moura
c9930d0a29 feat(library/blast/simplifier/simplifier): subsingleton normalization for application arguments and lambdas 2016-01-06 17:30:08 -08:00
Leonardo de Moura
e7bcb89314 fix(library/simplifier/simplifier): bug in cache_lookup 2016-01-06 17:30:01 -08:00
Leonardo de Moura
14d4ae7e97 chore(library/blast/simplifier/simplifier): remove dead variable 2016-01-06 17:29:54 -08:00
Leonardo de Moura
9fa1a7a01c refactor(abstract_expr_manager): use get_specialization_prefix_size to improve performance of abstract_expr_manager 2016-01-06 17:29:48 -08:00
Leonardo de Moura
d4a5aa6db0 refactor(library/fun_info_manager): improve performance and add get_prefix method 2016-01-06 17:29:41 -08:00
Leonardo de Moura
f3b8aef24c feat(library/fun_info_manager,library/congr_lemma_manager,blast/simplifier): specialized congruence lemmas 
We still need a lot of polishing.
 2016-01-06 17:29:35 -08:00
Leonardo de Moura
930fcddace feat(kernel/expr): add get_app_args_at_most 2016-01-06 17:29:28 -08:00
Leonardo de Moura
9a1a9f3b5a refactor(library/fun_info_manager): use expr_unsigned_map 2016-01-06 17:29:22 -08:00
Leonardo de Moura
7312dd77b8 refactor(library/congr_lemma_manager): move expr_unsigned_map to separate module 2016-01-06 17:29:16 -08:00
Leonardo de Moura
43c5cbd1bf feat(library/fun_info_manager): more general fun_info_manager 2016-01-06 17:29:10 -08:00
Leonardo de Moura
3ca785b0e7 refactor(library/fun_info_manager): remove dead code 2016-01-06 17:29:02 -08:00
Leonardo de Moura
a992bb46a6 feat(library/fun_info_manager): update interface 2016-01-06 17:28:52 -08:00
Rob Lewis
c0deac6a63 fix(src/emacs): add replace keyword to emacs syntax file 2016-01-05 11:01:00 -05:00
Rob Lewis
a57b7fadfb style(replace_tactic): remove extra whitespace 2016-01-04 15:10:51 -05:00
Rob Lewis
031831f101 feat(library/tactic): add replace tactic 2016-01-04 14:43:31 -05:00
Leonardo de Moura
ba392f504f feat(kernel/expr,library/blast/blast,frontends/lean/decl_cmds): add workaround for allowing users to use blast inside of recursive equations 2016-01-03 21:53:31 -08:00
Leonardo de Moura
4478d570bd chore(library/congr_lemma_manager): fix style 2016-01-03 18:02:50 -08:00
Leonardo de Moura
19ebedd480 feat(library/type_context): improve type_context get_level_core, add virtual method for checking types whenever a metavariable is assigned 
We add an example where app_builder fails without these new features.
That is, app_builder fails to solve the unification problem.
 2016-01-03 17:58:27 -08:00
Leonardo de Moura
1fc7bbceb2 chore(frontends/lean/builtin_cmds): handle FixedNoParam in the front-end 2016-01-03 15:18:26 -08:00
Leonardo de Moura
fcf532ea67 chore(library/app_builder): fix typo in trace message 2016-01-03 15:16:50 -08:00
Leonardo de Moura
d0fe59ef8a feat(library/congr_lemma_manager): add new kind of congr_arg 2016-01-03 15:10:07 -08:00
Leonardo de Moura
67d49aabd9 chore(library/congr_lemma_manager): document main methods 2016-01-03 14:39:34 -08:00
Leonardo de Moura
66a722ff5a feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore 
The "eager-delta hack" was added to minimize problems in the interaction
between coercions and delta-constraints.
 2016-01-03 12:39:32 -08:00
Leonardo de Moura
d02ead320a feat(library/unifier): remove unifier.computation option 2016-01-03 11:00:16 -08:00
Leonardo de Moura
9935cbc3d7 feat(library/blast/blast): communicate assigned metavariables back to tactic framework 
We need this feature to be able to solve (input) goals containing
metavariables using blast.
See new test for example.
 2016-01-02 20:05:44 -08:00
Leonardo de Moura
56d9b6b0d3 fix(library/blast/blast): convert uref and mref back into tactic metavariables 2016-01-02 19:23:04 -08:00
Leonardo de Moura
d85b4300b1 fix(library/blast/blast): bug at visit_meta_app 2016-01-02 19:08:56 -08:00
Leonardo de Moura
5feef27c2b feat(frontends/lean/notation_cmd): relax restriction on user defined tokens 
Before this commit, Lean would forbid new tokens containing '(' or ')'.
We relax this restriction. Now, we just forbid new tokens starting with '(' or ending with ')'.
 2016-01-02 13:58:46 -08:00
Leonardo de Moura
4eb2690c32 feat(library/scoped_ext): store set of opened namespaces 2016-01-02 13:35:08 -08:00
Leonardo de Moura
155df48665 feat(library): remove decl_stats 
We are not using (and will not use) this module in the blast proof procedures
 2016-01-02 13:00:43 -08:00
Leonardo de Moura
3c564fcc55 fix(library/user_recursors): 'print recursor-lemma' command 2016-01-01 18:12:12 -08:00
Leonardo de Moura
0963ce336f feat(library/blast): add 'grind' and 'grind_simp' blast strategies 
The use [intro] [intro!] [elim] [simp] lemmas.
The [simp] lemmas are only used by grind_simp.
 2016-01-01 17:32:13 -08:00