feat(frontends/lean/parser): add support for Lua expression code blocks

In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write

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

instead of

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/tactic): compilation warning

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/builtin): add is_* functions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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.
feat(library/rewriter): add apply_rewriter_fn which will be used in depth RW
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.
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>
fix(util/luaref): warnings produced by valgrind

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>
fix(library/rewriter): unused variable warnings