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

1882 commits

Author SHA1 Message Date
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
7b2fea3fab fix(kernel/normalizer): compilation problem with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 08:46:36 -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
23e518001a feat(kernel/normalizer): avoid unnecessary creation of closures for n-ary functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 18:10:13 -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
af4a6c9364 fix(kernel/normalizer): cache problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 14:52:14 -08:00
Leonardo de Moura
33789fad4c fix(kernel/builtin): make sure the if-then-else semantic attachment is not a simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 14:34:40 -08:00
Leonardo de Moura
c53233ea26 fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 14:33:42 -08:00
Leonardo de Moura
836357c65c fix(kernel/normalizer): bug in Let normalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-17 12:35:25 -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
f09fd0fc04 feat(kernel/printer): include de Bruijn index in the debug printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-16 16:56:46 -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
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
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
2253d8079b chore(util/pdeque): remove unused template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:31:44 -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
Leonardo de Moura
5aa9264091 feat(util/list): add remove_last template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 23:08:10 -08:00
Leonardo de Moura
1b1032eb99 feat(util/list): improved filter that reuses list cells 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 20:15:37 -08:00
Leonardo de Moura
bdbf85405a feat(library/elaborator): add extra occurs-check test 
The idea is to catch the inconsistency in constraints such as:

    ctx |- ?m[inst:0 v] == fun x, ?m a x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 19:47:33 -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
70b7e519f8 feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:54:49 -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
3d30664611 feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 15:13:56 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' 
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-14 12:25:00 -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
Soonho Kong
26afc6cf12 fix(cmake): fix problem of using LuaJit on OSX(64-bit) 
http://luajit.org/install.html

If you're building a 64 bit application on OSX which links directly or
indirectly against LuaJIT, you need to link your main executable with
these flags:

    -pagezero_size 10000 -image_base 100000000
 2013-12-13 19:52:40 -05: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
3416df85f8 fix(util/thread): warning 'thread.cpp.o has no symbols' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 14:00:40 -08:00
Leonardo de Moura
fa8b984e27 fix(kernel/environment): compilation warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-13 13:54:45 -08:00
Soonho Kong
46e7802d9a test(library/rewriter): add lambda_{body/type}_rewriter tests 2013-12-13 15:08:23 -05:00
Soonho Kong
5b95cf1e03 fix(shell/lua_repl.h): use loadstring for Lua-5.1 instead of load 2013-12-13 00:13:48 -05:00
Soonho Kong
f90a9e96d0 fix(shell/lean.cpp): fix not to overwrite optind by getopt_long 2013-12-12 23:20:47 -05:00
Leonardo de Moura
ae52c8062e chore(kernel/metavar): remove unused function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:39:14 -08:00
Leonardo de Moura
450d6a4b1e refactor(util/splay_tree): replace find with splay_find 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 17:27:30 -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
7b2cbd6926 chore(kernel/environment): remove implementation hack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:34 -08:00
Leonardo de Moura
7d184c3c4b fix(util/shared_mutex) missing pragma 
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
1852c86948 feat(kernel): improve instantiate and lift_free_vars (use metavar_env to minimize the number of lift and inst local_entries needed) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
058bdb88ac feat(kernel/context): add operator== for contexts, and new constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
38a25a1bd2 feat(kernel/metavar): (re-)enable add_lift simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 16:48:33 -08:00
Leonardo de Moura
6ed62247b0 chore(memcheck.supp): generalize Memcheck:Addr4 suppression for LuaJIT, there many warnings of this kind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-12 09:24:15 -08:00
Leonardo de Moura
98f5ce0512 fix(kernel/context): unused var warning in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 21:24:05 -08:00
Leonardo de Moura
3e77dd0c42 fix(kernel/context): make context remove more robust 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:51:57 -08:00
Leonardo de Moura
f728f80960 fix(library/elaborator): remove is_neutral_abstraction hack, and bug at process_metavar_lift_abstraction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:41:24 -08:00
Leonardo de Moura
8f67348c05 fix(library/elaborator): remove nasty hack, this hack was throwing away the local context at process_meta_app_core 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 19:27:21 -08:00
Leonardo de Moura
c29b155fdd feat(library/elaborator): use improved has_free_vars in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 16:15:20 -08:00
Leonardo de Moura
0e2b7973cf feat(kernel/free_vars): improve has_free_vars function, it produces better results for expressions containing metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 16:09:33 -08:00
Leonardo de Moura
af1b0d2e81 feat(library): add function free_var_range for computing the range [0, R) of free variables occurring in an expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 15:32:50 -08:00
Leonardo de Moura
1d33d3b5db fix(library/elaborator): the context of auxiliary metavariables created in the imitation step was incorrect 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 12:35:32 -08:00
Leonardo de Moura
55389cf6e5 feat(kernel/context): add find, a version of lookup that does not throw an exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-11 09:54:54 -08:00
Leonardo de Moura
cdec9762ce chore(util/pvector): remove unused template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 20:32:10 -08:00
Leonardo de Moura
f8e87436a7 perf(library/elaborator): avoid exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:40:59 -08:00
Leonardo de Moura
4de5f06a97 fix(library/elaborator): bug in process_metavar_inst, and disable simplification that is negatively impacting the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 19:26:58 -08:00
Leonardo de Moura
5ae71e75bd perf(library/elaborator): avoid exception 
Lean was spending 17% on the runtime "throwing exceptions" in the test tests/lean/implicit7.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 16:31:36 -08:00
Leonardo de Moura
1fb526a3d4 perf(library/type_inferer): improve is_proposition performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 16:18:45 -08:00
Leonardo de Moura
b270fb0030 refactor(library/elaborator): remove synthesizer 
Synthesizer is not part of the elaborator anymore.
The elaborator fills the "easy" holes.
The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 15:55:54 -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
88f80c9693 fix(shell): add 'file not found' error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-10 10:55:13 -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
7ab321f568 chore(util): remove dead file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:32:11 -08:00
Leonardo de Moura
0cd8e3e76b feat(split-stack): add support for split-stacks (no more stackoverflows) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:30:54 -08:00
Leonardo de Moura
fd2a04e9ac fix(util/stackinfo): bug on Fedora 
Signed-off-by: Leonardo de Moura <leonardo@nod1-2008.corp.crtest.com>
 2013-12-09 18:44:14 -08:00
Leonardo de Moura
e3403492a5 feat(build): -D STATIC=ON option for building a static Lean executable 
On Linux, -D STATIC=ON does not work if MULTI_THREAD support is enabled.
If we search for "pthread static crash" we find other projects with the same problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 18:02:10 -08:00
Leonardo de Moura
0b1789edf2 feat(shell): add command line option to set thread stack size (only available if using Boost) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:33:47 -08:00
Leonardo de Moura
e7ae749221 feat(boost): implement multi-threading support using Boost 
To use Boost instead of the standard library, we must use the cmake option
    -D BOOST=ON

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:24:32 -08:00
Leonardo de Moura
533ed51f51 feat(util/shared_mutex): skip shared_mutex implementation if LEAN_MULTI_THREAD is not defined 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:42:08 -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
0eaa98221b fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 12:25:19 -08:00
Leonardo de Moura
0d10cba4a0 refactor(util/sexpr/format): minimize the use of recursion, combine be and layout into a single procedure (without creating a temporary potentially big sexpr) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 21:06:24 -08:00
Leonardo de Moura
25a2f5f7e0 fix(kernel/formatter): clang++ errors and warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 18:54:04 -08:00
Leonardo de Moura
445d4f6793 refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 18:11:35 -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
a4afdfeace refactor(kernel/expr): remove the dangerous expr::release method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 14:45:18 -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
25b812f1c9 feat(kernel/expr): no overhead optional<expr> template specialization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 10:17:29 -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
b6b520302d feat(kernel/replace_visitor): relax replace_visitor contract, the input expression can be null 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:35:26 -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
5f3b9dbbbd fix(library/fo_unify): unify (?f ?x) with (g a b) 
We flat applications. So, (g a b) is actually ((g a) b).
So, we must be able to unify (?f ?x) with (g a b).
Solution:
        ?g <- (g a)
        ?x <- b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 10:25:11 -08:00
Leonardo de Moura
015bff8283 fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term 
This commit fixes a problem exposed by t13.lean.
It has a theorem of the form:

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form

 [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A

The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type).
Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions.
Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created
     A : Bool, B : Bool, assumption : A /\ B |- B /\ A
That is, the lemmas are not available when solving B /\ A.
Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used.

    Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
            let lemma1 := Conjunct1 assumption,
                lemma2 := Conjunct2 assumption
            in Conj (Conjunct2 assumption) (Conjunct1 assumption)

This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal
     A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A

After this commit, the proof for theorem T1 is

Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
    let lemma1 := Conjunct1 assumption,
        lemma2 := Conjunct2 assumption
    in Conj lemma2 lemma1

as expected.

Finally, this example suggests that the encoding

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 : A := (by auto),
              lemma2 : B := (by auto)
          in (show B /\ A by auto)

