Commit graph

69 commits

Author SHA1 Message Date
Leonardo de Moura
3aa1afdf51 refactor(util): file name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 14:15:28 -07:00
Leonardo de Moura
bf57f951ea refactor(util): move Lua named parameter support to a different file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 13:20:37 -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
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
8095783c36 refactor(library/kernel_bindings): use new functions for simulating python-like named arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-05 14:42:16 -07:00
Leonardo de Moura
850ec69538 feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-05 14:09:17 -07:00
Leonardo de Moura
10d8840cac feat(library/kernel_bindings): add environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 17:53:32 -07:00
Leonardo de Moura
4f3fad5d65 feat(library/kernel_bindings): add certified_definition Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 17:46:59 -07:00
Leonardo de Moura
8f5491447a feat(library/kernel_bindings): add environment_id Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 17:42:27 -07:00
Leonardo de Moura
fc2d5f1595 feat(library/kernel_bindings): add definition Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 17:00:59 -07:00
Leonardo de Moura
b83410f042 fix(library/kernel_bindings): g++ compilation error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 14:34:56 -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
6ef161824d feat(library/kernel_bindings): constraint Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 13:17:00 -07:00
Leonardo de Moura
802edd77d1 feat(kernel/justification): add is_eqp predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:15:29 -07:00
Leonardo de Moura
94ca82ec85 fix(library/kernel_bindings): incorrect use of pushinteger, and improve justification Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:03:43 -07:00
Leonardo de Moura
a5229e5283 chore(util/lua): name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 18:40:18 -07:00
Leonardo de Moura
7cd892464f feat(library/definition): macro definition and application Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 18:29:34 -07:00
Leonardo de Moura
9f5122b4c7 feat(library/kernel_bindings): justification Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 16:04:30 -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
686c307976 feat(library/kernel_bindings): expr Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 12:25:49 -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
884b3f9b53 refactor(library/kernel_bindings): part of expr Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-30 16:37:26 -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
412a3797f4 refactor(*): add pushboolean inline function, and replace lua_pushboolean with it
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 14:37:16 -07:00
Leonardo de Moura
f7e705badb refactor(library/kernel_bindings): reactive some of the kernel Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 11:52:09 -07:00
Leonardo de Moura
6d7ec9d7b6 refactor(kernel): add heterogeneous equality back to expr
The main motivation is that we will be able to move equalities between universes.

For example, suppose we have
    A : (Type i)
    B : (Type i)
    H : @eq (Type j) A B
where j > i

We didn't find any trick for deducing (@eq (Type i) A B) from H.
Before this commit, heterogeneous equality as a constant with type

   heq : {A B : (Type U)} : A -> B -> Bool

So, from H, we would only be able to deduce

   (@heq (Type j) (Type j) A B)

Not being able to move the equality back to a smaller universe is
problematic in several cases. I list some instances in the end of the commit message.

With this commit, Heterogeneous equality is a special kind of expression.
It is not a constant anymore. From H, we can deduce

   H1 : A == B

That is, we are essentially "erasing" the universes when we move to heterogeneous equality.
Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is

  (to_eq (Type i) A B (to_heq (Type j) A B H))  :  (@eq (Type i) A B)

So, it remains to explain why we need this feature.

For example, suppose we want to state the Pi extensionality axiom.

axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} :
      A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)

This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous
equality as a constant. The conclusion

     (∀ x, B x) == (∀ x, B' x)

is syntax sugar for

   (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x))

Even if A, A', B, B' live in a much smaller universe.

As I described above, it doesn't seem to be a way to move this equality back to a smaller universe.

So, if we wanted to keep the heterogeneous equality as a constant, it seems we would
have to support axiom schemas. That is, hpiext would be parametrized by the universes where
A, A', B and B'. Another possibility would be to have universe polymorphism like Agda.
None of the solutions seem attractive.

So, we decided to have heterogeneous equality as a special kind of expression.
And use the trick above to move equalities back to the right universe.

BTW, the parser is not creating the new heterogeneous equalities yet.
Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous
equality as a constant.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 10:28:10 -08:00
Leonardo de Moura
8eec289ce1 feat(kernel): add dependent pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 16:52:49 -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
6a63ef3bc5 feat(library/expr_lt): make sure the total order on terms is monotonic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 13:07:18 -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
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
d063828ff9 feat(library/kernel_bindings): expose abst_name, abst_domain and abst_body in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-16 00:03:16 -08:00
Leonardo de Moura
14c6218bdc chore(kernel): file name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 20:06:29 -08:00
Leonardo de Moura
94fa987814 fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool
The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 11:02:52 -08:00
Leonardo de Moura
28eb980484 fix(build): C++ module dependency problem, and style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 18:30:31 -08:00
Leonardo de Moura
c8e1ec87d2 feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 18:30:19 -08:00
Leonardo de Moura
7c2a4211a8 feat(kernel): expose imported predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 16:41:40 -08:00
Leonardo de Moura
4595c50f7e fix(library/hop_match): in locally bound variable management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 16:54:21 -08:00
Leonardo de Moura
411f14415d feat(builtin): automatically generate Lean/C++ interface for builtin theories
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 18:09:53 -08:00
Leonardo de Moura
8ce6266e6b feat(library/kernel_bindings): add new predicates for kernel objects in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 17:36:54 -08:00
Leonardo de Moura
d5ddb186d9 feat(library/kernel_bindings): add load method to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 14:21:24 -08:00
Leonardo de Moura
4424a314e0 feat(kernel): add get_universe_distance method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 17:13:13 -08:00
Leonardo de Moura
5fe8c32da9 feat(kernel): use new universe contraints in the environment, allow new constraints to be added
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 16:46:11 -08:00
Leonardo de Moura
ecc5d1bc3a refactor(kernel): move printer to library, cleanup io_state interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 13:37:50 -08:00
Leonardo de Moura
0592261847 refactor(kernel/io_state): move io_state_stream to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 13:14:21 -08:00