MACHINE STATE SYNTAX
~~~~~~~~~~~~~~~~~~~~~

colors		c  ::=  B  |  G  |  R
values 		v  ::=  c n
 
registers	r  ::=   ri  |  r1  |  ...  |  rn
reg file	R  ::=  {r->v,...,r->v}

instructions	i  ::=  movi rd v   	     	// rd := v
			|  sub rd rs1 rs2      	// rd := rs1 - rs2
			|  intend rt	     	// intend to jump to rt (ri := rt)
	 		|  intendz rz rt     	// if rz = 0 then intend to jump to rt 
			|  recovernz rz	     	// if rz != 0, branch to fault recovery code

block		b  ::=  i;b  | jmp rt  |  brz rz rt

Code Memory	C  ::=  {n->b,...,n->b}

History       	h  ::= l1 ... lk     		// often written (h,lk) when only the last loc is needed


State          S ::= (C, h, R, b) 
Machine States MS ::= S | recover(h) | hw-error(h)

 
 
 
TYPING SYNTAX
~~~~~~~~~~~~~~

Kinds		k  ::=  kint | kseq
Exp Contexts	D  ::=  .  |  D, x:k
Substitutions   S  ::=  .  |  S, E/x

ri types	rit::=  ok  |  go  |  goz  |  check
base types	t' ::=  int  |  All[D](G,A)  |  rit
static exps	E  ::=  x  |  n  |  E - E  |  E ? E : E

types		t  ::=	<c,t',E>  
reg file type	G  ::=  .  |  G, r->t

type option	to ::=  t  |  undef			
heap typing	P  ::=  .  |  P, n->t	// P(n) = undef if n not in Dom(P)

location seq	seq ::=  empty  |  alpha  |  seq o E

fault tag	f  ::=  c  |  cf
zap tag		Z  ::=  .  |  f   
 


   cf
  / \
  g  b  r
   \ | /
     .