is more efficient than

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:14:25 -08:00
Leonardo de Moura
bd9df3b08f fix(library/tactic/goal): null hypothesis being added by to_goal 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:03:06 -08:00
Leonardo de Moura
872434e632 fix(kernel/has_free_vars): return false for null expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 16:01:57 -08:00
Leonardo de Moura
147626c906 fix(kernel/printer): memory access violation when printing contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 15:50:29 -08:00
Leonardo de Moura
0390f3c39b feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 15:01:54 -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
d79a626523 fix(kernel/type_checker): Pi with metavariables case 
The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 13:07:59 -08:00
Leonardo de Moura
fa03ae2a26 fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints 
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 13:04:34 -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
c841763a05 feat(library/elaborator): add special treatment for constraints of the form ?m[inst:i v] << t, where t is a proposition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 04:51:07 -08:00
Leonardo de Moura
4e4fea1eca fix(examples/lean): add all examples to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 21:54:55 -08:00
Leonardo de Moura
13f9454fe1 feat(library/tactic/proof_state): add option tactic::proof_state::goal_names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 21:18:22 -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
0c059a9917 feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 20:06:32 -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
c1afefb873 feat(library/fo_unify): unify heterogeneous - homogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 19:00:31 -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
Leonardo de Moura
a564795fe6 fix(frontends/lean/parser): remove unnecessary '#' after error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 17:27:08 -08:00
Leonardo de Moura
e069ce640b feat(frontends/lean/parser): add tactic abort command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 17:15:19 -08:00
Leonardo de Moura
34654ad06b feat(tests/lean/interactive): add interactive mode test script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 16:56:20 -08:00
Leonardo de Moura
e3848d43a2 feat(frontends/lean): improve tactic command parsing in interactive mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 16:28:08 -08:00
Leonardo de Moura
a1b5a8e50f fix(frontends/lean): check wheter the synthesized proof term has metavars or not 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 14:22:19 -08:00
Leonardo de Moura
873a07d34c feat(kernel/replace_visitor): check interrupted flag and stackoverflow 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 05:42:12 -08:00
Leonardo de Moura
43ef8b9a4b refactor(library/tactic): rename boolean.* to boolean_tactics.* 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 05:03:18 -08:00
Leonardo de Moura
fa98c1358f feat(library/tactic): add disj_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 04:49:06 -08:00
Leonardo de Moura
056759880c feat(frontends/lean): add back (backtracking) command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 04:39:08 -08:00
Leonardo de Moura
029ef57abd feat(library/tactic): add apply_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 03:22:12 -08:00
Leonardo de Moura
7b4ea75dee fix(frontends/lean): do not display Ctrl-D message on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 11:39:30 -08:00
Leonardo de Moura
d949dfd46d fix(util/stackinfo): compilation warning on cygwin/mingw 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 11:32:39 -08:00
Leonardo de Moura
1e5518002b feat(shell/lean): add git hash to executable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 11:23:15 -08:00
Leonardo de Moura
e60e20a11d feat(frontends/lean): add Exit command 
Remark: on Windows, Ctrl-D does not seem to work.
So, this commit also changes the Lean startup message.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 10:40:22 -08:00
Leonardo de Moura
fa35fd6989 chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly 
When LEAN_THREAD_UNSAFE=ON, we:

- Do not run tests at tests/lua/threads
- Disable thread object at Lua API
- par tactical becomes an alias for interleave
- Disable some unit tests that use threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 10:27:22 -08:00
Leonardo de Moura
1a02abf7b2 feat(util/script_state): add a lua hook function that checks for the interrupt flag 
This is a very convenient feature for interrupting non-terminating user scripts.
Before this commit, the user had to manually invoke check_interrupt() in potentially expensive loops. Now, this is not needed anymore.

Remark: we still have to check whether this trick works with LuaJIT or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 09:57:36 -08:00
Leonardo de Moura
ef6a27fe84 feat(util/script_state): add join method to Lua threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 09:15:09 -08:00
Leonardo de Moura
def186a9cd fix(util/stackinfo): try to fix incorrect main thread stack size on OSX 
This fix tries to fix two failures on our unit tests.
     tests/kernel/normalizer
     tests/kernel/type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 08:56:46 -08:00
Leonardo de Moura
d481cb251d chore(memcheck): add another suppression for LuaJIT 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 08:32:44 -08:00
Leonardo de Moura
fd9781d58d fix(util/stackinfo): compilation warning on mingw and cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 08:26:50 -08:00
Leonardo de Moura
ef069e39b0 chore(*): replace to_expr with to_nonnull_expr (when appropriate) 
The goal is to make the Lua API more robust.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:53:53 -08:00
Leonardo de Moura
bcc8b67592 chore(*): consistent file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:40:52 -08:00
Leonardo de Moura
8e53643b61 feat(library/fo_unify): first order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:21:21 -08:00
Leonardo de Moura
f80106a895 chore(*): use 'explicit operator bool' everywhere. 
operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 23:02:45 -08:00
Leonardo de Moura
d79b2babd3 fix(*): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 08:46:47 -08:00
Leonardo de Moura
dd62af1641 feat(frontends/parser): simplified theorem definition using tactical proof 
When using tactics for proving theorems, a common pattern is

     Theorem T : <proposition> := _.
          apply <tactic>.
          ...
          done.

This commit allows the user to write the simplified form:

     Theorem T : <proposition>.
          apply <tactic>.
          ...
          done.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 08:20:18 -08:00
Leonardo de Moura
25978118df feat(library/tactic): add beta-reduction tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 08:10:51 -08:00
Leonardo de Moura
39b99683a8 fix(util/stackinfo): handle error codes in the Linux version 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 07:56:53 -08:00
Soonho Kong
31b26f53ad fix(util/stackinfo): fix typo 2013-12-02 00:03:57 -05:00
Soonho Kong
7776f4b24b fix(util/stackinfo): fix preprocessor directive 2013-12-01 23:44:58 -05:00
Soonho Kong
4de3b772fd feat(util/stackinfo): implement get_stack_size (Mac OSX version) 2013-12-01 22:24:12 -05:00
Soonho Kong
a2d6918348 fix(library/rewriter): use Abst axiom in lambda_body RW 2013-12-01 22:24:12 -05:00
Soonho Kong
0553d29078 test(library/rewriter): add lambda_rewrite tests 2013-12-01 22:24:12 -05:00
Leonardo de Moura
75f8d56eb1 fix(util/stackinfo): memory leak at get_stack_size 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 19:17:28 -08:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space 
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 17:19:27 -08:00
Leonardo de Moura
1ec8f9d536 feat(kernel): add abstraction (aka function extensionality) axiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 13:57:14 -08:00
Leonardo de Moura
09f98ecddc feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:41:05 -08:00
Leonardo de Moura
70e06f8e86 feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:27:27 -08:00
Leonardo de Moura
ca53a5a1cc feat(library/tactic): add unfold tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 08:51:56 -08:00
Leonardo de Moura
737e634556 fix(util/list): bug in map template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 08:51:24 -08:00
Leonardo de Moura
568931ccb1 refactor(library/tactic): remove duplicate code, add add_proofs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:01 -08:00
Leonardo de Moura
f91c4901e8 feat(library/tactic): add absurd_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:00 -08:00
Leonardo de Moura
bf2adb20e7 feat(library/tactic): add disj_hyp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 07:55:00 -08:00
Soonho Kong
6a6b69ddf4 test(library/rewriter): add test for depth RW 2013-12-01 01:59:21 -05:00
Soonho Kong
064e3fe20d refactor(library/rewriter): rename lc => ti 2013-12-01 01:59:20 -05:00
Soonho Kong
506cca0ac1 feat(library/rewriter): implement depth RW 2013-12-01 01:59:20 -05:00
Soonho Kong
ae0508128f refactor(library/rewriter): move apply_rewriter_fn into rewriter.h 2013-12-01 00:57:09 -05:00
Soonho Kong
d7ba5e3893 doc(library/rewriter): add doxygen annotations for rewrite_* funcs 2013-12-01 00:47:53 -05:00
Leonardo de Moura
1a221d8bbe feat(library/tactic): add focus tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
7ff791eb9f feat(util/name_set): add mk_unique (with respect to a name_set) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
6da13cc245 feat(util/list): map_append template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
fe79bbf2b7 feat(util/list): filter template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Soonho Kong
f205dd0763 fix(library/rewriter): unused variable warnings 2013-11-30 07:05:18 -05:00
Leonardo de Moura
83aaf64318 fix(library/tactic): memory leaks 
Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.

To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:44:39 -08:00
Leonardo de Moura
2372567a6e fix(util/luaref): warnings produced by valgrind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:34:38 -08:00
Leonardo de Moura
a7027a1d00 feat(library/tactic): polish tactic API, and add new example showing how to implement tactics using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 00:16:39 -08:00
Soonho Kong
aed8b1fc73 fix(tests/library/rewriter): app_rewriter1_tst 
There was a bug in the app_rewriter1_tst. If we apply the ADD_COMM RW to
f(0), then the result should be f(0) since there is nothing to do for
ADD_COMM.

    f(0) = f(0)

The proof for this equality should be Refl(Nat, f(0)). But it was

    Refl(Nat -> Nat, f)

which is wrong. Somehow, the previous kernel didn't detect this type
mismatch and recent changes of the kernel found the problem.

I fixed the bug and re-enable the test as it was.
 2013-11-30 02:25:30 -05:00
Soonho Kong
f5f7380fbe feat(library/rewriter): add apply_rewriter_fn which will be used in depth RW 2013-11-30 02:25:30 -05:00
Soonho Kong
1d76a6f71d feat(library/rewriter): add rewrite_* functions 
rewrite_* functions take the rewriting results of the sub-components and
construct the rewriting result for the main component.

For instance, rewrite_app function takes env, ctx, and the value v s.t.

v = (e_0 e_1 ... e_n)

and the rewriting results for e_i's as a vector(buffer)

(e'_0, pf_0 -- proof of e_0 = e'_0)
(e'_1, pf_1 -- proof of e_1 = e'_1)
...
(e'_n, pf_n -- proof of e_n = e'_n).

Then rewrite_app function construct the new v'

v' = (e'_0 e'_1 ... e'_n)

and the proof of v = v' which is constructed with pf_i's.

These functions are used in the component rewriters such as app_RW and
let_type_RW, as well as more complicated rewriters such as depth
rewriter.
 2013-11-30 02:25:29 -05:00
Leonardo de Moura
a9eb2a9307 feat(kernel/builtin): add is_* functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 11:35:58 -08:00
Leonardo de Moura
18eb9e427f fix(library/tactic): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 10:35:14 -08:00
Leonardo de Moura
98897b467d feat(frontends/lean/parser): add support for Lua expression code blocks 
In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write

apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)

instead of

apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 10:21:24 -08:00
Leonardo de Moura
f9874cd675 feat(library/tactic): add to_tactic_ext, it allows functions that return tactics to be used where a tactic is expected 
For example, after this commit, we can write

simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic

instead of

simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 09:40:21 -08:00
Leonardo de Moura
20a36e98ec feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. 
Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.

For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))

Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:

