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

2410 commits

Author SHA1 Message Date
Leonardo de Moura
2daad71d47 fix(kernel/type_checker): memory access violation, closures (for printing error messages) had a uninteded reference to the type_checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 08:59:32 -07:00
Leonardo de Moura
39e101d323 feat(kernel/formatter): improve simple printer support for Pi and lambda 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 08:16:32 -07:00
Leonardo de Moura
28b70b4e04 feat(kernel/inductive): use nondependent elimination when the datatype is in Bool/Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 15:39:48 -07:00
Leonardo de Moura
45252e2229 feat(kernel/inductive): add eliminator/recursor for inductive datatype declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 14:17:57 -07:00
Leonardo de Moura
f826e98196 feat(kernel/formatter): avoid hierarchical names when printing local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:50:29 -07:00
Leonardo de Moura
405b24861c feat(util/name): add methods append_after and append_before 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:49:24 -07:00
Leonardo de Moura
7bf0011905 feat(kernel/expr): add additional template for mk_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:15:58 -07:00
Leonardo de Moura
08aa4afb3e feat(kernel/abstract): add more Pi functions for simplifying the creation Pi-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-18 13:15:00 -07:00
Leonardo de Moura
950d69b977 test(lua): add tests for exercising datatype validation code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 20:10:45 -07:00
Leonardo de Moura
ff3a7bd734 fix(kernel/type_checker): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:21:09 -07:00
Leonardo de Moura
8fcb84c8f2 feat(kernel/inductive): finish inductive datatype declaration validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:19:32 -07:00
Leonardo de Moura
5c7d3c79c4 feat(kernel/expr): improve get_app_args interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:19:10 -07:00
Leonardo de Moura
28e8299f6d feat(kernel/type_checker): add swap method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:18:46 -07:00
Leonardo de Moura
4325b126d4 feat(util/list): add map2 for list<T1> -> list<T2>, where T1 and T2 may be different, we still keep map because compiler can automatically infer all template arguments, this is not the case for map2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 19:18:18 -07:00
Leonardo de Moura
f818c1a63e feat(kernel/inductive): add more inductive datatype validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 14:47:06 -07:00
Leonardo de Moura
d03e35aaac feat(kernel/inductive): add datatype and introduction rules declarations to environment, and fix tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:59:06 -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
18a17cd48b feat(kernel/level): add is_geq predicate, we need it for implementing the inductive datatype validation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 13:39:54 -07:00
Leonardo de Moura
4348d5e63f refactor(kernel): remove unnecessary module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 12:35:41 -07:00
Leonardo de Moura
a85a6b685b feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 12:30:03 -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
aafdd98acb refactor(kernel): remove telescope type, and procedures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:51:40 -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
ace5dee63d feat(kernel/inductive): add getters for inductive decls 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 17:47:37 -07:00
Leonardo de Moura
6dedb480ec fix(kernel/abstract): bug in abstract for telescopes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 17:47:04 -07:00
Leonardo de Moura
e6c52d17a6 fix(kernel/expr): memory leak introduced today 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 16:21:31 -07:00
Leonardo de Moura
7d76278506 fix(kernel/abstract): compilation warnining 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 15:39:19 -07:00
Leonardo de Moura
a0abbf7662 feat(kernel/formatter): make simple_formatter display Type instead of Bool if impredicativity is disabled 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 15:31:19 -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
28329a55b0 feat(util/name): use '.' instead of '::' as hierarchical name separator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 12:35:43 -07:00
Leonardo de Moura
91a1b62b9e feat(kernel): add telescope abstract procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:56:44 -07:00
Leonardo de Moura
9a689ab0c3 feat(kernel): add telescope instantiate procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:56:20 -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
eb0abf557d feat(kernel/inductive): add inductive datatype kernel extension module interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 09:53:51 -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
e79e0302d0 fix(frontends/lean): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 16:09:21 -07:00
Leonardo de Moura
391b2fe739 refactor(builtin): remove old library, we will build a new one for Lean 0.2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 15:56:28 -07:00
Leonardo de Moura
c6af56260e refactor(frontends/lean): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 15:51:41 -07:00
Leonardo de Moura
16553e77fa fix(kernel/type_checker): avoid assertion violation due to API misuse 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 14:17:34 -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
7c0cc3111a fix(kernel/type_checker): we must use different caches for infer_type and check 
The new test tc4.lua exposes the problem being fixed.
We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
687639a599 fix[kernel/justification.cpp]: style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
494874fbab fix(kernel/type_checker): trust level test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -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
830537a58b feat(kernel/justification): add function for creating simple justification objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
d58b8a8102 refactor(kernel): move delayed_justification to justification.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
84c1cf9600 feat(kernel/kernel_exception): add new auxiliary functions for throwing kernel exceptions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
3a19d9fee1 refactor(kernel): revise macro_definition API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
6d30141a31 fix(kernel/formatter): remove unnecessary parenthesis 
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
08ac9c1f05 feat(kernel): add is_def_eq predicate in the extension_context API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
a6dc6060e2 fix(kernel/formatter): typo 
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
606e6226c2 fix(kernel/type_checker): the type checker cache was not taking into account binder information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:14:57 -07:00
Leonardo de Moura
d5184a1751 feat(kernel/formatter): print binder_info in simple formater 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 16:51:49 -07:00
Leonardo de Moura
5d61d23bf6 refactor(kernel): move mk_tele_pi to expr.h, and rename it mk_pi 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 16:24:55 -07:00
Leonardo de Moura
9c5dfc387b refactor(kernel/replace_visitor): remove context from replace_visitor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 15:53:09 -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
893e4d4ae2 fix(kernel/expr): bug in m_free_var_range let-expr field 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:28:47 -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
cf55a1bcc2 fix(kernel/type_checker): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 10:35:42 -07:00
Leonardo de Moura
277e0e6d49 feat(kernel/formatter): prefix metavars with '?' and local vars with '!' in the simple formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 10:16:54 -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
a8124b41d0 feat(util/name): expose is_list_name function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 09:44:58 -07:00
Leonardo de Moura
01eda46b69 feat(util/trie): add for_each and display methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 18:23:27 -07:00
Leonardo de Moura
bfa6193bfe feat(util/trie): add merge method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 17:59:20 -07:00
Leonardo de Moura
479685cb97 feat(util): add basic trie datastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 17:40:33 -07:00
Leonardo de Moura
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
7b15e558a2 refactor(kernel/converter): implement eta in whnf instead of is_def_eq. 
Without cumulativity, we do not have problems with Eta at whnf anymore.
When we had cumulativity, we could not not simply reduce
     (fun x : A, f x) ==> f
