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

2176 commits

Author SHA1 Message Date
Leonardo de Moura
4103c85ce3 feat(library/kernel_bindings): improve Fun/Pi Lua APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 09:00:19 -07:00
Leonardo de Moura
bcb9965844 feat(library/kernel_bindings): improve Fun/Pi Lua APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:07:20 -07:00
Leonardo de Moura
9de8249d8f feat(kernel): let Pi/Fun also take local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:03:48 -07:00
Leonardo de Moura
df9c935f0a fix(kernel/inductive): remove unused argument, bug in is_rec_argument (free variable occurrence) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 17:02:20 -07:00
Leonardo de Moura
3e3d3c8380 feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 15:44:15 -07:00
Leonardo de Moura
a7aacaa782 feat(library/kernel_bindings): improve list_level support in the Lua interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 15:18:48 -07:00
Leonardo de Moura
a1086e440d feat(kernel/inductive): use non-dependent elimination for Bool/Prop only if it is proof irrelevant 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 13:33:29 -07:00
Leonardo de Moura
eb92f3722f fix(kernel/inductive): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 13:27:05 -07:00
Leonardo de Moura
f3ed20a229 feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 12:52:25 -07:00
Leonardo de Moura
edc8af7bb3 refactor(kernel): reduce code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 11:11:19 -07:00
Leonardo de Moura
0e582675d9 feat(kernel/inductive): store computational rules in an environment extension 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 10:45:52 -07:00
Leonardo de Moura
90d83fa2ad fix(kernel/environment): bug in get_extension 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 10:41:22 -07:00
Leonardo de Moura
1a9122f158 doc(kernel/inductive): improve module documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 10:04:28 -07:00
Leonardo de Moura
2aacb769dd feat(kernel/inductive): generate computational rules RHS for inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 09:08:19 -07:00
Leonardo de Moura
eb409a9ce3 feat(kernel/abstract): add more Fun functions for simplifying the creation lambda-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 09:01:20 -07:00
Leonardo de Moura
5566186c34 feat(util/list_fn): add get_ith function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 09:00:09 -07:00
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