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

3140 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
1681dc2389 test(kernel): add new environment tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:04:05 -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
7eb9496643 feat(util): add missing lbool.* files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-24 12:27:19 -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
f99444b130 chore(tests): move max_sharing unit tests to tests/kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 16:01:30 -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
3b78af0db5 chore(tests/library): enable old tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 12:05:49 -07:00
Leonardo de Moura
ad43d9177b refactor(util/name_set): implement name_sets using red black trees instead of hashtables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 11:09:13 -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
Leonardo de Moura
ee58a83e25 chore(kernel): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 14:25:09 -07:00
Leonardo de Moura
d0dc16355b chore(kernel): remove unnecessary file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 14:23:32 -07:00
Leonardo de Moura
582352d647 refactor(kernel/environment): simplified (functional) environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 14:21:49 -07:00
Leonardo de Moura
234abb1238 feat(kernel/definition): default constructor for definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 13:10:05 -07:00
Leonardo de Moura
984ac03ac7 refactor(kernel): replace kernel object with definition, disable affected files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 16:10:47 -07:00
Leonardo de Moura
cb479a75ae fix(kernel/expr): make sure we cannot create a free variable with index uint_max, reason: get_free_var_range would return an incorrect value 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 13:25:21 -07:00
Leonardo de Moura
3712da0b54 refactor(kernel/instantiate): use get_free_var_range to improve instantiate, remove instantiate_with_closed, fix index overflow bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 13:12:49 -07:00
Leonardo de Moura
1fd5e9682d refactor(kernel/free_vars): use get_free_var_range to improve lift_free_vars and lower_free_vars performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 12:41:06 -07:00
Leonardo de Moura
4ae958af56 refactor(kernel/free_vars): use get_free_var_range to improve has_free_var_in_range performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 12:18:19 -07:00