Leonardo de Moura
959c3ffc68
feat(frontends/lean/parser): add parse_id method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 15:09:16 -07:00
Leonardo de Moura
1972a09021
feat(frontends/lean/builtin_cmds): add simple 'print' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
7fd502993b
refactor(frontends/lean/cmd_table): remove register_builtin_cmd procedures, they would cause initialization problems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
2e8ebb6d9e
feat(frontends/lean/parser): add 'parse_commands' and 'parse_script'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:32:07 -07:00
Leonardo de Moura
8fcc25d55a
fix(frontends/lean/token_table): static initialization problem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 10:56:04 -07:00
Leonardo de Moura
3dc26666b9
feat(frontends/lean): add parser interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 18:20:59 -07:00
Leonardo de Moura
d3e3301208
refactor(frontends/lean/scanner): use the parser configuration in the environment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 10:59:12 -07:00
Leonardo de Moura
e2adb101d5
feat(frontends/lean): add parser_config environment extension
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 10:39:22 -07:00
Leonardo de Moura
d81df2efe2
feat(frontends/lean/parse_table): add use_lambda_abstraction flag to scoped_expr_actions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 09:39:01 -07:00
Leonardo de Moura
546f9dc00b
chore(frontends/lean): use consistent name conventions, rename token_set to token_table
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 09:18:57 -07:00
Leonardo de Moura
00e0cc15ba
feat(frontends/lean/token_set): add token_set Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 16:49:22 -07:00
Leonardo de Moura
af0c93e0eb
feat(frontends/lean/parse_table): add typedef for notation::parse_table
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 15:54:56 -07:00
Leonardo de Moura
439b6c1e96
feat(frontends/lean/parse_table): add parse_table Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 15:33:39 -07:00
Leonardo de Moura
722ea7273e
feat(frontends/lean): add parse_table datastructure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 13:20:33 -07:00
Leonardo de Moura
d10d70423a
feat(frontends/lean): add new scanner
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 18:57:26 -07:00
Leonardo de Moura
4cf1b05831
refactor(library/token_set): move to frontends/lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 13:10:50 -07:00
Leonardo de Moura
e79e0302d0
fix(frontends/lean): style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 16:09:21 -07:00
Leonardo de Moura
c6af56260e
refactor(frontends/lean): remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 15:51:41 -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
af927ecb7a
refactor(frontends/lua): reactivate some of the Lua extensions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-28 17:57:39 -07:00
Leonardo de Moura
aa8240985a
test(examples/lean): small version of algebraic hierarchy (proof of concept)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-24 20:51:19 -08:00
Leonardo de Moura
d79e9af210
fix(frontends/lean): help msg
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-18 09:31:30 -08:00
Leonardo de Moura
0878b44fc7
feat(frontends/lean): allow user to import several theories using a single import
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-11 17:15:12 -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
633ed6bb69
fix(frontends/lean/parser): bug in add_rewrite
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 09:46:56 -08:00
Leonardo de Moura
b24c085cb0
feat(frontends/lean): avoid warning message
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 09:26:51 -08:00
Leonardo de Moura
24528ff685
fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 18:02:08 -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
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
ff955f9830
chore(frontends/lean/parser): update comments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 20:56:31 -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
4b4b5e3345
fix(frontends/lean): import explicit versions when using the command 'using'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 17:33:58 -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
e85b1f1ac0
feat(library/elaborator): expose elaborator configuration options
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 17:26:38 -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
493007b7bc
fix(frontends/lean/pp): bug in tuple/pair pretty printing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 13:58:01 -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
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
61d0c792ff
fix(frontends/lean/parser): bug in tuple/proj1/proj2
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 22:46: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
5e5ab1429d
feat(frontends/lean): parse and pretty print sigma types
...
This commit also fixes some bugs in the implementation of Sigma types.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 18:16:00 -08: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
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
b45ab9dc30
feat(library/elaborator): use equality constraints instead of convertability constraints on definitions
...
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 14:13:21 -08:00
Leonardo de Moura
ea6bf224e5
feat(frontends/lean): make the parser accept (Type -> ...)
...
Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 15:23:20 -08:00
Leonardo de Moura
4dc3aa46c3
feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 12:02:12 -08:00
Leonardo de Moura
f0a2d3627e
refactor(frontends/lean): use ascii prefix for auxiliary let-declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 11:58:09 -08:00
Leonardo de Moura
7f53cb9601
feat(frontends/lean/parser): add_rewrite take the 'using' command into account
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 01:15:28 -08:00
Leonardo de Moura
4d25cb7f47
feat(library/tactic): add simplify_tactic based on the simplifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-26 18:53:18 -08:00
Leonardo de Moura
e8bba1ebf3
fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f
...
Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.
For example, if we had
variable f {A : Type} : A -> Bool
Then, the definition of @f was
definition @f (A : Type) (a : A) : Bool := f A a
This definition is equivalent to
fun A a, f A a
which is not definitionally equal to
f
since definitionally equality in Lean ignores Eta conversion.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 20:34:28 -08:00
Leonardo de Moura
6bc1537e25
feat(frontends/lean/parser): allow the user to write (Type) without providing a level
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 20:17:36 -08:00
Leonardo de Moura
8f455f5965
fix(frontends/lean): bug in scope construct
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:23:29 -08:00
Leonardo de Moura
7f3e2b3ef4
fix(frontends/lean/parser): bug in 'using' construct
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:09:46 -08:00
Leonardo de Moura
1638a7bb02
fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 21:44:24 -08:00
Leonardo de Moura
ad219d43d9
refactor(*): semantic attachment parsing and simplification
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 14:44:45 -08:00
Leonardo de Moura
90ffb9d5ec
fix(frontends/lean/pp): bug in pp_abstraction_core
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 19:47:40 -08:00
Leonardo de Moura
d322f63113
feat(frontends/lea): add commands for creating and managing rewrite rule sets
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:03:59 -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
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
3ab2d2a441
fix(frontends/lean/parser): memory leak due to g++ bug
...
g++ implementation of std::initializer_list has bug.
http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html
This commit memory leaks triggered by this bug.
It also adds minimal tests to expose three different instances of the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 10:15:04 -08:00
Leonardo de Moura
83efa644d1
fix(frontends/lean/parser): uninitialized var error reported by valgrind
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 08:43:43 -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
ccb9faf065
refactor(*): error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 16:54:21 -08:00
Leonardo de Moura
55aa4cbfa3
feat(frontends/lean): improve error message for expressions containing unsolved metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 13:21:44 -08:00
Leonardo de Moura
12451e4a35
feat(frontends/lean/pp): display implicit arguments when expression contains metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 12:42:05 -08:00
Leonardo de Moura
35bacf95fc
feat(shell): provide the default environment when parsing Lua files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 18:21:14 -08:00
Leonardo de Moura
582569b793
feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 16:46:53 -08:00
Leonardo de Moura
65bdb9c7e0
fix(frontends/lean): unprotected call to Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 19:56:20 -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
a339a53f50
feat(util/options): 'verbose' as a system option, add -q (quiet) option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 15:31:58 -08:00
Leonardo de Moura
2179e57db3
refactor(builtin): move if_then_else to its own module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 14:08:39 -08:00
Leonardo de Moura
fdeb457a81
feat(kernel/pos_info_provider): add support for file names in pos_info_provider
...
The idea is to include the file name when displaying justification objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:19:30 -08:00
Leonardo de Moura
84e211b81b
fix(frontends/lean): missing ':' in error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4
feat(frontends/lean): include filename in error messages, use GNU error message style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:01:27 -08:00
Leonardo de Moura
57c0006916
chore(*): cleanup lean builtin symbols, replace :: with _
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00
Leonardo de Moura
048151487e
feat(kernel): use Pi as forall/implication
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 00:38:39 -08:00
Leonardo de Moura
6f4ca7bd2a
feat(frontends/lean): expose is_explicit function in the Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 17:36:27 -08:00
Leonardo de Moura
a3af87f8d3
chore(frontends/lean/frontend): remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:28:21 -08:00
Leonardo de Moura
0363faeec8
fix(frontends/lean/scanner): assertion violation, and add more tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:12:34 -08:00
Leonardo de Moura
fb73514913
fix(frontends/lean/parser): parser aborted if the scanner throws an exception in the first call to scan(); position information was being shown twice for scanner exceptions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:04:30 -08:00
Leonardo de Moura
c7338a8eab
chore(frontends/lean/scanner): remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 14:37:28 -08:00
Leonardo de Moura
0f1737d62c
fix(frontends/lean): more precise position information for infix operators
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 13:19:26 -08:00
Leonardo de Moura
abb9b8af83
fix(frontends/lean): bug in pop::context command, and add new tests for the universe command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 17:14:07 -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
645e748302
feat(frontends/lean): add 'using' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 11:41:14 -08:00
Leonardo de Moura
8c956280d9
chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 11:41:03 -08:00
Leonardo de Moura
935c2a03a3
feat(*): change name conventions for Lean builtin libraries
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 19:21:44 -08:00
Leonardo de Moura
771b099c0c
fix(frontends/lean): must invoke lua GC before closing a scope, reason: we may still have references to the current environment inside of the Lua state object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 16:38:29 -08:00
Leonardo de Moura
4ba097a141
feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 13:06:36 -08:00
Leonardo de Moura
6569b07b7c
feat(frontends/lean/parser): rename 'show' expression to 'have'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 11:25:58 -08:00
Leonardo de Moura
9f08156a73
feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 11:03:35 -08:00
Leonardo de Moura
ce1213a020
feat(frontends/lean): use '(* ... *)' instead of '(** ... **)' for script code blocks
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 10:32:47 -08:00
Leonardo de Moura
028a9bd9bd
feat(frontends/lean/scanner): use Lua style comments in Lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 08:53:27 -08:00
Leonardo de Moura
f5cc2458a9
fix(frontends/lean/parser_calc): missing save calls
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-03 18:26:30 -08:00
Leonardo de Moura
9eb4dc4a81
feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend
...
This commit affects different modules.
I used the following approach:
1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure.
2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads.
3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-03 17:18:23 -08:00
Leonardo de Moura
cf35e7bed7
feat(frontends/lean): add support for disequalities in calculational proofs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 22:47:45 -08:00
Leonardo de Moura
6329d1828d
feat(frontends/lean): reuse name expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 20:08:21 -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
Leonardo de Moura
b81d3309b9
fix(kernel): remove ios hack
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 13:03:25 -08:00
Leonardo de Moura
e714bd7982
feat(frontends/lean): add syntax sugar for applying Subst in calculational proofs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 11:23:55 -08:00
Leonardo de Moura
111949b9be
feat(frontends/lean): calculational proofs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 10:53:14 -08:00
Leonardo de Moura
0cb741285c
chore(*): do not type check imported modules when running .cpp tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 07:11:55 -08:00
Leonardo de Moura
d7493ea86c
refactor(frontends/lean/parser): use std::function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 06:53:34 -08:00
Leonardo de Moura
5540fc861a
refactor(frontends/lean/parser): break parser in smaller chunks
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 06:48:40 -08:00
Leonardo de Moura
7d18e9b32e
refactor(frontends/lean/parser): cleanup
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 04:37:21 -08:00
Leonardo de Moura
43909ca66b
feat(frontends/lean/pp): pretty print SetOpaque command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 13:16:44 -08:00
Leonardo de Moura
770145a361
feat(builtin): use namespaces when defining nat, int and real.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 12:55:09 -08:00
Leonardo de Moura
d633622d90
feat(frontends/lean/parser): namespaces
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 12:28:18 -08:00
Leonardo de Moura
0d815b8594
refactor(kernel/context): hide that the context is implemented using lists
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-31 19:43:50 -08:00
Leonardo de Moura
390a78a8d2
chore(frontends/lean/parser): remove 'Skipped' message
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 15:35:12 -08:00
Leonardo de Moura
08718e33dc
refactor(builtin): only load the kernel and natural numbers by default
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 13:35:37 -08:00
Leonardo de Moura
ecd62a1783
refactor(builtin/basic): rename basic.lean to kernel.lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:46:03 -08:00
Leonardo de Moura
72761f14e4
refactor(library/io_state): move to the kernel
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:20:23 -08:00
Leonardo de Moura
46a8300a2d
refactor(library/arith): move real and special function declarations to .lean files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:02:22 -08:00
Leonardo de Moura
c3bc6afb12
refactor(library/arith): move int and nat declarations to .lean files.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 10:32:14 -08:00
Leonardo de Moura
097b10e424
refactor(kernel/builtin): move builtin declarations to basic
...
There is a lot to be done. We should do the same for Nat, Int and Real.
We also should cleanup the file builtin.cpp and builtin.h.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 22:00:03 -08:00
Leonardo de Moura
dbd122301a
feat(kernel/object): compact object serialization kind ids
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 19:19:24 -08:00
Leonardo de Moura
15621610e9
refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments
...
This commit also fixes bugs in the Alias command.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 17:04:36 -08:00
Leonardo de Moura
a1a5fb101d
feat(frontends/lean): add Alias command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 16:25:45 -08:00
Leonardo de Moura
dfe46b9d25
refactor(kernel/builtin): move definition and axioms to basic.lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 14:01:30 -08:00
Leonardo de Moura
b1efdac07b
feat(frontends/lean/parser): universe declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 13:15:09 -08:00
Leonardo de Moura
411ebbc3c1
refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file
...
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:04:49 -08:00
Leonardo de Moura
41c1010043
feat(frontends/lean/parser): make Import command use binary Lean files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 19:20:04 -08:00
Leonardo de Moura
aee1c6d3f3
feat(kernel): export/import (.olean) binary files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 17:31:35 -08:00
Leonardo de Moura
22bebbf242
feat(kernel/object): serializer for kernel objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 14:39:10 -08:00
Leonardo de Moura
1fd81dd3a1
feat(frontends/lean/parser): disable verbose messages when importing files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 12:24:13 -08:00
Leonardo de Moura
44a31dd8fb
feat(frontends/lean/parser): improve Import command
...
- The extension does not have to be provided.
- It can also import Lua files.
- Hierachical names can be used instead of strings.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 12:05:01 -08:00
Leonardo de Moura
755e8b735f
feat(kernel/expr): serializer for kernel expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 01:23:21 -08:00
Leonardo de Moura
8cf65f354b
fix(frontends/lean/pp): forall and exists pretty printing when used as constants
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 12:50:41 -08:00
Leonardo de Moura
a02c6e70fa
fix(frontends/lean/pp): missing parenthesis around nested forall/exists
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 12:13:36 -08:00
Leonardo de Moura
3f0279b88c
refactor(frontends/lua): replace lean.lua.h with util.lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 19:49:26 -08:00
Leonardo de Moura
a9ee92aa3f
fix(frontends/lean/parser): macro precedence
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 19:17:43 -08:00
Leonardo de Moura
3abfad7a88
feat(frontends/lean/parser): add support for integer arguments in macros
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 18:51:37 -08:00
Leonardo de Moura
f1b97b18b4
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 15:54:53 -08:00
Leonardo de Moura
ef18cc4a92
fix(frontends/lean/parser): add existing command macros when creating parser object
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:38:14 -08:00
Leonardo de Moura
8e4560a866
feat(frontends/lean/parser): protect imported modules from Lua definitions and macros in the file importing the module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:21:36 -08:00
Leonardo de Moura
ba02132a90
feat(frontends/lean/parser): add command macros
...
The idea is to allow users to define their own commands using Lua.
The builtin command Find is now written in Lua.
This commit also fixes a bug in the get_formatter() Lua API.
It also adds String arguments to macros.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:00:28 -08:00
Leonardo de Moura
480781d13e
feat(frontends/lean/parser): provide environment as an argument to macros, allow macros to parse tactics
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 11:15:45 -08:00
Leonardo de Moura
3673f2ac1d
feat(frontends/lean/parser): add Find command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 18:31:52 -08:00
Leonardo de Moura
a3dde29f3c
feat(frontends/lua/parser): allow users to specify the precedence of macros
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 12:27:56 -08:00
Leonardo de Moura
f418491c70
fix(frontends/lua/parser): typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 12:03:04 -08:00
Leonardo de Moura
8e45064f25
feat(library/tactic/apply_tactic): improved parametric apply_tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 22:40:34 -08:00
Leonardo de Moura
75cf751959
feat(library/tactic/apply_tactic): allow apply_tac Lua binding to take expressions as argument
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 16:03:16 -08:00
Leonardo de Moura
879ab6924a
tests(test/lean): remove 'Importing...' message, the tests using the Import command fail when running on a different machine
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 12:26:53 -08:00
Soonho Kong
de018220e1
feat(*): use std::make_shared to create shared_ptr
2013-12-24 14:32:50 -05:00
Leonardo de Moura
00e89190c2
refactor(library/cast): use .lean file instead of .cpp file to define casting library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 22:04:19 -08:00
Leonardo de Moura
d5dc5cb576
feat(frontends/lean/parser): use LEAN_PATH in the Import command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 22:00:44 -08:00
Leonardo de Moura
8c8cefcb0c
feat(frontends/lean/parser): compact definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 21:24:50 -08:00
Leonardo de Moura
5043cc75f6
fix(frontends/lean/parser): allow parenthesis in level expressions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 13:31:55 -08:00
Leonardo de Moura
5244ccafe8
fix(frontends/lean/parser): readline compilation problem on Fedora19
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 13:12:39 -08:00
Leonardo de Moura
7c05eb4695
fix(frontends/lean/parser): make sure Lean passes all tests when being compiled with the readline library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 12:57:25 -08:00
Leonardo de Moura
f0833b6f46
chore(frontends/lua/lean.lua.h): fix style warnings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 21:34:20 -08:00
Leonardo de Moura
e91fdaed00
refactor(frontends/lean): rename lean.lua to lean.lua.h
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 20:16:31 -08:00
Leonardo de Moura
baf99779dc
feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 17:57:51 -08:00
Leonardo de Moura
3e32d9bef2
feat(library/tactic): add support for Pi's at to_proof_state
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 16:40:55 -08:00
Leonardo de Moura
21d244d880
feat(frontends/lean/parser): allow tactic to be used to fill holes in definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 12:08:25 -08:00
Leonardo de Moura
4229e498d2
refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 11:51:38 -08:00
Leonardo de Moura
9bac91f5ef
fix(frontends/lean): libreadline support
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 18:57:15 -08:00
Leonardo de Moura
9128a437b8
refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 18:23:37 -08:00
Leonardo de Moura
df58eb132e
feat(frontends/lean): simplify explicit version names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 17:05:25 -08:00
Leonardo de Moura
ce84fe5d33
feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 22:00:50 -08:00
Leonardo de Moura
bb81311e0a
feat(frontends/lean/parser): include proof state in exception for tactic failure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 17:15:12 -08:00
Leonardo de Moura
7772c16033
refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
...
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 12:47:47 -08:00
Leonardo de Moura
96ea8b81c8
feat(frontends/lean/parser): change show-expression binder name
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 01:30:18 -08:00
Leonardo de Moura
c730dd7872
feat(frontends/lean/parser): propagate position information to expressions created by macro implemented in Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 01:07:37 -08:00
Leonardo de Moura
3eb4de6760
fix(frontends/lean/parser): fix deadlock in macro parser
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 21:40:00 -08:00
Leonardo de Moura
c77464703f
feat(frontends/lean): macro definition using Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 19:08:10 -08:00
Leonardo de Moura
d9e692f506
feat(frontends/lean): improve coercion manangement
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:45:46 -08:00
Leonardo de Moura
f43db96e1f
fix(frontends/lean/pp): pretty printer for Type
...
Add parenthesis around Type when it has a universe.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:24:45 -08:00
Leonardo de Moura
ae01d3818d
fix(frontends/lean/parser): parse_type method
...
The parser had a nasty ambiguity. For example,
f Type 1
had two possible interpretations
(f (Type) (1))
or
(f (Type 1))
To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis.
Examples:
(Type 1)
(Type U)
(Type M + 1)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:24:34 -08:00
Leonardo de Moura
d3d24696f4
feat(frontends/lean): hide builtin object in the 'Show Environment' command
...
The user can still display builtin objects by using
Show Environment all
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:00:58 -08:00
Leonardo de Moura
ad3f771b1d
feat(frontends/lean): hide 'explicit' version of objects with implicit arguments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 13:12:39 -08:00
Leonardo de Moura
bff5a6bfb2
fix(frontends/lean/pp): make sure pp and parser are using the same precedences
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 12:46:14 -08:00
Leonardo de Moura
dd72269b13
feat(frontends/lean): rename command Set to SetOption
...
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 21:18:48 -08:00
Leonardo de Moura
d7886c4f5f
doc(examples/lean): new example
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 21:03:16 -08:00
Leonardo de Moura
8cfe5cf9ed
fix(frontends/lean/pp): pretty printer was ignoring notation decls in the local scope
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 18:00:37 -08:00
Leonardo de Moura
79fa6e4940
feat(frontends/lean): Scopes in the default Lean frontend
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 17:40:21 -08:00
Leonardo de Moura
97b872a05c
refactor(frontends/lean): remove frontend class, it is not needed anymore
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 14:37:55 -08:00
Leonardo de Moura
2aaa9a5273
feat(frontends/lean/parser): change function application precedence
...
Now, we can write
Pi (x y : A), R x y -> R y x
instead of
Pi (x y : A), (R x y) -> (R y x)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 12:44:15 -08:00
Leonardo de Moura
47c7bb1bde
refactor(*): uses aliases for unordered_map and unordered_set
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 12:30:45 -08:00
Leonardo de Moura
1e4fa76a47
feat(util/name_map): add template alias
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 11:34:40 -08:00
Leonardo de Moura
418623b874
feat(kernel/replace_fn): add template replace that captures commonly used pattern
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 18:31:59 -08:00
Leonardo de Moura
af42078205
fix(kernel): incorrect use of scoped_map
...
This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 15:11:39 -08:00
Leonardo de Moura
2fee2def72
feat(library/basic_thms): simplify DoubleNegElim
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 13:19:19 -08:00
Leonardo de Moura
de53e92de8
feat(library/basic_thms): add ExistsElim theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 12:43:34 -08:00
Leonardo de Moura
8f5c2b7d9f
feat(library/basic_thms): add Refute theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 12:03:31 -08:00
Leonardo de Moura
19ad39159e
feat(library/basic_thms): add ForallIntro theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 17:35:31 -08:00
Leonardo de Moura
82dfb553d5
feat(library/basic_thms): add ExistsIntro theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 16:26:23 -08:00
Leonardo de Moura
160a8379ef
feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed
...
The modifications started at commit 1852c86948
made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:
[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0 , inst:1 #2 , inst:2 #4 , inst:3 #6 , inst:5 #5 , inst:6 #7 , inst:7 #9 , inst:9 #9 , inst:10 #11 , inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1 , inst:2 #3 , inst:3 #5 , inst:4 #7 , inst:6 #6 , inst:7 #8 , inst:8 #10 , inst:10 #10 , inst:11 #12 , inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a
After the changes, only very simple constraints are generated. The most complicated one is:
[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:59:35 -08:00
Leonardo de Moura
02ee31b786
feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:41:50 -08:00
Leonardo de Moura
51aee83b70
refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env
...
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.
example showing that the approach for caching metavar_env is broken in the type_checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 18:59:15 -08:00
Leonardo de Moura
2e5e5e187f
chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-13 15:01:24 -08:00
Leonardo de Moura
f97c260b0b
refactor(kernel/environment): add ro_environment
...
The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
environment rw_env(env);
Now, f can use rw_env to update env.
To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.
ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-12 16:48:34 -08:00