[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

Now, ?M::1 is assigned to the term
     if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

This is bad, since the original structure was lost.

This commit also contains an example that only works after the commit is applied.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 09:15:01 -08:00
Leonardo de Moura
066dacea31 feat(library/tactic): add show_tactic, and optional '.' in the end of tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-29 01:33:26 -08:00
Leonardo de Moura
b3f87e2e4f feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 22:11:07 -08:00
Leonardo de Moura
6832b265e9 style(frontends/lean/parse): missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:50:55 -08:00
Leonardo de Moura
5dfb3b8b56 feat(frontends/lean/parse): allow script-code blocks to be used in the apply command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:48:30 -08:00
Leonardo de Moura
67def8da21 fix(library/type_inferer): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:47:29 -08:00
Leonardo de Moura
dae86c2ffa feat(frontends/lean/parser): add basic tactic support in the frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:08:12 -08:00
Leonardo de Moura
73bbf67702 refactor(library/elaborator): simplify synthesizer interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 19:00:48 -08:00
Leonardo de Moura
c6b05bcfcb feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 18:23:38 -08:00
Leonardo de Moura
e3f3ec5553 feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 18:17:15 -08:00
Leonardo de Moura
d36a91e145 feat(library/tactic): expose COND and WHEN tacticals in Lua, add HOL-like tactical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 17:57:24 -08:00
Leonardo de Moura
ff052d41ee chore(*): fix cygwin compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:49:18 -08:00
Leonardo de Moura
ce674d2d43 feat(library/tactic): execute Lua tactics using coroutines 
This is very important when several Lua tactics are implemented in the
same Lua State object.  In this case, even if we use the par
combinator, a Lua tactic will block the other Lua tactics running in
the same Lua State object.

With this commit, a Lua tactic can use yield to allow other tactics
in the same State object to execute.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:09:33 -08:00
Leonardo de Moura
6cb8300076 doc(lua): add S-expression documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 10:33:32 -08:00
Leonardo de Moura
09bc7ddf91 feat(library/tactic): add support for migratic tactic framework object between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 08:03:05 -08:00
Leonardo de Moura
3dc7a856f0 refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 18:11:46 -08:00
Leonardo de Moura
b4a8418d38 feat(library/tactic): expose tactics in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 17:47:29 -08:00
Leonardo de Moura
55f86f79a8 fix(util/optional): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 16:57:29 -08:00
Leonardo de Moura
a2aa90ae66 refactor(util/script_state): replace std::recursive_mutex with std::mutex, and use unlock_guard 
The unlock_guard and exec_unprotected will be useful also for implementing the Lua tactic API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 15:40:41 -08:00
Leonardo de Moura
b038636ff5 refactor(util/script_state): remove unsafe unguarded_apply 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 15:14:26 -08:00
Leonardo de Moura
75b4a96d0e chore(tests/lua/threads): break lua thread tests into individual tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 15:06:07 -08:00
Leonardo de Moura
f7e8545e97 refactor(frontends/lua): rename leanlua_state to script_state, and move it to util 
This commit also minimizes the dependencies of script_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 14:57:36 -08:00
Leonardo de Moura
0934d7b2f4 fix(frontends/lua): make sure Lua 'sleep' function support interruption 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 13:25:06 -08:00
Leonardo de Moura
3a93212d5e chore(kernel/expr): fix cpplint warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 12:59:16 -08:00
Leonardo de Moura
e737f501e4 fix(frontends/lua): remove unnecessary function reference 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 12:58:35 -08:00
Leonardo de Moura
262670abd6 fix(frontends/lua/leanlua_thread): propagate C++ thread over Lua thread boundaries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 12:49:12 -08:00
Leonardo de Moura
d87ad9eb7e refactor(util/lua): propagate C++ Lean exceptions in Lua 
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 12:25:29 -08:00
Leonardo de Moura
a6f6f49b5f refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular 
copy_values is not a big if-then-else anymore.
Before this change, whenever we added a new kind of userdata, we would have to update copy_values.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 10:32:19 -08:00
Leonardo de Moura
4c323093ac refactor(frontends/lua/leanlua_state): minimize the use of 'friend' directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 09:25:56 -08:00
Leonardo de Moura
4c5ec53a44 chore(util/lua): remove dead code 
I removed lua_module helper class because it does not work.
The problem is that the linker may eliminate ignore a object file that contains a lua_module global object used for initialization. When this happens, the associated Lua bindings will not be exposed in the Lua API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:36:32 -08:00
Leonardo de Moura
feca9dbdf8 refactor(bindings/lua): move to frontends/lua 
Lua API is an integral part of Lean. It does *not* have the same status
of external APIs (e.g., Python) we will add in the future.

We will reserve the directory bindings for external APIs for using Lean
as a library.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:30:07 -08:00
Leonardo de Moura
fb06a2b1df refactor(bindings/lua/leanlua_state): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:24:18 -08:00
Leonardo de Moura
956f203a55 refactor(bindings/lua): move Lua bindings to the file associated with them 
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:15:56 -08:00
Leonardo de Moura
99a811a586 feat(bindings/lua): expose io_state object in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 12:54:47 -08:00
Leonardo de Moura
861be072d8 feat(bindings/lua): add proof_state to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:58 -08:00
Leonardo de Moura
4e66a2e14a fix(library/tactic/goal): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:58 -08:00
Leonardo de Moura
b41789d085 feat(kernel): add is_bool predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:50 -08:00
Leonardo de Moura
fd3b9e39f6 feat(bindings/lua): add cex_builder to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 09:17:57 -08:00
Leonardo de Moura
4d9075bdfd feat(bindings/lua): add proof_map, assignment and proof_builder to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 08:37:37 -08:00
Leonardo de Moura
3ebc099ec5 feat(bindings/lua/options): improve options Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 21:05:05 -08:00
Leonardo de Moura
feeb6d9105 feat(bindings/lua): add goal object to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 20:51:47 -08:00
Leonardo de Moura
e29a2f4d11 chore(util/interrupt): improve comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 17:23:36 -08:00
Leonardo de Moura
4eb62fef91 fix(util/interrupt): fix nasty bug on interruptible_thread, it seems to occur only on cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 17:14:22 -08:00
Leonardo de Moura
c22f863114 refactor(library/tactic): improve solve method 
Now, it produces the following outcomes:
1- A proof
2- A counterexample
3- A list of (unsolved) final states

Remark: the solve method does not check whether the proof or counterexample is correct.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 13:04:12 -08:00
Leonardo de Moura
9a8ea0c735 feat(library/tactic): add precision and counterexample builder to proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 11:43:16 -08:00
Leonardo de Moura
ccaa272f9a refactor(library/tactic): simplify proof_builder API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:50:33 -08:00
Leonardo de Moura
500ed7a05b refactor(library/tactic): remove dead code, make proof_state a smart pointer, cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:39:40 -08:00
Leonardo de Moura
5af648030d chore(memcheck.supp): hide another false positive at luajit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:07:40 -08:00
Leonardo de Moura
2c65fdb346 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 01:06:34 -08:00
Soonho Kong
03791b099c chore(ctest): fix typo in CTEST_DROP_LOCATION 2013-11-25 03:14:35 -05:00
Soonho Kong
ac5a061f2a chore(ctest): use CDash server located at borel.modck.cs.cmu.edu 2013-11-25 02:48:04 -05:00
Leonardo de Moura
9dcfa03dd2 feat(library/tactic): add conj_hyp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 21:00:38 -08:00
Leonardo de Moura
d75bd2ae98 feat(library/tactic/proof_state): remove goal name when pretty printing the proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 20:22:47 -08:00
Leonardo de Moura
48d7afb0e8 feat(library/tactic): add trace_state_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:44:02 -08:00
Leonardo de Moura
6f05276acd refactor(library/tactic): remove unnecessary tactic_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:31:49 -08:00
Leonardo de Moura
9c42a05b08 feat(library/tactic): add conj_tactic and imp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:29:04 -08:00
Leonardo de Moura
1c607f3350 feat(library/tactic): add cond and when tacticals. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 12:04:32 -08:00
Leonardo de Moura
40d612eca0 feat(library/tactic): add repeat1 and determ tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:38:51 -08:00
Leonardo de Moura
cb7a5288c5 refactor(library/tactic): minimize the amount of copying in the tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:27:06 -08:00
Leonardo de Moura
22c49146ae feat(library/tactic): refine repeat and repeat_at_most tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:18:32 -08:00
Leonardo de Moura
8e87ef5da8 feat(util/lazy_list): add repeat and repeat_at_most templates for lazy_lists 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:16:37 -08:00
Leonardo de Moura
e839787b74 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 00:38:52 -08:00
Leonardo de Moura
b74aeb1216 fix(util/lazy_list): par template missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 00:38:31 -08:00
Leonardo de Moura
4e24dfd5a6 fix(util/optional): move constructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 00:22:02 -08:00
Leonardo de Moura
40a2f0a588 refactor(util/lazy_list): polish lazy_list API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:45:01 -08:00
Leonardo de Moura
9da95dc6e6 style(library/tactic): missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:06:00 -08:00
Leonardo de Moura
bcd88cac08 style(util): missing includes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:05:46 -08:00
Leonardo de Moura
16cf60a04b refactor(library/tactic): modify par and try_for tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:03:59 -08:00
Leonardo de Moura
924187b055 feat(util/lazy_list): add par template for lazy lists) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 16:51:17 -08:00
Leonardo de Moura
157a2b36db feat(lazy_list): add timeout template for lazy_lists 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 16:27:36 -08:00
Leonardo de Moura
cb3c685fb1 feat(util/lazy_list): check for interruption between pulls 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:54:32 -08:00
Leonardo de Moura
d1adfd52e6 feat(library/tactic): add mk_simple_tactic template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:53:45 -08:00
Leonardo de Moura
f19944cf09 refactor(util/lazy_list): 'lazier' lazy_lists 
In the new implementation, even the head of the lazy list is computed on demand.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:33:30 -08:00
Leonardo de Moura
9eb6da2a31 feat(util): add optional template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 13:27:22 -08:00
Leonardo de Moura
18d114416f feat(library/tactic): add take and force tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 17:05:18 -08:00
Leonardo de Moura
d258a4b7b8 feat(library/tactic): add repeat and repeat_at_most tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 16:39:25 -08:00
Leonardo de Moura
8bece1b53d feat(library/tactic): add append, interleave and par tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 16:15:03 -08:00
Leonardo de Moura
df96068caa fix(library/tactic): clean up try_for 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 15:51:17 -08:00
Leonardo de Moura
9fd594533d refactor(library/tactic): simplify tactic framework, add orelse and try_for combinators/tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 15:46:43 -08:00
Leonardo de Moura
a776c8b158 feat(util/interrupt): add sleep_for, and simplify request_interrupt 
The Lean sleep_for checks the interrupt flag from time to time.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 11:32:12 -08:00
Leonardo de Moura
935349ec91 fix(tests/util/thread): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 10:23:20 -08:00
Leonardo de Moura
1f225d2752 feat(util/lazy_list): add useful lazy_list function templates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 09:40:56 -08:00
Leonardo de Moura
796fb3c3bf refactor(library/tactic): remove justification_builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
41062fdf9f feat(library/tactic): add pretty printer for goal and proof_state objects, add solve method for tactics, add trivial example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
28a56e3acf fix(kernel/expr_eq): the cached type should ignored when comparing expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
5346b67651 refactor(library/state): rename Lean state object to io_state 
The idea is to make it clear that io_state is distinguish it from proof_state, and from leanlua_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
680ec8abba refactor(library/tactic): reorganize tactic API, add assumption_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
ca74d069b9 feat(util/interrupt): reset interrupt flag before throwing exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
8515821d56 feat(util/list): add map_filter template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
f6bfd11aed chore(util/list_fn): fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
df04dbe096 chore(util): use && when appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
63bbf07f64 feat(library/tactic): add 'idtac' tactic and 'then' tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
a03841c18b feat(tactic): refine tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
367108edfa fix(library/tactic): compilation problem reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 08:53:37 -08:00
Leonardo de Moura
f6d1f4db60 chore(library/tactic): remove trash 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 17:25:00 -08:00
Leonardo de Moura
3a6aa2dc75 feat(library/tactic): add tactic framework APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 17:19:05 -08:00
Leonardo de Moura
be8fe1b902 fix(kernel/replace): make it more robust, and add clear method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 13:19:21 -08:00
Leonardo de Moura
87eb254a1a fix(tests/util/thread): incorrect unit test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 11:28:19 -08:00
Leonardo de Moura
b0a4d60174 fix(util/interval): add missing explicit template instantiation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 09:56:19 -08:00
Leonardo de Moura
a3a90f8e69 feat(shell): add command line options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 19:30:39 -08:00
Leonardo de Moura
eba31a0516 test(util/interval): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 19:07:09 -08:00
Leonardo de Moura
7b8bd97699 feat(lua/expr): add method for extracting semantic attachment data 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 19:06:47 -08:00
Leonardo de Moura
f78cf6a415 feat(shell): add getopt 
Let travis find out which platforms support it

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 17:04:55 -08:00
Leonardo de Moura
a98fdd9be6 refactor(shell): combine lean and leanlua executables in a single executable 
The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files.
Example:
        ./lean extension1.lua extension2.lua file.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 16:48:21 -08:00
