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

656 commits

Author SHA1 Message Date
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
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
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
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
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
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
46e7802d9a test(library/rewriter): add lambda_{body/type}_rewriter tests 2013-12-13 15:08:23 -05: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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
d79b2babd3 fix(*): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-02 08:46:47 -08: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
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
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
Soonho Kong
6a6b69ddf4 test(library/rewriter): add test for depth RW 2013-12-01 01:59:21 -05:00
Soonho Kong
ae0508128f refactor(library/rewriter): move apply_rewriter_fn into rewriter.h 2013-12-01 00:57:09 -05: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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
c50bc13be0 test(library/rewriter): add more tests 2013-10-01 00:30:38 -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
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
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
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
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
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
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
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
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
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
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
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
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
Soonho Kong
9ba6068858 Update fo_match 2013-09-24 01:19:03 -07:00
Soonho Kong
f89ededddc Add rewrite and first-order pattern matching skeletal 2013-09-24 01:19:03 -07:00
Leonardo de Moura
b78b2e0585 Add remaining splay tree methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 01:04:02 -07:00
Leonardo de Moura
d31f3facac Implement splay trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-23 22:31:18 -07:00
Leonardo de Moura
46d6c41835 Fix bug in the type checker (when type checking terms with meta-variables). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-22 19:12:19 -07:00
Leonardo de Moura
c847d27763 Improve higher order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-21 00:41:49 -07:00
Leonardo de Moura
d29ec9ab6f Add tests for memory.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 22:37:13 -07:00
Leonardo de Moura
7ac94ee976 Add max_sharing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 22:01:40 -07:00
Leonardo de Moura
d34cfe3f8a Add simple formatter tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 21:46:32 -07:00
Leonardo de Moura
42482622f6 Add imitation for lambdas and Pis 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Leonardo de Moura
d7cc5d2404 Fix bug in ho_unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Leonardo de Moura
2f29ff70d7 Implement higher-order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-18 20:46:00 -07:00
Soonho Kong
27d5ae13d7 Move src/interval to src/util/interval 2013-09-17 14:10:53 -07:00
Leonardo de Moura
3df6149daa Add support for metavariables in the type checker. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 11:09:59 -07:00
Leonardo de Moura
30b19c314a Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 07:15:47 -07:00
Leonardo de Moura
a26c7d47f2 Add simplification to add_lift 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 03:14:02 -07:00
Leonardo de Moura
99e8d2feae Add simplification rule to add_inst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 02:57:28 -07:00
Leonardo de Moura
21c7a45f67 Relax definition of identity_stack. Fix printer for metavariable contexts. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 02:09:45 -07:00
Leonardo de Moura
d3bce584f4 Add support for new metavariable representation in the normalizer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 01:57:21 -07:00
Leonardo de Moura
99a163f11d Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
cad562a448 Add support for metavariables in the normalizer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
f79f046294 Add partial support for metavariables in the normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 21:23:50 -07:00
Leonardo de Moura
2800292947 Add timestamp to metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:50:48 -07:00
Leonardo de Moura
5a4bc331d2 Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:38:36 -07:00
Leonardo de Moura
63e102055e Move metavariables to the kernel. This is the first step for implementing the new elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 12:09:01 -07:00
Soonho Kong
e4b327bbaa Use C++11's <random> in pdeque/pvector tests (cygwin doesn't support rand_r) 2013-09-15 01:38:57 -07:00
Soonho Kong
c96a6982a0 Add <ctime> header for time() in pdeque/pvector tests 2013-09-13 20:42:49 -07:00
Soonho Kong
eda25e77a4 Use time(0) as an initial seed for rand_r() in pvector/pdeque tests 2013-09-13 20:28:15 -07:00
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -07:00
Leonardo de Moura
8c735f1daa Use consistent coding style for spaces after ',' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:49:03 -07:00
Leonardo de Moura
573ec5ccc2 Rename import_all. The idea is to use consistent name for library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 09:06:46 -07:00
Leonardo de Moura
070c87bef0 Rename arith library files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:55:09 -07:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -07:00
Leonardo de Moura
4c19cc6957 Rename lean frontend files. The prefix lean_ is not necessary anymore. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:09:35 -07:00
Leonardo de Moura
26097475fd Use fullpath in #include directives. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:04:10 -07:00
Leonardo de Moura
c655e9fe7b Move sexpr_funcs to sexpr_fn. Using consistent file name conventions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 18:27:46 -07:00
Leonardo de Moura
2e990ef7d3 Fix warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 14:02:40 -07:00
Leonardo de Moura
bc69e7803f Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:18:26 -07:00
Leonardo de Moura
74b8a4f0ac Add support for writing a[i] = v instead of a.set(i, v) in the pvector class. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:12:02 -07:00
Leonardo de Moura
f972cc9aae Fix bugs in pvector. Improve test driver 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:01:40 -07:00
Leonardo de Moura
55ff49d2d5 Replace queue.h with pdeque.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 10:09:54 -07:00
Leonardo de Moura
cd5e45bae2 Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 08:28:24 -07:00
Soonho Kong
5858c9d5e0 Update tests/util/list.cpp to suppress a g++ warning 2013-09-12 01:39:04 -07:00
Leonardo de Moura
f7196e05ff Add 'persistent' vectors. We should use the same approach for queues. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:55 -07:00
Leonardo de Moura
ef0e0ad382 Add (optional) performance tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:55 -07:00
Leonardo de Moura
37498f9fb8 Add persistent queues 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:54 -07:00
Leonardo de Moura
3657320edb Add basic list functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:54 -07:00
Soonho Kong
3505ed8adb Use suppressions file to ignore certain valgrind warnings 2013-09-10 15:37:09 -07:00
Leonardo de Moura
6fe86ffefd Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-10 13:51:02 -07:00
Leonardo de Moura
1cee392483 Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-07 22:33:18 -07:00
Leonardo de Moura
33c4b44b2b Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-07 11:15:11 -07:00
Leonardo de Moura
c674bb3790 Add castlib as an independent library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:40:47 -07:00
Leonardo de Moura
7a9d53d0d7 Refactor arith libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:19:47 -07:00
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 10:06:26 -07:00
Leonardo de Moura
87d3961158 Improve elaborator error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 16:36:58 -07:00
Leonardo de Moura
e955c054ca Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 08:30:04 -07:00
Leonardo de Moura
9f64e2b14b Fix another cdash warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 04:43:55 -07:00
Leonardo de Moura
6f3fa63ccb Add missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 14:51:34 -07:00
Leonardo de Moura
a154f4e439 Modify Set command in the default lean frontend. Now, the lean prefix (for lean default frontend specific options) is optional when we are in the lean front-end. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 11:07:28 -07:00
Leonardo de Moura
a341643335 Fix unit tests for Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 10:44:51 -07:00
Leonardo de Moura
544229e5d3 Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 10:11:45 -07:00
Leonardo de Moura
fd44ec8d79 Improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 18:28:12 -07:00
Leonardo de Moura
b483d0dc45 Replace Int::sub and Real::sub with definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 16:31:30 -07:00
Leonardo de Moura
0a67679afb Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 12:24:29 -07:00
Leonardo de Moura
db88920f81 Rename normalize and type_check to normalizer and type_checker (using a consistent naming convention) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 08:43:38 -07:00
Leonardo de Moura
e8c09015ad Move elaborator to lean default frontend. It is getting too specific 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 18:22:24 -07:00
Leonardo de Moura
61a8fd16db Remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 14:57:08 -07:00
Leonardo de Moura
9d9f9797e4 Improve elaborator interface. Now, the metavariables are created inside the elaborator. The elaborator-user only needs to create placeholders. Motivaton: the placeholders are meaningful independently of the elaborator. On the other hand, the metavariables depend on the elaborator state. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 17:11:06 -07:00
Leonardo de Moura
2aac94f2e6 Refactor elaborator using new metavar library. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 01:25:06 -07:00