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

703 commits

Author SHA1 Message Date
Leonardo de Moura
611f29a954 chore(library/elaborator): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 16:35:00 -07:00
Leonardo de Moura
fedbf8595b feat(kernel/metavar): collect unassigned metavariables while instantiating 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 16:58:09 -07:00
Leonardo de Moura
2c3e3cb544 refactor(kernel/abstract): add abstract_locals, and remove abstract_p 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
9e50d5a1b8 test(util/lazy_list): add simple lazy_list example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
07f2379dec refactor(kernel): add mk_local function that has only two arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:27:26 -07:00
Leonardo de Moura
34dfacc10e refactor(frontends/lean): Bool does not need to be a reserved keyword 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 10:52:12 -07:00
Leonardo de Moura
e7019ec840 feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 22:13:25 -07:00
Leonardo de Moura
b347117cf3 feat(util/scoped_map): add 'keep' method for closing a scope without undoing operations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 11:25:14 -07:00
Leonardo de Moura
3bde699fbe feat(frontends/lean/parser): add parse_level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 12:34:55 -07:00
Leonardo de Moura
5a008717a4 feat(frontends/lean/parser): add parse_notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 21:00:34 -07:00
Leonardo de Moura
3dc26666b9 feat(frontends/lean): add parser interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 18:20:59 -07:00
Leonardo de Moura
d3e3301208 refactor(frontends/lean/scanner): use the parser configuration in the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 10:59:12 -07:00
Leonardo de Moura
546f9dc00b chore(frontends/lean): use consistent name conventions, rename token_set to token_table 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 09:18:57 -07:00
Leonardo de Moura
25b822b1c7 fix(tests/util/memory): remove reference to deleted function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 13:29:45 -07:00
Leonardo de Moura
7847f8a0ca fix(tests/util): disable some tests that do not compile on OSX + Boost + MULTI_THREAD 2014-06-07 13:14:17 -07:00
Leonardo de Moura
d827b56777 fix(util/memory): remove get_thread_allocated_memory, it used thread_local 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 13:05:03 -07:00
Leonardo de Moura
15f0899efb refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive 
Motivation: clang++ on OSX does not support 'thread_local'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 10:18:36 -07:00
Leonardo de Moura
06d2ff021b feat(util/thread_script_state): add system_import procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-06 16:23:24 -07:00
Leonardo de Moura
e9ef59ab3e feat(util): add global (thread local) script_state objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-06 15:46:16 -07:00
Leonardo de Moura
c1796d0ce4 chore(*): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-06 10:35:17 -07:00
Leonardo de Moura
d10d70423a feat(frontends/lean): add new scanner 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-05 18:57:26 -07:00
Leonardo de Moura
4a25e7442a feat(kernel/expr): add optional expression caching (aka "partial" hash-consing) 
We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 15:35:47 -07:00
Leonardo de Moura
df3280e86e feat(util): add lru cache 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 13:26:02 -07:00
Leonardo de Moura
5a5d66edc8 feat(util/trie): add value() method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 01:19:23 -07:00
Leonardo de Moura
7b28419260 chore(*): disable multi thread support for OSX, remove the !defined(APPLE) directives 
We should re-enable multi thread support for OSX as soon as the bug in clang is fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 18:23:26 -07:00
Leonardo de Moura
1b4c9f63ce perf(kernel/environment): improve is_descendant performance, optimize for the common case: the is_descendant tree is huge but has few deep branches 
This is an important optimization for module.cpp. The benchmark tests/lua/slow/mod2.lua is a good example where the cost of is_descendant was neutralizing the benefit of the replace method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 22:29:03 -07:00
Leonardo de Moura
f375ed5f7a test(tests/kernel/environment): add more tests for environment objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 12:42:29 -07:00
Leonardo de Moura
8872d4a531 refactor(kernel): rename definition class to declaration 
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:41:38 -07:00
Leonardo de Moura
5ce134e24e chore(kernel): binder => binding where appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:37:27 -07:00
Leonardo de Moura
d625c9a26c refactor(kernel): move max_sharing to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:15:08 -07:00
Leonardo de Moura
69e72c278d feat(kernel): add proof irrelevance for classes 
We can use this feature to implement proof irrelevance for Identity types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 15:30:32 -07:00
Leonardo de Moura
862c5e354d feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 13:08:09 -07:00
Leonardo de Moura
40b3129e7b refactor(kernel): improve names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:28:05 -07:00
Leonardo de Moura
660b9299ad refactor(kernel): (de)serialization procedures don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 17:23:36 -07:00
Leonardo de Moura
01eda46b69 feat(util/trie): add for_each and display methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 18:23:27 -07:00
Leonardo de Moura
bfa6193bfe feat(util/trie): add merge method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 17:59:20 -07:00
Leonardo de Moura
479685cb97 feat(util): add basic trie datastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 17:40:33 -07:00
Leonardo de Moura
2593f65ce1 feat(kernel): add tag to kernel expressions 
Frontends can used tags to associate expressions with line number information.
The update_* procedures automatically propagate tags.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:33:25 -07:00
Leonardo de Moura
ff9004dae2 refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-11 18:05:02 -07:00
Leonardo de Moura
e942aecca6 refactor(kernel/type_checker): remove method is_conv 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:29:35 -07:00
Leonardo de Moura
7b6d555433 refactor(kernel): remove level constraints from definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:11:50 -07:00
Leonardo de Moura
23ed003389 refactor(kernel): remove diff_cnstrs module 
We don't need them anymore. We will drop universe cumulativity from the kernel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 19:58:25 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:08:32 -07:00
Leonardo de Moura
850ec69538 feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:09:17 -07:00
Soonho Kong
468abb72b8 tests(util/rb_tree): wrap tst6 with #if !defined 2014-05-02 01:39:13 -04:00
Leonardo de Moura
120c24319e fix(tests/kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:58:09 -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
2b97474958 test(util/rb_tree): reduce test time for rb_tree 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:08:18 -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
cd30bb49c1 chore(library/arith): remove unnecessary library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 16:14:15 -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
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
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
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
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
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
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
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
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
1fd447b451 chore(util): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:54:10 -07:00
Leonardo de Moura
bc8379256a refactor(kernel): remove pairs from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:52:07 -07:00
Leonardo de Moura
c78e6787aa test(util/rb_tree): multi-thread test for rb trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-20 10:20:28 -07:00
Leonardo de Moura
3651b4ecd0 refactor(kernel): replace_fn functional object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
eb487e44c1 refactor(kernel): use names instead of unsigned integers to encode level parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
aa4a7acccf feat(kernel/level): is_trivial predicate for level constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
41782c0894 test(kernel/metavar): add metavar tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
bf13441bd7 fix(kernel): bugs in justification module, add missing metavar methods, add basic metavar tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
42e253c962 fix(*): style and clang warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
f855dbb7b0 feat(util): add maps based on red-black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
1ab12eb105 refactor(util/splay_map): remove unnecessary operation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
528ea367ad feat(util): add red-black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
2a73389ed3 refactor(kernel): justification objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
50300126a5 refactor(util/name_generator): make sure there is no risk of overflow, name generators will be extensively used in version 0.2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
501435f6fc feat(kernel): add has_local predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
6baa59376c refactor(kernel): normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
eb046c11fb refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
3c8ccdd33d test(util/exception): experiment with exceptions with nested std::function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
737fe6830f test(tests/kernel): adjust expr tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
73c8bf4436 refactor(tests/kernel): move tests to new kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
72e1678ad9 refactor(kernel): cleanup instantiate and abstract procedures, implement update procedures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
76b1ddb967 feat(kernel): add difference constraint solver with backtracking support, and justification generation, this solver will be used to check the satisfiability of universe level constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
9f93b5d97e feat(kernel/level): new universe level datastructure for universe level polymorphism 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
1739b5c153 fix(kernel/type_checker): caching bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 10:43:01 -08:00
Leonardo de Moura
6d7ec9d7b6 refactor(kernel): add heterogeneous equality back to expr 
The main motivation is that we will be able to move equalities between universes.

For example, suppose we have
    A : (Type i)
    B : (Type i)
    H : @eq (Type j) A B
where j > i

We didn't find any trick for deducing (@eq (Type i) A B) from H.
Before this commit, heterogeneous equality as a constant with type

   heq : {A B : (Type U)} : A -> B -> Bool

So, from H, we would only be able to deduce

   (@heq (Type j) (Type j) A B)

Not being able to move the equality back to a smaller universe is
problematic in several cases. I list some instances in the end of the commit message.

With this commit, Heterogeneous equality is a special kind of expression.
It is not a constant anymore. From H, we can deduce

   H1 : A == B

That is, we are essentially "erasing" the universes when we move to heterogeneous equality.
Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is

  (to_eq (Type i) A B (to_heq (Type j) A B H))  :  (@eq (Type i) A B)

So, it remains to explain why we need this feature.

For example, suppose we want to state the Pi extensionality axiom.

axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} :
      A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)