Leonardo de Moura
2265ef78c4 feat(util/list): add emplace_front 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 16:27:31 -08:00
Leonardo de Moura
20c6789d1c feat(extra): add extension that demonstrates how to parse 'templates' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 15:56:44 -08:00
Leonardo de Moura
6989f1f9ba refactor(kernel/metavar): remove unnecessary variable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 14:41:54 -08:00
Leonardo de Moura
0126fa0499 refactor(kernel): add find_fn, replace for_each_fn with find_fn when appropriate, remove unnecessary function has_cached_type 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 13:03:46 -08:00
Leonardo de Moura
5cfcb7e144 chore(kernel/for_each): use consistent naming convetions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 11:24:02 -08:00
Leonardo de Moura
7f088b7635 feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework 
This field should not be visible in the external API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 11:21:52 -08:00
Leonardo de Moura
9bafa5a9e8 chore(memcheck): suppress memory leak at awk 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 23:50:41 -08:00
Leonardo de Moura
57bf4f3e67 feat(kernel/expr): avoid recursion when deleting expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 18:41:08 -08:00
Leonardo de Moura
2951c92ad1 feat(kernel/for_each): avoid recursion at for_each template 
It saves a lot of stack space.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 18:08:31 -08:00
Leonardo de Moura
e10d17a0f4 feat(util/sexpr): avoid recursion when destructing sexpr's 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 17:46:53 -08:00
Leonardo de Moura
64379a5a10 perf(util/list): use buffer of cells instead of buffer of T 
T may be a big object. We minimize the ammount of copying using buffer of (pointers to) cells.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 17:12:02 -08:00
Leonardo de Moura
76252816ac perf(util/list): avoid recursion in map and destructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 16:47:52 -08:00
Leonardo de Moura
d67bf995ed feat(util/list): avoid recursion at for_each template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 15:52:31 -08:00
Leonardo de Moura
06c004aa75 fix(build): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 15:36:07 -08:00
Leonardo de Moura
adf4856f88 feat(util/list): add map_reuse template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 15:32:02 -08:00
Soonho Kong
20756c382c test(*): split leantests, leanslowtests, leanluatests, leanluadocs into singletons 2013-11-18 18:27:11 -05:00
Leonardo de Moura
53dc8c8c57 test(util/shared_mutex): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 14:03:18 -08:00
Leonardo de Moura
88b2feff6f test(doc/lua): add script for validating examples in the Lua API documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 12:49:57 -08:00
Leonardo de Moura
4d1d3d7cc7 fix(build): cygwin also needs the LEAN_WINDOWS flag 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 12:40:02 -08:00
Leonardo de Moura
bfc4023a9e fix(tests/kernel/expr): remove unused function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 10:09:47 -08:00
Leonardo de Moura
80fccc5533 fix(util/realpath): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:55:16 -08:00
Leonardo de Moura
e0c23e5984 fix(kernel/environment): compilation problem on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:52:47 -08:00
Leonardo de Moura
b2d1acd0b7 test(lua/environment): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:27:46 -08:00
Leonardo de Moura
1315378ebb test(*): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:13:34 -08:00
Leonardo de Moura
93b02a6fad fix(lua): fix C++ stack unwinding bug, we should never invoke lua_error from a catch block 
lua_error and luaL_error are based on the longjmp C function. They will not correctly unwind the C++ stack. We should only invoke them after we finished handling the C++ exceptions and unwinding the C++ stack, and invoking the destructors for each object living on the stack.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 06:49:54 -08:00
Leonardo de Moura
2ccd5cc559 fix(lua): workaround memory leak problem with __cxa_thread_atexit code generated by g++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 06:40:32 -08:00
Leonardo de Moura
7976937e4c test(lua/metavar_env): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 19:18:47 -08:00
Leonardo de Moura
69be5f6c94 feat(kernel/environment): track which modules were already imported 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 18:15:44 -08:00
Leonardo de Moura
5254dba195 test(library/update_expr): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 13:36:15 -08:00
Leonardo de Moura
df94e44806 test(lua/expr): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:46:24 -08:00
Leonardo de Moura
f586e58ac3 test(lua/justification): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:13:10 -08:00
Leonardo de Moura
d0bac61e74 fix(lua/numerics): bug in bindings, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:02:44 -08:00
Leonardo de Moura
0e6df0a55b fix(lua): warning message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 19:58:34 -08:00
Leonardo de Moura
926ed0a02d feat(lua): add type_inferer object to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 19:18:15 -08:00
Leonardo de Moura
4ebb3c572a feat(kernel/environment): make the environment throw an exception when weak-ref has expired 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 18:35:17 -08:00
Leonardo de Moura
590b14570f feat(lua): improve error handling in Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 18:21:42 -08:00
Leonardo de Moura
516c5c8fea feat(lua): add metavar_env objects to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 14:44:33 -08:00
Leonardo de Moura
c8fff45319 feat(lua): add justification objects to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 11:12:58 -08:00
Leonardo de Moura
9398ea5a59 feat(util/shared_mutex): add support for recursive lock at shared_mutex 
We need support for recursive locks. The main user of this class is
the environment object. This commit adds a test that demonstrates that
the shared_lock of the environment object may be recursively requested.
Before this fix, the Lean was deadlocking in this example.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 22:01:11 -08:00
Leonardo de Moura
209a2d10f7 fix(lua): replace std::mutex with std::recursive_mutex, add test that demonstrates the problem that is being fixed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 21:26:16 -08:00
Leonardo de Moura
8525e8534b feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 16:11:26 -08:00
Leonardo de Moura
d9d9c05e4f refactor(lua/options): remove unnecessary function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 12:53:27 -08:00
Leonardo de Moura
19533c811b feat(library/script_evaluator): add abstract class that exposes only the API needed by frontend objects 
The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua.
This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 12:13:09 -08:00
Leonardo de Moura
1cb0262ec5 chore(memcheck): make the suppression entries for LuaJIT more general 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 11:34:50 -08:00
Leonardo de Moura
e7552d35e0 chore(memcheck): hide another tcmalloc bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 11:33:34 -08:00
Leonardo de Moura
a74412963a chore(build): only execute lua multi-threading tests when on cygwin or linux, and using g++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 09:27:58 -08:00
Leonardo de Moura
782335581b fix(lua/thread): uninitialized memory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 09:07:18 -08:00
Leonardo de Moura
b5dcb93550 feat(lua): communication channels for threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 21:10:46 -08:00
Leonardo de Moura
bd1e9c7548 feat(lua): throw an exception if the user tries to create a thread and Lean was compiled without multi-threading support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 19:06:36 -08:00
Leonardo de Moura
3a924a5fb1 perf(lua/name): improve to_name_ext performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 18:06:09 -08:00
Leonardo de Moura
cd6bd79d63 refactor(lua): cleanup Lua API, improve performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 17:33:46 -08:00
Leonardo de Moura
6575566f9f fix(lua): rename lua_ref to lref, lua_ref is a macro in LuaJIT 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 15:50:56 -08:00
Leonardo de Moura
09bed4786c feat(lua): add semantic attachments for builtin arithmetical values to Lua API, improve mk_constant 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 15:15:04 -08:00
Leonardo de Moura
05f254f605 refactor(lua): move lua_ref to separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 14:41:54 -08:00
Leonardo de Moura
bdea42b2a9 style(lua): ignore bogus warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 14:13:06 -08:00
Leonardo de Moura
abe93dfec0 fix(lua/splay_tree): for_each method was crashing if the map was updated during for_each 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:48:23 -08:00
Leonardo de Moura
64cce595a5 feat(lua): add splay_maps to the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:35:36 -08:00
Leonardo de Moura
8e56726116 fix(library/expr_lt): fix bug when using hash codes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:18:33 -08:00
Leonardo de Moura
b0322787ff feat(lua): add has_metavar method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 10:28:50 -08:00
Leonardo de Moura
9e445d1917 feat(lua): interrupt and sleep Lua APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 10:04:32 -08:00
Leonardo de Moura
691893258d feat(kernel/expr): add hash code based on allocation time 
The new hash code has the property that given expr_cell * c1 and expr_cell * c2,
if c1 != c2 then there is a high propbability that c1->hash_alloc() != c2->hash_alloc().

