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

493 commits

Author SHA1 Message Date
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