[Tactic] Outline
This tactic comes in two flavours: procedure outlining, and statement outlining.
Procedure outlining aims to provide an inverse operation for the tactic inline.
Given a program containing a slice that matches the body of a procedure, it will attempt to replace that slice with a single call to the procedure, inferring the necessary arguments.
When the procedure contains a return statement, there are two possibilities that can be handled:
- The program slice ends with an assignment whose expression matches the return expression.
- The return expression is a single variable or tuple of variables.
The first case captures a more precise inverse to inline whereas the second permits slightly more flexible usage by allowing direct recovery of local variables. (see example below).
This variation is much more general, allowing you to replace one program slice with another.
A call with this tactic will result in two goals: one requiring a proof that replacement is valid (often will be automatically discharged), and another that continues with the original goal but with the replacement performed.
Procedure outlining: outline {m} [s - e] lv? <@ M.foo
Statement outlining: outline {m} [s - e] { s1; s2; ... }
where
- m: 1 or 2
-
s, e: code position - when s = e, one can use
[s]instead of[s-s] - M.foo: path to procedure
- lv: a left-value
pRHL judgements
Given the following,
proc sample2(dt: t distr) = {
var x, y : t;
x <$ dt;
y <$ dt;
return (x, y);
}.
Consider a left hand program of the form,
i) ...
j) x <$ dt';
k) y <$ dt';
l) ...
This is almost an inline of sample, however we are missing the return statement. Fortunately, since the return is just a tuple of variables, we can provide (x, y) as a left-value to outline to compactly represent the reassignment and destruction of the result.
So the tactic call would be outline {1} [j-k] (x,y) <@ sample, leaving us with
i) ...
j) (x, y) <@ sample(dt');
k) ...
For more examples see: tests/outline.ec