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

1254 commits

Author SHA1 Message Date
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
Leonardo de Moura
8095783c36 refactor(library/kernel_bindings): use new functions for simulating python-like named arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:42:16 -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
Leonardo de Moura
10d8840cac feat(library/kernel_bindings): add environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:53:32 -07:00
Leonardo de Moura
4f3fad5d65 feat(library/kernel_bindings): add certified_definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:46:59 -07:00
Leonardo de Moura
8f5491447a feat(library/kernel_bindings): add environment_id Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:42:27 -07:00
Leonardo de Moura
fc2d5f1595 feat(library/kernel_bindings): add definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:00:59 -07:00
Leonardo de Moura
b83410f042 fix(library/kernel_bindings): g++ compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 14:34:56 -07:00
Leonardo de Moura
dc627c9965 test(lua): add constraint API tests, and fix minor bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:37:46 -07:00
Leonardo de Moura
6ef161824d feat(library/kernel_bindings): constraint Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:17:00 -07:00
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
94ca82ec85 fix(library/kernel_bindings): incorrect use of pushinteger, and improve justification Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:03:43 -07:00
Leonardo de Moura
a5229e5283 chore(util/lua): name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:40:18 -07:00
Leonardo de Moura
7cd892464f feat(library/definition): macro definition and application Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:29:34 -07:00
Leonardo de Moura
9f5122b4c7 feat(library/kernel_bindings): justification Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 16:04:30 -07:00
Leonardo de Moura
340c0e0945 feat(library/kernel_bindings): substitution Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:30:30 -07:00
Leonardo de Moura
686c307976 feat(library/kernel_bindings): expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:25:49 -07:00
Leonardo de Moura
305815cb56 feat(library/kernel_bindings): expose expr_binder_info in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 11:23:37 -07:00
Leonardo de Moura
884b3f9b53 refactor(library/kernel_bindings): part of expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 16:37:26 -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
fd034521dc feat(library/kernel_bindings): cleanup level Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 17:05:25 -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
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
984048f40d feat(library/kernel_bindings): new level Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 15:08:58 -07:00
Leonardo de Moura
412a3797f4 refactor(*): add pushboolean inline function, and replace lua_pushboolean with it 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 14:37:16 -07:00
Leonardo de Moura
f7e705badb refactor(library/kernel_bindings): reactive some of the kernel Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 11:52:09 -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
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
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
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
0b3599851d refactor(library): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
d836e45452 refactor(library): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
4b7fe064fe refactor(kernel): finish formatter interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
28516a8dc2 refactor(library): remove unnecessary file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
e0ef6b2e9a refactor(library): monotonic total order on terms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
8cd78e00f1 refactor(library): deep_copy procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
1d10953da4 fix(library/elaborator): add hack for experimenting with algebraic hierarchy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-25 11:20:40 -08:00
Leonardo de Moura
309e7ba880 fix(library/elaborator): temporary fix for bug reported by Jeremy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-24 15:26:21 -08:00
Leonardo de Moura
bfe64a7031 fix(library/elaborator): hack for fixing a bug due to pairs/projs, this is temporary fix until we build a new elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-11 21:30:26 -08:00
Leonardo de Moura
b7b868de85 fix(library/elaborator): bug reported by Jeremy Avigad 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 14:01:22 -08:00
Leonardo de Moura
57982135d9 fix(library/simplifier): bug using congr1 theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 16:24:29 -08:00
Leonardo de Moura
c45c1748d8 refactor(builtin/kernel): reorder congr1 arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 16:15:44 -08:00
Leonardo de Moura
2d70e2f4f2 fix(library/tactic/goal): bug in the proof builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 15:02:36 -08:00
Leonardo de Moura
1c43020fc9 fix(library/tactic/goal): bug creating main proof builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 09:11:07 -08:00
Leonardo de Moura
24528ff685 fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 18:02:08 -08:00
Leonardo de Moura
1ec01f5757 refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 16:04:44 -08:00
Leonardo de Moura
ad7b13104f feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 15:03:16 -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
d4b08fcf96 feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator 
Unification constraints of the form

         ctx |- ?m[inst:i v] == T

         and

         ctx |- (?m a1 ... an) == T

are delayed by elaborator because the produce case-splits.
On the other hand, the step that puts terms is head-normal form is eagerly applied.
This is a bad idea for constraints like the two above. The elaborator will put T in head normal form
before executing process_meta_app and process_meta_inst. This is just wasted work, and creates
fully unfolded terms for solvers and provers.

The new test demonstrates the problem. In this test, we mark several terms as non-opaque.
Without this commit, the produced goal is a huge term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 21:08:00 -08:00
Leonardo de Moura
363c4dc5c2 feat(library/elaborator): improve support for dependent pairs in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -08:00
Leonardo de Moura
e85b1f1ac0 feat(library/elaborator): expose elaborator configuration options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -08:00
Leonardo de Moura
e4579b93e4 fix(library/elaborator): try first projection before imitation in the higher-order unifier 
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 13:35:05 -08:00
Leonardo de Moura
c01f82aeb7 feat(builtin): add sum types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-05 23:04:44 -08:00
Leonardo de Moura
f4ec874c6e refactor(builtin): remove dead module heq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 14:42:28 -08:00
Leonardo de Moura
0283887ee9 refactor(builtin/kernel): move the heq axioms into kernel.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 14:17:34 -08:00
Leonardo de Moura
f03c09c10b feat(library/elaborator): add support for proj/pair/sigma in the the higher-order unification procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 13:53:30 -08:00
Leonardo de Moura
cc96b50644 feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 20:53:11 -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
6be50f0133 refactor(builtin/heq): merge cast and heq modules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 15:01:48 -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
e3dc552c39 fix(library/simplifier): nontermination 
The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition

    definition a := 1

it will match 'a' with '1' since they are definitionally equal.

Then, if we have a theorem

    theorem a_eq_1 : a = 1

as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"

   a --> 1 --> 1 --> 1 ...

The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.

