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.
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>
