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

172 commits

Author SHA1 Message Date
Leonardo de Moura
abd238aef0 feat(*): add [quasireducible] attribute 2015-03-04 22:12:49 -08:00
Leonardo de Moura
7db6ed7c14 refactor(library/unifier): move m_pattern configuration option to unifier_config 2015-03-03 20:24:18 -08:00
Leonardo de Moura
341a9a2010 refactor(library/unifier): remove dead code 2015-03-03 20:14:17 -08:00
Leonardo de Moura
7e2f0f9a36 fix(library/unifier): in the context_check, we should not consider local constants that occur in the type of other constants 
This was a performance bug.
We were missing higher-order pattern constraints due to this bug.
 2015-03-02 17:28:56 -08:00
Leonardo de Moura
72eed42ac8 feat(library/unifier): ignore irrelevant branches when solving flex-rigid constraints 2015-02-26 13:43:54 -08:00
Leonardo de Moura
fcd67649ed refactor(kernel): expose may_reduce_later method 2015-02-07 20:36:26 -08:00
Leonardo de Moura
b57f93bad5 refactor(kernel): remove unnecessary procedures 2015-02-07 20:14:19 -08:00
Leonardo de Moura
dbc8e9e13a refactor(*): add method get_num_univ_params 2015-01-28 17:22:18 -08:00
Leonardo de Moura
2717adde94 feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant 2015-01-19 16:23:29 -08:00
Leonardo de Moura
2e4a2451e6 refactor(library/reducible): simplify reducible/irreducible semantics 2015-01-08 18:52:18 -08:00
Leonardo de Moura
597f7385e8 fix(library/unifier): incorrect fix 2015-01-07 16:57:02 -08:00
Leonardo de Moura
2990a6d029 fix(library/unifier): missing "set_conflict" in process_delta 2015-01-07 12:41:01 -08:00
Leonardo de Moura
2867789bec fix(library/unifier): handle missing first-order flex-flex case 2014-12-10 22:11:30 -08:00
Leonardo de Moura
050104cdfd fix(library/unifier): assertion violation 2014-12-02 12:17:59 -08:00
Leonardo de Moura
06f436840f fix(library/unifier): postpone class-instance constraints whose type could not be inferred 2014-12-01 22:27:23 -08:00
Leonardo de Moura
19d14678ef refactor(library/unifier): remove dead code 2014-12-01 21:57:34 -08:00
Leonardo de Moura
f1e915a188 feat(frontends/lean): add 'find_decl' command 2014-11-23 23:00:59 -08:00
Leonardo de Moura
8c8bf41e39 feat(frontends/lean/server): do not unfold definitions in FINDG 2014-11-23 19:03:39 -08:00
Leonardo de Moura
00df34a1c4 feat(library/unifier): generalize method process_succ_eq_max_core 2014-11-14 14:25:41 -08:00
Leonardo de Moura
51719145f9 feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2) 2014-11-12 17:28:33 -08:00
Leonardo de Moura
ea739100b3 fix(library/unifier): broken optimization in the unifier 
See new comments and tests for details.
 2014-10-28 16:09:41 -07:00
Leonardo de Moura
78bc3ef7e4 feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization 
This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean
 2014-10-27 16:49:29 -07:00
Leonardo de Moura
096c67b2e5 fix(library/unifier): occurs-check bug 2014-10-25 00:16:02 -07:00
Leonardo de Moura
8974b52f7b perf(library/unifier): avoid unnecessary wasteful computation 2014-10-16 17:16:49 -07:00
Leonardo de Moura
9ba59c6b25 feat(library/universe): improve support for universe level constraints in the unifier 2014-10-09 20:28:39 -07:00
Leonardo de Moura
8fa171cb92 refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument 2014-10-07 17:30:57 -07:00
Leonardo de Moura
60d8369688 fix(library/unifier): missing justification when updating choice constraints 
The bug was not producing incorrect results, but really bad error
messages.
See: empty.lean.expected.out
 2014-10-04 10:40:53 -07:00
Leonardo de Moura
9f6a8827e0 refactor(*): use name_map 2014-09-28 10:23:11 -07:00
Leonardo de Moura
22e47430b5 feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore 2014-09-27 21:50:39 -07:00
Leonardo de Moura
cd87539de5 fix(library/unifier): bug in the new next_delta_unfold_case_split 2014-09-25 09:56:32 -07:00
Leonardo de Moura
0488ee4ee2 perf(library/unifier): process delta expansion case split lazily 2014-09-24 19:16:12 -07:00
Leonardo de Moura
4dd7abb14e refactor(library): explicit initialization/finalization 2014-09-23 10:45:14 -07:00
Leonardo de Moura
b1ee888aae refactor(*): start move to explicit initialization/finalization, 
explicitly initialize/finalize options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-22 10:41:07 -07:00
Leonardo de Moura
08ccd58eb6 feat(frontends/lean): add 'reducible' modifier for controlling which 
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
d647954f93 feat(frontends/lean/elaborator): constraints associated with 'proof-qed' 
blocks are solved independently, closes #82
 2014-09-13 10:21:10 -07:00
Leonardo de Moura
85f7132efe feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175, closes #173, closes #68 2014-09-11 14:49:35 -07:00
Leonardo de Moura
03902d4b45 refactor(library/unifier): add option m_discard too unifier, if m_discard == false, then unsolved flex-flex constraints are returned, the unifier also does not apply "last resource" techniques that may miss many solutions. 2014-09-11 14:49:35 -07:00
Leonardo de Moura
935ba35292 feat(library/unifier): keep normalization result when processing universe level unification constraints 2014-09-11 14:49:35 -07:00
Leonardo de Moura
187661aa6a feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs 2014-09-09 09:27:26 -07:00
Leonardo de Moura
a5698a55ec fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions 2014-09-09 09:27:26 -07:00
Leonardo de Moura
fd85d4702e refactor(library/unifier): move all_local outside of the class 2014-09-09 09:27:26 -07:00
Leonardo de Moura
ebde1bcfad feat(library/unifier): option 'unifier.computation true' will force elaborator to always consider an extra case-split when the right-hand-side of a flex-rigid constraint is not in weak-head-normal-form 2014-09-09 09:27:26 -07:00
Leonardo de Moura
b9628842cf feat(library/unifier): remove mk_macro_imitation, we instead expand the macro before solving flex-rigid constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 17:34:03 -07:00
Leonardo de Moura
641624a277 fix(library/unifier): bug in expand_rhs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 14:35:11 -07:00
Leonardo de Moura
e303651dee refactor(library/unifier): cleanup mk_macro_imitation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 13:19:19 -07:00
Leonardo de Moura
4c9723e5ed fix(library/unifier): assertion violation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 09:07:34 -07:00
Leonardo de Moura
fbf13994d8 refactor(*): use + for concatenating format objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-24 09:35:25 -07:00
Leonardo de Moura
b746492ac8 refactor(library/simple_formatter): rename simple_formatter to print 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:32:08 -07:00
Leonardo de Moura
7d987df429 refactor(kernel/formatter): move simple_formatter to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:26:45 -07:00
Leonardo de Moura
937c465685 fix(library/unifier): too much reduction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 21:37:51 -07:00