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;