Commit graph

7571 commits

Author SHA1 Message Date
Leonardo de Moura
809168c05b test(tests/lean/extra): add temp test for congruence manager 2015-11-08 14:05:02 -08:00
Leonardo de Moura
9b34526030 feat(frontends/lean): add #congr debugging command 2015-11-08 14:05:02 -08:00
Leonardo de Moura
22dcf6825e feat(library/congr_lemma_manager): add congr_lemma_manager skeleton and compute type of congruence lemma
proof is still missing
2015-11-08 14:05:02 -08:00
Leonardo de Moura
01bde866d6 feat(library/util): add auxiliary recognizers 2015-11-08 14:05:01 -08:00
Leonardo de Moura
2d04156959 fix(library/app_builder): bug in eq_drec 2015-11-08 14:05:01 -08:00
Leonardo de Moura
34d5882b9a refactor(library/util): rename old is_eq_rec 2015-11-08 14:05:01 -08:00
Leonardo de Moura
2482c49729 test(frontends/lean): add #replace command for debugging purposes 2015-11-08 14:05:01 -08:00
Leonardo de Moura
6519e570f3 feat(library/fun_info_manager): safer "replace" function 2015-11-08 14:05:01 -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
7e7919950d fix(library/type_context): compilation warning 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
749d468440 feat(library): add fun_info_manager 2015-11-08 14:05:01 -08:00
Leonardo de Moura
e23523bb02 feat(library/type_context): add mk_subsingleton_instance 2015-11-08 14:05:01 -08:00
Daniel Selsam
a104b478f3 feat(library/type_context): make expand_macro public 2015-11-08 14:05:01 -08:00
Leonardo de Moura
f84f024b92 refactor(library/app_builder): change app_builder constructor 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
b2c9f2f6c5 feat(library/type_context): document our approach for managing meta-variables in 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
01259a2d1c feat(library/app_builder): add helper functions for creating eq.rec applications 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
dc203b28db test(tests/lean/run): add more tests 2015-11-08 14:05:01 -08:00
Leonardo de Moura
d1fa547335 feat(frontends/lean/builtin_cmds): change mask notation at #app_builder command 2015-11-08 14:05:01 -08:00
Leonardo de Moura
f21102a725 feat(frontends/lean): add test commands for new app_builder features 2015-11-08 14:05:01 -08:00
Leonardo de Moura
1c2c2a6077 feat(library/app_builder): mk_app with mask 2015-11-08 14:05:01 -08:00
Leonardo de Moura
8e0a3eec3f chore(library/relation_manager): fix bogus style warnings 2015-11-08 14:05:01 -08:00
Leonardo de Moura
0f631889b7 feat(library/app_builder): add helper methods for creating binary relations, and refl/symm/trans proofs 2015-11-08 14:05:00 -08:00
Leonardo de Moura
b5c40e30ef feat(library/app_builder): add set_context 2015-11-08 14:05:00 -08:00
Leonardo de Moura
137ec27059 feat(library/app_builder): add constructor for app_builder that may take subclasses of tmp_type_context
We need this feature because blast has its own version of tmp_type_context.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
ee0974650a feat(library/app_builder): new app_builder on top of type_context
The new version is more robust, and invokes type class resolution if needed.
2015-11-08 14:05:00 -08:00
Leonardo de Moura
87ec7383dd fix(library/tmp_type_context): initialization 2015-11-08 14:05:00 -08:00
Leonardo de Moura
a26ea2a249 feat(frontends/lean/builtin_cmds): add command for testing app_builder 2015-11-08 14:05:00 -08:00
Leonardo de Moura
3804281919 refactor(library/app_builder): remove app_builder Lua API 2015-11-08 14:05:00 -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
e01f2ec6a5 feat(library/tmp_type_context): add temporary type_context 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
3bc5084bf6 refactor(library/simplifier): disable file
We will eventually delete it.
It will be subsumed by blast.
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
2f06a480fe test(tests/lean/run/partial_explicit): add test for '@@' operator 2015-11-08 14:05:00 -08:00
Daniel Selsam
ffc168d63a fix(frontends/lean/elaborator): visit_app partial 2015-11-08 14:05:00 -08:00
Leonardo de Moura
ab940a2001 feat(frontends/lean/elaborator): add support for partial explicit in the elaborator 2015-11-08 14:05:00 -08:00
Daniel Selsam
6b06a19294 chore(frontends/lean): remove whitespace 2015-11-08 14:05:00 -08:00
Daniel Selsam
fa58d7c71e feat(frontends/lean): basic support for partial explicit 2015-11-08 14:05:00 -08:00
Daniel Selsam
946e00f71a feat(library/explicit): support partial explicit 2015-11-08 14:05:00 -08:00
Leonardo de Moura
1d670e3193 feat(frontends/lean): support for '@@' -- the partial explicit operator 2015-11-08 14:05:00 -08:00