The structural hash code hash() does not have this property because we may have
c1 != c2, but c1 and c2 are structurally equal.

The new hash code is only compatible with pointer equality.
By compatible we mean, if c1 == c2, then c1->hash_alloc() == c2->hash_alloc().
This property is obvious because hash_alloc() does not have side-effects.

The test tests/lua/big.lua exposes the problem fixed by this commit.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 02:43:11 -08:00
Leonardo de Moura
ae7ea99b56 fix(lua): copy_values and add tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 21:31:27 -08:00
Leonardo de Moura
c759fc93f7 test(lua): object Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 20:59:28 -08:00
Leonardo de Moura
6e0fc0ca9b chore(build): include dl.so when compiling on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 18:44:28 -08:00
Leonardo de Moura
6964e374c0 fix(lua): luajit incompatibility 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 18:08:00 -08:00
Leonardo de Moura
cbc4254ff5 feat(lua): add occurs method to expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 17:10:09 -08:00
Leonardo de Moura
ad1180c5b4 fix(kernel/occurs): typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 17:04:56 -08:00
Leonardo de Moura
351ef867d2 feat(lua): add abstract, instantiate, has_free_vars, lift/lower free_vars to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 17:02:49 -08:00
Leonardo de Moura
ed3cf8152b feat(lua): add for_each to expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 16:30:59 -08:00
Leonardo de Moura
eacd60de9c feat(frontends/lean): return the operator associated with constant expressions that are names of builtin values 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 16:08:21 -08:00
Leonardo de Moura
1bf6051866 test(lua): expr LUA API test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 15:29:31 -08:00
Leonardo de Moura
9a22702383 feat(lua): make objects() and localobjects() methods return iterators in the environment LUA API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 14:26:01 -08:00
Leonardo de Moura
8c52d47692 chore(lua): rename env() to get_env() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 13:58:51 -08:00
Leonardo de Moura
ba0889265e refactor(lua): cleanup Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 13:55:05 -08:00
Leonardo de Moura
b5f0185729 fix(lua): replace lua_pushfstring with lua_pushstring 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 12:14:55 -08:00
Leonardo de Moura
a80adae1c3 feat(lua): add fields method to sexpr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 12:10:24 -08:00
Leonardo de Moura
e2efce6b62 style(util/sexpr): name convetion for enumeration types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 11:50:12 -08:00
Leonardo de Moura
450128e28b refactor(lua): cleanup Lua bindings, and add accessor/tester to expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 11:46:09 -08:00
Leonardo de Moura
c4c548dc5d feat(*): simplify interrupt propagation 
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.

The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:

    try-for (T1 ORELSE T2) 5

It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 21:45:48 -08:00
Leonardo de Moura
b31233e8c2 feat(util/interrupt): restore interrupt module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 21:16:10 -08:00
Leonardo de Moura
126c45626c chore(memcheck.supp): add suppressions for LuaJIT bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 18:52:03 -08:00
Leonardo de Moura
be093ecf90 feat(lua): use formatter available in the state object to convert Lean objects into strings in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 16:56:30 -08:00
Leonardo de Moura
9a5f86fce6 feat(lua): use (** ... **) instead of {{ ... }} for nested Lua scripts 
The token }} is a bad delimiter for blocks of Lua script code nested in Lean files.
The problem is that the sequence }} occurs very often in Lua code because Lua uses { and } to build tables/lists/arrays.
Here is an example of Lua code that contains the sequence }}
     t = {{1, 2}, {2, 3}, {3, 4}}

In Lean, (* ... *) is used to create comments. Thus, (** ... **) code blocks will not affect
valid Lean files. It also looks reasonably good.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 16:05:49 -08:00
Leonardo de Moura
8190d4fed5 feat(lua): allow Lua scripts to update 'global' options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 15:38:00 -08:00
Leonardo de Moura
0a6f622aec chore(build): remove CheckLuaObjlen, it is easier to check the Lua version 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 12:58:22 -08:00
Leonardo de Moura
b986af09ed feat(lua): add support for copying closures between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 12:54:34 -08:00
Leonardo de Moura
c46edcf370 feat(lua): expose formatter in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 11:19:15 -08:00
Leonardo de Moura
2af2a69fc6 feat(lua): expose kernel objects in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 09:40:29 -08:00
Leonardo de Moura
d257156b88 fix(lua): memory leaks, we should not use luaL_error because it does not unwind C++ stack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 21:45:13 -08:00
Leonardo de Moura
a30e02d862 fix(lua): redefine Lua 'print' function, and make sure it is thread safe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 21:15:21 -08:00
Leonardo de Moura
eb9d0f0552 test(lua): add example showing how to access/update an environment object using multiple threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:53:23 -08:00
Leonardo de Moura
0af8f17834 feat(lua): allow Booleans to be copied between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:39:46 -08:00
Leonardo de Moura
7cb15cdac5 feat(lua): allow environment object references to be moved between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:32:36 -08:00
Leonardo de Moura
ac6c18321a fix(lua): make sure environment objects can be safely accessed/updated from current threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:29:53 -08:00
Leonardo de Moura
596e4aeb57 feat(util/shared_mutex): add shared_mutex object, this is a temporary replacement for std::shared_mutex that will be available in C++11 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:00:21 -08:00
Leonardo de Moura
cc7b5b7e50 fix(lua): disable custom allocation for Lua, it is crashing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 18:20:52 -08:00
Leonardo de Moura
7d49df3985 style(lua): fix cpplint.py warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 17:46:39 -08:00
Leonardo de Moura
69b41eae70 feat(lua): add support for multiple execution threads in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 16:25:17 -08:00
Leonardo de Moura
95785c7aaa feat(lua): add State objects, it allows us to create several Lua State objects in a lua script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 15:05:50 -08:00
Leonardo de Moura
f158b0b311 fix(util/memory): make sure realloc behaves like free when sz == 0 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:42:22 -08:00
Leonardo de Moura
7cc6c35eee feat(lua/name): add hash method to name objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:32:56 -08:00
Leonardo de Moura
8dd85ebc15 fix(lua): typos and a bug in the expr Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:11:06 -08:00
Leonardo de Moura
b227775a07 test(lua): add tests for format object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 12:58:47 -08:00
Leonardo de Moura
31abc00db8 chore(*): add LCOV_EXCL_LINE to lean_unreachable statements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 09:19:38 -08:00
Leonardo de Moura
dbdb9a41af style(lua): use C++-style cast 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
7683188ab0 chore(emplace_back): use emplace_back when appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
8c140ff86f feat(lua): allow lua scripts (embedded in Lean files) to access the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
3078923ea4 fix(kernel/type_checker): add missing test, and kernel_exception has_no_type_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
9d61fcf85b feat(lua): expose environment objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
119e0ba5e6 feat(lua): add to_nonnull_expr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
8dd62e76be feat(lua): add mk_metavar to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Soonho Kong
1cf037f11e chore(cmake): do not delete coverage.info.cleaned which will be used for coveralls.io 2013-11-09 22:19:08 -05:00
Leonardo de Moura
6b71fb346c fix(lua): add missing files for local_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-09 12:47:52 -08:00
Leonardo de Moura
554defe89d feat(lua): expose local_context objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-09 12:18:46 -08:00
Leonardo de Moura
183080294b fix(cmake/Modules/CheckLuaNewstate.cc): compilation problem on cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-09 12:18:20 -08:00
Leonardo de Moura
ad2de3b53c feat(lua): expose level objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 17:08:24 -08:00
Leonardo de Moura
5a97f730af feat(lua): add Type function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 15:52:58 -08:00
Leonardo de Moura
32605d8266 feat(lua): expose level objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 15:38:00 -08:00
Soonho Kong
d4dbc18404 chore(cmake/Modules/FindLua): disable TRY_RUN in cross-compilation. 2013-11-08 18:04:55 -05:00
Leonardo de Moura
bbab454b6c fix(lua): cpplint.py does not like multiline strings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 13:27:20 -08:00
Leonardo de Moura
ec56ba72ea fix(lua): cygwing compilation problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 13:27:20 -08:00
Leonardo de Moura
cc17be1ef1 feat(lua): add is_* predicates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 12:40:28 -08:00
Leonardo de Moura
5c35a9ad0a feat(lua): add Consts function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 12:09:46 -08:00
Leonardo de Moura
b7d8391306 refactor(lua): remove duplicate code, separate lua_exception, add missing #pragma once 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 11:59:47 -08:00
Leonardo de Moura
c8b0c10c88 refactor(lua): make Lua a required (non-optional) package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 10:56:29 -08:00
Leonardo de Moura
c5207489fd fix(memory): realloc must behave like malloc when ptr is nullptr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 10:31:57 -08:00
Leonardo de Moura
a10aa0880f fix(build): add CheckLuaObjlen.cc test, not every Lua version has the function lua_objlen 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 08:26:04 -08:00
Leonardo de Moura
b57ad80d5e feat(lua): expose basic API for Lean expressions in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 21:54:57 -08:00
Leonardo de Moura
fb09fc9fe6 feat(lua): add set_global_function template, and to_name_ext function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 21:54:57 -08:00
Leonardo de Moura
db8b16641c chore(build): check if the Lua installed in the system supports lua_newstate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 21:54:57 -08:00
Leonardo de Moura
9000c7c2fa feat(lua): expose format objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 21:54:42 -08:00
Leonardo de Moura
6f432b4094 feat(lua): make Lua use our malloc/realloc, catch error when initializing Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 15:52:39 -08:00
Leonardo de Moura
57b9657bf0 feat(lua): add lua_exception for wrapping lua errors, and improve Lua error messages in the Lean frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 15:19:26 -08:00
Leonardo de Moura
a9b2be0b9c feat(frontends/lean): add support for embedded Lua scripts in Lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 13:56:04 -08:00
Leonardo de Moura
ff16ffaea3 fix(kernel/environment): warning produced by clang 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 11:36:08 -08:00
Leonardo de Moura
8012c4f644 fix(kernel/environment): add weak reference to environment objects 
We need weak references to environment objects because the environment has a reference to the type_checker and the type_checker has a reference back to the environment. Before, we were breaking the cycle using an "environment const &". This was a dangerous hack because the environment smart pointer passed to the type_checker could be on the stack. The weak_ref is much safer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 11:29:08 -08:00
Leonardo de Moura
9c60eed93c refactor(kernel/metavar): avoid using unique names for default metavariable prefix 
The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file.
Avoiding unique name feature in the default metavariable prefix avoids this problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 10:16:25 -08:00
Leonardo de Moura
2141ee12f4 refactor(frontends/lean): use extension objects to store lean default frontend data in the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 10:00:12 -08:00
Leonardo de Moura
80e23f98c7 feat(kernel/environment): add environment extension objects, the environment can be extended with frontend specific objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-06 19:22:30 -08:00
Soonho Kong
c5fd828a71 chore(cmake): switch the ordering between gmp and mpfr 2013-11-05 19:31:10 -05:00
Leonardo de Moura
e7d508043b fix(lua/numerics): errors when cross-compiling for Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-05 13:35:34 -08:00
Leonardo de Moura
40fde1a69c test(lua): invoke Lua binding tests from ctest 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-05 13:17:10 -08:00
Leonardo de Moura
0cc475e581 fix(lua/sexpr): make sexpr bindings robust 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-05 13:03:32 -08:00
Leonardo de Moura
055cc7f957 fix(lua): make testudata compatible with Lua 5.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-05 11:35:09 -08:00
Leonardo de Moura
5a01f167df fix(lua): expose missing functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 21:33:33 -08:00
Leonardo de Moura
0ac8f2d8d9 feat(lua/sexpr): improve sexpr Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 21:28:17 -08:00
Leonardo de Moura
f13a97397f feat(lua): expose s-expressions in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 19:58:32 -08:00
Leonardo de Moura
1e12ddc7a9 refactor(lua): add goodies for accessing Lean values on the Lua stack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 19:45:15 -08:00
Leonardo de Moura
47c289a24b refactor(lua/name): improve name bindings for Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 18:48:21 -08:00
Leonardo de Moura
3c475e890d refactor(lua/options): improve options bindings for Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 18:46:58 -08:00
Leonardo de Moura
7b77863507 refactor(lua/name): improve name bindings for Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 18:44:20 -08:00
Leonardo de Moura
f488e6bbfc fix(lua): safe_function_wrapper 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 18:12:53 -08:00
Leonardo de Moura
92b2591a6f style(lua): add missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 16:29:47 -08:00
Leonardo de Moura
32d3990fc7 fix(lua): problem when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 15:05:04 -08:00
Leonardo de Moura
0579970fc5 feat(lua): expose options object in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 14:38:49 -08:00
Leonardo de Moura
543aea65c9 chore(lua): rename init_* functions to open_* 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 13:54:51 -08:00
Leonardo de Moura
fd7e85f0bb feat(lua): add safe_function template that catches Lean and C++ exceptions and convert them into Lua errors 
I'm using the approach described at:
http://stackoverflow.com/questions/4615890/how-to-handle-c-exceptions-when-calling-functions-from-lua