This step is correct only if domain(f) was definitionally equal to f.
Here is a problematic example for systems with cumulativity
Given, f : Type.{2} -> Bool
     (fun x : Type.{1}, f x)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 17:49:53 -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
3bc83fae56 refactor(kernel/type_checker): remove trace capability, we get it for free with tags 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:38:53 -07:00
Leonardo de Moura
2593f65ce1 feat(kernel): add tag to kernel expressions 
Frontends can used tags to associate expressions with line number information.
The update_* procedures automatically propagate tags.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:33:25 -07:00
Leonardo de Moura
3196cd19dc chore(util/thread): add atomic_uint type 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:14:31 -07:00
Leonardo de Moura
2e753e2cc0 fix(kernel/error_msgs): application type mismatch error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:49:42 -07:00
Leonardo de Moura
b18263a014 feat(kernel/formatter): adjust simple formatter to the new convention for displaying universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:42:01 -07:00
Leonardo de Moura
d4922daedf fix(kernel/level): add missing LEAN_THREAD_LOCAL directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:39:37 -07:00
Leonardo de Moura
a8a6bb1b7f fix(kernel/level): bug in get_undef_global 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:34:24 -07:00
Leonardo de Moura
89d6a1e691 fix(kernel/type_checker): check for undefined global/local levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:23:04 -07:00
Leonardo de Moura
b6d6df161f fix(kernel/level): bug in get_undef_param 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 14:22:23 -07:00
Leonardo de Moura
ad2b1d0d91 chore(util/lua_list): improve error message in table_to_list aux function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 12:58:10 -07:00
Leonardo de Moura
1244a951f2 fix(kernel/type_checker): add missing test: number of universe level parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 12:57:27 -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
0eaf1bb2cf fix(util/lua_named_param): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 12:21:48 -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
7176181b42 refactor(kernel/converter): cleanup and remove universe cumulativity support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:43:11 -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
d4400d6135 refactor(library/kernel_bindings): remove level_cnstrs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:16:51 -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
23ed003389 refactor(kernel): remove diff_cnstrs module 
We don't need them anymore. We will drop universe cumulativity from the kernel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 19:58:25 -07:00
Leonardo de Moura
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
6493ff5388 fix(kernel/formatter): print level parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 19:50:04 -07:00
Leonardo de Moura
813eba6b3a chore(build): add Lua thread tests to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:53:36 -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
bc1a91496a feat(util/lua_list): allow Lua list objects to be moved between states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:49:27 -07:00
Leonardo de Moura
fca65a9d69 fix(kernel/environment): is_descendant optimization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:48:25 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:08:32 -07:00
Leonardo de Moura
5a7f181efc feat(util/name_set): improve name_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 17:17:00 -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
1e4c5f1761 feat(util/lua_named_param): add new functions for handling named parameters in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 14:12:15 -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
1a8d75c4f0 feat(util): name_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 18:32:53 -07:00
Leonardo de Moura
7fe61bc69c feat(util): name_generator Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:28:11 -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
db39458c30 fix(kernel/level): predicate is_param_core 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:22:08 -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
9c760132e2 feat(kernel): add global levels to environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:07:31 -07:00
Leonardo de Moura
208384b5b6 fix(util/rb_tree): missing const 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 14:07:15 -07:00
Leonardo de Moura
2424cf7ece fix(kernel/expr): old comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 13:07:17 -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
f568ed97b8 feat(util/lua): add functions for simulating python-like named arguments using Lua tables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:41:33 -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
b928f313d3 feat(util): add macro for exposing the type std::pair<T1, T2> in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 16:30:17 -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
91069c5f7f feat(util/list_lua): add length method to list Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:37:15 -07:00
Leonardo de Moura
107f139764 fix(util/list_lua): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:33:49 -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
e4f69bd780 fix(kernel/justification): bug in depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:15:01 -07:00
Leonardo de Moura
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
50089dc64e feat(kernel/error_msgs): expose pp_indent_expr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:03:12 -07:00
Soonho Kong
468abb72b8 tests(util/rb_tree): wrap tst6 with #if !defined 2014-05-02 01:39:13 -04: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
65486b2dec refactor(kernel/expr): add macro_definition smart pointer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:05:46 -07:00
Leonardo de Moura
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
0bc101ac28 fix(kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:28:34 -07:00
Leonardo de Moura
739f98b642 fix(util/script_state): deadlock 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 14:10:57 -07:00
Leonardo de Moura
ddd980aa63 fix(kernel/level): warning messages when compiling in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 13:06:00 -07:00
Leonardo de Moura
120c24319e fix(tests/kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:58:09 -07:00
Leonardo de Moura
027614cebb fix(kernel/metavar): wierd memory leak that only happens when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:55:55 -07:00
Leonardo de Moura
9452d164ec feat(util/script_state): use recursive_mutex instead of mutex 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:27:12 -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
6fb7039746 refactor(kernel): use structural hashing in type_checker and converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:41:53 -07:00
Leonardo de Moura
a5ae4b6570 feat(kernel): add binder annotations (implicit, cast) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:35:02 -07:00
Leonardo de Moura
2b97474958 test(util/rb_tree): reduce test time for rb_tree 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:08:18 -07:00
Leonardo de Moura
b0e0e82350 refactor(kernel): separate type_checker and converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 18:42:01 -07:00
Leonardo de Moura
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
dbf327bad9 feat(util): expose list<name> in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 16:32:10 -07:00
Leonardo de Moura
03a32dcc77 feat(util): add macro for exposing the type list<T> in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 16:31:44 -07:00
Leonardo de Moura
aba5b65319 feat(util/lua): add macro pushnil 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 10:29:08 -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
097f562016 refactor(*): add pushinteger and pushnumeral inline functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 14:47:08 -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
a6116e3156 test(lua): reactivate some of the Lua unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 10:36:57 -07:00
Leonardo de Moura
49e626a0e0 refactor(kernel/metavar): switch to functional substitution datastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 10:22:36 -07:00
Leonardo de Moura
af927ecb7a refactor(frontends/lua): reactivate some of the Lua extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 17:57:39 -07:00
Leonardo de Moura
5fdd2fe3a9 refactor(util/script_state): replace splay_map with rb_map in the Lua environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 17:53:34 -07:00
Leonardo de Moura
2a59beee0a feat(shell): reactivate lean shell, only Lua frontend is working 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 17:49:23 -07:00
Leonardo de Moura
cdae3ee780 fix(kernel/type_checker): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:17:34 -07:00
Leonardo de Moura
1681dc2389 test(kernel): add new environment tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:04:05 -07:00
Leonardo de Moura
b70bac0e8d feat(kernel/type_checker): add backtracking trick to minimize the number of delta-reduction steps 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:03:46 -07:00
Leonardo de Moura
e62254fbb3 fix(kernel/expr): relax macro_definition interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:02:48 -07:00
Leonardo de Moura
1b9e2efb0c fix(kernel/environment): relax normalizer_extesion interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 14:01:44 -07:00
Leonardo de Moura
f320277248 feat(kernel/definition): add mk_definition procedure that automatically computes the weight 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 12:48:21 -07:00
Leonardo de Moura
6c3a796119 fix(kernel/type_checker): bug in whnf method, and missing call to max_sharing in is_conv and is_def_eq methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 12:09:23 -07:00
Leonardo de Moura
4e893d3902 fix(kernel/constraint): printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 12:02:59 -07:00
Leonardo de Moura
54936c201a fix(kernel/kernel_exception): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 11:31:39 -07:00
Leonardo de Moura
6dfeff92f8 fix(kernel/constraint): add dealloc method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 11:13:51 -07:00
Leonardo de Moura
e3b79730ba fix(kernel/level): initialization error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 11:03:23 -07:00
Leonardo de Moura
2ddadfc920 fix(kernel/environment): compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 10:58:14 -07:00
Leonardo de Moura
9f57ec059a fix(kernel/constraint): missing inline directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 10:53:53 -07:00
Leonardo de Moura
272463bd66 feat(kernel/type_checker): add check function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-28 10:47:50 -07:00
Leonardo de Moura
e769c26800 refactor(kernel): move files that don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:30:40 -07:00
Leonardo de Moura
b2518f873d feat(kernel/type_checker): handle ensure_pi when whnf is a meta application 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:17:32 -07:00
Leonardo de Moura
6b05146eca fix(kernel/type_checker): preserve bound variable name when inferring type of a lambda expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 17:29:47 -07:00
Leonardo de Moura
63b6564b78 refactor(kernel): define extension_context API for normalizer_extesions and macro_definitions 
A particular macro definition may use the extra information to retrieve information necessary to expand/type a given macro application. Example: it may need to invoke whnf.

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

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 15:38:22 -07:00
Leonardo de Moura
086dd6b1a1 chore(kernel/environment): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 15:36:52 -07:00
Leonardo de Moura
3b78af0db5 chore(tests/library): enable old tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 12:05:49 -07:00
Leonardo de Moura
ad43d9177b refactor(util/name_set): implement name_sets using red black trees instead of hashtables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 11:09:13 -07:00
Leonardo de Moura
cc1cfba8ad refactor(kernel/type_checker): new API for type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-21 16:12:47 -07:00
Leonardo de Moura
6417c79569 feat(kernel/environment): add is_descendant method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-21 14:28:50 -07:00
Leonardo de Moura
bfeb51ce58 feat(kernel/environment): add trust level field 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-21 13:39:47 -07:00
Leonardo de Moura
ee58a83e25 chore(kernel): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 14:25:09 -07:00
Leonardo de Moura
d0dc16355b chore(kernel): remove unnecessary file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 14:23:32 -07:00
Leonardo de Moura
582352d647 refactor(kernel/environment): simplified (functional) environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 14:21:49 -07:00
Leonardo de Moura
234abb1238 feat(kernel/definition): default constructor for definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-18 13:10:05 -07:00
Leonardo de Moura
984ac03ac7 refactor(kernel): replace kernel object with definition, disable affected files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 16:10:47 -07:00
Leonardo de Moura
cb479a75ae fix(kernel/expr): make sure we cannot create a free variable with index uint_max, reason: get_free_var_range would return an incorrect value 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 13:25:21 -07:00
Leonardo de Moura
3712da0b54 refactor(kernel/instantiate): use get_free_var_range to improve instantiate, remove instantiate_with_closed, fix index overflow bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 13:12:49 -07:00
Leonardo de Moura
1fd5e9682d refactor(kernel/free_vars): use get_free_var_range to improve lift_free_vars and lower_free_vars performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 12:41:06 -07:00
Leonardo de Moura
4ae958af56 refactor(kernel/free_vars): use get_free_var_range to improve has_free_var_in_range performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 12:18:19 -07:00
Leonardo de Moura
dc864bf7b9 feat(kernel): store free variable range in composite expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 11:31:48 -07:00
Leonardo de Moura
1fd447b451 chore(util): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:54:10 -07:00
Leonardo de Moura
bc8379256a refactor(kernel): remove pairs from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:52:07 -07:00
Leonardo de Moura
9a3959eed1 feat(util): add method get_rc (mainly for debugging purposes) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:36:54 -07:00
Leonardo de Moura
c78e6787aa test(util/rb_tree): multi-thread test for rb trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-20 10:20:28 -07:00
Leonardo de Moura
fb2ec8fb12 fix(kernel): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
9b161b825f refactor(kernel): instantiate_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
3651b4ecd0 refactor(kernel): replace_fn functional object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
3939b93c2d refactor(kernel): substitution 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
25948ac534 refactor(kernel): cleanup interfaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
08087ea9c6 refactor(kernel): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
eb487e44c1 refactor(kernel): use names instead of unsigned integers to encode level parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
ddbb3a7944 refactor(kernel): add error msg formatters, remove unnecessary files, add new type_checker interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
916301bdfb refactor(kernel): parametric kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
54801bbd05 refactor(kernel): constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
aa4a7acccf feat(kernel/level): is_trivial predicate for level constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
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
41782c0894 test(kernel/metavar): add metavar tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
bf13441bd7 fix(kernel): bugs in justification module, add missing metavar methods, add basic metavar tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
4c30ea9251 fix(kernel/justification): none is the unit of mk_composite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
3c6002e969 refactor(kernel): add mk_rev_app, update_rev_app, implement instantiate_metavars functions, modify instantiate (free vars) API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
42e253c962 fix(*): style and clang warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
968c0d799f refactor(kernel): implement substitution methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
5f4b1cf47e feat(kernel): define metavar substitution based on red-black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
f855dbb7b0 feat(util): add maps based on red-black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
54d5088c98 feat(util/rb_tree): add check_invariant for red black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
1ab12eb105 refactor(util/splay_map): remove unnecessary operation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
528ea367ad feat(util): add red-black trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
fdde12e6af refactor(kernel): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
2a73389ed3 refactor(kernel): justification objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
50300126a5 refactor(util/name_generator): make sure there is no risk of overflow, name generators will be extensively used in version 0.2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
501435f6fc feat(kernel): add has_local predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
e1f4f1f0d1 feat(util/thread): add atomic_uchar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
997f32378c refactor(kernel): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
6baa59376c refactor(kernel): normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
eb046c11fb refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
410d5cc8ed fix(kernel): remove unnecessary file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
16aa1ebbac refactor(kernel): replace_visitor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
101888e079 refactor(kernel): delete update_expr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
b5f0f28009 refactor(kernel): environment, kernel object and exceptions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
3c8ccdd33d test(util/exception): experiment with exceptions with nested std::function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
737fe6830f test(tests/kernel): adjust expr tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
f986963a95 refactor(kernel): serializer and deserializer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
74f74d2f79 refactor(kernel): shallow copy procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
5da501d538 fix(kernel): style warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
73c8bf4436 refactor(tests/kernel): move tests to new kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
565dbe1700 fix(kernel/instantiate): bug in new head_beta_reduce 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
d17990ed78 refactor(kernel): add formatter and simplify contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
53ee205dc6 fix(kernel): memory corruption bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
72e1678ad9 refactor(kernel): cleanup instantiate and abstract procedures, implement update procedures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
db31cc37a1 refactor(kernel/free_vars): cleanup free_vars procedures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
533f44e224 refactor(kernel/expr): for_each_fn, replace_fn, and find_fn without templates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
69b9f2dd37 refactor(kernel/expr): for_each and find functional objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
23988f528c refactor(kernel/expr): add expr constructors, and expression equality test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
9d3db8de1f fix(kernel/diff_cnstrs): missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
02413d7c44 refactor(kernel/expr): adding suport for universe polymorphism, and simplify metavariable representation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
13cfd60622 fix(kernel/diff_cnstrs): copyright msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
76b1ddb967 feat(kernel): add difference constraint solver with backtracking support, and justification generation, this solver will be used to check the satisfiability of universe level constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
9f93b5d97e feat(kernel/level): new universe level datastructure for universe level polymorphism 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
1b6b33b3f5 refactor(kernel): start version 0.2, new kernel with universe polymorphism and better/cleaner support for metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:54 -07:00
Leonardo de Moura
0c1674ab70 feat(builtin): quotient types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-12 00:20:46 -07:00
Leonardo de Moura
e0eacd1f9f feat(builtin): simpler encoding of sum types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-03 18:30:45 -08: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
aa8240985a test(examples/lean): small version of algebraic hierarchy (proof of concept) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-24 20:51:19 -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
16844fff73 feat(builtin): simulate binary encoding 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-20 20:44:05 -08:00
Leonardo de Moura
d79e9af210 fix(frontends/lean): help msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-18 09:31:30 -08:00
Leonardo de Moura
f781ad823c doc(builtin): Diaconescu’s theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-18 09:12:09 -08:00
Leonardo de Moura
e9dada5e14 refactor(builtin/kernel): use standard definition for 'or' and 'and' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-17 12:05:34 -08:00
Leonardo de Moura
4692e04d70 feat(builtin/proof_irrel): prove proof irrelevance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-16 18:06:10 -08:00
Leonardo de Moura
c526e5ec00 feat(builtin/kernel): prove false_elim without using case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-15 14:26:13 -08:00
Leonardo de Moura
1739b5c153 fix(kernel/type_checker): caching bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 10:43:01 -08:00
Leonardo de Moura
c740d9d799 fix(builtin/num): bug in the factorial definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 10:04:32 -08:00
Leonardo de Moura
45a0dbcc34 feat(builtin/num): define fact and exp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 09:51:49 -08:00
Leonardo de Moura
368fcb5ff9 refactor(builtin/kernel): rename refute to by_contradiction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 08:49:19 -08:00
Leonardo de Moura
69bccb6014 feat(builtin): define list, cons, nil and prove basic theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-11 21:32:05 -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
0878b44fc7 feat(frontends/lean): allow user to import several theories using a single import 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-11 17:15:12 -08:00
Leonardo de Moura
11a2b3016f fix(builtin/num): remove hacks for making the elaborator happy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 14:05:51 -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
a2d2e36f04 refactor(frontends/lean): remove notation for creating tuples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 09:03:42 -08:00
Leonardo de Moura
4e08a3233e fix(builtin): build dependency issue 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 08:33:07 -08:00
Leonardo de Moura
273f78d1cb feat(builtin/num): prove strong induction and other theorems for num 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 21:09:50 -08:00
Leonardo de Moura
b119c11473 feat(builtin/tactic): add simp_no_assump tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 20:28:30 -08:00
Leonardo de Moura
4317f67bd2 fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 18:57:33 -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
fd6f8b1945 refactor(builtin/num): simplify proofs using 'by simp' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 15:03:45 -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
4c76f6abb9 chore(builtin/num): remove leftover 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 11:39:26 -08:00
Leonardo de Moura
8df7c7b02d feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker 
We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 11:31:24 -08:00
Leonardo de Moura
4c4c8b3e0d feat(builtin/num): prove basic theorems using simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 11:24:53 -08:00
Leonardo de Moura
633ed6bb69 fix(frontends/lean/parser): bug in add_rewrite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 09:46:56 -08:00
Leonardo de Moura
b24c085cb0 feat(frontends/lean): avoid warning message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 09:26:51 -08:00
Leonardo de Moura
d6167eae32 feat(builtin/num): define add and mul 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 22:28:15 -08:00
Leonardo de Moura
cc4148a98d feat(builtin/num): primitive recursion theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 22:05:57 -08:00
Leonardo de Moura
f28c56b188 feat(builtin/num): add auxiliary definitions and theorems for proving the primitive recursion theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 19:36:17 -08:00
Leonardo de Moura
fa4b60963b feat(builtin/num): define lt predicate, and prove basic theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 10:57:17 -08:00
Leonardo de Moura
1f3e0f7a38 chore(builtin/num): update object file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 09:16:52 -08:00
Leonardo de Moura
aeaa803f9a feat(builtin): add num type (the base type that will be used to build nat, int, real) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-08 09:12:53 -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
354d5607af chore(builtin/sum): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 21:25:57 -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
ff955f9830 chore(frontends/lean/parser): update comments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -08:00
Leonardo de Moura
593f1f2ebd fix(frontends/lean): allow user set constants defined in other namespaces as opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -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
4b4b5e3345 fix(frontends/lean): import explicit versions when using the command 'using' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:33:58 -08:00
Leonardo de Moura
ea06bb2885 feat(frontends/lean/pp): change how lift local entries are pretty printed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -08:00
Leonardo de Moura
a51139e63b feat(frontends/lean): position information in error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -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