Commit graph

2548 commits

Author SHA1 Message Date
Leonardo de Moura
203a59b682 test(lua): add more tests for the environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 12:36:04 -07:00
Leonardo de Moura
e39feabb72 feat(library/module): add declaration reader
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:54:29 -07:00
Leonardo de Moura
9f4bae6856 feat(library/kernel_bindings): add hott_environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:49:30 -07:00
Leonardo de Moura
45d473d44e feat(kernel): add mk_hott_environment function for creating HoTT compatible environments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:31:34 -07:00
Leonardo de Moura
4d1fecb21d refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:24:24 -07:00
Leonardo de Moura
f08a852da8 feat(library/kernel_bindings): expose environment::add(declaration) method in the Lua API, and add example to demonstrate its usage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:12:55 -07:00
Leonardo de Moura
9b9041fa2e feat(kernel/environment): add method for adding declarations that were not type checked (if trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:12:26 -07:00
Leonardo de Moura
8ffe66dc4f feat(library): add module system API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 18:35:59 -07:00
Leonardo de Moura
dd3edcb19f feat(library): add shared environment object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 15:42:52 -07:00
Leonardo de Moura
3726688711 test(lua): add test to demonstrate the different between list(A) where A is a parameter, and where A is an index
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 12:17:16 -07:00
Leonardo de Moura
11fc917102 test(lua): add tests for improving kernel_bindings coverage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 12:16:12 -07:00
Leonardo de Moura
c5e8c10c9d fix(library/normalize): bug in normalize
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 11:53:58 -07:00
Leonardo de Moura
fae07771ec test(lua): add more universe level expression tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 11:41:17 -07:00
Leonardo de Moura
8872d4a531 refactor(kernel): rename definition class to declaration
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:41:38 -07:00
Leonardo de Moura
00b1a84051 feat(library/kernel_bindings): expose environment::for_each method in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:16:19 -07:00
Leonardo de Moura
34a9c8304a feat(kernel/environment): add for_each method for traversing environment declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:15:28 -07:00
Leonardo de Moura
9e55c8766f test(lua): add normalize and type_check tests for terms containing metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:56:27 -07:00
Leonardo de Moura
ddccca529a test(lua): add test for mutually recursive inductive type recursor/eliminator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:41:50 -07:00
Leonardo de Moura
8a8c5a2b84 feat(library/kernel_bindings): add normalize, whnf, type_check, infer_type methods to environment object Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:40:50 -07:00
Leonardo de Moura
11793e7998 feat(library): add simple normalization procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:40:30 -07:00
Leonardo de Moura
4103c85ce3 feat(library/kernel_bindings): improve Fun/Pi Lua APIs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:00:19 -07:00
Leonardo de Moura
eb6807e1d3 test(lua): add another add_inductive example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 17:48:35 -07:00
Leonardo de Moura
4f15240a71 test(lua): add tests for new Pi/Fun notation in Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 17:17:15 -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
a72be5eea4 test(lua): add example suggested by Cody
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 17:06:19 -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
48b436c1c8 test(lua): add Martin-lof identity type test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 13:42:49 -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
f53254b389 test(lua): fix n6.lua, and add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-18 13:52:16 -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
fcf94ad7c2 test(lua): add test for inductive datatype positivity check
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 20:12:55 -07:00