BTW, in some Lua versions, the C++ exceptions are correctly propagated.
I think we should not rely on features of particular implementations.
For example, LuaJIT does not propagate C++ exceptions.
Whenever an exception is thrown from C++ code invoked from LuaJit, LuaJit interrupts the execution and converts it to an error "C++ exception".
On the other hand, Lua 5.2 PUC-Rio interpreter (for Ubuntu) seem to propagate the C++ exceptions.
The template safe_function solves the issue. It will also produce a Lua error whenever the function being wrapped throws an exception. The error message is based on the "what()" method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 14:42:57 -08:00
Leonardo de Moura
1a734979b4 fix(shell/lua): catch lean exceptions in the leanlua frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 13:46:15 -08:00
Leonardo de Moura
6f2183fafe feat(FindLua.cmake): search also for LuaJit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 13:45:23 -08:00
Leonardo de Moura
9884c056ce feat(lua): allow Lean to be compiled with Lua 5.1 and LuaJit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 12:40:44 -08:00
Leonardo de Moura
df7dbe17b5 feat(lua/util): remove dependency on luaL_setfuncs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 12:16:23 -08:00
Leonardo de Moura
e2da8c1f4d feat(lua/numerics): expose mpz and mpq numbers in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 12:05:54 -08:00
Soonho Kong
88ebdbcfb6 fix(shell/lua): move "#include<iostream>" 2013-11-03 13:25:33 -05:00
Soonho Kong
a9d55bf036 fix(lua): use updated FindLua and check version 5.2 2013-11-03 13:24:46 -05:00
Soonho Kong
044813615e fix: add '#include <tuple>' 2013-11-03 13:00:42 -05:00
Soonho Kong
0d0d0cd533 chore(cmake): add gmp/mpfr include paths to cmakelists.txt 2013-11-03 13:00:42 -05:00
Leonardo de Moura
ccd95a9b66 fix(lua/name): fix memory leak 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 20:57:41 -07:00
Leonardo de Moura
dbf2d56c77 feat(lua/name): expose hierarchical names in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 20:49:42 -07:00
Leonardo de Moura
1b9cf816c4 fix(lua): mark package as optional 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 11:43:23 -07:00
Leonardo de Moura
ac08e244a6 feat(lua): add Lua support to build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 11:16:30 -07:00
Leonardo de Moura
bf998d8661 feat(frontends/lean/parser): allow 'typeless' definitions, the type is inferred by the system 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-01 08:51:49 -07:00
Leonardo de Moura
fdea8aba10 feat(frontends/lean/scanner): allow '#' to be used in class B identifiers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-01 08:42:25 -07:00
Leonardo de Moura
96dcd003c6 fix(frontends/lean/parser): associated position with 'type' placeholder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-31 16:27:36 -07:00
Leonardo de Moura
aa99ac6618 feat(kernel/value): allow semantic attachments to use coercions when being pretty printed 
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-30 11:42:26 -07:00
Leonardo de Moura
032f5cd7b3 feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-30 10:45:43 -07:00
Leonardo de Moura
bc92671ae4 fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 17:12:50 -07:00
Leonardo de Moura
7fc87faa8f feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 17:07:30 -07:00
Leonardo de Moura
a57ca284ec fix(tests/library/elaborator): replace eq with my_eq because eq is now a builtin symbol 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 17:06:32 -07:00
Leonardo de Moura
4dd6cead83 refactor(equality): make homogeneous equality the default equality 
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.

- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
     l = nil
will not propagate the type (List Int) to nil.

- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.

Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 16:20:06 -07:00
Leonardo de Moura
d0009d0242 feat(frontends/lean): make the first argument of if-expression implicit, add support for marking implicit arguments on builtin symbols (aka semantic attachments) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 15:53:50 -07:00
Leonardo de Moura
2d88922543 feat(frontends/lean/elaborator): solve easy overloads at preprocessing time 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 10:07:15 -07:00
Leonardo de Moura
577ca128a1 fix(library/elaborator): add missing conflict justification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 03:01:17 -07:00
Leonardo de Moura
521fa1ddb8 style(kernel/metavar): add missing includes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 03:00:43 -07:00
Leonardo de Moura
7c8daf8974 fix(kernel/metavar): make sure the justification and substitution are always matching each other 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225 fix(kernel/normalizer): do not apply substitutions in the normalizer 
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-29 02:14:48 -07:00
Leonardo de Moura
5f11392fcc test(numerics/numeric_traits): add missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-28 07:50:33 -07:00
Leonardo de Moura
1d18f60dd5 fix(numerics): add missing numeric_traits<float>::zero() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-28 07:47:23 -07:00
Leonardo de Moura
b16a64f44b fix(library/elaborator): missing normalization step for semantic attachments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-28 07:42:14 -07:00
Leonardo de Moura
4564bfa1d3 feat(library/elaborator): improve simple_ho_match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-27 11:17:03 -07:00
Leonardo de Moura
dbefc91151 fix(kernel/metavar): add normalize assignment justification 
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-27 11:02:34 -07:00
Leonardo de Moura
92f5a31976 feat(kernel/expr): add new mk_app template for creating applications using a collection 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-27 08:53:58 -07:00
Leonardo de Moura
eaccdcb558 refactor(assumption_justification): move to the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-26 14:21:29 -07:00
Leonardo de Moura
4bed9f85b0 feat(kernel/for_each): add option for disabling cache of atomic expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 15:25:17 -07:00
Leonardo de Moura
ce10bfeaf6 perf(kernel/metavar): improve performance of has_assigned_metavar by avoiding for_each+exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 15:19:59 -07:00
Leonardo de Moura
57d9d23bd4 feat(kernel/for_each): allow function F to interrupt for_each search 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 14:58:02 -07:00
Leonardo de Moura
2dd44bdf1a perf(kernel/for_each): delay initialization of visited set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 14:52:08 -07:00
Leonardo de Moura
e765105ea5 fix(frontends/lean/pp): let expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 12:30:39 -07:00
Leonardo de Moura
c3c66b6c90 feat(make): add THREAD_SAFE build option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 11:50:35 -07:00
Leonardo de Moura
c53d559f7f perf(library/elaborator): improve process_metavar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 11:19:17 -07:00
Leonardo de Moura
471bbd4040 refactor(kernel/metavar): combine several splay_trees (at metavar_env) into a single one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 11:02:19 -07:00
Leonardo de Moura
5e34f410b3 refactor(splay_map): modify splay_find signature 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 10:47:15 -07:00
Leonardo de Moura
5812dfcf44 perf(kernel/justification): remove cache from depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 10:26:05 -07:00
Leonardo de Moura
2b5c951de3 perf(name): add quick_cmp for hierarchical names 
It first compare names using hash codes.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 09:58:06 -07:00
Leonardo de Moura
66f4834dbc perf(kernel/metavar): add quick test that catches many cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 09:24:01 -07:00
Leonardo de Moura
f38178311c perf(kernel/expr_eq): delay hashtable initialization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 09:21:47 -07:00
Leonardo de Moura
e0ca27bfb3 fix(tests/library/rewriter): warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 08:33:53 -07:00
Leonardo de Moura
412bc792c9 fix(style): missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 08:10:28 -07:00
Leonardo de Moura
0c21f45292 fix(kernel/unification_constraint): memory leak 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-25 08:06:21 -07:00
Leonardo de Moura
f0e149d77b fix(frontends/lean/pp): fix how Type expressions are pretty printed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 20:02:34 -07:00
Leonardo de Moura
a5c3829d1b feat(kernel): add unexpected_metavar_occurrence exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:56:44 -07:00
Leonardo de Moura
83907d7c73 fix(elaborator): max constraints 
elaborator was not handling max constraints where one of the arguments was a Bool. Example:
      ctx |- max(Bool, Type) == ?M

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:27:57 -07:00
Leonardo de Moura
65a514ad8a fix(frontends/lean/parser): option propagation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:04:06 -07:00
Leonardo de Moura
576b4e2169 fix(frontends/lean/pp): missing comma when printing contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:00:24 -07:00
Leonardo de Moura
df07a84d11 feat(frontends/lean/parser): display elaborator error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 18:48:53 -07:00
Leonardo de Moura
ca6a6d71e5 fix(kernel/printer): bug when printing let expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 18:05:23 -07:00
Leonardo de Moura
e3efe39eeb fix(elaborator): fix bug in higher-order matching/unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 17:53:37 -07:00
Leonardo de Moura
d1a2a4ea7e feat(frontends/lean/elaborator): add support for coercions in let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 17:01:06 -07:00
Leonardo de Moura
872b698bc3 feat(elaborator): add option m_assume_injectivity for getting more concise solutions 
We may miss solutions, but the solutions found are much more readable.
For example, without this option, for elaboration problem

Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
    DisjCases H
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
                   in CongrH AeqC (Symm AeqC))
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
                   in CongrH AeqC (Symm AeqC))

