Commit graph

932 commits

Author SHA1 Message Date
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
30570c843f feat(builtin): add optional type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-05 17:33:06 -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
9dc86e3cf5 fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 10:06:29 -08:00
Leonardo de Moura
9a677331da feat(builtin): simulate subtypes using sigma types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 01:46:50 -08:00
Leonardo de Moura
4fcc292332 feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 22:10:01 -08:00
Leonardo de Moura
5c991f8fbf feat(frontends/lean): parse and pretty print tuples/pairs
This commit also fixes a bug in the type checker when processing dependent pairs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:10:30 -08:00
Leonardo de Moura
5e5ab1429d feat(frontends/lean): parse and pretty print sigma types
This commit also fixes some bugs in the implementation of Sigma types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 18:16:00 -08:00
Leonardo de Moura
8eec289ce1 feat(kernel): add dependent pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 16:52:49 -08:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 14:48:27 -08:00
Leonardo de Moura
2aaded261e fix(kernel/environment): imported predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 23:02:19 -08:00
Leonardo de Moura
4d533c6a25 feat(builtin/kernel): add nonempty_range theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 22:13:34 -08:00
Leonardo de Moura
ddaf948c72 feat(builtin/kernel): add nonempty_fun theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 19:38:51 -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
8c1f6b9055 fix(kernel/typechecker): allow elaborator to infer (Type U+1)
In the new test elab8.lean, the parameter B is in (Type U+1).
Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 14:00:01 -08:00
Leonardo de Moura
01259b1e84 feat(kernel): make sure U is the maximal universe
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 16:31:00 -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
b6985bd713 feat(builtin/kernel): add another rewrite rule
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 15:56:26 -08:00
Leonardo de Moura
55fde28954 feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 17:47:03 -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
05b4d8411b refactor(kernel/normalizer): normalizer only needs read access to metavariable environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 17:03:36 -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
b26035fcf6 feat(kernel/type_checker): improve application type mismatch error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 09:45:17 -08:00
Leonardo de Moura
ceff335bb8 doc(doc/lean/tutorial): update tutorial
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-26 22:58:44 -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
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
2bb33c55fe feat(builtin/kernel): add more theorems useful for simplification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 18:52:50 -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
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
66553268d0 feat(builtin/kernel): add skolem_th, we need it to justify skolemization preprocessing step
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 09:41:07 -08:00
Leonardo de Moura
d9b5ebc738 refactor(builtin/kernel): cleanup Hilbert operator definition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 09:18:40 -08:00
Leonardo de Moura
94a3136904 feat(builtin/kernel): add Hilbert's operator, and derive axiom of choice using it
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 08:21:11 -08:00
Leonardo de Moura
029d74ec11 chore(kernel): remove comment, we decided to have Eta as a simplification rule
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 14:35:05 -08:00
Leonardo de Moura
95b6e61738 feat(kernel/max_sharing): check for imminent stack overflows and interruptions in the expression sharing maximizer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 14:33:49 -08:00
Leonardo de Moura
2089b85532 refactor(kernel/instantiate): remove code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 14:30:38 -08:00
Leonardo de Moura
7299b2d5d6 chore(kernel): remove dead file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 14:21:13 -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
217e56ea03 feat(kernel/expr): make sure semantic attachments are smaller than other kinds of expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 14:10:44 -08:00
Leonardo de Moura
5060bdbf14 fix(kernel/expr): compilation warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 13:12:49 -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
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
6db10c577b feat(builtin/kernel): add proof irrelevance axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:20:09 -08:00
Leonardo de Moura
475df3d94e chore(builtin/kernel): add theorem for rewriter/simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 10:34:18 -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
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
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
1da4294793 refactor(builtin): more theorems, fix iff notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-16 09:26:50 -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
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
7fb0aa4800 chore(kernel/expr): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 17:24:31 -08:00
Leonardo de Moura
c096eec1d6 chore(kernel/expr): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 17:09:04 -08:00
Leonardo de Moura
8c2f78a756 feat(builtin): minimize use of heterogenous equality in the kernel, add simpler version of congruence theorems for non-dependent types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 16:34:23 -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
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
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
acfb11e290 fix(kernel/instantiate): relax apply_beta pre-condition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 14:36:51 -08:00
Leonardo de Moura
a968a43487 fix(kernel/free_vars): make sure has_free_var does not return incorrect result due to arithmetic overflows
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 14:36:14 -08:00
Leonardo de Moura
f8eaae7218 feat(builtin/kernel): add new useful theorems for the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 18:21:22 -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
e6c322d97f feat(kernel/free_vars): make free_vars module functions more robust
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:44:28 -08:00
Leonardo de Moura
5d9a95addd refactor(kernel/free_vars): replace max_free_var with relaxed free_var_range
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:06:57 -08:00
Leonardo de Moura
4d9eb4ac6c feat(kernel): add max_free_var function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 16:45:34 -08:00
Leonardo de Moura
781720a26a feat(builtin/kernel): add left_comm theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 18:08:08 -08:00
Leonardo de Moura
a1a467a65f refactor(builtin): move congruence theorems to kernel/if_then_else modules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 13:48:28 -08:00
Leonardo de Moura
53537d0684 feat(builtin/kernel): 'implication' simplification theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 13:35:20 -08:00
Leonardo de Moura
50f281b430 feat(builtin/kernel): add eqf_intro and eqf_elim theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 11:13:54 -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
fdeb457a81 feat(kernel/pos_info_provider): add support for file names in pos_info_provider
The idea is to include the file name when displaying justification objects.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:19:30 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00
Leonardo de Moura
e42b616438 fix(kernel/normalizer): equality between semantic attachments
Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 19:10:30 -08:00
Leonardo de Moura
8e9d88c2cf refactor(builtin/kernel): prove iff::intro, and add a new name for it boolext (Boolean extensionality)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 18:31:45 -08:00
Leonardo de Moura
a4b3d6d6c8 refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 17:25:14 -08:00
Leonardo de Moura
2b2aa228e3 refactor(builtin/kernel): start with small universes
The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 12:35:00 -08:00
Leonardo de Moura
85de05e5cf chore(kernel/unification_constraint): update max_constraint comment to reflect its new semantics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 01:09:47 -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
d12d0f036f feat(kernel/environment): universe variables now live in their own namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:57:36 -08:00
Leonardo de Moura
95515ca5df chore(*): fix warnings produced by clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:39:49 -08:00
Leonardo de Moura
29db6accb8 test(tests/lean): new tests for exercising the environment object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 14:34:21 -08:00
Leonardo de Moura
0a20356a51 fix(kernel/environment): we should not add an universe contraint object to the set of object when an integer overflow occurs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 13:43:22 -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
b5a30855f8 feat(kernel/universe_constraints): add new class for managing universe constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 15:01:28 -08:00
Leonardo de Moura
8c956280d9 chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 11:41:03 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 19:21:44 -08:00
Leonardo de Moura
4ba097a141 feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 13:06:36 -08:00
Leonardo de Moura
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
43909ca66b feat(frontends/lean/pp): pretty print SetOpaque command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 13:16:44 -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
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
0d815b8594 refactor(kernel/context): hide that the context is implemented using lists
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-31 19:43:50 -08:00
Leonardo de Moura
1cb7408c46 fix(kernel/normalizer): metavariable reification was incorrect, add tst11 at tests/kernel/normalizer.cpp to expose the bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-31 16:24:36 -08:00
Leonardo de Moura
cd3bbb1ebf fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-31 10:14:17 -08:00
Leonardo de Moura
c485b4bc4c fix(kernel/environment): binary file reader, force the file to be read in binary mode
We need this flag to be able to read the file on Windows.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 18:20:40 -08:00
Leonardo de Moura
1f6e959139 feat(deserializer): protect against corrupted binary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 18:05:38 -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
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
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
de77851a00 refactor(util/object_serializer): add methods write_core and read_core that allows to pack information in the byte used to indicate whether an object is already in the cache or not
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:59:53 -08:00
Leonardo de Moura
dbd122301a feat(kernel/object): compact object serialization kind ids
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:19:24 -08:00
Leonardo de Moura
d0fdc3619b feat(kernel/expr): compress application serialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:11:57 -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
92404c511c refactor(kernel/builtin): Bool type does not need to be a semantic attachment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 15:12:08 -08:00
Leonardo de Moura
dfe46b9d25 refactor(kernel/builtin): move definition and axioms to basic.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 14:01:30 -08:00
Leonardo de Moura
1b300d3598 chore(kernel/builtin): remove unnecessary functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 12:55:51 -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
9fdf2a3f55 feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules
"Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip
type checking when importing these files.
TODO: add a check-sum.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:43:53 -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
5e0b344871 fix(kernel/object): uninitialized variable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 21:57:56 -08:00
Leonardo de Moura
41c1010043 feat(frontends/lean/parser): make Import command use binary Lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 19:20:04 -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
22bebbf242 feat(kernel/object): serializer for kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 14:39:10 -08:00
Leonardo de Moura
755e8b735f feat(kernel/expr): serializer for kernel expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 01:23:21 -08:00
Leonardo de Moura
0ef8ba2939 feat(kernel/level): serializer for level objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 23:30:13 -08:00
Leonardo de Moura
8cf65f354b fix(frontends/lean/pp): forall and exists pretty printing when used as constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 12:50:41 -08:00
Leonardo de Moura
2aa691ccb3 fix(kernel/replace_fn): ignore the cached type in constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 21:11:25 -08:00
Leonardo de Moura
1a0f0c1609 feat(kernel/normalizer): let normalizer ignore 'undefined' constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 20:54:15 -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
b83b17d3ab fix(kernel/metavar): bug at cached_metavar_env::update method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 15:41:02 -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
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
90dbdaec40 feat(kernel/expr): cache is_arrow result
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 13:59:45 -08:00
Leonardo de Moura
1faf42e2e1 chore(kernel/expr): remove unnecessary #if-#then-#else
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 13:36:41 -08:00
Leonardo de Moura
7b0b363b32 fix(kernel/normalizer): metavariable reification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 06:40:26 -08:00