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
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
e9dada5e14
refactor(builtin/kernel): use standard definition for 'or' and 'and'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-17 12:05:34 -08:00
Leonardo de Moura
1739b5c153
fix(kernel/type_checker): caching bug
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-12 10:43:01 -08:00
Leonardo de Moura
368fcb5ff9
refactor(builtin/kernel): rename refute to by_contradiction
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-12 08:49:19 -08:00
Leonardo de Moura
b7b868de85
fix(library/elaborator): bug reported by Jeremy Avigad
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-10 14:01:22 -08:00
Leonardo de Moura
a2d2e36f04
refactor(frontends/lean): remove notation for creating tuples
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-10 09:03:42 -08:00
Leonardo de Moura
4317f67bd2
fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 18:57:33 -08:00
Leonardo de Moura
c45c1748d8
refactor(builtin/kernel): reorder congr1 arguments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 16:15:44 -08:00
Leonardo de Moura
8df7c7b02d
feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker
...
We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as
is_convertible(num, Nat)
If is_convertible starts unfolding opaque definitions, we would keep expanding num.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 11:31:24 -08:00
Leonardo de Moura
1ec01f5757
refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 16:04:44 -08:00
Leonardo de Moura
ad7b13104f
feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 15:03:16 -08:00
Leonardo de Moura
d4b08fcf96
feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator
...
Unification constraints of the form
ctx |- ?m[inst:i v] == T
and
ctx |- (?m a1 ... an) == T
are delayed by elaborator because the produce case-splits.
On the other hand, the step that puts terms is head-normal form is eagerly applied.
This is a bad idea for constraints like the two above. The elaborator will put T in head normal form
before executing process_meta_app and process_meta_inst. This is just wasted work, and creates
fully unfolded terms for solvers and provers.
The new test demonstrates the problem. In this test, we mark several terms as non-opaque.
Without this commit, the produced goal is a huge term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 21:08:00 -08:00
Leonardo de Moura
593f1f2ebd
fix(frontends/lean): allow user set constants defined in other namespaces as opaque
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 20:56:31 -08:00
Leonardo de Moura
363c4dc5c2
feat(library/elaborator): improve support for dependent pairs in the elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 20:56:31 -08:00
Leonardo de Moura
ea06bb2885
feat(frontends/lean/pp): change how lift local entries are pretty printed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 17:26:38 -08:00
Leonardo de Moura
a51139e63b
feat(frontends/lean): position information in error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 17:26:38 -08:00
Leonardo de Moura
e4579b93e4
fix(library/elaborator): try first projection before imitation in the higher-order unifier
...
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 13:35:05 -08:00
Leonardo de Moura
ef321e730f
feat(builtin/tactic): add the 'skip' (bogus) tactic for ignoring a proof hole in a big proof
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 12:47:23 -08:00
Leonardo de Moura
eab0456b27
test(tests/lean): test super opaque style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 11:33:27 -08:00
Leonardo de Moura
fdc4c9b53c
test(tests/lean): add nested 'have' expression test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 08:13:04 -08:00
Leonardo de Moura
1d23d93e60
feat(frontends/lean): new 'have' expression
...
Add 'have' notation suggested by Jeremy Avigad.
Add his example to the test suite.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 08:03:59 -08:00
Leonardo de Moura
ba9a8f9d98
feat(frontends/lean): add 'show' expression syntax sugar
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 07:50:22 -08:00
Leonardo de Moura
419fb7464e
fix(tests/lean): adjust tests to reflect recent changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-05 21:04:06 -08:00
Leonardo de Moura
aec9c84d0d
fix(util/lua): deadlock
...
Errors in the Lua library produce longjmps.
The longjmp will not unwind the C++ stack.
In the new test, the lock was not being released, and the system was deadlocking in the next call that tried to lock the environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 15:16:29 -08:00
Leonardo de Moura
f4ec874c6e
refactor(builtin): remove dead module heq
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 14:42:28 -08:00
Leonardo de Moura
0283887ee9
refactor(builtin/kernel): move the heq axioms into kernel.lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 14:17:34 -08:00
Leonardo de Moura
f03c09c10b
feat(library/elaborator): add support for proj/pair/sigma in the the higher-order unification procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 13:53:30 -08:00
Leonardo de Moura
413391b2b4
chore(tests/lean/sig2): remove unnecessary parenthesis from test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 11:37:08 -08:00
Leonardo de Moura
c9b72df34b
fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 11:36:26 -08:00
Leonardo de Moura
96c9c7505a
test(tests/lean): add another sigma-type test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 10:12:39 -08:00
Leonardo de Moura
9dc86e3cf5
fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 10:06:29 -08:00
Leonardo de Moura
4fcc292332
feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 22:10:01 -08:00
Leonardo de Moura
cc96b50644
feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:53:11 -08:00
Leonardo de Moura
5c991f8fbf
feat(frontends/lean): parse and pretty print tuples/pairs
...
This commit also fixes a bug in the type checker when processing dependent pairs.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:10:30 -08:00
Leonardo de Moura
640ebcc040
test(tests/lean/exp): add example for Steve
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 11:35:40 -08:00
Leonardo de Moura
e4afa3dc43
fix(tests/lean/map): incorrect output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 00:05:19 -08:00