To avoid this loop, we test if the new expression is not equal to the previous one.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 15:55:21 -08:00
Leonardo de Moura
1d85267d26 fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 15:38:22 -08:00
Leonardo de Moura
110ca84984 feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 13:49:24 -08:00
Leonardo de Moura
b444756d20 fix(library/simplifier): missing condition in implication simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 22:14:01 -08:00
Leonardo de Moura
759aa61f70 refactor(builtin/kernel): define if-then-else using Hilbert's operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 19:28:42 -08:00
Leonardo de Moura
b45ab9dc30 feat(library/elaborator): use equality constraints instead of convertability constraints on definitions 
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 14:13:21 -08:00
Leonardo de Moura
41f5e2a067 feat(library/simplifier): statically check (conditional) equations (aka rewrite rules) to verify whether we can skip type checking when using them in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 18:32:40 -08:00
Leonardo de Moura
4f3127d3d5 fix(library/simplifier): check if the given types are convertible to ceq expected types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 15:15:55 -08:00
Leonardo de Moura
a19f9d4846 feat(library/simplifier): discard conditional equations that are clearly non-terminating 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 13:56:45 -08:00
Leonardo de Moura
dd6aae378f fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 13:29:20 -08:00
Leonardo de Moura
069e5edf6b fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:01:01 -08:00
Leonardo de Moura
92ba4e8b2d feat(library/simplifier): add support for metavariables in conditional rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 08:34:04 -08:00
Leonardo de Moura
24452289dd feat(library/simplifier): make sure the simplifier can handle meta-variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 20:30:47 -08:00
Leonardo de Moura
ee4344076e feat(library/simplifier): improve error message when simplifier is looping 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 19:36:31 -08:00
Leonardo de Moura
b31ef34787 feat(library/simplifier): preserve binder names when applying higher-order rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:50:27 -08:00
Leonardo de Moura
6da1b447f0 fix(library/hop_match): do not match iff with = 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:21:05 -08:00
Leonardo de Moura
dbdbd211e3 fix(library/simplifier): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 23:29:53 -08:00
Leonardo de Moura
160dc71cb5 refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 17:38:06 -08:00
Leonardo de Moura
3b152d1a9e refactor(kernel): use ro_metavar_env instead of metavar_env in places where we only need to read the metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 16:44:43 -08:00
Leonardo de Moura
8bccfb947a feat(library/simplifier): expose simplier and simplifier_monitor objects in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:02:05 -08:00
Leonardo de Moura
c088825ef0 feat(library/simplifier): add simplifier_monitor interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 11:46:28 -08:00
Leonardo de Moura
579b751e01 fix(library/simplifier): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 23:16:24 -08:00
Leonardo de Moura
4d25cb7f47 feat(library/tactic): add simplify_tactic based on the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 18:53:18 -08:00
Leonardo de Moura
5e6c1d4904 refactor(builtin/heq): remove axiom hpiext since we don't use it anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 13:11:17 -08:00
Leonardo de Moura
50df761d90 refactor(library/simplifier): remove the is_typem hack, it is not needed anymore now that we don't use hpiext anymore 
Now, we are again using the following invariant for simplifier_fn::result
The type of in the equality of the result is definitionally equal to the
type of the resultant expression.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 12:21:23 -08:00
Leonardo de Moura
29e448f034 fix(library/simplifier): remove support in the simplifier for (forall x : A, B x) when it is not a proposition, the problem is that hpiext axiom produces an equality in a too big universe 
For example, in the hpiext axiom, the resultant equality if for (Type M+1)

axiom hpiext {A A' : TypeM} {B : A -> TypeM} {B' : A' -> TypeM} :
      A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x)

even if the actual arguments A, A’, B, B’ "live" in a much smaller universe (e.g., Type).

So, it would be great if we could move the resultant equality back to the right universe.
I don't see how to do it right now.

The other solution would require a major rewrite of the code base.
We would have to support universe level arguments like Agda, and write the axiom hpiext as:

axiom hpiext {l : level} {A A' : (Type l)} {B : A -> (Type l)} {B' : A' -> (Type l)} :
      A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x)

This is the first instance I found where it is really handy to have this feature.
I think this would be a super clean solution, but it would require a big rewrite in the code base.
Another problem is that the actual semantics that Agda has for this kind of construction is not clear to me.
For instance, sometimes Agda reports that the type of an expression is (Set omega).

An easier to implement hack is to support "axiom templates".
We create instances of hipext "on-demand" for different universe levels.
This is essentially what Coq does, since the universe levels are implicit in Coq.
This is not as clean as the Agda approach, but it is much easier to implement.

A super dirty trick is to include some instances of hpiext for commonly used universes
(e.g., Type and (Type 1)).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 12:10:34 -08:00
Leonardo de Moura
52ee9b35dd feat(library/simplifier): add support for simplifying even when heq module is not available 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 11:29:36 -08:00
Leonardo de Moura
fafaa7e78e fix(library/simplifier): remove hack for handling some constants that expect an argument of type TypeU, the new approach is general 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 10:10:57 -08:00
Leonardo de Moura
89bb5fbf19 chore(library/simplifier): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 00:36:17 -08:00
Leonardo de Moura
844572c382 feat(library/simplifier): support for dependent simplification in Pi/forall expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 00:32:05 -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
7015089734 fix(library/simplifier): move to locally nameless approach in the simplifier. Contextual simplification may add rewriting rules with free variables, and it is a mess to manage them when using de Bruijn indices 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 10:49:44 -08:00
Leonardo de Moura
df3129e80d fix(library/hop_match): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 10:08:53 -08:00
Leonardo de Moura
7a4eb4b8ed feat(library/simplifier): contextual simplification for A -> B 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 22:32:55 -08:00
Leonardo de Moura
c2381e43f1 fix(library/simplifier): bug in cast elimination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 21:25:09 -08:00
Leonardo de Moura
8e0888828d fix(library/simplifier): missing check in mk_hcongr_th 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
26bea77721 fix(library/simplifier): bug in heterogeneous equality support, and universe commutativity support in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
dbc100cc2e feat(library/simplifier): cast elimination in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 17:28:14 -08:00
Leonardo de Moura
180be5c4a2 feat(library/simplifier): improve contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 13:11:58 -08:00
Leonardo de Moura
33193e1ab3 feat(library/simplifier): improve contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:54:29 -08:00
Leonardo de Moura
d6692264e8 feat(library/simplifier): contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:23:22 -08:00
Leonardo de Moura
17cce340f6 fix(library/elaborator): in optimization for metavariable free terms 
The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 18:06:00 -08:00
Leonardo de Moura
8214c7add4 feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer 
Before this commit, the elaborator was solving constraints of the form

       ctx |- (?m x) == (f x)
as
       ?m <- (fun x : A, f x)    where A is the domain of f.

In our kernel, the terms f and (fun x, f x) are not definitionally equal.
So, the solution above is not the only one. Another possible solution is

       ?m  <- f

Depending of the circumstances we want  ?m <- (fun x : A, f x) OR ?m <- f.
For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used:
       ?m <- (fun x : A, f x)

When we are elaborating the axiom_of_choice theorem, we need to use the second one:
       ?m <- f

Of course, we can always provide the parameters explicitly and bypass the elaborator.
However, this goes against the idea that the elaborator can do mechanical steps for us.

This commit addresses this issue by creating a case-split
       ?m <- (fun x : A, f x)
       OR
       ?m <- f

Another solution is to implement eta-expanded normal forms in the Kernel.

