[Feature] Module Tweaks

Module tweaks is a feature that allows one to make small changes to previously defined modules.

Syntax

The general syntax for module tweaks is as follows:

module N = M with {
  (* add module variables *) 
  var x, y, z : t
  var a, b : s

  (* update procedures *)
  proc f [
    (* introduce new local variables *)
    var h, i : v
    var j : w
    (* updates *)
    _stmt_update_
    _cond_update_
  ] res ~ (e) (* Change the return expression of `g` *)
}.

There are two types of procedure updates:

• Statement updates:
  • cp - : delete the statement at code-position cp
  • cp + { s } : add the statement s after code-position cp
  • cp - { s } : add the statement s before code-position cp
  • cp ~ { s } : change the statement s at code-position cp
• Condition updates:
  • cp - . : collapse a conditional at code-position cp to it's true branch
  • cp - ? : collapse a conditional at code-position cp to it's false branch
  • cp - #C. : collapse a match at code-position cp to the C constructor branch
  • cp ~ (e) : change the condition of the conditional at code-position cp to e
  • cp + (e) : introduce an if statement with condition e after code-position cp with the true branch containing the rest of the block.

Note: Updates are applied one after the other, from bottom to top. Listing changes in chronological order is simplest way to apply updates safely.

For more detail on the structure of code positions, see here

More

For more examples see: tests/fine-grained-module-defs.ec