Commit graph

647 commits

Author SHA1 Message Date
Leonardo de Moura
72f9e26dab refactor(library/private): add hidden_to_user_name and user_to_hidden_name functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 17:52:01 -07:00
Leonardo de Moura
cba52b76c7 test(lua): add integer datatype test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 16:30:33 -07:00
Leonardo de Moura
6587d0f8f3 test(lua): add is_sorted inductive predicate example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 16:30:32 -07:00
Leonardo de Moura
128d668f03 feat(library): add support for creating 'private/hidden' names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 18:37:09 -07:00
Leonardo de Moura
bfa9b90af0 feat(library/kernel_bindings): used 'named' parameters in import_modules API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 11:03:44 -07:00
Leonardo de Moura
ade5d99023 feat(library/modules): add option for discarding the proof of imported theorems (after checking them)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 10:56:28 -07:00
Leonardo de Moura
0f894f4618 chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 17:47:53 -07:00
Leonardo de Moura
162fa25250 test(lua): move slow tests to tests/lua/slow
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 10:24:18 -07:00
Leonardo de Moura
3608826e4c test(lua): add inductive decl serialization test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 15:54:41 -07:00
Leonardo de Moura
bb9830f10c test(shell): add command line tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 04:53:04 -07:00
Leonardo de Moura
dbe55bf84a test(lua): add Lua State tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 04:43:44 -07:00
Leonardo de Moura
701b60d2d9 test(lua): add Lua 'yield' test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 04:39:53 -07:00
Leonardo de Moura
38a826013c test(lua): add import Lua file test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 04:34:34 -07:00
Leonardo de Moura
2d31c6c0b2 feat(library/coercion): improve get_user_coercions API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 11:35:47 -07:00
Leonardo de Moura
bb6db41414 test(lua): add 'multiple inheritance' test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 11:15:25 -07:00
Leonardo de Moura
e058839d24 fix(library/coercion): allow cycles in the coercion graph
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 11:08:49 -07:00
Leonardo de Moura
71b555ab15 test(lua): coercion module error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 10:01:04 -07:00
Leonardo de Moura
ef14c3d67e fix(library/coercion): coercion replacement
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 09:49:26 -07:00
Leonardo de Moura
fc1819aadd test(lua): coercion serialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 08:38:50 -07:00
Leonardo de Moura
0d02f933cb test(lua): add coercion sort-class tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 08:29:47 -07:00
Leonardo de Moura
e28446710e test(lua): add coercion to function-class tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 08:22:28 -07:00
Leonardo de Moura
a9a5f8628f test(lua): add coercion module tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 07:45:49 -07:00
Leonardo de Moura
69e5156034 test(lua): add import 'diamond' tst
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 16:49:43 -07:00
Leonardo de Moura
879572ee7e fix(kernel/module): non-termination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 15:12:47 -07:00
Leonardo de Moura
e4f09335ce test(lua): new module system test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 14:54:20 -07:00
Leonardo de Moura
46c292be71 test(lua): add simple module export/import test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 11:26:28 -07:00
Leonardo de Moura
69f6930bd7 test(lua): add Acc datatype declaration test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 11:26:02 -07:00
Leonardo de Moura
ce634d4459 test(lua): well-founded induction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-22 14:10:25 -07:00
Leonardo de Moura
1447d7e765 test(lua): add another inductive datatype example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-22 14:10:25 -07:00
Leonardo de Moura
6246fae32c fix(kernel/inductive): inductive datatype declaration validation bug pointed out by Cody Roux
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 16:29:25 -07:00
Leonardo de Moura
b9d7f8e867 test(lua): make sure bug reported by Floris does not happen in Lean 0.2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 13:34:04 -07:00
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
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
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
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
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
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
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
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
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
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
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
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
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
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
b5d07bec2e test(lua): add some comments to inductive datatype test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:30:43 -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
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
53e02a902c test(lua): add is_geq (for universe level) tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 13:42:12 -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
3a0861bca7 test(lean): remove old test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:42:10 -07:00
Leonardo de Moura
9f06cd553e test(lean): remove tests using Lean old syntax and kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:38:53 -07:00
Leonardo de Moura
989bcdc7ad test(lua): add inductive datatype simple tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 09:25:03 -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
755fac8114 test(lua): add test simulating HoTT compatible environment
Type.{0} is predicative
   Type.{0} is proof relevant
   Id       is proof irrelevant
   Path     is proof relevant

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:32:01 -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
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
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
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
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
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
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
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
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
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
20947de2f1 test(lua): add replace method test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 15:51:22 -07:00
Leonardo de Moura
9f86aa73c8 test(lua): add basic universe level tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:51:18 -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
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
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
a650a4f9b5 fix(library/kernel_bindings): bug in mk_app, add expr_lt tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 19:54:52 -07:00
Leonardo de Moura
21e3e22017 test(lua/threads): re-activate Lua thread examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:52:15 -07:00
Leonardo de Moura
129d108d0b test(lua): add example for testing is_descendant
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:50:24 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:08:32 -07:00
Leonardo de Moura
5a7f181efc feat(util/name_set): improve name_set Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 17:17:00 -07:00
Leonardo de Moura
f3c7bc948a feat(library/kernel_bindings): type_checker Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 19:04:15 -07:00
Leonardo de Moura
1a8d75c4f0 feat(util): name_set Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 18:32:53 -07:00
Leonardo de Moura
7fe61bc69c feat(util): name_generator Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 17:28:11 -07:00
Leonardo de Moura
62db010ba3 feat(library/kernel_bindings): add optional arguments to empty_environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 17:06:27 -07:00
Leonardo de Moura
4c5f88e63b feat(library/kernel_bindings): global level constructor/accessor/recognizer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 16:22:45 -07:00