With this change, we were able to cleanup the following "hacks" in kernel.lean:
     @eps_ax A (nonempty_ex_intro H) P w Hw
     @axiom_of_choice A B P H
where we had to explicitly provided the implicit arguments

This commit also improves the imitation step for Pi-terms that are actually arrows.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 13:28:54 -08:00
Leonardo de Moura
425d31f513 chore(library/simplifier): fix style warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 21:45:55 -08:00
Leonardo de Moura
cca15f1390 feat(library/simplifier): congruence theorem compilation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 21:16:23 -08:00
Leonardo de Moura
ead54bbf57 feat(library/simplifier): enforce max_steps option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 12:12:17 -08:00
Leonardo de Moura
1ccfac5873 feat(library/simplifier): conditional rewriting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 21:15:46 -08:00
Leonardo de Moura
6bcd8e3ee5 fix(library/expr_lt): use expression depth instead of size to obtain a monotonic total order on terms 
It is not incorrect to use size, but it can easily overflow due to sharing.
The following script demonstrates the problem:

local f = Const("f")
local a = Const("a")
function mk_shared(d)
   if d == 0 then
      return a
   else
      local c = mk_shared(d-1)
      return f(c, c)
   end
end
print(mk_shared(33):size())

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 17:40:49 -08:00
Leonardo de Moura
cd19d4da01 feat(library/simplifier): memoize intermediate results 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 17:03:44 -08:00
Leonardo de Moura
97ead50a3e feat(builtin/Nat): flip orientation of associativity axioms for + and * 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 15:38:00 -08:00
Leonardo de Moura
ad219d43d9 refactor(*): semantic attachment parsing and simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 14:44:45 -08:00
Leonardo de Moura
56f5657ee7 fix(library/simplifier): ordered rewriting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 13:13:16 -08:00
Leonardo de Moura
6a63ef3bc5 feat(library/expr_lt): make sure the total order on terms is monotonic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 13:07:18 -08:00
Leonardo de Moura
ac9f8f340d feat(kernel/expr): add efficient get_size() function for expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 12:28:37 -08:00
Leonardo de Moura
913d893204 feat(library/simplifier): add support for 'permutation' rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 08:29:31 -08:00
Leonardo de Moura
8e90d17a0b fix(library/hop_match): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 23:28:12 -08:00
Leonardo de Moura
69d7ee316f feat(library/simplifier): improve simplification by evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 23:26:34 -08:00
Leonardo de Moura
08053c1172 feat(library/hop_match): make the higher order pattern matcher slightly stronger 
It now can handle (?m t) where t is not a locally bound variable, but ?m and all free variables in t are assigned.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 20:35:50 -08:00
Leonardo de Moura
d322f63113 feat(frontends/lea): add commands for creating and managing rewrite rule sets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 12:03:59 -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
3bbadddc94 chore(library/simplifier): cleanup and add comments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 10:54:09 -08:00
Leonardo de Moura
7492fd5a2c feat(library/simplifier): add support for simplification by evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 10:34:55 -08:00
Leonardo de Moura
11719713ec feat(library/hop_match): optionally unfold constants when performing higher order matching 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 10:32:06 -08:00
Leonardo de Moura
39c3b17eb7 feat(library/simplifier): add support for Eta-reduction in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 00:40:35 -08:00
Leonardo de Moura
ed009f4c88 feat(kernel/simplifier): add support for Beta-reduction in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 00:40:20 -08:00
Leonardo de Moura
32c5bc25e3 refactor(library/simplifier): cleanup rewrite_rule_set, and use it in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 20:52:33 -08:00
Leonardo de Moura
466285c577 refactor(library/simplifier): rewriter_rule_set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 17:26:01 -08:00
Leonardo de Moura
feea96e84d feat(library/simplifier): add rewrite_rule_set extension for managing rewrite rules in an environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 15:43:24 -08:00
Leonardo de Moura
eae79877ae feat(library/simplifier): add rewrite_rule_set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 12:50:46 -08:00
Leonardo de Moura
27ab49ae9d feat(library/simplifier): bottom-up simplifier skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-18 12:49:41 -08:00
Leonardo de Moura
40b7ed13c2 fix(tests/lean): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-17 19:27:32 -08:00
Leonardo de Moura
534838a36c chore(build): update automatically generated files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-17 18:30:45 -08:00
Leonardo de Moura
d711ca4d1b feat(builtin/heq): add heq C++/Lean interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-17 18:30:21 -08:00
Leonardo de Moura
2434024272 fix(library/rewriter): warning in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-17 15:46:49 -08:00
Leonardo de Moura
5bee259a00 refactor(kernel): remove unnecessary universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 18:06:25 -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
4dc98bc73b refactor(builtin/kernel): use iff instead of = for Booleans 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 02:05:09 -08:00
Leonardo de Moura
d063828ff9 feat(library/kernel_bindings): expose abst_name, abst_domain and abst_body in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 00:03:16 -08:00
Leonardo de Moura
8d73fb5699 fix(library/hop_match): Lua bindings gotcha 
See http://www.luafaq.org/gotchas.html#T6.4

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 23:51:26 -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
3238c7e2a0 feat(library/simplifier): add is_permutation_ceq predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 19:53:52 -08:00
Leonardo de Moura
c73398a0b8 refactor(library/simplifier): relax rule for conditional equalities 
The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:

theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 16:06:00 -08:00
Leonardo de Moura
3daac17ea8 feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 15:30:16 -08:00
Leonardo de Moura
1176093afa refactor(library/simplifier): simplifier should only use homogeneous equalities 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 14:58:32 -08:00
Leonardo de Moura
f177c8d1ec fix(library/elaborator): missing condition 
The elaborator was failing in the following higher-order constraint

   ctx |- (?M a) = (?M b)

This constraint has solution, but the missing condition was making the elaborator to reduce this problem to

   ctx |- a = b

