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
• ^()<-: assignment to a tuple
• ^(x)<-: assignment to a tuple that contains the 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

Code Position Ranges

To select a block of code you can use a range of code positions. There are two flavours:

1. Explicit [cp .. cp] : specify the start and end of the block with two code positions. These must delimit the same block.
2. Relative [cp - c1p & x] : specify the start of the block with a code position and the end with a core position c1p, with optional offset x, that is relative to the start position. This will always delimit the same code block.

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;
  (x, y) <- (1,0);
}
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?^ ()<- = (x, y) <- (1,0);
• ^ if?^ (y)<- = (x, y) <- (1,0);
• ^ if.^ match#Some.1 = z <- 2;
• ^ if.^ match#None.^ <- = z <- 1;
• ^ if.^ <@ & 1 #Some.^ z<- = z <- 2;
• [^ x<- .. ^ x<-{2}] = x <- 2; y <$ {0,1};x <- x + y;
• [^ x<- - ^ x<-] = x <- 2; y <$ {0,1};x <- x + y;