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

871 commits

Author SHA1 Message Date
Leonardo de Moura
150d285b39 fix (library/unifier): occurs_context_check 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 14:45:36 -07:00
Leonardo de Moura
16bdc51fc4 refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 13:36:31 -07:00
Leonardo de Moura
5e0e737213 feat(library/scoped_ext): do not import 'children' namespace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:32:34 -07:00
Leonardo de Moura
6085a54416 feat(library/error_handling): improve unifier_exception error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:49:50 -07:00
Leonardo de Moura
e735a8e5ff fix(library/unifier): bug in conflict resolution 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:42:40 -07:00
Leonardo de Moura
52ff29a6f7 feat(frontends/lean): add 'coercion' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:08:39 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:50:49 -07:00
Leonardo de Moura
a42a80407a fix(library/unifier): when imitating (f a), abstract local constants occurring in f 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 16:11:31 -07:00
Leonardo de Moura
f981a4c1fe fix(library/unifier): bug in lambda_abstract_locals auxiliary function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 09:59:08 -07:00
Leonardo de Moura
6db6048bf8 feat(library/error_handling): pretty print unifier exceptions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 09:41:25 -07:00
Leonardo de Moura
18a883ab1b fix(library/unifier): set conflict if type mismatch during metavariable assignment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 09:33:34 -07:00
Leonardo de Moura
d055c4880f feat(frontends/lean): connect new elaborator to frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 08:31:00 -07:00
Leonardo de Moura
d7436e600b fix(library/resolve_macro): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 17:40:58 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
2c0f596665 fix(library/choice): avoid assertion violation when Lua API is misused 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 12:14:38 -07:00
Leonardo de Moura
3169f8c126 feat(library): add mk_explicit/is_explicit procedures for '@'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 12:11:27 -07:00
Leonardo de Moura
aa8b5655dd feat(frontends/lean): add notation overwrite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 16:10:36 -07:00
Leonardo de Moura
60f230a206 doc(library/unifier): ignore flex-flex constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 14:33:09 -07:00
Leonardo de Moura
7df397fe63 test(lua): add universe constraint unifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 14:19:02 -07:00
Leonardo de Moura
a0e4dccdac refactor(kernel/constraint): rename choice constraint fields 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 13:52:03 -07:00
Leonardo de Moura
60c60c6cf5 feat(library/kernel_bindings): add mk_choice_cnstr to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 13:39:21 -07:00
Leonardo de Moura
6d14de76f3 feat(kernel/constraint): add 'delayed' flag to choice constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 12:56:06 -07:00
Leonardo de Moura
66016df0ad feat(library/unifier): add imitation step for macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 12:44:22 -07:00
Leonardo de Moura
2fa5b17592 feat(library/unifier): add unifier.max_steps unifier.use_exceptions options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 12:38:57 -07:00
Leonardo de Moura
7b188ea37e feat(library/unifier): implement flex-rigid case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 11:00:35 -07:00
Leonardo de Moura
68d55ef398 doc(library/unifier): document some of the unifier_fn methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 08:22:38 -07:00
Leonardo de Moura
9f7b92a410 refactor(library/unifier): combine active and delayed constraint sets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 21:10:59 -07:00
Leonardo de Moura
228f51dcfa feat(library/unifier): add support for choice constraint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 17:21:24 -07:00
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
c8a07dee53 feat(library/unifier): add unifier_plugin support, and unit test with plugin implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 16:27:04 -07:00
Leonardo de Moura
238a0dbfba fix(library/unifier): memory violation, and missing set_conflict 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 14:09:06 -07:00
Leonardo de Moura
29a00c46d0 feat(library/unifier): add main loop and resolve_conflict 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 11:57:10 -07:00
Leonardo de Moura
644c387cfe refactor(kernel/constraint): rename: level constraints are also equality constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:50:47 -07:00
Leonardo de Moura
73666af4a4 fix(library/register_module): missing open_unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:01:51 -07:00
Leonardo de Moura
3953d4d122 feat(kernel/type_checker): add push/pop methods to type_checker, they control the cache, and allow the type checker to reuse results even when it is used inside of a backtracking search 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:58:05 -07:00
Leonardo de Moura
9c745057b4 feat(library/unifier): add unify_fn skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 20:08:39 -07:00
Leonardo de Moura
bf8f3318d8 feat(library): add unifier module skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 13:38:17 -07:00
Leonardo de Moura
37bee8c852 refactor(kernel/type_checker): simplify replace constraint_handler with closure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
86a56fbd2d feat(library/kernel_bindings): expose methods substitution::for_each_expr and substitution::for_each_level in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
67088b130e refactor(kernel/constraint): simplify constraint interface, and add choice constraint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
05d1832425 refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-19 22:33:58 -07:00
Leonardo de Moura
77c5319c4a chore(*): remove Lua 'migrate' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 07:01:34 -07:00
Leonardo de Moura
3ea24c0f32 fix(library/kernel_bindings): set_environment and set_io_state objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 22:36:47 -07:00
Leonardo de Moura
f9d81c24d3 feat(library/expr_lt): add lex comparison for expression pairs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 12:14:22 -07:00
Leonardo de Moura
0779db7ae9 fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 16:56:11 -07:00
Leonardo de Moura
2c4175341c feat(library/placeholder): allow types to be attached to placeholders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:35:55 -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
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
a65c43c0db feat(frontends/lean/builtin_cmds): add definition command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 17:30:35 -07:00
Leonardo de Moura
01cecb76db feat(frontends/lean/builtin_cmds): add 'variable' command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 15:13:50 -07:00
Leonardo de Moura
ce259e6265 feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 11:34:43 -07:00
Leonardo de Moura
5aca452439 feat(library/aliases): add 'exceptions' and support for universes to add_aliases procedure, add for_each_universe method to environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 08:26:05 -07:00
Leonardo de Moura
a914345d29 feat(library): new scoping framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 19:33:02 -07:00
Leonardo de Moura
d50376249f feat(library/aliases): add level aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 12:35:02 -07:00
Leonardo de Moura
1c5d3295cc refactor(library/deep_copy): use replace to implement deep_copy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:35:34 -07:00
Leonardo de Moura
4f83b1a50b feat(library): add choice expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:35:34 -07:00
Leonardo de Moura
431b47377d feat(library/kernel_bindings): add 'set_env/set_environment' commands for updating the global environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 11:03:12 -07:00
Leonardo de Moura
637eae40ad feat(library/aliases): add support for alias overloading 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 10:05:51 -07:00
Leonardo de Moura
439b6c1e96 feat(frontends/lean/parse_table): add parse_table Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-09 15:33:39 -07:00
Leonardo de Moura
1c49b4d85f chore(*): replace unique_lock with lock_guard when we do not need to use conditional variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 20:55:25 -07:00
Leonardo de Moura
7124866a4f fix(library/module): potential deadlock when child thread threw an exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 20:34:18 -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
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
4cf1b05831 refactor(library/token_set): move to frontends/lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-05 13:10:50 -07:00
Leonardo de Moura
70c3ae8692 feat(library/token_set): register builtin commands 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-05 13:05:40 -07:00
Leonardo de Moura
5b898aa3ed refactor(util/trie): modify interface to avoid the creation of many temporary optional values and inc/dec reference counters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-05 12:40:51 -07:00
Leonardo de Moura
220f94d36e feat(library/kernel_bindings): expose instantiate_levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-04 16:26:26 -07:00
Leonardo de Moura
1c96373c1a feat(library/kernel_bindings): expose replace_fn in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-04 15:26:55 -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
45a3ab5141 refactor(library/aliases): it is bad design to instantiate parameter using the parameter name, the parameter names have no semantic value 
Moreover, we could create type incorrect aliases by "accident".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 15:20:14 -07:00
Leonardo de Moura
1f6cfce05c refactor(library/placeholder): use different names for different placeholders, it is bad design to assume that two structurally identical expressions are different when they are allocated twice (this design is not compatible with any form of hash-consing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 14:59:00 -07:00
Leonardo de Moura
076414693a feat(library/kernel_bindings): improve argument validation in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 10:17:12 -07:00
Leonardo de Moura
7dba2c29d2 feat(library): add token set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 02:34:12 -07:00
Leonardo de Moura
ab5f570924 refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-03 00:46:28 -07:00
Leonardo de Moura
045fa911d1 fix(library/kernel_bindings): missing kind in lean_kind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 18:12:02 -07:00
Leonardo de Moura
ab7469c175 fix(library/scope): warning message, and old comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 18:08:46 -07:00
Leonardo de Moura
1467bb256e chore(library): remove unnecessary code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 16:22:38 -07:00
Leonardo de Moura
33bbcd9526 chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 16:20:34 -07:00
Leonardo de Moura
82e1f87e08 feat(kernel): add function param_names_to_levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 16:17:04 -07:00
Leonardo de Moura
712c10f818 fix(library/scope): make sure the local universe names do not conflict with universe parameter names when close a section, add declaration parameter name sanitizers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 15:39:57 -07:00
Leonardo de Moura
f82658f213 feat(library): add helper functions for 'updating' declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 15:13:38 -07:00
Leonardo de Moura
dcacf6fbca refactor(util): rename name_map to name_hash_map 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 14:34:22 -07:00
Leonardo de Moura
b6d2328c1d fix(library/scope): make sure local levels are added in the beginning of the universe parameter list 
The idea is to make sure it is consistent with the behavior used for regular local parameters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 14:06:31 -07:00
Leonardo de Moura
9b6b162a7c fix(library/scope): bug when abstracting inductive declaration in the end of a section 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 13:46:16 -07:00
Leonardo de Moura
6ee272477a fix(library/private): bug when preserving private names at end_section 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 11:32:14 -07:00
Leonardo de Moura
936ca80b9b fix(library/scope): bug in add_definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 11:04:34 -07:00
Leonardo de Moura
e56307f006 fix(library/scope): bug in end_scope procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 10:43:28 -07:00
Leonardo de Moura
6e113206b6 feat(library/scope): add support for inductive datatypes in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 10:28:07 -07:00
Leonardo de Moura
d36ef5dcbe feat(library/private): preserve 'hidden/private name => user name' map when section is closed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-01 18:09:11 -07:00
Leonardo de Moura
585f3adde1 feat(library/scope): add sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-01 17:55:11 -07:00
Leonardo de Moura
286d7f0e64 feat(library): add namespace management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 15:41:01 -07:00
Leonardo de Moura
3145cee51f refactor(library/aliases): move replace_prefix to util/name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 15:11:22 -07:00
Leonardo de Moura
f7b3061a66 feat(library/module): improve 'import module' error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 12:52:06 -07:00
Leonardo de Moura
75abcea83f fix(library/kernel_bindings): Lua API consistency, environment:add method also register declaration in the export table 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 12:20:57 -07:00
Leonardo de Moura
7bd10c2d2d feat(library/module): export global universe level declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-31 12:12:41 -07:00
Leonardo de Moura
1b5366cfb7 feat(library): add module for implementing aliases and 'using' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 21:42:40 -07:00
Leonardo de Moura
6902d8cb05 feat(library): add simple placeholder module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 20:28:28 -07:00
Leonardo de Moura
72f9e26dab refactor(library/private): add hidden_to_user_name and user_to_hidden_name functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-30 17:52:01 -07:00
Leonardo de Moura
128d668f03 feat(library): add support for creating 'private/hidden' names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 18:37:09 -07:00
Leonardo de Moura
13f9db26b7 refactor(library): add module namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 13:58:47 -07:00
Leonardo de Moura
fc7d5461b1 feat(library/kernel_bindings): add to_io_state_ext helper function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 13:35:11 -07:00
Leonardo de Moura
f8e71f711f feat(library/expr_lt): add expr_quick_cmp functional object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 13:34:16 -07:00
Leonardo de Moura
bfa9b90af0 feat(library/kernel_bindings): used 'named' parameters in import_modules API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 11:03:44 -07:00
Leonardo de Moura
ade5d99023 feat(library/modules): add option for discarding the proof of imported theorems (after checking them) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-29 10:56:28 -07:00
Leonardo de Moura
28b9d17a14 perf(library/module): do not use multiple threads when skipping type checking, add flag to disable/enable type checking theorems asynchronously 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-28 10:04:42 -07:00
Leonardo de Moura
e206fcc1af perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications 
We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 23:16:52 -07:00
Leonardo de Moura
6129cccc66 perf(library/shared_environment): replace shared_mutex with simple mutex, the shared_mutex is just overhead and impacts negatively on performance tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 08:34:44 -07:00
Leonardo de Moura
75117bede8 fix(library/kernel_bindings): use standard environment in import_modules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 15:54:08 -07:00
Leonardo de Moura
eca906b074 feat(library/module): add inductive decls to .olean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 15:38:09 -07:00
Leonardo de Moura
49e1f78a33 feat(library/kernel_serializer): add serializer/deserializer for inductive decls 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-26 15:37:53 -07:00
Leonardo de Moura
2d31c6c0b2 feat(library/coercion): improve get_user_coercions API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 11:35:47 -07:00
Leonardo de Moura
e058839d24 fix(library/coercion): allow cycles in the coercion graph 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 11:08:49 -07:00
Leonardo de Moura
71b555ab15 test(lua): coercion module error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 10:01:04 -07:00
Leonardo de Moura
ef14c3d67e fix(library/coercion): coercion replacement 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 09:49:26 -07:00
Leonardo de Moura
eb6d72a20c fix(library/coercion): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 08:55:20 -07:00
Leonardo de Moura
fc1819aadd test(lua): coercion serialization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 08:38:50 -07:00
Leonardo de Moura
f598c6a110 fix(library/coercion): bug in coercion to function-class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 08:21:53 -07:00
Leonardo de Moura
118eae2733 fix(library/coercion): bug add_coercion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 07:45:49 -07:00
Leonardo de Moura
e9e61fec51 feat(library/coercion): add for_each_coercion procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 07:45:49 -07:00
Leonardo de Moura
a408883c92 fix(library/coercion): bug in de-Bruijn indices 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 07:45:49 -07:00
Leonardo de Moura
1ee6bb48fc fix(library/coercion): bug in add_coercion_trans 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 06:25:31 -07:00
Leonardo de Moura
6536232107 feat(library/coercion): expose coercion module in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-25 06:05:31 -07:00
Leonardo de Moura
2be9bcef78 feat(library/coercion): add coercion management implementation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-24 19:28:42 -07:00
Leonardo de Moura
1cff37a084 feat(library/module): use io_state to report warning messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-24 14:08:15 -07:00
Leonardo de Moura
5df2331159 feat(library/io_state): add constructor for copying io_state, but replacing channels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-24 13:51:39 -07:00
Leonardo de Moura
f8255ddac6 fix(library/module): deadlock 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 16:46:53 -07:00
Leonardo de Moura
d30c600eb2 fix(library/module): bug in module import 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 16:23:47 -07:00
Leonardo de Moura
879572ee7e fix(kernel/module): non-termination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 15:12:47 -07:00
Leonardo de Moura
902b6160fa fix(kernel/module): deadlock 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 14:43:03 -07:00
Leonardo de Moura
a3b0200d32 feat(library/module): do not use threads when lean is not compiled with LEAN_MULTI_THREAD 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 11:32:24 -07:00
Leonardo de Moura
be96dc2ddf fix(library/module): bug in next_task method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 11:13:38 -07:00
Leonardo de Moura
c593247fcc fix(library/kernel_serializer): bug in declaration serialization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 11:11:16 -07:00
Leonardo de Moura
61b662151e fix(library/module): bug in export_module procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 10:57:11 -07:00
Leonardo de Moura
6bbb9d3667 feat(library/kernel_bindings): declarations added with the function add_decl are automatically registered in the to-export list 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 10:52:47 -07:00
Leonardo de Moura
1a663afda4 feat(library/module): add extra function for adding uncertified declarations when trust_lvl > LEAN_BELIEVER_TRUST_LEVEL 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 10:50:34 -07:00
Leonardo de Moura
a0a70bcea7 feat(library/kernel_bindings): expose import/export functions in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-23 09:35:32 -07:00
Leonardo de Moura
21905289fa feat(library/module): add module import procedure 
The modules are processed in parallel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-22 18:15:44 -07:00
Leonardo de Moura
76177d7765 feat(library/kernel_bindings): improve type_checker:check Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-22 14:10:25 -07:00
Leonardo de Moura
e39feabb72 feat(library/module): add declaration reader 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:54:29 -07:00
Leonardo de Moura
9f4bae6856 feat(library/kernel_bindings): add hott_environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:49:30 -07:00
Leonardo de Moura
4d1fecb21d refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:24:24 -07:00
Leonardo de Moura
f08a852da8 feat(library/kernel_bindings): expose environment::add(declaration) method in the Lua API, and add example to demonstrate its usage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-21 11:12:55 -07:00
Leonardo de Moura
8ffe66dc4f feat(library): add module system API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 18:35:59 -07:00
Leonardo de Moura
dd3edcb19f feat(library): add shared environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 15:42:52 -07:00
Leonardo de Moura
11fc917102 test(lua): add tests for improving kernel_bindings coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 12:16:12 -07:00
Leonardo de Moura
c5e8c10c9d fix(library/normalize): bug in normalize 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 11:53:58 -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
00b1a84051 feat(library/kernel_bindings): expose environment::for_each method in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:16:19 -07:00
Leonardo de Moura
8a8c5a2b84 feat(library/kernel_bindings): add normalize, whnf, type_check, infer_type methods to environment object Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 09:40:50 -07:00
Leonardo de Moura
11793e7998 feat(library): add simple normalization procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 09:40:30 -07:00
Leonardo de Moura
4103c85ce3 feat(library/kernel_bindings): improve Fun/Pi Lua APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 09:00:19 -07:00
Leonardo de Moura
bcb9965844 feat(library/kernel_bindings): improve Fun/Pi Lua APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:07:20 -07:00
Leonardo de Moura
a7aacaa782 feat(library/kernel_bindings): improve list_level support in the Lua interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 15:18:48 -07:00
Leonardo de Moura
f3ed20a229 feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 12:52:25 -07:00
Leonardo de Moura
f7bc5ac514 fix(library/kernel_bindings): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:44:51 -07:00
Leonardo de Moura
d0e7c88ea8 feat(library/kernel_bindings): improve universe level Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:40:35 -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
33ae79cd9e refactor(kernel): move shallow copy function to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:20:24 -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
36b070cb5b refactor(kernel/inductive): simplify inductive datatype API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 09:24:34 -07:00
Leonardo de Moura
4ec89e8561 feat(library/kernel_bindings): add sugar for level expressions in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 08:10:36 -07:00
Leonardo de Moura
5fc0f06a8d feat(library/kernel_bindings): add Lua API for declaring datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 18:08:50 -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
193aa4a83f feat(library/kernel_bindings): improve Pi and Fun Lua APIs, and allow users to provide binder information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 14:09:00 -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
d6d72ba80e refactor(kernel): add binder structure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 10:51:54 -07:00
Leonardo de Moura
c0d8a3195c fix(library/kernel_serializer): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 18:00:09 -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
2e3ffea2ec feat(library): add new coercion API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 16:50:12 -07:00
Leonardo de Moura
1be758e4ef feat(library/resolve_macro.cpp): add macro to encode propositional resolution proofs compactly 
This is also a test for the macro_definition infrastructure that we have in the kernel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
e644419463 feat(library/bin_app): add simpler is_bin_app predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
24d8092a73 feat(library): add goodies for binary functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
6f8f074f20 feat(library/kernel_bindings): make mk_arrow nary in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
0edcea55de fix(library/kernel_bindings): clang++ compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:48:04 -07:00
Leonardo de Moura
6e78256b87 feat(library/kernel_bindings): expose is_bi_equal predicate in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:24:49 -07:00
Leonardo de Moura
2e1a0bd50c feat(kernel/expr): add is_contextual binder info 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:54:27 -07:00
Leonardo de Moura
ab1a89e24c refactor(library): remove dead files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:44:52 -07:00
Leonardo de Moura
956b775c48 feat(library/kernel_bindings): add let field accessors in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:17:30 -07:00
Leonardo de Moura
2bb537f3fb feat(library/kernel_bindings): add sugar for creating Let expressions from Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 12:28:10 -07:00
Leonardo de Moura
f903626b78 feat(library/kernel_bindings): allow a list of level params/globals to be provided to declarations (instead of a list of names) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 09:45:48 -07:00
Leonardo de Moura
9ed700a5a6 feat(kernel/environment): add forget method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 08:40:46 -07:00
Leonardo de Moura
c883c638d6 feat(library/kernel_bindings): expose expression tags in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:50:43 -07:00
Leonardo de Moura
6f03064c46 fix(library/kernel_bindings): bug in mk_definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 12:56:50 -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
9d96f24766 refactor(kernel): remove convertability constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:25:27 -07:00
Leonardo de Moura
aaea298839 refactor(library/kernel_bindings): remove level pair and list of level pairs from Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:13:10 -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
a650a4f9b5 fix(library/kernel_bindings): bug in mk_app, add expr_lt tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 19:54:52 -07:00
Leonardo de Moura
9676f48470 feat(library/kernel_bindings): add list of certified_definitions in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:51:34 -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
95262fb68d feat(library/kernel_bindings): add remaining type_checker constructors in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 17:13:06 -07:00
Leonardo de Moura
3aa1afdf51 refactor(util): file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 14:15:28 -07:00
Leonardo de Moura
bf57f951ea refactor(util): move Lua named parameter support to a different file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 13:20:37 -07:00
Leonardo de Moura
f3c7bc948a feat(library/kernel_bindings): type_checker Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 19:04:15 -07:00
Leonardo de Moura
62db010ba3 feat(library/kernel_bindings): add optional arguments to empty_environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:06:27 -07:00
Leonardo de Moura
4c5f88e63b feat(library/kernel_bindings): global level constructor/accessor/recognizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:22:45 -07:00
Leonardo de Moura
8ae0e46e9d feat(library/kernel_bindings): add new global level methods to environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:17:04 -07:00
Leonardo de Moura
503d8dfa9e feat(kernel): add global universe level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-06 16:13:29 -07:00