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

239 commits

Author SHA1 Message Date
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
Leonardo de Moura
3457fe5935 chore(kernel): rename read_only_environment and read_write_environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
bbaa83e16a feat(frontends/lean): implement relaxed operator compatibility in the parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 15:42:43 -08:00
Leonardo de Moura
c0b9c7ffc4 refactor(library/io_state): simplify regular/diagnostic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 13:09:35 -08:00
Leonardo de Moura
e0eeb7c8d5 feat(frontends/lean/operator_info): add << for diagnostic and regular streams 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:52:31 -08:00
Leonardo de Moura
90f88acf42 feat(frontends/lean): relax compatible_denotation predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:42:29 -08:00
Leonardo de Moura
abe2cf2fb5 feat(frontends/lean): simplify how implicit parameters are marked 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 12:11:04 -08:00
Leonardo de Moura
78ec4b152b feat(frontends/lean): relax restricitions on parsing applications of functions containing implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 09:48:24 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency 
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:20:26 -08:00
Leonardo de Moura
3ea09daf44 fix(frontends/lean/frontend): is_coercion for environment objects that have parents 
Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:47:00 -08:00
Leonardo de Moura
2a80807fef refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:33:18 -08:00
Leonardo de Moura
340d643d89 fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 16:55:55 -08:00
Leonardo de Moura
da613f67a8 refactor(frontends/lean/pp): replace dangerous frontend reference with a weak_ref to the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 16:42:12 -08:00
Leonardo de Moura
759fcb7b4f refactor(kernel/formatter): hide 'unsafe' constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:39:26 -08:00
Leonardo de Moura
68c2e5cc7d fix(frontends/lean/parser): reachable code 
The new test nbug1.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:22:21 -08:00
Leonardo de Moura
8add5571f1 refactor(library/tactic): remove 'null' tactic, and operator bool tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 15:00:16 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 14:37:38 -08:00
Leonardo de Moura
2f88d6710c feat(kernel/expr): add some_expr and none_expr for building values of type optional<expr> 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 10:34:38 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression 
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 23:21:10 -08:00
Leonardo de Moura
e4dff52d7a refactor(frontends/lean/parser): cleanup method apply_tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:44:47 -08:00
Leonardo de Moura
1ff6013594 fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes 
The test tactic14.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:37:59 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system 
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:11:55 -08:00
Leonardo de Moura
33b72f1dd0 feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 13:09:39 -08:00
Leonardo de Moura
bc3a6a3185 refactor(frontends/lean/parser): cleanup tactic support in the default lean parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 12:15:03 -08:00
Leonardo de Moura
195ea24d71 refactor(kernel/type_checker): pass buffer<unification_constraint> as a pointer 
The idea is to make it an optional parameter independent of metavar_env.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 10:27:11 -08:00
Leonardo de Moura
1df9d18891 feat(frontends/lean): allow 'tactic hints' to be associated with 'holes' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 14:49:39 -08:00
Leonardo de Moura
2ddcc32c1d fix(frontends/lean/notation): change the precedence of '->' 
It should match the precedence of the implication '=>'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 13:23:24 -08:00
Leonardo de Moura
d46cf5fdd5 fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 05:13:29 -08:00
Leonardo de Moura
e6fb6f7d1e feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 20:08:51 -08:00
Leonardo de Moura
1b176204b4 feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 19:03:12 -08:00
Leonardo de Moura
e1d44eec6b fix(frontends/lean/parser): bug in parse_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 17:40:55 -08:00