s ::=	x := n
	|  x1 :=  x2 - x3
	|  if x = 0 then s1 else s2
	|  while x=/=0 do s
	|  s1 ; s2	
	
X ::=   .  |  X,x

L  ::=   l1...lm
is ::=   .  |  is; movi rd v  |  is; sub rd ra rb




MACROS:
-------

intendjmp lt =def=					// lt is target  
movi tb B lt; intend tb; movi tg G lt; jmp tg

intendbrz rz lt lf =def=				// rz is cond reg, lf is fallthrough label, lt is target
movi tb B lf; intend tb; movi tb B lt;  intendz rz' tb; movi tg G lt; brz rz tg

check l =def=						// l is current label
movi tg R l; sub tg tg ri; recovernz tg




 -------- 
| X |- s |
 --------
 
x in X
------------ (wf-assign)
X |- x := n

x1 in X   x2 in X  x3 in X
--------------------------- (wf-sub)
X |- x1 := x2 - x3

x in X   X |- s1   X |- s2
----------------------------- (wf-if)
X |- if x = 0 then s2 else s2

x in X   X |- s
------------------------ (wf-while)
X |- while x =/= 0 do s

X |- s1  X |- s2
------------------ (wf-seq)
X |- s1; s2




 ---------
| Blks(s) |  The number of blocks added by translating s
 ---------

Blks(x := n) = 0
Blks(x1 :=  x2 - x3) = 0
Blks(if x = 0 then s1 else s2) = Blks(s1) + Blks(s2) + 3
Blks(while x=/=0 do s) = 3 + Blks(s)
Blks(s1 ; s2) = Blks(s1) + Blks(s2)	


 
 ---------------- 
| InitRegFile(X) |  Make the initial register file corresponding to X 
 ----------------
 
X = x1 ... xn
R = r1 -> G 0, r1' -> B 0,..., rn -> G 0, rn' -> B 0,
    ri -> B 0,
    tg -> G 0, tb -> B 0
-------------------------------------------------
InitRegFile(X) = R



 
 ---------
| [[X]]_l |	Generate type for label l given variable context X
 ---------
 
 
X = x1 ... xn
a1...an,ahist,ari,atg1,atb1,atb2,atr1 fresh
D = a1:kint, ..., an:kint, ahist:khist, ari: int, atg:kint, atb:kint
A = ahist o l
G = { r1:<G,int,a1>, r1':<g,int,a1>, ..., rn:<G,int,an>, rn':<G,int,an>,
      ri:<R,check,ari>, 
      tg:<G,int,atg>, tb:<B,int,atb> }
--------------------------------------------------------------------------------
[[X]]_l = Forall[D](G,A)
	
	


	
	
	
 ----------------	
| X;P1 |- C : P2 |  Code Memory C is well-typed, but labels in P1 may not have corresponding blocks built yet.
 ----------------

Dom(C) = Dom(P2)
Dom(P1) intersect Dom(P2) = emptyset
Forall n in Dom(P1).
  P1(n) = [[X]]_n
Forall n in Dom(P2).
  P2(n) = [[X]]_n
  [[X]]_n = All[D]((G,ri-><R,check,Y>),alpha o n)											
  D; (P1 union P2); (G,ri-><R,check,Y>); alpha o n; Y; (P1 u P2) (n+1) |- C(n)	
--------------------------------------------------------------------------------------------- (trans-C-t)
X;P1 |- C : P2





 -------------
| GenPsi(X,L) |	Generate the Code Typing for a set of labels
 -------------
 
 GenPsi(.) = .
 GenPsi(L,l) = GenPsi(L), [[X]]_l





 -----------------
| X |- (D,G) good |
 -----------------
 
D |- G
Forall xk in X. G(rk) = <G,tk,Ek> and G(rk') = <B,tk,Ek'> and D |- Ek = Ek'
G(ri) = <c,ok,Ei>
----------------------------------------------------------------------------------- (GD-good)
X |- (D,G) good





 ------------------
| D;P;G |- is : G' |	Strings together instances of D;P;G |- i : G'  to get the effect of a sequence of instructions
 ------------------

----------------- (is-empty-t)
D;P;G |- . : G


D;P;G |- i : G'  D;P;G' |- is : Gs
----------------------------------- (is-seq-t)
D;P;G |- i;is : Gs




 --------------
| X |- is good |   Good instruction sequences always duplicate code and use valid registers
 --------------

--------------- (is-empty-good)
X |- empty good

xd in X   X |- is good
--------------------------------------- (is-movi-good)
X |- is; movi rd G n; movi rd' B n good

xd in X   X |- is good
xa in X   xb in X
------------------------------------------- (is-sub-good)
X |- is; sub rd ra rb; sub rd' ra' rb' good






 ----------------------
| X |- (L,C,is,l) good |
 ----------------------


Let P1 = GenPsi(L,l)
Let P2 = GenPsi(Dom(C))
X; P1 |- C : P2
X |- is good
---------------------------------------------------------------------------- (partial-trans-ok)
X |- (L,C,is,l) good







 ----------------------------------------
| [[X |- s]] (L,C,is,l) = (L',C',is',l') |   Statement Translation
 ----------------------------------------
 

is' = is; movi rk G v; movi rk' B v
----------------------------------------------------------------- (trans-assign)
[[X |- xk := v ]] (L,C,is,l) = (L,C,is',l)
 

is' = is; sub rk rm rn; sub rk' rm' rn'
----------------------------------------------------------------- (trans-sub)
[[X |- xk := xm - xn ]] (L,C,is,l) = (L,C,is',l)


let lf = l+1									// fallthrough (false) label
let lt = lf + Blks(s1)								// target (true) label
let lj = lt + Blks(s2)								// join label
let bl = (check l); is; intendzbrz rk lf lt
[[X |- s1]] ( (L,lf), C[l -> bl], ., lt ) = (Lt', Ct', ist', lt')
[[X |- s2]] ( (L,lt), C[l -> bl], ., lf ) = (Lf', Cf', isf', lf')
let C' = (Ct' union Cf')[ lt' -> check lt'; ist'; intendjmp lj ][ lf' -> check lf'; isf'; intendjmp lj ]
-------------------------------------------------------------------------------------------------------------- (trans-if)
[[X |- if xk = 0 then s1 else s2 ]] ( L, C, is, l ) = (L,C',.,lj)


let lb = l + 1									// beginning label
let ls = lb + 1									// body (s) label
let le = ls + Blks(s)								// end label
let bl = check l; is; intendjmp lb
let bb = (check lb); intendzbrz rk le ls
[[X |- s]] ( (L,le), C[l -> bl][lb -> bb], ., ls ) = (Ls', Cs', iss', ls')
let bs = check ls'; iss'; intendjmp lb
let C' = Cs'[ ls' -> bs ]
------------------------------------------------------------------------------------------ (trans-while)
[[X |- while xk =/= 0 do s ]] ( L, C, is, l ) = (L, C', . le)



[[X |- s1]] ( L, C, is, l ) = (L1', C1', is1', l1')
[[X |- s2]] ( L1', C1', is1', l1') = (L', C', is', l')
-------------------------------------------------------------- (trans-seq)
[[X |- s1;s2 ]] ( L, C, is, l ) = (L', C', is', l')