That does not have a solution.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 14:11:36 -08:00
Leonardo de Moura
c651d3ea2d feat(library/simplifier): filter out propositions that cannot be used as conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 12:06:27 -08:00
Leonardo de Moura
94fa987814 fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool 
The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 11:02:52 -08:00
Leonardo de Moura
28eb980484 fix(build): C++ module dependency problem, and style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 18:30:31 -08:00
Leonardo de Moura
c8e1ec87d2 feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 18:30:19 -08:00
Leonardo de Moura
7c2a4211a8 feat(kernel): expose imported predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 16:41:40 -08:00
Leonardo de Moura
07059b0531 feat(library): add if_then_else Lean/C++ interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 16:10:49 -08:00
Leonardo de Moura
8217a544cc fix(library/hop_match): bugs in the higher-order matching procedure, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 14:37:28 -08:00
Leonardo de Moura
4595c50f7e fix(library/hop_match): in locally bound variable management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 16:54:21 -08:00
Leonardo de Moura
55aa4cbfa3 feat(frontends/lean): improve error message for expressions containing unsolved metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 13:21:44 -08:00
Leonardo de Moura
7f818ecd92 feat(library): match procedure for higher-order patterns 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:45:24 -08:00
Leonardo de Moura
d4a7d796a5 feat(builtin): prove strong induction theorem, add < theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-10 18:46:33 -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
2179e57db3 refactor(builtin): move if_then_else to its own module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 14:08:39 -08:00
Leonardo de Moura
57640ecf19 fix(library/elaborator): array bounds 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 13:18:49 -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
cfe576f551 fix(library/elaborator): bug in the elaborator 
The elaborator was not handling correctly constraints of the form

    ctx |- ?m << (Pi x : A, B)
    and
    ctx |- (Pi x : A, B) << ?m

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 12:10:50 -08:00
Leonardo de Moura
abf61be8f6 chore(library/tactic): remove imp_tac, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 00:57:04 -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
8ce6266e6b feat(library/kernel_bindings): add new predicates for kernel objects in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 17:36:54 -08:00
Leonardo de Moura
d5ddb186d9 feat(library/kernel_bindings): add load method to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 14:21:24 -08:00
Leonardo de Moura
17c4cce89c fix(library/elaborator): remove_detail procedure was keeping a lot of details when typeof_mvar_justification was being used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 13:24:46 -08:00
Leonardo de Moura
4424a314e0 feat(kernel): add get_universe_distance method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 17:13:13 -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
9eb4dc4a81 feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend 
This commit affects different modules.
I used the following approach:
1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure.
2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads.

3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-03 17:18:23 -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
9620b00e24 feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. 
This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator.

For example, suppose we have the constraint

   ctx |- ?M1[inst:0 ?M2] == a

If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions:

        ?M1 == a
    or
        ?M1 == #0 and ?M2 == a

On the other hand, if ?M2 is assigned to b, then we can ignore the second case.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 16:08:38 -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
b81d3309b9 fix(kernel): remove ios hack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 13:03:25 -08:00
Leonardo de Moura
9c5fa72f56 fix(library/elaborator): avoid unused variable warning in release build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 12:40:41 -08:00
Leonardo de Moura
49425f1a5b feat(builtin/Nat): multiplication axioms and theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 21:32:07 -08:00
Leonardo de Moura
b2a8f4118d feat(library/elaborator): process ho-match before normalizing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 14:46:19 -08:00
Leonardo de Moura
7726ccad28 chore(builtin): rename nat, int and real modules to Nat, Int and Real. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 13:52:25 -08:00
Leonardo de Moura
74cae2a154 refactor(library/elaborator): remove hackish rule 
After the recent fixes, the hack in process_metavar is not needed anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 10:55:39 -08:00
Leonardo de Moura
5f29146e0b feat(library/elaborator): use is_convertible for constraints without metavariables in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:14:01 -08:00
Leonardo de Moura
cbd1f98365 fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:02:41 -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
a80fccea93 chore(*): cleanup builtin registration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 12:19:00 -08:00
Leonardo de Moura
2a2f0b0d89 refactor(kernel/builtin): move helper decl macros to a separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:51:30 -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
4401b390fe refactor(library/arith): do not load specialfn by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:25:43 -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
46a8300a2d refactor(library/arith): move real and special function declarations to .lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:02:22 -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
097b10e424 refactor(kernel/builtin): move builtin declarations to basic 
There is a lot to be done. We should do the same for Nat, Int and Real.
We also should cleanup the file builtin.cpp and builtin.h.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 22:00:03 -08:00
Leonardo de Moura
37e8738a5f refactor(kernel/expr): value deserializer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 20:47:14 -08:00
Leonardo de Moura
15621610e9 refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments 
This commit also fixes bugs in the Alias command.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 17:04:36 -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
df3686634d refactor(kernel/builtin): remove unnecessary predicates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 12:20:29 -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
aee1c6d3f3 feat(kernel): export/import (.olean) binary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-28 17:31:35 -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
f1b97b18b4 refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 15:54:53 -08:00
Leonardo de Moura
ba02132a90 feat(frontends/lean/parser): add command macros 
The idea is to allow users to define their own commands using Lua.
The builtin command Find is now written in Lua.
This commit also fixes a bug in the get_formatter() Lua API.
It also adds String arguments to macros.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 13:00:28 -08:00
Leonardo de Moura
88235d2922 feat(library/tactic/apply_tactic): try other solutions produced by the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-25 11:51:27 -08:00
Leonardo de Moura
8e45064f25 feat(library/tactic/apply_tactic): improved parametric apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 22:40:34 -08:00
Leonardo de Moura
75cf751959 feat(library/tactic/apply_tactic): allow apply_tac Lua binding to take expressions as argument 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 16:03:16 -08:00
Leonardo de Moura
6cc57cc4b5 fix(library/tactic/apply_tactic): bug in apply_tac 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 15:54:56 -08:00
Leonardo de Moura
cb95b14332 feat(library/tactic/apply_tactic): improve apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 14:23:06 -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
00e89190c2 refactor(library/cast): use .lean file instead of .cpp file to define casting library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 22:04:19 -08:00
Leonardo de Moura
3e32d9bef2 feat(library/tactic): add support for Pi's at to_proof_state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 16:40:55 -08:00
Leonardo de Moura
104bd990e1 feat(library/tactic): add normalize_tac, eval_tac and trivial_tac 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 14:10:42 -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
9128a437b8 refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 18:23:37 -08:00
Leonardo de Moura
36b2ec9abb fix(library/cast): bugs in Cast semantic attachment 
TODO: revise cast semantic attachment.
It should be axioms instead of semantic attachments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 16:16:54 -08:00
Leonardo de Moura
aebff0b4d3 fix(library/type_inferer): bug in get_range method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 14:55:07 -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
fddcdb8f40 fix(library/elaborator): bug in process_lower 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 04:13:14 -08:00
Leonardo de Moura
4d05a8b65b fix(library/tactic/apply_tactic): provide the metavar_env to instantiate, the goal is to avoid add_lift and add_inst local entries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:17:04 -08:00
Leonardo de Moura
1ed4aa391c fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality 
For homogeneous equality, arg #1 is the Type of the lhs/rhs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:14:20 -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
812c1a2960 feat(library/elaborator): only expand definitions that are not marked as hidden 
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 02:16:49 -08:00
Leonardo de Moura
cb48fbf3c4 fix(library/elaborator): missing case 
The elaborator was failing in the following scenario:
- Failing constraint of the form
     ctx |- ?m1 =:= ?m2