This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous
equality as a constant. The conclusion

     (∀ x, B x) == (∀ x, B' x)

is syntax sugar for

   (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x))

Even if A, A', B, B' live in a much smaller universe.

As I described above, it doesn't seem to be a way to move this equality back to a smaller universe.

So, if we wanted to keep the heterogeneous equality as a constant, it seems we would
have to support axiom schemas. That is, hpiext would be parametrized by the universes where
A, A', B and B'. Another possibility would be to have universe polymorphism like Agda.
None of the solutions seem attractive.

So, we decided to have heterogeneous equality as a special kind of expression.
And use the trick above to move equalities back to the right universe.

BTW, the parser is not creating the new heterogeneous equalities yet.
Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous
equality as a constant.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 10:28:10 -08:00
Leonardo de Moura
8eec289ce1 feat(kernel): add dependent pairs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 16:52:49 -08:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 14:48:27 -08:00
Leonardo de Moura
9fb3ccb4c0 feat(library/simplifier): support for dependent simplification in lambda expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 16:54:42 -08:00
Leonardo de Moura
abfeacb8f0 fix(tests/library/expr_lt): adjust is_lt unit tests to reflect recent modifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 13:44:44 -08:00
Leonardo de Moura
bbf6e6a256 feat(builtin/kernel): create default rule set in the kernel, and adjust unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 11:24:20 -08:00
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 17:39:12 -08:00
Leonardo de Moura
14c6218bdc chore(kernel): file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 20:06:29 -08:00
Leonardo de Moura
438fa8251b test(kernel/expr): check if the serializer works for metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:15:56 -08:00
Leonardo de Moura
5058e403b5 test(kernel/expr): check if the serializer works for applications with many argumets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:09:46 -08:00
Leonardo de Moura
411f14415d feat(builtin): automatically generate Lean/C++ interface for builtin theories 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 18:09:53 -08:00
Leonardo de Moura
84e211b81b fix(frontends/lean): missing ':' in error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:01:27 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 08:33:52 -08:00
Leonardo de Moura
a4b3d6d6c8 refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 17:25:14 -08:00
Leonardo de Moura
2b2aa228e3 refactor(builtin/kernel): start with small universes 
The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 12:35:00 -08:00
Leonardo de Moura
048151487e feat(kernel): use Pi as forall/implication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 00:38:39 -08:00
Leonardo de Moura
f12a76a5cd test(frontends/lean/scanner): missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 15:03:46 -08:00
Leonardo de Moura
5fe8c32da9 feat(kernel): use new universe contraints in the environment, allow new constraints to be added 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 16:46:11 -08:00
Leonardo de Moura
b5a30855f8 feat(kernel/universe_constraints): add new class for managing universe constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 15:01:28 -08:00
Leonardo de Moura
8c956280d9 chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 11:41:03 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 19:21:44 -08:00
Leonardo de Moura
4ba097a141 feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 13:06:36 -08:00
Leonardo de Moura
9f08156a73 feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 11:03:35 -08:00
Leonardo de Moura
028a9bd9bd feat(frontends/lean/scanner): use Lua style comments in Lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 08:53:27 -08:00
Leonardo de Moura
92c7145d7f feat(kernel/expr): maximize sharing before serializing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 20:03:42 -08:00
Leonardo de Moura
ecc5d1bc3a refactor(kernel): move printer to library, cleanup io_state interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 13:37:50 -08:00
Leonardo de Moura
0592261847 refactor(kernel/io_state): move io_state_stream to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 13:14:21 -08:00
Leonardo de Moura
0cb741285c chore(*): do not type check imported modules when running .cpp tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 07:11:55 -08:00
Leonardo de Moura
1cb7408c46 fix(kernel/normalizer): metavariable reification was incorrect, add tst11 at tests/kernel/normalizer.cpp to expose the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-31 16:24:36 -08:00
Leonardo de Moura
49698bd053 chore(library/all): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:37:25 -08:00
Leonardo de Moura
08718e33dc refactor(builtin): only load the kernel and natural numbers by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:35:37 -08:00
Leonardo de Moura
ecd62a1783 refactor(builtin/basic): rename basic.lean to kernel.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:46:03 -08:00
Leonardo de Moura
72761f14e4 refactor(library/io_state): move to the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:20:23 -08:00
Leonardo de Moura
c3bc6afb12 refactor(library/arith): move int and nat declarations to .lean files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 10:32:14 -08:00
Leonardo de Moura
14c3e11289 refactor(kernel/builtin): emove mk_bin_rop and mk_bin_lop to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 15:23:18 -08:00
Leonardo de Moura
dfe46b9d25 refactor(kernel/builtin): move definition and axioms to basic.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 14:01:30 -08:00
Leonardo de Moura
411ebbc3c1 refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file 
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 03:04:49 -08:00
Leonardo de Moura
22bebbf242 feat(kernel/object): serializer for kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 14:39:10 -08:00
Leonardo de Moura
755e8b735f feat(kernel/expr): serializer for kernel expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 01:23:21 -08:00
Leonardo de Moura
0ef8ba2939 feat(kernel/level): serializer for level objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 23:30:13 -08:00
Leonardo de Moura
3715b10ce7 feat(util/sexpr/options): serialization for options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 20:40:00 -08:00
Leonardo de Moura
dbebb4a4a1 feat(util/sexpr): serialization for sexpr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 20:19:56 -08:00
Leonardo de Moura
9c6dc5d230 feat(util/serializer): add hackish write_double/read_double 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 19:46:45 -08:00
Leonardo de Moura
abc370a011 feat(util/numerics): serialization for mpz and mpq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 18:32:01 -08:00
Leonardo de Moura
49df0c435d feat(util/serializer): make sure the read/write is portable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 18:07:19 -08:00
Leonardo de Moura
d05695c331 feat(util/name): serialization for hierarchical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 17:47:20 -08:00
Leonardo de Moura
b72937c02c feat(util/serializer): simple serialization infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-27 16:50:06 -08:00
Leonardo de Moura
60ac0b508d fix(tests/kernel/environment): adjust the test to reflect (recent) change in the normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 21:14:22 -08:00
Soonho Kong
de018220e1 feat(*): use std::make_shared to create shared_ptr 2013-12-24 14:32:50 -05:00
Leonardo de Moura
702f0c2190 fix(tests/kernel/free_vars): reduce example stack size consumption 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 12:57:25 -08:00
Leonardo de Moura
4229e498d2 refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 11:51:38 -08:00
Leonardo de Moura
df58eb132e feat(frontends/lean): simplify explicit version names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 17:05:25 -08:00
Leonardo de Moura
97145c0f88 fix(library/elaborator): bug in free variable normalization (lift was missing) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:41:09 -08:00
Leonardo de Moura
7b0b363b32 fix(kernel/normalizer): metavariable reification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:40:26 -08:00
Leonardo de Moura
7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque 
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 12:47:47 -08:00
Leonardo de Moura
daef2b7b24 feat(util/sexpr/options): add is_eqp predicate for options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 10:53:53 -08:00
Leonardo de Moura
ae01d3818d fix(frontends/lean/parser): parse_type method 
The parser had a nasty ambiguity. For example,
    f Type 1
had two possible interpretations
    (f (Type) (1))
or
    (f (Type 1))

To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis.
Examples:
    (Type 1)
    (Type U)
    (Type M + 1)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 15:24:34 -08:00
Leonardo de Moura
dd72269b13 feat(frontends/lean): rename command Set to SetOption 
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 21:18:48 -08:00
Leonardo de Moura
97b872a05c refactor(frontends/lean): remove frontend class, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 14:37:55 -08:00
Leonardo de Moura
10f28c7bec feat(kernel/replace_fn): non-recursive replace_fn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 16:35:39 -08:00
Leonardo de Moura
836357c65c fix(kernel/normalizer): bug in Let normalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 12:35:25 -08:00
Leonardo de Moura
f09fd0fc04 feat(kernel/printer): include de Bruijn index in the debug printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 16:56:46 -08:00
Leonardo de Moura
af42078205 fix(kernel): incorrect use of scoped_map 
This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 15:11:39 -08:00
Leonardo de Moura
2253d8079b chore(util/pdeque): remove unused template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:31:44 -08:00