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

330 commits

Author SHA1 Message Date
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
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
6cc57cc4b5 fix(library/tactic/apply_tactic): bug in apply_tac 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 15:54:56 -08:00
Leonardo de Moura
cb95b14332 feat(library/tactic/apply_tactic): improve apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-24 14:23:06 -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
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
104bd990e1 feat(library/tactic): add normalize_tac, eval_tac and trivial_tac 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 14:10:42 -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
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
36b2ec9abb fix(library/cast): bugs in Cast semantic attachment 
TODO: revise cast semantic attachment.
It should be axioms instead of semantic attachments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 16:16:54 -08:00
Leonardo de Moura
aebff0b4d3 fix(library/type_inferer): bug in get_range method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 14:55:07 -08:00
Leonardo de Moura
97145c0f88 fix(library/elaborator): bug in free variable normalization (lift was missing) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 06:41:09 -08:00
Leonardo de Moura
fddcdb8f40 fix(library/elaborator): bug in process_lower 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-21 04:13:14 -08:00
Leonardo de Moura
4d05a8b65b fix(library/tactic/apply_tactic): provide the metavar_env to instantiate, the goal is to avoid add_lift and add_inst local entries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:17:04 -08:00
Leonardo de Moura
1ed4aa391c fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality 
For homogeneous equality, arg #1 is the Type of the lhs/rhs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 14:14:20 -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
812c1a2960 feat(library/elaborator): only expand definitions that are not marked as hidden 
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 02:16:49 -08:00
Leonardo de Moura
cb48fbf3c4 fix(library/elaborator): missing case 
The elaborator was failing in the following scenario:
- Failing constraint of the form
     ctx |- ?m1 =:= ?m2
where
     ?m2 is assigned to ?m1,
     and ?m1 is unassigned.

has_metavar(?m2, ?m1) returns true, and a cycle is incorrectly reported.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 01:39:43 -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
b08c606696 fix(library/io_state): bug in the io_state Lua bindings 
This commit also includes a new test that exposes the problem.
The options in the io_state object were being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 16:39:42 -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
02bd166793 chore(library/basic_thms): fix typo in comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-19 12:22:05 -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
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
10f28c7bec feat(kernel/replace_fn): non-recursive replace_fn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 16:35:39 -08:00
Leonardo de Moura
84bfe2a222 fix(library/elaborator): bug in process_meta_app 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 10:56:20 -08:00
Leonardo de Moura
09b51a0fb7 fix(library/elaborator): missing condition 
The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 17:13:36 -08:00
Leonardo de Moura
91f4ced83b feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 16:41:20 -08:00
Leonardo de Moura
7792561b20 fix(library/type_inferer): another incorrect use of scoped_map 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 15:17:19 -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
8f9405c8b3 fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive 
This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 09:39:02 -08:00
Leonardo de Moura
61bd27ff06 fix(library/elaborator): bug in simple_ho_match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-15 21:48:55 -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
993bea8206 refactor(library/elaborator): improve elaborator state data-structure 
The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:27:08 -08:00