where
     ?m2 is assigned to ?m1,
     and ?m1 is unassigned.

has_metavar(?m2, ?m1) returns true, and a cycle is incorrectly reported.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 01:39:43 -08:00
Leonardo de Moura
3eb4de6760 fix(frontends/lean/parser): fix deadlock in macro parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 21:40:00 -08:00
Leonardo de Moura
b08c606696 fix(library/io_state): bug in the io_state Lua bindings 
This commit also includes a new test that exposes the problem.
The options in the io_state object were being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 16:39:42 -08:00
Leonardo de Moura
ad3f771b1d feat(frontends/lean): hide 'explicit' version of objects with implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 13:12:39 -08:00
Leonardo de Moura
02bd166793 chore(library/basic_thms): fix typo in comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 12:22:05 -08:00
Leonardo de Moura
79fa6e4940 feat(frontends/lean): Scopes in the default Lean frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 17:40:21 -08:00
Leonardo de Moura
47c7bb1bde refactor(*): uses aliases for unordered_map and unordered_set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 12:30:45 -08:00
Leonardo de Moura
1e4fa76a47 feat(util/name_map): add template alias 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 11:34:40 -08:00
Leonardo de Moura
418623b874 feat(kernel/replace_fn): add template replace that captures commonly used pattern 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 18:31:59 -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
84bfe2a222 fix(library/elaborator): bug in process_meta_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 10:56:20 -08:00
Leonardo de Moura
09b51a0fb7 fix(library/elaborator): missing condition 
The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 17:13:36 -08:00
Leonardo de Moura
91f4ced83b feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 16:41:20 -08:00
Leonardo de Moura
7792561b20 fix(library/type_inferer): another incorrect use of scoped_map 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 15:17:19 -08:00
Leonardo de Moura
2fee2def72 feat(library/basic_thms): simplify DoubleNegElim 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 13:19:19 -08:00
Leonardo de Moura
de53e92de8 feat(library/basic_thms): add ExistsElim theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 12:43:34 -08:00
Leonardo de Moura
8f5c2b7d9f feat(library/basic_thms): add Refute theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 12:03:31 -08:00
Leonardo de Moura
8f9405c8b3 fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive 
This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 09:39:02 -08:00
Leonardo de Moura
61bd27ff06 fix(library/elaborator): bug in simple_ho_match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 21:48:55 -08:00
Leonardo de Moura
19ad39159e feat(library/basic_thms): add ForallIntro theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 17:35:31 -08:00
Leonardo de Moura
82dfb553d5 feat(library/basic_thms): add ExistsIntro theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 16:26:23 -08:00
Leonardo de Moura
993bea8206 refactor(library/elaborator): improve elaborator state data-structure 
The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:27:08 -08:00
Leonardo de Moura
bdbf85405a feat(library/elaborator): add extra occurs-check test 
The idea is to catch the inconsistency in constraints such as:

    ctx |- ?m[inst:0 v] == fun x, ?m a x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 19:47:33 -08:00
Leonardo de Moura
160a8379ef feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed 
The modifications started at commit 1852c86948 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:

[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a

After the changes, only very simple constraints are generated. The most complicated one is:

[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:59:35 -08:00
Leonardo de Moura
70b7e519f8 feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:54:49 -08:00
Leonardo de Moura
02ee31b786 feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:41:50 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' 
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 12:25:00 -08:00
Leonardo de Moura
51aee83b70 refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env 
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.

example showing that the approach for caching metavar_env is broken in the type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 18:59:15 -08:00
Leonardo de Moura
2e5e5e187f chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 15:01:24 -08:00
Leonardo de Moura
450d6a4b1e refactor(util/splay_tree): replace find with splay_find 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:27:30 -08:00
Leonardo de Moura
f97c260b0b refactor(kernel/environment): add ro_environment 
The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
       void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
       environment rw_env(env);
Now, f can use rw_env to update env.

To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.

ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:34 -08:00
Leonardo de Moura
3457fe5935 chore(kernel): rename read_only_environment and read_write_environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
f728f80960 fix(library/elaborator): remove is_neutral_abstraction hack, and bug at process_metavar_lift_abstraction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:41:24 -08:00
Leonardo de Moura
8f67348c05 fix(library/elaborator): remove nasty hack, this hack was throwing away the local context at process_meta_app_core 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:27:21 -08:00
Leonardo de Moura
c29b155fdd feat(library/elaborator): use improved has_free_vars in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 16:15:20 -08:00
Leonardo de Moura
1d33d3b5db fix(library/elaborator): the context of auxiliary metavariables created in the imitation step was incorrect 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 12:35:32 -08:00
Leonardo de Moura
55389cf6e5 feat(kernel/context): add find, a version of lookup that does not throw an exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 09:54:54 -08:00
Leonardo de Moura
f8e87436a7 perf(library/elaborator): avoid exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:40:59 -08:00
Leonardo de Moura
4de5f06a97 fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:26:58 -08:00
Leonardo de Moura
5ae71e75bd perf(library/elaborator): avoid exception 
Lean was spending 17% on the runtime "throwing exceptions" in the test tests/lean/implicit7.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 16:31:36 -08:00
Leonardo de Moura
1fb526a3d4 perf(library/type_inferer): improve is_proposition performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 16:18:45 -08:00
Leonardo de Moura
b270fb0030 refactor(library/elaborator): remove synthesizer 
Synthesizer is not part of the elaborator anymore.
The elaborator fills the "easy" holes.
The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 15:55:54 -08:00
Leonardo de Moura
c0b9c7ffc4 refactor(library/io_state): simplify regular/diagnostic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 13:09:35 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency 
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:20:26 -08:00
Leonardo de Moura
445d4f6793 refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 18:11:35 -08:00
Leonardo de Moura
2a80807fef refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:33:18 -08:00
Leonardo de Moura
340d643d89 fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 16:55:55 -08:00
Leonardo de Moura
8add5571f1 refactor(library/tactic): remove 'null' tactic, and operator bool tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:00:16 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 14:37:38 -08:00
Leonardo de Moura
2f88d6710c feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr> 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 10:34:38 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression 
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 23:21:10 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system 
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:11:55 -08:00
Leonardo de Moura
195ea24d71 refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer 
The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 10:27:11 -08:00
Leonardo de Moura
5f3b9dbbbd fix(library/fo_unify): unify (?f ?x) with (g a b) 
We flat applications. So, (g a b) is actually ((g a) b).
So, we must be able to unify (?f ?x) with (g a b).
Solution:
        ?g <- (g a)
        ?x <- b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 10:25:11 -08:00
Leonardo de Moura
015bff8283 fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term 
This commit fixes a problem exposed by t13.lean.
It has a theorem of the form:

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form

 [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A

The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type).
Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions.
Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created
     A : Bool, B : Bool, assumption : A /\ B |- B /\ A
That is, the lemmas are not available when solving B /\ A.
Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used.

    Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
            let lemma1 := Conjunct1 assumption,
                lemma2 := Conjunct2 assumption
            in Conj (Conjunct2 assumption) (Conjunct1 assumption)

This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal
     A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A

After this commit, the proof for theorem T1 is

Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
    let lemma1 := Conjunct1 assumption,
        lemma2 := Conjunct2 assumption
    in Conj lemma2 lemma1

as expected.

Finally, this example suggests that the encoding

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 : A := (by auto),
              lemma2 : B := (by auto)
          in (show B /\ A by auto)

is more efficient than

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:14:25 -08:00
Leonardo de Moura
bd9df3b08f fix(library/tactic/goal): null hypothesis being added by to_goal 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:03:06 -08:00
Leonardo de Moura
0390f3c39b feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 15:01:54 -08:00
Leonardo de Moura
1df9d18891 feat(frontends/lean): allow 'tactic hints' to be associated with 'holes' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 14:49:39 -08:00
Leonardo de Moura
d79a626523 fix(kernel/type_checker): Pi with metavariables case 
The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 13:07:59 -08:00
Leonardo de Moura
fa03ae2a26 fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints 
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 13:04:34 -08:00
Leonardo de Moura
c841763a05 feat(library/elaborator): add special treatment for constraints of the form ?m[inst:i v] << t, where t is a proposition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 04:51:07 -08:00
Leonardo de Moura
13f9454fe1 feat(library/tactic/proof_state): add option tactic::proof_state::goal_names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 21:18:22 -08:00
Leonardo de Moura
0c059a9917 feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 20:06:32 -08:00
Leonardo de Moura
c1afefb873 feat(library/fo_unify): unify heterogeneous - homogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 19:00:31 -08:00
Leonardo de Moura
a1b5a8e50f fix(frontends/lean): check wheter the synthesized proof term has metavars or not 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 14:22:19 -08:00
Leonardo de Moura
43ef8b9a4b refactor(library/tactic): rename boolean.* to boolean_tactics.* 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 05:03:18 -08:00
Leonardo de Moura
fa98c1358f feat(library/tactic): add disj_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 04:49:06 -08:00
Leonardo de Moura
029ef57abd feat(library/tactic): add apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 03:22:12 -08:00
Leonardo de Moura
ef069e39b0 chore(*): replace to_expr with to_nonnull_expr (when appropriate) 
The goal is to make the Lua API more robust.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:53:53 -08:00
Leonardo de Moura
bcc8b67592 chore(*): consistent file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:40:52 -08:00
Leonardo de Moura
8e53643b61 feat(library/fo_unify): first order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:21:21 -08:00
Leonardo de Moura
f80106a895 chore(*): use 'explicit operator bool' everywhere. 
operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 23:02:45 -08:00
Leonardo de Moura
d79b2babd3 fix(*): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 08:46:47 -08:00
Leonardo de Moura
25978118df feat(library/tactic): add beta-reduction tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 08:10:51 -08:00
Soonho Kong
a2d6918348 fix(library/rewriter): use Abst axiom in lambda_body RW 2013-12-01 22:24:12 -05:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space 
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 17:19:27 -08:00
Leonardo de Moura
09f98ecddc feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:41:05 -08:00
Leonardo de Moura
70e06f8e86 feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:27:27 -08:00
Leonardo de Moura
ca53a5a1cc feat(library/tactic): add unfold tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 08:51:56 -08:00
Leonardo de Moura
568931ccb1 refactor(library/tactic): remove duplicate code, add add_proofs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:01 -08:00
Leonardo de Moura
f91c4901e8 feat(library/tactic): add absurd_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:00 -08:00
Leonardo de Moura
bf2adb20e7 feat(library/tactic): add disj_hyp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:00 -08:00
Soonho Kong
064e3fe20d refactor(library/rewriter): rename lc => ti 2013-12-01 01:59:20 -05:00
Soonho Kong
506cca0ac1 feat(library/rewriter): implement depth RW 2013-12-01 01:59:20 -05:00
Soonho Kong
ae0508128f refactor(library/rewriter): move apply_rewriter_fn into rewriter.h 2013-12-01 00:57:09 -05:00
Soonho Kong
d7ba5e3893 doc(library/rewriter): add doxygen annotations for rewrite_* funcs 2013-12-01 00:47:53 -05:00
Leonardo de Moura
1a221d8bbe feat(library/tactic): add focus tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Soonho Kong
f205dd0763 fix(library/rewriter): unused variable warnings 2013-11-30 07:05:18 -05:00
Leonardo de Moura
83aaf64318 fix(library/tactic): memory leaks 
Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.

To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:44:39 -08:00
Leonardo de Moura
a7027a1d00 feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:16:39 -08:00
Soonho Kong
f5f7380fbe feat(library/rewriter): add apply_rewriter_fn which will be used in depth RW 2013-11-30 02:25:30 -05:00
Soonho Kong
1d76a6f71d feat(library/rewriter): add rewrite_* functions 
rewrite_* functions take the rewriting results of the sub-components and
construct the rewriting result for the main component.

For instance, rewrite_app function takes env, ctx, and the value v s.t.

v = (e_0 e_1 ... e_n)

and the rewriting results for e_i's as a vector(buffer)

(e'_0, pf_0 -- proof of e_0 = e'_0)
(e'_1, pf_1 -- proof of e_1 = e'_1)
...
(e'_n, pf_n -- proof of e_n = e'_n).

Then rewrite_app function construct the new v'

v' = (e'_0 e'_1 ... e'_n)

and the proof of v = v' which is constructed with pf_i's.

These functions are used in the component rewriters such as app_RW and
let_type_RW, as well as more complicated rewriters such as depth
rewriter.
 2013-11-30 02:25:29 -05:00
Leonardo de Moura
a9eb2a9307 feat(kernel/builtin): add is_* functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 11:35:58 -08:00
Leonardo de Moura
18eb9e427f fix(library/tactic): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 10:35:14 -08:00
Leonardo de Moura
f9874cd675 feat(library/tactic): add to_tactic_ext, it allows functions that return tactics to be used where a tactic is expected 
For example, after this commit, we can write

simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic

instead of

simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 09:40:21 -08:00
Leonardo de Moura
20a36e98ec feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. 
Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.

For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))

Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:

