Commit graph

2557 commits

Author SHA1 Message Date
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
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
ff3a7bd734 fix(kernel/type_checker): style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:21:09 -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
5c7d3c79c4 feat(kernel/expr): improve get_app_args interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:19:10 -07:00
Leonardo de Moura
28e8299f6d feat(kernel/type_checker): add swap method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:18:46 -07:00
Leonardo de Moura
4325b126d4 feat(util/list): add map2 for list<T1> -> list<T2>, where T1 and T2 may be different, we still keep map because compiler can automatically infer all template arguments, this is not the case for map2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:18:18 -07:00
Leonardo de Moura
f818c1a63e feat(kernel/inductive): add more inductive datatype validation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 14:47:06 -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
f7bc5ac514 fix(library/kernel_bindings): style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 13:44:51 -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
d0e7c88ea8 feat(library/kernel_bindings): improve universe level Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 13:40:35 -07:00
Leonardo de Moura
18a17cd48b feat(kernel/level): add is_geq predicate, we need it for implementing the inductive datatype validation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 13:39:54 -07:00
Leonardo de Moura
4348d5e63f refactor(kernel): remove unnecessary module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 12:35:41 -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
33ae79cd9e refactor(kernel): move shallow copy function to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:20:24 -07:00
Leonardo de Moura
d625c9a26c refactor(kernel): move max_sharing to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:15:08 -07:00
Leonardo de Moura
aafdd98acb refactor(kernel): remove telescope type, and procedures
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:51:40 -07:00
Leonardo de Moura
7142c0fed3 doc(demo): remove Lean 0.1 demo files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:43:30 -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
36b070cb5b refactor(kernel/inductive): simplify inductive datatype API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 09:24:34 -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
5fc0f06a8d feat(library/kernel_bindings): add Lua API for declaring datatypes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 18:08:50 -07:00
Leonardo de Moura
ace5dee63d feat(kernel/inductive): add getters for inductive decls
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 17:47:37 -07:00
Leonardo de Moura
6dedb480ec fix(kernel/abstract): bug in abstract for telescopes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 17:47:04 -07:00
Leonardo de Moura
e6c52d17a6 fix(kernel/expr): memory leak introduced today
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 16:21:31 -07:00
Leonardo de Moura
7d76278506 fix(kernel/abstract): compilation warnining
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:39:19 -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
a0abbf7662 feat(kernel/formatter): make simple_formatter display Type instead of Bool if impredicativity is disabled
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:31:19 -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
862c5e354d feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 13:08:09 -07:00
Leonardo de Moura
28329a55b0 feat(util/name): use '.' instead of '::' as hierarchical name separator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 12:35:43 -07:00
Leonardo de Moura
91a1b62b9e feat(kernel): add telescope abstract procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 11:56:44 -07:00
Leonardo de Moura
9a689ab0c3 feat(kernel): add telescope instantiate procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 11:56:20 -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
d6d72ba80e refactor(kernel): add binder structure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 10:51:54 -07:00
Leonardo de Moura
eb0abf557d feat(kernel/inductive): add inductive datatype kernel extension module interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 09:53:51 -07:00