[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.

Code-Positions

Code-positions are simply paths to particular instructions within a code block. Each part of the path has the same form: c1p & x, where c1p is a core position and & x specifies an optional offset from that position. To specify instructions that are nested inside code blocks, you can use branch selectors bsel to piece together these parts to form the full path: c1p & x bsel c1p & y.

The branch selectors are:

• . : true branch of a conditional
• ? : false branch of a conditional
• #C. : the branch of a match corresponding to the constructor C

There are two types of core positions:

• Direct, n: The n'th instruction in the block
• Instruction, ^ i{n}: The n'th instruction of type i. (defaults to first if left unspecified)

For specifying the instruction type, there are the following options:

• <-: assignment
• x<-: assignment to variable x
• <$: sampling
• x<$: sampling to variable x
• <@: procedure call
• x<@: procedure call returning to variable x
• if: if statement
• while: while statement
• match: match statement

Example

Consider the following meaningless code:

x <- 2;
y <$ {0,1};
x <- x + y;
if (y = 0) {
  r <@ M.Check(x);
  match r with
  | Some v => {
    z <- 2;
  } 
  | None => {
    z <- 1;
  }
  end;
} else {
  z <- 3;
}
z <- x + z;

Let's evaluate some code positions.

• 1 = x <- 2;
• ^ <- = x <+ 2;
• ^ x<- = x <- 2;
• ^ x<-{2} = x <- x - y;
• ^ <$ = y <$ {0,1};
• ^ y<$ = y <$ {0,1};
• ^ x<-{2} & -1 = y <$ {0, 1};
• ^ if = if (y = 0) ...
• ^ if?1 = z <- 3;
• ^ if?^ z<- = z <- 3;
• ^ if.^ match#Some.1 = z <- 2;
• ^ if.^ match#None.^ <- = z <- 1;
• ^ if.^ <@ & 1 #Some.^ z<- = z <- 2;

More

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