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

641 commits

Author SHA1 Message Date
Leonardo de Moura
802edd77d1 feat(kernel/justification): add is_eqp predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:15:29 -07:00
Leonardo de Moura
e4f69bd780 fix(kernel/justification): bug in depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:15:01 -07:00
Leonardo de Moura
50089dc64e feat(kernel/error_msgs): expose pp_indent_expr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:03:12 -07:00
Leonardo de Moura
65486b2dec refactor(kernel/expr): add macro_definition smart pointer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:05:46 -07:00
Leonardo de Moura
0bc101ac28 fix(kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:28:34 -07:00
Leonardo de Moura
ddd980aa63 fix(kernel/level): warning messages when compiling in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 13:06:00 -07:00
Leonardo de Moura
027614cebb fix(kernel/metavar): wierd memory leak that only happens when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:55:55 -07:00
Leonardo de Moura
6fb7039746 refactor(kernel): use structural hashing in type_checker and converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:41:53 -07:00
Leonardo de Moura
a5ae4b6570 feat(kernel): add binder annotations (implicit, cast) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:35:02 -07:00
Leonardo de Moura
b0e0e82350 refactor(kernel): separate type_checker and converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 18:42:01 -07:00
Leonardo de Moura
3e222e2f22 refactor(kernel/formatter): add environment as an extra argument to the formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 10:28:07 -07:00
Leonardo de Moura
93a61748e9 fix(kernel/level): bug in optional<level>() constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 17:00:57 -07:00
Leonardo de Moura
49e626a0e0 refactor(kernel/metavar): switch to functional substitution datastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 10:22:36 -07:00
Leonardo de Moura
cdae3ee780 fix(kernel/type_checker): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:17:34 -07:00
Leonardo de Moura
b70bac0e8d feat(kernel/type_checker): add backtracking trick to minimize the number of delta-reduction steps 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:03:46 -07:00
Leonardo de Moura
e62254fbb3 fix(kernel/expr): relax macro_definition interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:02:48 -07:00
Leonardo de Moura
1b9e2efb0c fix(kernel/environment): relax normalizer_extesion interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:01:44 -07:00
Leonardo de Moura
f320277248 feat(kernel/definition): add mk_definition procedure that automatically computes the weight 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 12:48:21 -07:00
Leonardo de Moura
6c3a796119 fix(kernel/type_checker): bug in whnf method, and missing call to max_sharing in is_conv and is_def_eq methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 12:09:23 -07:00
Leonardo de Moura
4e893d3902 fix(kernel/constraint): printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 12:02:59 -07:00
Leonardo de Moura
54936c201a fix(kernel/kernel_exception): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 11:31:39 -07:00
Leonardo de Moura
6dfeff92f8 fix(kernel/constraint): add dealloc method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 11:13:51 -07:00
Leonardo de Moura
e3b79730ba fix(kernel/level): initialization error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 11:03:23 -07:00
Leonardo de Moura
2ddadfc920 fix(kernel/environment): compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 10:58:14 -07:00
Leonardo de Moura
9f57ec059a fix(kernel/constraint): missing inline directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 10:53:53 -07:00
Leonardo de Moura
272463bd66 feat(kernel/type_checker): add check function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 10:47:50 -07:00
Leonardo de Moura
e769c26800 refactor(kernel): move files that don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:30:40 -07:00
Leonardo de Moura
b2518f873d feat(kernel/type_checker): handle ensure_pi when whnf is a meta application 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:17:32 -07:00
Leonardo de Moura
6b05146eca fix(kernel/type_checker): preserve bound variable name when inferring type of a lambda expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 17:29:47 -07:00
Leonardo de Moura
63b6564b78 refactor(kernel): define extension_context API for normalizer_extesions and macro_definitions 
A particular macro definition may use the extra information to retrieve information necessary to expand/type a given macro application. Example: it may need to invoke whnf.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 15:43:17 -07:00
Leonardo de Moura
4842ae4fc7 refactor(kernel): store macro arguments in the macro_expr 
Before this commit, we "stored" macro arguments using applications.
This representation had some issues. Suppose we use [m a] to denote a macro
application. In the old representation, ([m a] b) and [m a b] would have
the same representation. Another problem is that some procedures (e.g., type inference)
would not have a clean implementation.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 15:02:56 -07:00
Leonardo de Moura
9d5ed2bae1 chore(kernel/type_checker): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 12:04:14 -07:00
Leonardo de Moura
a39a5b4195 refactor(kernel): remove normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 12:02:33 -07:00
Leonardo de Moura
a55c3c617d feat(kernel/type_checker): add infer_type 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 11:58:29 -07:00
Leonardo de Moura
3e122ed355 feat(kernel/error_msgs): add error message for unsatisfied level constraints, remove messages for dependent pairs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 10:47:05 -07:00
Leonardo de Moura
508bccb0c5 fix(kernel/max_sharing): add example exposing bug in max_sharing_fn, and fix it 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-24 15:55:48 -07:00
Leonardo de Moura
1c8e78e3ae fix(kernel/justification): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-24 15:08:10 -07:00
Leonardo de Moura
4be4f21de6 fix(kernel/type_checker): bug in quick_is_conv, it was not converting free variables to local constants. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-24 12:46:31 -07:00
Leonardo de Moura
0d7902f9eb feat(kernel/type_checker): finish is_convertible predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-23 20:16:14 -07:00
Leonardo de Moura
e78de448aa feat(kernel/type_checker): add is_convertible predicate (and support for proof irrelevance and eta-reduction) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-23 19:21:26 -07:00
Leonardo de Moura
cdbef0bf15 fix(kernel/type_checker): is_opaque predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-23 10:51:39 -07:00
Leonardo de Moura
a3554c85fe fix(kernel/definition): clang compilation warning, and add module_idx typedef 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-23 10:50:55 -07:00
Leonardo de Moura
ed37bf650d chore(kernel/environment): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 18:34:55 -07:00
Leonardo de Moura
04a61bdffe feat(kernel/type_checker): remove dead code, add basic whnf procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 18:32:50 -07:00
Leonardo de Moura
188da7e4c6 feat(kernel/max_sharing): add method already_processed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 18:30:07 -07:00
Leonardo de Moura
9fda7e2529 fix(kernel): incorrect optimization in max_sharing_fn class 
The resultant expression may failed to be fully shared.
Add an example that demonstrates the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 15:38:22 -07:00
Leonardo de Moura
086dd6b1a1 chore(kernel/environment): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 15:36:52 -07:00
Leonardo de Moura
cc1cfba8ad refactor(kernel/type_checker): new API for type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-21 16:12:47 -07:00
Leonardo de Moura
6417c79569 feat(kernel/environment): add is_descendant method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-21 14:28:50 -07:00
Leonardo de Moura
bfeb51ce58 feat(kernel/environment): add trust level field 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-21 13:39:47 -07:00