michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
1710 commits 3 branches 0 tags 28 MiB
Commit graph

320 commits

Author SHA1 Message Date
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