[tactic] outline

[Cameron-Low]

The main idea is to provide an inverse to inline when proving an equiv.

Currently, it supports basic procedure unification that requires manual selection of the program slice to unify with, as well as, requiring near exact matches on program structure. An optional return value can be supplied for situations where the return expression is just a program variable and needs to be renamed/deconstructed.

There is also support for statement outlining although, this is more of a transitivity * with program slicing so may require change.

Syntax and variants:

• Procedure outlining: outline {m} [s - e] M.foo or outline {m} [s - e] M.foo @ lv
• Statement outlining: outline {m} [s - e] { s1; s2; ... }

m: 1 or 2
s,e: code position
M.foo: path to procedure
lv: a left-value

when s = e, one can use [s] instead of [s-s]

For example usage see: examples/tactics/outline.ec

[fdupress]

To note, this is part of the re-engineering of rewrite equiv into separate code matching and contextual call rewriting (as per discussions on the old PR).

Providing smarter code matching could help in reduction steps. Providing better contextual call rewriting could help in Hoare goals. (Where we rewrite a procedure call into another procedure on which we may already have a useful lemma.)

[fdupress]

@Cameron-Low Not a fan of the @ notation for the LV. Does the following work?

outline {m} [s - e] lv <@ M.foo

[Cameron-Low]

Without playing shift/reduce whack-a-mole, I can get outline {m} [s - e] lv <@ M.foo but for the non LV variant it would need to be something like outline {m} [s - e] _ <@ M.foo.

[fdupress]

@strub and @bgregoir do you have opinions on the syntax?

It would also be good to have a quick look at code if you have time.
Cameron will be removing zip soon, and creating a wiki page once generally content with quality.

[strub]

I left 2 comments. Otherwise, LGTM.

[strub]

Also, your PR description should be in the commit description.

[Cameron-Low]

@strub, the most recent commit should address all the comments you had.

[Cameron-Low]

Most recent push was just an amendment to the commit message. Otherwise shall I merge this?

[fdupress]

It's approved: merge and add doc to the wiki. (Not necessarily in that order, but merging is probably best done with a bit of padding before people leave for the holidays.)