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

370 commits

Author SHA1 Message Date
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
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
7f818ecd92 feat(library): match procedure for higher-order patterns 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:45:24 -08:00
Leonardo de Moura
d4a7d796a5 feat(builtin): prove strong induction theorem, add < theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-10 18:46:33 -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
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
57640ecf19 fix(library/elaborator): array bounds 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 13:18:49 -08:00
Leonardo de Moura
2b2aa228e3 refactor(builtin/kernel): start with small universes 
The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 12:35:00 -08:00
Leonardo de Moura
cfe576f551 fix(library/elaborator): bug in the elaborator 
The elaborator was not handling correctly constraints of the form

    ctx |- ?m << (Pi x : A, B)
    and
    ctx |- (Pi x : A, B) << ?m

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 12:10:50 -08:00
Leonardo de Moura
abf61be8f6 chore(library/tactic): remove imp_tac, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 00:57:04 -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
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
17c4cce89c fix(library/elaborator): remove_detail procedure was keeping a lot of details when typeof_mvar_justification was being used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 13:24:46 -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
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
92c7145d7f feat(kernel/expr): maximize sharing before serializing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 20:03:42 -08:00
Leonardo de Moura
9620b00e24 feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. 
This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator.

For example, suppose we have the constraint

   ctx |- ?M1[inst:0 ?M2] == a

If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions:

        ?M1 == a
    or
        ?M1 == #0 and ?M2 == a

On the other hand, if ?M2 is assigned to b, then we can ignore the second case.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 16:08:38 -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
9c5fa72f56 fix(library/elaborator): avoid unused variable warning in release build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-02 12:40:41 -08:00
Leonardo de Moura
49425f1a5b feat(builtin/Nat): multiplication axioms and theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 21:32:07 -08:00
Leonardo de Moura
b2a8f4118d feat(library/elaborator): process ho-match before normalizing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 14:46:19 -08:00
Leonardo de Moura
7726ccad28 chore(builtin): rename nat, int and real modules to Nat, Int and Real. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 13:52:25 -08:00
Leonardo de Moura
74cae2a154 refactor(library/elaborator): remove hackish rule 
After the recent fixes, the hack in process_metavar is not needed anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 10:55:39 -08:00
Leonardo de Moura
5f29146e0b feat(library/elaborator): use is_convertible for constraints without metavariables in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:14:01 -08:00
Leonardo de Moura
cbd1f98365 fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 03:02:41 -08:00
Leonardo de Moura
49698bd053 chore(library/all): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:37:25 -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
a80fccea93 chore(*): cleanup builtin registration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 12:19:00 -08:00
Leonardo de Moura
2a2f0b0d89 refactor(kernel/builtin): move helper decl macros to a separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:51:30 -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
4401b390fe refactor(library/arith): do not load specialfn by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 11:25:43 -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
37e8738a5f refactor(kernel/expr): value deserializer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 20:47:14 -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
14c3e11289 refactor(kernel/builtin): emove mk_bin_rop and mk_bin_lop to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 15:23:18 -08:00
Leonardo de Moura
df3686634d refactor(kernel/builtin): remove unnecessary predicates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-29 12:20:29 -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
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
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
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
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
88235d2922 feat(library/tactic/apply_tactic): try other solutions produced by the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-25 11:51:27 -08:00