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
42cdda227a
feat(library/congr_lemma_manager): add heterogeneous equality congruence lemmas
2016-01-09 15:41:08 -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
1fc7bbceb2
chore(frontends/lean/builtin_cmds): handle FixedNoParam in the front-end
2016-01-03 15:18:26 -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
b117a10f82
refactor(library/blast/simplifier): use priority_queue to store simp/congr lemmas, use name convention used at forward/backward lemmas, normalize lemmas when blast starts, cache get_simp_lemmas
2015-12-28 17:52:57 -08:00
Leonardo de Moura
f177082c3b
refactor(*): normalize metaclass names
...
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).
Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write
definition foo [coercion] ...
definition bla [forward] ...
and
open [coercion] nat
open [forward] nat
It is easier to remember and is uniform.
2015-12-28 10:39:15 -08:00
Leonardo de Moura
96bec8b4f9
fix(frontends/lean/builtin_cmds): allow token and metaclass to have the same name
2015-12-28 09:57:45 -08:00
Leonardo de Moura
f679ce0da9
refactor(frontends/lean): move 'print_cmd' to separate module
2015-12-28 09:08:18 -08:00
Leonardo de Moura
d81b2d0f29
feat(library/attribute_manager, frontends/lean/builtin_cmds): use attribute manager information when pretty print definitions
2015-12-17 21:16:31 -08:00
Leonardo de Moura
7f1800962a
feat(frontends/lean/pp): allow user to override pp.all setting
...
see #922
2015-12-11 10:40:48 -08:00
Leonardo de Moura
0acdcd487b
feat(frontends/lean): add 'print aliases' command
2015-12-09 10:39:40 -08:00
Leonardo de Moura
34b944a71e
refactor(frontends/lean): remove broken 'migrate' command
2015-12-08 15:40:49 -08:00
Leonardo de Moura
7da64a768f
refactor(library/type_context): with the new tracing infrastructure, type_context doesn't need an io_state
2015-12-08 14:58:08 -08:00
Leonardo de Moura
50df6b5698
feat(frontends/lean): rename '[intro]' ==> '[intro!]' and '[backward]' ==> '[intro]'
2015-12-07 21:33:35 -08:00
Leonardo de Moura
295b1d21f5
feat(frontends/lean): add '[intro]' and '[elim]' annotations
2015-12-07 18:43:15 -08:00
Leonardo de Moura
c3b5ce0785
feat(frontends/lean/builtin_cmds): show metavariable arguments when pretty printing patterns
2015-12-07 12:39:51 -08:00
Daniel Selsam
a9aeb69789
feat(frontends/lean/builtin_cmds): print metas for patterns
2015-12-07 12:32:22 -08:00
Daniel Selsam
25a3cff54e
refactor(library/abstract_expr_manager): remove fun_info_manager
2015-12-04 08:31:38 -08:00
Daniel Selsam
7854158751
fix(library/abstract_expr_manager): only squash Cast subsingletons
2015-12-04 08:31:38 -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
028ef47c84
feat(frontends/lean,library/blast/forward/pattern): check whether patterns can be inferred at declaration time
2015-12-02 22:52:55 -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
950f356d9a
refactor(library/blast,frontends/lean): forward pattern index
2015-12-02 22:52:55 -08:00
Leonardo de Moura
4129b398da
fix(frontends/lean/builtin_cmds): private constants in the print command
2015-12-02 22:52:54 -08:00
Leonardo de Moura
e4e9c30e66
fix(frontends/lean/builtin_cmds): print patterns
2015-12-02 22:52:54 -08:00
Leonardo de Moura
41ff4bc193
feat(library/blast/forward/pattern): pattern inference and heuristic instantiation index
2015-11-25 23:45:08 -08:00
Leonardo de Moura
0ceaf0b4fe
feat(frontends/lean/builtin_cmds): display '[forward]' annotation for heuristic instantiation lemmas
2015-11-25 17:53:13 -08:00
Leonardo de Moura
67a4cd3972
feat(frontends/lean): add print [no_pattern] command
2015-11-24 18:48:22 -08:00
Leonardo de Moura
a2f43212d6
feat(frontends/lean): add '[no_pattern]' attribute
2015-11-24 18:48:22 -08:00
Daniel Selsam
21cb409e6c
refactor(library/blast/simplifier): move simplifier module into blast
2015-11-19 19:43:04 -08:00
Daniel Selsam
413989afd6
feat(library/blast/backward): backward chaining strategy
2015-11-18 17:48:39 -08:00
Leonardo de Moura
f363975856
feat(frontends/lean): add command #congr_rel for testing new congruence lemma for equivalence relations
2015-11-17 18:45:22 -08:00
Leonardo de Moura
8e4fd50913
chore(frontends/lean/builtin_cmds): fix style
2015-11-16 16:10:01 -08:00
Leonardo de Moura
7abb0d6b96
chore(frontends/lean/builtin_cmds,library/blast/simplifier): fix style
2015-11-16 11:10:12 -08:00
Daniel Selsam
5e8068b2b2
feat(library/blast/simplifier): draft of fusion
2015-11-16 09:13:07 -08:00
Leonardo de Moura
ff73fb22fb
feat(library/user_recursors): store whether recursor is recursive or not
2015-11-15 12:37:35 -08:00
Daniel Selsam
f17320eccf
fix(library/abstract_expr_manager): remove weight and lt
2015-11-12 21:21:52 -08:00
Daniel Selsam
3703938e55
feat(library/abstract_expr_manager): compare exprs ignoring subsingletons
2015-11-12 21:21:51 -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
e1f81cfdcd
feat(library/type_context): add normalizer for type_context
2015-11-12 20:31:36 -08:00
Leonardo de Moura
9aaa2d0991
feat(frontends/lean): add new command for testing new congruence lemmas
...
Remark: #congr_simp is the old command, and #congr is the new one.
2015-11-12 18:55:25 -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
1d1f043192
refactor(library/app_builder): throw exception instead of returning none_expr
2015-11-08 14:05:03 -08:00
Leonardo de Moura
f74e8288bd
refactor(library/congr_lemma_manager): API
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
8e5e8e6540
feat(library/blast/simplifier): basic infrastructure
2015-11-08 14:05:02 -08:00