the elaborator generates

Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
    DisjCases
        H
        (λ H1 : if
               Bool
               (if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤)
               ⊥
               ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
        (λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))

The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 16:47:50 -07:00
Leonardo de Moura
d2f9c24d3c fix(tests/lean): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:42:17 -07:00
Leonardo de Moura
a7f94b55db fix(frontends/lean/elaborator): fix bugs and adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:29:56 -07:00
Leonardo de Moura
bbc265ded4 feat(frontends/lean): hook new elaborator in the default frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:14:29 -07:00
Leonardo de Moura
c9f7b8bce2 feat(frontends/lean): add get_coercions method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 14:38:09 -07:00
Leonardo de Moura
71ccec5b9e refactor(frontends/lean/elaborator): delete old_elaborator, and create frontend_elaborator class that will be based on library/elaborator/elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 10:45:59 -07:00
Leonardo de Moura
449454efdb fix(debug): remove typeid information from assertion, the names are mangled and are not very useful 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:41:51 -07:00
Leonardo de Moura
434c33f225 feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda 
This feature is useful for problems that require higher-order matching and/or unification.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:35:50 -07:00
Leonardo de Moura
873e56844a refactor(beta_reduction): add function apply_beta 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:03:52 -07:00
Leonardo de Moura
f1e0d6ec29 refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:44:26 -07:00
Leonardo de Moura
c1e451151a feat(replace_visitor): add an abstract class for applying transformations on expressions 
I also removed replace_using_ctx since it is subsumed by the new class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:01:37 -07:00
Leonardo de Moura
13531b7d3e refactor(kernel): rename trace to justification 
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:42:17 -07:00
Leonardo de Moura
8e1a75ce1c feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:09:13 -07:00
Leonardo de Moura
172567a2fb feat(elaborator): add support for upper bounds, max constraints, and fix bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:01:39 -07:00
Leonardo de Moura
17b48010b7 fix(unification_constraint): fix printer for max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:00:29 -07:00
Leonardo de Moura
274b11530f feat(metavar): improve apply_local_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 11:59:36 -07:00
Leonardo de Moura
b57f492e2d fix(kernel/printer): improve printer for Type expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 11:58:49 -07:00
Leonardo de Moura
c635c16637 refactor(ho_unifier): remove ho_unifier, it has been subsumed by the elaborator class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:51:54 -07:00
Leonardo de Moura
019f64671b fix(elaborator): add basic support for flex-flex pairs, add more tests, fix bug when enumerating different solutions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:49:37 -07:00
Leonardo de Moura
80a507cf45 refactor(tests/frontends/lean/implicit_args): remove implicit_args unit tests from frontends/lean, all tests were moved to tests/library/elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:42:07 -07:00
Leonardo de Moura
7ad256131e feat(elaborator): add support for constraints of the form ?m[inst, ...] == t, fix bugs, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:39:22 -07:00
Leonardo de Moura
891d22b3de feat(kernel/context): add method for remove context entries at positions [s, s+n). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:52:24 -07:00
Leonardo de Moura
3fa4eac4ef fix(replace_using_ctx_fn): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:46:11 -07:00
Leonardo de Moura
8142726923 fix(type_inferer): bug when inferring the type of free variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:41:22 -07:00
Leonardo de Moura
874f67c605 feat(normalizer): remove normalization rule t == t ==> true 
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:

Theorem Th : a = a := Refl b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 14:02:48 -07:00
Leonardo de Moura
5e61496381 test(elaborator): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:20 -07:00
Leonardo de Moura
a5b4908f71 fix(elaborator): process_simple_ho_match and missing cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:04 -07:00
Leonardo de Moura
cb2c73cf37 feat(elaborator): add higher-order matching support to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 11:22:00 -07:00
Leonardo de Moura
f4592da87f feat(elaborator): solve more unification constraints, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
c3e87f106f fix(kernel/trace): fix typo in depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
dc51d35dc0 feat(library/type_inferer): add support for metavariables at type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
7f96c07a01 refactor(library): rename light_checker to type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
dc0e7a4472 feat(pos_info_provider): add position information provider for expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
8663ac550f feat(kernel/trace): add function depends_on for trace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
42edc4a72d test(set): add set of pointers test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
b1b49e86e7 test(elaborator): add simple test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
1548ffabb1 feat(elaborator): add new elaborator interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
827c65b5e9 feat(kernel): add static_assert for update_metavar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
61ccaf741c fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
7cf83800c0 refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
1f0eab7a14 test(type_checker): add new tests for type_checker trace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
fc288929a2 feat(type_checker): add trace objects to justify constraints created by the type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
5b1b03bafd refactor(is_convertible): move from normalizer to type_checker class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
85bfa45e6a refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
d843d432d3 refactor(kernel): move printer and formatter objects to the kernel 
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
ddb90d3038 feat(kernel): add unification_constraint and trace objects to the kernel 
Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.

The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.

Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
e741cc29ef test(metavar): encode two of the bad examples as unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
59914a36f3 refactor(metavar): reorganize and simplify metavariables 
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
3387c300a0 feat(polynomial): add multivariate polynomials 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:22:14 -07:00
Leonardo de Moura
93d4466d06 refactor(interval): move interval unit tests to tests/util/interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:17:34 -07:00
Leonardo de Moura
f18d35555e refactor(interval): organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:15:27 -07:00
Leonardo de Moura
e208309abd refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 17:23:56 -07:00
Leonardo de Moura
f1d9312521 feat(numerics/zpz): add numeric_traits for zpz numerals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-18 14:41:18 -07:00
Leonardo de Moura
1429cc9df2 feat(numerics): add finite field Z/pZ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-18 13:27:28 -07:00
Leonardo de Moura
bdade0e638 fix(numerics): problem with gcd tests on OSX 
Now, we only test gcd(a, b) for a != b && a != 0 && b != 0.
When one of these conditions do not hold, the result is implementation dependent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-17 10:38:02 -07:00
Leonardo de Moura
cf2c0f8ebb feat(numerics): add gcd and extended gcd templates (for primitive types) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 18:18:20 -07:00
Leonardo de Moura
39f68ed0d6 feat(numerics): add is_prime function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 17:25:08 -07:00
Leonardo de Moura
1097bbfb22 fix(style): fix warnings produced by cpplint.py, disable sizeof(type) warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 17:04:39 -07:00
Leonardo de Moura
105f55c68b feat(numerics): add zero() method to all numeric_traits 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 16:55:17 -07:00
Leonardo de Moura
ff04c5a2e2 test(numerics): add test to make sure that zeros of different precision mpfp numbers are the equal. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 16:54:43 -07:00
Leonardo de Moura
467eff4662 add(numerics): add prime number generator/iterator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 16:05:45 -07:00
Leonardo de Moura
0783805671 feat(kernel): add weight to kernel definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-15 14:50:08 -07:00
Leonardo de Moura
5bd6ba37d0 fix(light_checker): fix inconsistent cache bug in light_checker, add tests that expose the problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-01 19:25:58 -07:00
Leonardo de Moura
aa5be3262f fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-01 19:23:55 -07:00
Leonardo de Moura
2089d12bd0 fix(replace_using_ctx): fix inconsistent cache bug in replace_using_ctx, and add tests that expose the problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-01 18:52:18 -07:00
Soonho Kong
760f2e15ce feat(library/replace_using_ctx): add static_assert 2013-10-01 16:47:49 -07:00
Soonho Kong
e3b762e909 feat(kernel): add static_assert to expr,expr_eq,replace 2013-10-01 16:47:36 -07:00
Soonho Kong
b823c7d779 feat(util): add static_assert to {scoped,splay}_{map,set} 2013-10-01 16:47:28 -07:00
Soonho Kong
a726f5fbb7 feat(util/list): add static_asserts for map/for_each/compare 2013-10-01 09:05:53 -07:00
Soonho Kong
3381df0150 fix(util/list_fn): rename iter to for_each 2013-10-01 09:03:07 -07:00
Soonho Kong
c50bc13be0 test(library/rewriter): add more tests 2013-10-01 00:30:38 -07:00
Soonho Kong
7c0b56ad0d feat(library/rewriter): implement repeat/app/lambda/pi/try rewriter 
- refactor to use rewriter_cell
 - implement display and operator<< for debugging
 2013-10-01 00:30:31 -07:00
