Location matching

Syntax

Extend the syntax of declarations with:
 
D ::= ...
| if (a == b) { D } else { D } (Dec If)
 

Dynamic semantics

The new rules are:
 
l[if (m == m) { D } else { E } t] l[D t] ( If true)
l[if (m == n) { D } else { E } t] l[E t] ( If false) [m  n]
 

Static semantics

Add hypotheses a == b to contexts, typed as:
 
a : location
b : location
(Con If)
a == b : context
 
a : location
b : location
(Serializable If)
a == b : serializable context
 
Add the location matching judgements:
 
(Eq Id)
, a == b,  a == b
 
(Eq Refl)
a == a
 
a == b
b == c
(Eq Trans)
a == c
 
a == b
(Eq Symm)
b == a
 
Add the subtyping rules:
 
a == b
(Sub Eq)
at a T <: at b T
 
a == b
a : T
(Val Eq)
b : T
 
Add the type rule:
 
a : location
b : location
, a == b D : 
E : 
(Dec If)
if (a == b) { D } else { E } : 
 

Subject reduction

Proposition If   N : network and N * M then   M : network.