[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

Now, ?M::1 is assigned to the term
     if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

This is bad, since the original structure was lost.

This commit also contains an example that only works after the commit is applied.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 09:15:01 -08:00
Leonardo de Moura
066dacea31 feat(library/tactic): add show_tactic, and optional '.' in the end of tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 01:33:26 -08:00
Leonardo de Moura
b3f87e2e4f feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 22:11:07 -08:00
Leonardo de Moura
67def8da21 fix(library/type_inferer): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:47:29 -08:00
Leonardo de Moura
dae86c2ffa feat(frontends/lean/parser): add basic tactic support in the frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:08:12 -08:00
Leonardo de Moura
73bbf67702 refactor(library/elaborator): simplify synthesizer interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 19:00:48 -08:00
Leonardo de Moura
c6b05bcfcb feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 18:23:38 -08:00
Leonardo de Moura
e3f3ec5553 feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 18:17:15 -08:00
Leonardo de Moura
d36a91e145 feat(library/tactic): expose COND and WHEN tacticals in Lua, add HOL-like tactical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 17:57:24 -08:00
Leonardo de Moura
ff052d41ee chore(*): fix cygwin compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:49:18 -08:00
Leonardo de Moura
ce674d2d43 feat(library/tactic): execute Lua tactics using coroutines 
This is very important when several Lua tactics are implemented in the
same Lua State object.  In this case, even if we use the par
combinator, a Lua tactic will block the other Lua tactics running in
the same Lua State object.

With this commit, a Lua tactic can use yield to allow other tactics
in the same State object to execute.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:09:33 -08:00
Leonardo de Moura
09bc7ddf91 feat(library/tactic): add support for migratic tactic framework object between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 08:03:05 -08:00
Leonardo de Moura
3dc7a856f0 refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 18:11:46 -08:00
Leonardo de Moura
b4a8418d38 feat(library/tactic): expose tactics in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 17:47:29 -08:00
Leonardo de Moura
f7e8545e97 refactor(frontends/lua): rename leanlua_state to script_state, and move it to util 
This commit also minimizes the dependencies of script_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 14:57:36 -08:00
Leonardo de Moura
d87ad9eb7e refactor(util/lua): propagate C++ Lean exceptions in Lua 
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 12:25:29 -08:00
Leonardo de Moura
a6f6f49b5f refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular 
copy_values is not a big if-then-else anymore.
Before this change, whenever we added a new kind of userdata, we would have to update copy_values.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 10:32:19 -08:00
Leonardo de Moura
956f203a55 refactor(bindings/lua): move Lua bindings to the file associated with them 
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:15:56 -08:00
Leonardo de Moura
4e66a2e14a fix(library/tactic/goal): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:58 -08:00
Leonardo de Moura
b41789d085 feat(kernel): add is_bool predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:50 -08:00
Leonardo de Moura
c22f863114 refactor(library/tactic): improve solve method 
Now, it produces the following outcomes:
1- A proof
2- A counterexample
3- A list of (unsolved) final states

Remark: the solve method does not check whether the proof or counterexample is correct.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 13:04:12 -08:00
Leonardo de Moura
9a8ea0c735 feat(library/tactic): add precision and counterexample builder to proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 11:43:16 -08:00
Leonardo de Moura
ccaa272f9a refactor(library/tactic): simplify proof_builder API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:50:33 -08:00
Leonardo de Moura
500ed7a05b refactor(library/tactic): remove dead code, make proof_state a smart pointer, cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:39:40 -08:00
Leonardo de Moura
2c65fdb346 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 01:06:34 -08:00
Leonardo de Moura
9dcfa03dd2 feat(library/tactic): add conj_hyp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 21:00:38 -08:00
Leonardo de Moura
d75bd2ae98 feat(library/tactic/proof_state): remove goal name when pretty printing the proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 20:22:47 -08:00
Leonardo de Moura
48d7afb0e8 feat(library/tactic): add trace_state_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:44:02 -08:00
Leonardo de Moura
6f05276acd refactor(library/tactic): remove unnecessary tactic_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:31:49 -08:00
Leonardo de Moura
9c42a05b08 feat(library/tactic): add conj_tactic and imp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:29:04 -08:00
Leonardo de Moura
1c607f3350 feat(library/tactic): add cond and when tacticals. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 12:04:32 -08:00
Leonardo de Moura
40d612eca0 feat(library/tactic): add repeat1 and determ tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:38:51 -08:00
Leonardo de Moura
cb7a5288c5 refactor(library/tactic): minimize the amount of copying in the tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:27:06 -08:00
Leonardo de Moura
22c49146ae feat(library/tactic): refine repeat and repeat_at_most tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:18:32 -08:00
Leonardo de Moura
e839787b74 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 00:38:52 -08:00
Leonardo de Moura
40a2f0a588 refactor(util/lazy_list): polish lazy_list API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:45:01 -08:00
Leonardo de Moura
9da95dc6e6 style(library/tactic): missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:06:00 -08:00
Leonardo de Moura
16cf60a04b refactor(library/tactic): modify par and try_for tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:03:59 -08:00
Leonardo de Moura
d1adfd52e6 feat(library/tactic): add mk_simple_tactic template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:53:45 -08:00
Leonardo de Moura
f19944cf09 refactor(util/lazy_list): 'lazier' lazy_lists 
In the new implementation, even the head of the lazy list is computed on demand.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:33:30 -08:00
Leonardo de Moura
18d114416f feat(library/tactic): add take and force tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 17:05:18 -08:00
Leonardo de Moura
d258a4b7b8 feat(library/tactic): add repeat and repeat_at_most tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 16:39:25 -08:00
Leonardo de Moura
8bece1b53d feat(library/tactic): add append, interleave and par tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 16:15:03 -08:00
Leonardo de Moura
df96068caa fix(library/tactic): clean up try_for 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 15:51:17 -08:00
Leonardo de Moura
9fd594533d refactor(library/tactic): simplify tactic framework, add orelse and try_for combinators/tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 15:46:43 -08:00
Leonardo de Moura
796fb3c3bf refactor(library/tactic): remove justification_builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
41062fdf9f feat(library/tactic): add pretty printer for goal and proof_state objects, add solve method for tactics, add trivial example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
5346b67651 refactor(library/state): rename Lean state object to io_state 
The idea is to make it clear that io_state is distinguish it from proof_state, and from leanlua_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
680ec8abba refactor(library/tactic): reorganize tactic API, add assumption_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
63bbf07f64 feat(library/tactic): add 'idtac' tactic and 'then' tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
a03841c18b feat(tactic): refine tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
367108edfa fix(library/tactic): compilation problem reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 08:53:37 -08:00
Leonardo de Moura
f6d1f4db60 chore(library/tactic): remove trash 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 17:25:00 -08:00
Leonardo de Moura
3a6aa2dc75 feat(library/tactic): add tactic framework APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 17:19:05 -08:00
Leonardo de Moura
7f088b7635 feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework 
This field should not be visible in the external API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 11:21:52 -08:00
Leonardo de Moura
69be5f6c94 feat(kernel/environment): track which modules were already imported 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 18:15:44 -08:00
Leonardo de Moura
590b14570f feat(lua): improve error handling in Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 18:21:42 -08:00
Leonardo de Moura
19533c811b feat(library/script_evaluator): add abstract class that exposes only the API needed by frontend objects 
The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua.
This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 12:13:09 -08:00
Leonardo de Moura
8e56726116 fix(library/expr_lt): fix bug when using hash codes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:18:33 -08:00
Leonardo de Moura
691893258d feat(kernel/expr): add hash code based on allocation time 
The new hash code has the property that given expr_cell * c1 and expr_cell * c2,
if c1 != c2 then there is a high propbability that c1->hash_alloc() != c2->hash_alloc().

The structural hash code hash() does not have this property because we may have
c1 != c2, but c1 and c2 are structurally equal.

The new hash code is only compatible with pointer equality.
By compatible we mean, if c1 == c2, then c1->hash_alloc() == c2->hash_alloc().
This property is obvious because hash_alloc() does not have side-effects.

The test tests/lua/big.lua exposes the problem fixed by this commit.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 02:43:11 -08:00
Leonardo de Moura
c4c548dc5d feat(*): simplify interrupt propagation 
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.

The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:

    try-for (T1 ORELSE T2) 5

It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 21:45:48 -08:00
Leonardo de Moura
31abc00db8 chore(*): add LCOV_EXCL_LINE to lean_unreachable statements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 09:19:38 -08:00
Leonardo de Moura
3078923ea4 fix(kernel/type_checker): add missing test, and kernel_exception has_no_type_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Soonho Kong
044813615e fix: add '#include <tuple>' 2013-11-03 13:00:42 -05:00
Leonardo de Moura
96dcd003c6 fix(frontends/lean/parser): associated position with 'type' placeholder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-31 16:27:36 -07:00
Leonardo de Moura
aa99ac6618 feat(kernel/value): allow semantic attachments to use coercions when being pretty printed 
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-30 11:42:26 -07:00
Leonardo de Moura
7fc87faa8f feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 17:07:30 -07:00
Leonardo de Moura
577ca128a1 fix(library/elaborator): add missing conflict justification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 03:01:17 -07:00
Leonardo de Moura
7c8daf8974 fix(kernel/metavar): make sure the justification and substitution are always matching each other 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225 fix(kernel/normalizer): do not apply substitutions in the normalizer 
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 02:14:48 -07:00
Leonardo de Moura
b16a64f44b fix(library/elaborator): missing normalization step for semantic attachments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-28 07:42:14 -07:00
Leonardo de Moura
4564bfa1d3 feat(library/elaborator): improve simple_ho_match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-27 11:17:03 -07:00
Leonardo de Moura
dbefc91151 fix(kernel/metavar): add normalize assignment justification 
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-27 11:02:34 -07:00
Leonardo de Moura
92f5a31976 feat(kernel/expr): add new mk_app template for creating applications using a collection 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-27 08:53:58 -07:00
Leonardo de Moura
eaccdcb558 refactor(assumption_justification): move to the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-26 14:21:29 -07:00
Leonardo de Moura
c53d559f7f perf(library/elaborator): improve process_metavar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 11:19:17 -07:00
Leonardo de Moura
a5c3829d1b feat(kernel): add unexpected_metavar_occurrence exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:56:44 -07:00
Leonardo de Moura
83907d7c73 fix(elaborator): max constraints 
elaborator was not handling max constraints where one of the arguments was a Bool. Example:
      ctx |- max(Bool, Type) == ?M

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:27:57 -07:00
Leonardo de Moura
e3efe39eeb fix(elaborator): fix bug in higher-order matching/unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 17:53:37 -07:00
Leonardo de Moura
872b698bc3 feat(elaborator): add option m_assume_injectivity for getting more concise solutions 
We may miss solutions, but the solutions found are much more readable.
For example, without this option, for elaboration problem

Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
    DisjCases H
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
                   in CongrH AeqC (Symm AeqC))
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
                   in CongrH AeqC (Symm AeqC))