Soonho Kong
e6c76fbe76 refactor(library/rewriter/fo_match): add more lean_trace for debugging 2013-10-01 00:20:12 -07:00
Soonho Kong
a832173f5f feat(kernel/expr): add expr::operator() which takes 8 args 2013-10-01 00:19:30 -07:00
Soonho Kong
1a3ea26032 feat(util/list_fn): add iter function 2013-10-01 00:18:55 -07:00
Leonardo de Moura
15979ab991 fix(lean): fix warnings produced by cppcheck 
Fix (relevant) warnings produced by http://cppcheck.sourceforge.net.
Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-30 21:38:55 -07:00
Leonardo de Moura
30089aa4f8 test(type_checker): add example showing how to use the kernel exception formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-30 16:39:29 -07:00
Soonho Kong
54f4c4d9bc test(library/rewriter/fo_match): clean up enable_trace 2013-09-29 18:36:01 -07:00
Leonardo de Moura
8d3ae665e7 fix(splay_map): fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:30:08 -07:00
Leonardo de Moura
21f9699661 test(splay_tree): add missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:28:10 -07:00
Leonardo de Moura
790c2a72d5 test(safe_arith): add unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:20:32 -07:00
Leonardo de Moura
1179b6b52b test(hash): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:20:32 -07:00
Leonardo de Moura
57b6148bbb test(buffer): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:20:32 -07:00
Leonardo de Moura
02f621aa45 test(lazy_list): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 14:38:35 -07:00
Leonardo de Moura
3c8dff9085 feat(lazy_list): implement ML-like lazy lists 
We will use lazy lists to represent the set of solutions produced by the elaborator. The elaborator plugins will also use lazy lists.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 12:35:26 -07:00
Soonho Kong
841a1fb20c fix(debug): print type in lean_assert, print bool correctly 
- use typeinfo to print out a type of value when an assertion fails.
   need to use "c++filt --types" to demangle names for non-basic types.
 - use std::boolalpha and std::noboolalpha to control the printed values
   for "true" and "false"
 2013-09-28 23:38:21 -07:00
Soonho Kong
4602dfd209 test(util/numerics): more tests to improve coverage 2013-09-28 23:38:17 -07:00
Soonho Kong
fb3635a9ef test(util/numerics/mpbp): add more tests for improving coverage 2013-09-28 01:01:52 -07:00
Soonho Kong
6519d4bb0f chore(memcheck.supp): generalize TCmalloc_Bug2 pattern 
to suppress a warning from MSR 32bit build
[skip-ci]
 2013-09-27 19:16:02 -07:00
Soonho Kong
0065d69e0a chore(build): put --coverage CXX_FLAGS for TESTCOV build 2013-09-27 10:24:31 -07:00
Leonardo de Moura
d2667d56c0 test(lean/parser): add more tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-27 09:59:50 -07:00
Leonardo de Moura
0ff69d28f3 test(lean/scanner): add more tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-27 09:59:50 -07:00
Leonardo de Moura
6fc177056e refactor(tests/frontends/lean): use consistent name convention for file names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-27 09:59:50 -07:00
Soonho Kong
6a0d211d54 test(fo_match): add more unittests 
[skip ci]
 2013-09-27 01:53:42 -07:00
Soonho Kong
285495313b refactor(rewrite): use scoped_map as a type of substitution 2013-09-27 01:45:22 -07:00
Soonho Kong
1d4a1b68f5 refactor(fo_match): use scoped_map 2013-09-27 01:44:05 -07:00
Soonho Kong
6307beedc9 feat(scoped_map): add operator<< to scoped_map for debugging 2013-09-27 01:42:11 -07:00
Soonho Kong
a05b6b476e fix(testcov): install lcov and include testcov only when it's on 2013-09-26 22:24:24 -07:00
Soonho Kong
6abb7bf2ff chore(testcov): add missing CodeCoverage.cmake 2013-09-26 21:26:52 -07:00
Soonho Kong
3a5a565594 feat(splay_map): add operator<< to splay_map for debugging 2013-09-26 20:44:20 -07:00
Soonho Kong
5e5087b0a3 chore(testcov): add compile target "cov" to run code-coverage locally 
- need to run cmake with "-DTESTCOV=ON" and "-DCMAKE_BUILD_TYPE=Debug"
 - type "make/ninja cov"
 - open "coverage/index.html" to check the code coverage
 2013-09-26 20:28:52 -07:00
Leonardo de Moura
9d8ff0eadb test(mpz): add unit tests for mpz 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 20:01:39 -07:00
Leonardo de Moura
5cce74d116 test(library): add tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 19:43:10 -07:00
Soonho Kong
60157aa92a fix(splay_map): add 'const' to coersion operator of ref class 
[skip ci]
 2013-09-26 19:09:37 -07:00
Leonardo de Moura
54e63fd4de feat(splay_tree): add fold and for_each templates for splay_tree and splay_map 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:20 -07:00
Leonardo de Moura
1aca1d2d77 refactor(list): improve append function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:20 -07:00
Leonardo de Moura
24c173a519 feat(debug): add assert_ne (not equal) macro 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:20 -07:00
Leonardo de Moura
d7ed1560a9 feat(name_generator): add name_generator for unique names modulo a prefix 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:06 -07:00
Leonardo de Moura
e5d312dc18 fix(kernel): the hash code of expressions was not being used to compare them 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 08:41:20 -07:00
Leonardo de Moura
19f4554145 test(exception): add tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 08:35:13 -07:00
Leonardo de Moura
a24dbc3527 test(buffer): add tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 08:35:13 -07:00
Soonho Kong
bc31322a78 chore(memcheck): add another memcheck.supp entry for tcmalloc bug 
suppress a valgrind warning we had on "normalizer" testcase (only with g++-4.8.1)
 2013-09-26 00:49:43 -07:00
Soonho Kong
a2a5a77a44 fix(memory): increase memory counters by the actual size of reallocated memory 
On OSX, we had a test failure on memory module. The problem was in
the realloc function (line 38):

    void * realloc(void * ptr, size_t sz) {
        size_t old_sz = malloc_size(ptr);
        g_global_memory.dec(old_sz);
        g_global_memory.inc(sz);
        g_thread_memory.dec(old_sz);
        g_thread_memory.inc(sz);
        void * r = realloc_core(ptr, sz);
        if (r || sz == 0)
            return r;
        else
            ...

The size of r could be bigger than sz. For instance,

    |ptr| = 40 but |r| = 48

In the current code, here we only increase counters by 40.
But later when we free it, we decrease them by 48, and this
caused the problem, underflow of an unsigned counter in
g_global_memory.
 2013-09-26 00:33:56 -07:00
Leonardo de Moura
4bae715350 fix(memory): disable problematic test when tcmalloc is used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 22:39:49 -07:00
Leonardo de Moura
c00534209a test(splay_map): add tests for improving code coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 22:12:49 -07:00
Leonardo de Moura
98b4e09063 refactor(kernel): simplify expr_eq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 22:09:08 -07:00
Leonardo de Moura
23e2f72f42 test(list): add tests for improving code coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 22:04:24 -07:00
Leonardo de Moura
db4e5ab0ad feat(expr_lt): improve expr_lt performance by using hash codes, and add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 21:59:58 -07:00
Leonardo de Moura
6477708d78 refactor(debug): improve lean_unreachable(), now we can avoid 'fake' return statements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 21:27:20 -07:00
Leonardo de Moura
a7707dd669 test(bit_tricks): add tests for log2 2013-09-25 20:58:01 -07:00
Leonardo de Moura
44a16cab6a test(exception): add new tests exception and parser_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:57:53 -07:00
Leonardo de Moura
87e749cd12 test(trace): add unit test for trace module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:30:05 -07:00
Leonardo de Moura
e16f45854b refactor(deep_copy): simplify deep_copy implementation, and move unit test to separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:25:24 -07:00
Leonardo de Moura
037ebfd1d4 refactor(util): make 'util/test.h' the first include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:13:05 -07:00
Soonho Kong
ad62f9762b fix(tests/util): use lean_assert_eq 2013-09-25 19:22:36 -07:00
Soonho Kong
475338080f fix(tests/interval): use new lean_assert and lean_assert_eq 2013-09-25 18:40:45 -07:00
Leonardo de Moura
9f0dab1add fix(kernel): add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel 
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include
'library/printer.h', but contains

    expr a;
    ...
    std::cout << a << "\n";
    ...

The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
 2013-09-25 17:45:54 -07:00
Leonardo de Moura
1452e9319e feat(debug): improve lean_assert macro 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 17:29:00 -07:00
Soonho Kong
1d8b7dc193 Update 'orelse' and 'then' rewriter to take a list of rewriters 2013-09-25 16:46:39 -07:00
Soonho Kong
a50f5f92b8 Rename 'rewrite' to 'Rewriter', change type of rewriter::operator() 2013-09-25 15:38:16 -07:00
Soonho Kong
573ca92a08 Fix typo in CTestConfig.cmake 2013-09-24 21:46:51 -07:00
Soonho Kong
6d10e978dc Add "--gen-suppressions=all" to valgrind option 2013-09-24 21:36:03 -07:00
Soonho Kong
0ef633a3c5 Fix to be compiled by clang++-3.4 
Clang++-3.4 is starting to enforce the following item of C++11 standard,
thus it's making lean not compiling:

It's illegal in C++11: §8.3.6.4 [dcl.fct.default]
"If a friend declaration specifies a default argument expression, that
declaration shall be a definition and shall be the only declaration of
the function or function template in the translation unit."
 2013-09-24 21:30:56 -07:00
Soonho Kong
8e9bd9ee67 Add Repeat/Success/Fail to rewrite (skeleton) 2013-09-24 20:04:08 -07:00
Soonho Kong
ac0eafa1b6 Fix style-warning 2013-09-24 19:34:58 -07:00
Soonho Kong
57e9e2c658 Re-implement rewrite module using rewrite_cell 2013-09-24 19:11:09 -07:00
Leonardo de Moura
ba0528c298 Implement total order on expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 12:16:32 -07:00
Leonardo de Moura
e23813f15d Add support for creating unique internal names. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 11:01:30 -07:00
Leonardo de Moura
1779b29355 Implement map using splay_trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 01:44:46 -07:00
Soonho Kong
71fb150333 Fix type of rewrite() to take an env. Add skeletons for other rewriters 2013-09-24 01:20:45 -07:00
Soonho Kong
81c9de229b Add then and orelse rewrite combinators and tests 2013-09-24 01:19:03 -07:00