Commit graph

2405 commits

Author SHA1 Message Date
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
847d8b8c47 chore(examples/lean): remove old examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 16:06:42 -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
924b2344af fix(lua/res1): make sure the test works with Lua 5.1
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 14:47:42 -07:00
Leonardo de Moura
da31e60b02 test(lua): add more tests for type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 14:17:58 -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
90c4957071 test(lua): add tests for resolve macro
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:11 -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
52d682b832 test(lua): unit tests for let expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 14:29:44 -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
e57b943adf test(lua): add constraint generation test when type checking with metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 11:06:48 -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
eea561c74b test(lua): add more expr API unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-13 09:20:25 -07:00
Leonardo de Moura
cfa9520655 test(lua): add more level API unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-13 09:20:10 -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