Fine Grained Module Definitions

[Cameron-Low]

The goal of this PR is to introduce a new mechanism that permits the user to create a new module by slightly tweaking an existing module definition.

At present the draft has the following features:

• Introduce new module variables.
• Introduce new local variables.
• Delete/Modify/Add statements at particular code positions
• Delete branches (match support is not currently working fully)
• Modify branch conditions
• Insert new branches around a chunk of code
• Modify the return expression

Syntax (needs work) :

module N = M with {
  var x : t (* add new module variable *)
  proc f [
     var y  : s (* add new local variable *)
     cp +/-/~ { s } (* insert after/insert before/modify a statement *)
     cp -  (* delete a statement *)
     cp + ( e ) (* insert new if statement with condition `e` surrounding the suffix code block *)
     cp - ./?/#cstr (* delete all other branches except true/false/cstr *)
  ] res ~ ( e ) (* change the return expression *)
}

[fdupress]

Can you please edit the message above to add syntax for each of the transformations? This will help in reviewing, independently of also creating a wiki page.

[Cameron-Low]

This is now ready for review. I've made a wiki page to document the features present.