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

678 commits

Author SHA1 Message Date
Soonho Kong
a2d6918348 fix(library/rewriter): use Abst axiom in lambda_body RW 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
2c65fdb346 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 01:06:34 -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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Soonho Kong
044813615e fix: add '#include <tuple>' 2013-11-03 13:00:42 -05: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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
3381df0150 fix(util/list_fn): rename iter to for_each 2013-10-01 09:03:07 -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
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
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
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
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
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
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
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
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
651c5d6751 Fix warnings and bugs related to unused variables. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 22:41:07 -07:00
Soonho Kong
ab6ca82e6f Update to suppress unused-parameter warnings 2013-09-19 22:40:34 -07:00
Leonardo de Moura
80a1b96925 Remove duplicate solutions in the higher order matching module. Simplify solutions when higher-order matching is used, and we don't have a residue. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 18:59:28 -07:00
Leonardo de Moura
ffef055e34 Add options to ho_unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 18:19:25 -07:00
Leonardo de Moura
8c5c17ee12 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:30:37 -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
4afeb1a400 Add imitation step for equalities. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Leonardo de Moura
b3aa8b37f3 Remove cleanup_subst. The residue may still reference auxiliary variable. So, it is not safe to remove then from the resultant partial substitution. 
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
Leonardo de Moura
ad901ce087 Use consistent naming conventions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 14:43:07 -07:00
Leonardo de Moura
22949051f1 Higher-order unifier skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 14:43:07 -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
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
da09e7217a Cleanup meta_entry code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -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
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
Leonardo de Moura
bcc3827a99 Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 13:46:22 -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
18f9378f97 Rename numtype.h to num_type.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 09:07:44 -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
0c09e4524a Use consistent names for import functions, and library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:58:34 -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
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
a8ba50531b Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 20:38:11 -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
bab11b57ad Move Symm and Trans back to basic_thms.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:49:35 -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
b92bbeb83b Add casting propagation and normalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 20:45:26 -07:00
Leonardo de Moura
8840b37258 Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 11:02:00 -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
eb96e6441f Moved kernel exception formatting to kernel_exception_formatter.cpp. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 10:15:43 -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
613d83cdf4 Improve application type mismatch errors. We also show the implicit arguments (not just their types) 
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
887f696f66 Factor duplicate code. Add more comments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 23:27:58 -07:00
Leonardo de Moura
e031d7bc10 Improve error messages when overloads+coercions do not work 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 20:05:47 -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
abc939382b Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 13:20:00 -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
42be7a4989 Add coercion declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 18:11:28 -07:00
Leonardo de Moura
75f4ec5092 Add functions for 'updating expressions'. The new functions are used to simplify the elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 15:37:30 -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
d27680d7fc Add support for overloads in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 14:54:02 -07:00
Leonardo de Moura
598daa40bc Refactor elaborator for supporting overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 10:24:10 -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
71b8b6408e Handle (and pretty print) elaborator error messages in the lean default frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 16:46:41 -07:00
Leonardo de Moura
64788320f2 Fix elaborator for let-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 14:24:07 -07:00
Leonardo de Moura
793468072b Fix nontermination problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 12:32:16 -07:00
Leonardo de Moura
4c27530930 Fix missing case in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 17:07:45 -07:00
Leonardo de Moura
6efb6c6e83 Fix clang++ compilation problem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 09:04:11 -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
Leonardo de Moura
1f6943e3a4 Add head_reduce_mmv (reduction function modulo metavariables) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-29 14:15:17 -07:00
Leonardo de Moura
2cf9ca9345 Add metavariable utilities. They will be used to refactor the elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-29 13:49:22 -07:00
Leonardo de Moura
cdab19b88c Simplify the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-27 20:39:38 -07:00
Leonardo de Moura
0a34959716 Fix a bug. Add another test. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 20:43:50 -07:00
Leonardo de Moura
3721577700 Fix bugs in elaborator. Cleanup tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 18:46:33 -07:00
Leonardo de Moura
8f4a844598 Fix unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:42:36 -07:00
Leonardo de Moura
b42e04297d Add support for creating meta-variables in the parser. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:18:19 -07:00
Leonardo de Moura
25e47a8a2f Add check_interrupted 'macro' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:03:09 -07:00
Leonardo de Moura
ece6e6ca6a Add interrupt to parser. Add elaborator to parser. Add placeholder support in the scanner. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:02:34 -07:00
Leonardo de Moura
ac1267bef3 Add expression elaborator to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 18:14:09 -07:00
Leonardo de Moura
68e1a1a24a Add metavar_env to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 17:51:53 -07:00
Leonardo de Moura
dc91a7adb8 Add Ctrl-C support for interrupting Lean shell. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 16:11:35 -07:00
Leonardo de Moura
f0edf2b4a3 Pretty print kernel exceptions. Improve default lean frontend error messages. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 13:16:43 -07:00
Leonardo de Moura
bf608a38aa Add head_reduce 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 19:35:33 -07:00
Leonardo de Moura
e95a0c2559 Modify basic printer for contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 12:11:16 -07:00
Leonardo de Moura
e7487a1fec Add head_beta function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
d30c6b2c9d Fix spaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
0f6a7e4a95 Rename exprlib to library. Name was misleading, it is more than a library for manipulating expressions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 10:26:52 -07:00