[Tactic] Outline

Overview

This tactic comes in two flavours: procedure outlining, and statement outlining.

Procedure 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:

1. The program slice ends with an assignment whose expression matches the return expression.
2. 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).

Statement outlining

This variation is much more general, allowing you to replace one program slice with another.

A call with this tactic will result one goal: the original goal but with the replacement performed. It will fail if the replacement code cannot be shown equivalent to the original via the simple tactic chain: by inline; sim; auto => />..

Syntax

Procedure outlining: outline {m} cp(r) ~? M.foo

Statement outlining: outline {m} cp(r) by { s1; s2; ... }

where

• m: 1 or 2
• cp(r) : a code position or a code position range (See Code Positions) specifying the block of statements to outline.
• ~? : optionally ~, where if ~ is present the second variant of procedure matching is used to allow for local variable recovery.
• M.foo: path to procedure

Permitted contexts

pRHL judgements

Examples

Providing a left-value

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 use the ~ option with outline to enable this .

So the tactic call would be outline {1} [j-k] ~ sample, leaving us with

i) ...
j) (x, y) <@ sample(dt');
k) ...

More

For more examples see: tests/outline.ec