the elaborator generates

Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
    DisjCases
        H
        (λ H1 : if
               Bool
               (if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤)
               ⊥
               ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
        (λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))

The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 16:47:50 -07:00
Leonardo de Moura
d2f9c24d3c fix(tests/lean): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:42:17 -07:00
Leonardo de Moura
bbc265ded4 feat(frontends/lean): hook new elaborator in the default frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:14:29 -07:00
Leonardo de Moura
434c33f225 feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda 
This feature is useful for problems that require higher-order matching and/or unification.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:35:50 -07:00
Leonardo de Moura
f1e0d6ec29 refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:44:26 -07:00
Leonardo de Moura
c1e451151a feat(replace_visitor): add an abstract class for applying transformations on expressions 
I also removed replace_using_ctx since it is subsumed by the new class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:01:37 -07:00
Leonardo de Moura
13531b7d3e refactor(kernel): rename trace to justification 
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:42:17 -07:00
Leonardo de Moura
8e1a75ce1c feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:09:13 -07:00
Leonardo de Moura
172567a2fb feat(elaborator): add support for upper bounds, max constraints, and fix bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:01:39 -07:00
Leonardo de Moura
c635c16637 refactor(ho_unifier): remove ho_unifier, it has been subsumed by the elaborator class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:51:54 -07:00
Leonardo de Moura
019f64671b fix(elaborator): add basic support for flex-flex pairs, add more tests, fix bug when enumerating different solutions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:49:37 -07:00
Leonardo de Moura
7ad256131e feat(elaborator): add support for constraints of the form ?m[inst, ...] == t, fix bugs, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:39:22 -07:00
Leonardo de Moura
3fa4eac4ef fix(replace_using_ctx_fn): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:46:11 -07:00
Leonardo de Moura
8142726923 fix(type_inferer): bug when inferring the type of free variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:41:22 -07:00
Leonardo de Moura
874f67c605 feat(normalizer): remove normalization rule t == t ==> true 
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:

Theorem Th : a = a := Refl b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 14:02:48 -07:00
Leonardo de Moura
a5b4908f71 fix(elaborator): process_simple_ho_match and missing cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:04 -07:00
Leonardo de Moura
cb2c73cf37 feat(elaborator): add higher-order matching support to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 11:22:00 -07:00
Leonardo de Moura
f4592da87f feat(elaborator): solve more unification constraints, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
dc51d35dc0 feat(library/type_inferer): add support for metavariables at type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
7f96c07a01 refactor(library): rename light_checker to type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
dc0e7a4472 feat(pos_info_provider): add position information provider for expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
b1b49e86e7 test(elaborator): add simple test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00