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
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
Leonardo de Moura
8ae0e46e9d
feat(library/kernel_bindings): add new global level methods to environment Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 16:17:04 -07:00
Leonardo de Moura
9bf83390dc
test(lua): add definition API tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 17:01:22 -07:00
Leonardo de Moura
dc627c9965
test(lua): add constraint API tests, and fix minor bugs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 13:37:46 -07:00
Leonardo de Moura
7b4b862faa
test(lua): add justification API tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:16:24 -07:00
Leonardo de Moura
340c0e0945
feat(library/kernel_bindings): substitution Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 15:30:30 -07:00
Leonardo de Moura
305815cb56
feat(library/kernel_bindings): expose expr_binder_info in the Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 11:23:37 -07:00
Leonardo de Moura
97e7e4e762
test(lua): remove obsolete test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 17:08:50 -07:00
Leonardo de Moura
fd034521dc
feat(library/kernel_bindings): cleanup level Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 17:05:25 -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
984048f40d
feat(library/kernel_bindings): new level Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 15:08:58 -07:00
Leonardo de Moura
a6116e3156
test(lua): reactivate some of the Lua unit tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 10:36:57 -07: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
e3dc552c39
fix(library/simplifier): nontermination
...
The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition
definition a := 1
it will match 'a' with '1' since they are definitionally equal.
Then, if we have a theorem
theorem a_eq_1 : a = 1
as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"
a --> 1 --> 1 --> 1 ...
The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.
To avoid this loop, we test if the new expression is not equal to the previous one.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 15:55:21 -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
dd6aae378f
fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 13:29:20 -08:00
Leonardo de Moura
92ba4e8b2d
feat(library/simplifier): add support for metavariables in conditional rewrite rules
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 08:34:04 -08:00
Leonardo de Moura
1ef75a9ba6
test(tests/lua): add test/example that demonstrates how to collect statistics of used theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 18:04:22 -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
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
bbf6e6a256
feat(builtin/kernel): create default rule set in the kernel, and adjust unit tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 11:24:20 -08:00
Leonardo de Moura
7492fd5a2c
feat(library/simplifier): add support for simplification by evaluation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 10:34:55 -08:00
Leonardo de Moura
11719713ec
feat(library/hop_match): optionally unfold constants when performing higher order matching
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 10:32:06 -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
ed009f4c88
feat(kernel/simplifier): add support for Beta-reduction in the simplifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 00:40:20 -08:00
Leonardo de Moura
32c5bc25e3
refactor(library/simplifier): cleanup rewrite_rule_set, and use it in the simplifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-18 20:52:33 -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
5453a8f2f1
test(tests/lua): hop_match experiment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-16 00:15:31 -08:00
Leonardo de Moura
3238c7e2a0
feat(library/simplifier): add is_permutation_ceq predicate
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 19:53:52 -08:00
Leonardo de Moura
2368c936d3
test(tests/lua): exercise fields method for semantic attachments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 17:24:18 -08:00
Leonardo de Moura
c73398a0b8
refactor(library/simplifier): relax rule for conditional equalities
...
The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:
theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 16:06:00 -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
f67b5c4d00
test(tests/lua): more to_ceqs tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 13:50:35 -08:00
Leonardo de Moura
c651d3ea2d
feat(library/simplifier): filter out propositions that cannot be used as conditional equations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 12:06:27 -08:00