{-# LANGUAGE TypeSynonymInstances, ScopedTypeVariables, MultiParamTypeClasses, 
             FlexibleInstances, FunctionalDependencies #-}

-- JavaLight+ and its compiler into an assembly language

-- 16.3.2018

module Java2 where
		      
import Painter (readFileAndDo,Tree(F),update,updList)
import Compiler (Compiler,Trans,runC,cplus,csum,token,tchar,string,tstring,
		 tbool,tint,tidentifier,trelation,rel)

mkInt b = if b then 1 else 0

-- stack machine

data Jstate = Jstate {stack,io :: [Int],ba,stp,pc :: Int}

data SymAdr = BA | STP | TOP | Dex SymAdr Int | Con Int deriving (Eq,Show)

baseAdr :: Int -> Int -> SymAdr
baseAdr declDep dep = if declDep == dep then BA else Dex BA declDep
			
absAdr,contents :: Jstate -> SymAdr -> Int
absAdr _ (Con i)           = i
absAdr state BA            = ba state
absAdr state STP           = stp state
absAdr state TOP           = length $ stack state
absAdr state (Dex BA i)    = ba state+i
absAdr state (Dex STP i)   = stp state+i
absAdr state (Dex TOP i)   = length (stack state)+i
absAdr state (Dex adr i)   = contents state adr+i
contents state (Dex adr i) = s!!!(k-i) where (s,k) = stackPos state adr
contents state adr         = absAdr state adr

(x:s)!!!0 = x
(x:s)!!!n | n > 0 = s!!!(n-1)
s!!!n = error $ show n

stackPos :: Jstate -> SymAdr -> ([Int],Int)
stackPos state adr = (s,length s-1-contents state adr) where s = stack state

updState :: Jstate -> SymAdr -> Int -> Jstate
updState state BA x          = state {ba = x}
updState state STP x         = state {stp = x}
updState state (Dex adr i) x = state {stack = updList s (k-i) x}
			       where (s,k) = stackPos state adr
		
-- assembly language

data StackCom = PushA SymAdr | Push SymAdr | Pop | Save SymAdr |
		Move SymAdr SymAdr | Add | Sub | Mul | Div | Or_ | And_ | Inv | 
		Cmp String | Jump SymAdr | JumpF Int | Read SymAdr | Write
		deriving (Eq,Show)

executeCom :: StackCom -> Jstate -> Jstate
executeCom com state = 
           case com of 
	        PushA adr     -> state' {stack = absAdr state adr:stack state}
                Push adr      -> state' {stack = contents state adr:stack state}
	        Pop           -> state' {stack = tail $ stack state}
	        Save adr      -> updState state' adr $ head $ stack state
		Move adr adr' -> updState state' adr' $ contents state adr     
		Add           -> applyOp state' (+)
		Sub           -> applyOp state' (-) 
		Mul           -> applyOp state' (*) 
		Div           -> applyOp state' div 
		Or_           -> applyOp state' max
		And_          -> applyOp state' (*)
		Inv           -> state' {stack = (a+1)`mod`2:s}  
	                         where a:s = stack state
	        Cmp str       -> state' {stack = mkInt (rel str b a):s}
			         where a:b:s = stack state
                Jump adr      -> state {pc = contents state adr}
		JumpF lab     -> state {pc = if a == 0 then lab else pc state+1, 
	                                stack = s}
			         where a:s = stack state
	        Read adr    -> if null s then state' 
		 	       else (updState state' adr $ head s) {io = tail s}
			       where s = io state
	        Write       -> if null s then state' 
		 	       else state' {io = io state++[head s]}
		               where s = stack state
	   where state' = state {pc = pc state+1}				

applyOp :: Jstate -> (Int -> Int -> Int) -> Jstate
applyOp state op = state {stack = op b a:s} where a:b:s = stack state

execute :: [StackCom] -> Jstate -> Jstate
execute cs state = if curr >= length cs then state
	           else execute cs $ executeCom (cs!!curr) state
		   where curr = pc state

-- JavaLight+

data JavaLightP commands command exp sum prod factor disjunct conjunct literal 
		formals actuals =
     JavaLightP {seq_         :: command -> commands -> commands,
	         embed        :: command -> commands,
     	         block        :: commands -> command,
     	         assign       :: String -> exp -> command,
	         applyProc    :: String -> actuals -> command,
	         cond         :: disjunct -> command -> command -> command,
	         cond1,loop   :: disjunct -> command -> command,
	         read_        :: String -> command,
		 write_       :: exp -> command,
		 vardecl      :: String -> TypeDesc -> command,
		 fundecl      :: String -> formals -> TypeDesc -> commands 
	      			        -> command,
		 formals      :: [Formal] -> formals,
		 embedS       :: sum -> exp,
		 sum_         :: prod -> sum,
		 plus,minus   :: sum -> prod -> sum,
		 prod         :: factor -> prod,
     	         times,div_   :: prod -> factor -> prod,
     	         embedI	      :: Int -> factor,
     	         varInt       :: String -> factor,
		 applyInt     :: String -> actuals -> factor,
		 encloseS     :: sum -> factor,
		 embedD       :: disjunct -> exp,
		 disjunct     :: conjunct -> disjunct -> disjunct,
		 embedC       :: conjunct -> disjunct,
     	         conjunct     :: literal -> conjunct -> conjunct,
		 embedL       :: literal -> conjunct,
     	         not_         :: literal -> literal,
		 atom         :: String -> sum -> sum -> literal,
		 embedB       :: Bool -> literal,
		 varBool      :: String -> literal,
		 applyBool    :: String -> actuals -> literal,
		 encloseD     :: disjunct -> literal,
		 actuals      :: [exp] -> actuals}

-- subsignature of derec(JavaLightP)

data SumProd sum sumsect prod prodsect factor = 
     SumProd {sum'         :: prod -> sumsect -> sum,
              plus',minus' :: prod -> sumsect -> sumsect,
              nilS         :: sumsect,
              prod'        :: factor -> prodsect -> prod,
              times',div'  :: factor -> prodsect -> prodsect,
              nilP         :: prodsect}
     	        
-- extension of JavaLightP- to SumProd-algebras

derec :: JavaLightP s1 s2 s3 sum prod factor s4 s5 s6 s7 s8
	 -> SumProd sum (sum -> sum) prod (prod -> prod) factor
	 
derec alg = SumProd {sum' = \a g -> g $ sum_ alg a,
		     plus' = \a g x -> g $ plus alg x a,
		     minus' = \a g x -> g $ minus alg x a,
		     nilS = id,
		     prod' = \a g -> g $ prod alg a,
		     times' = \a g x -> g $ times alg x a,
		     div' = \a g x -> g $ div_ alg x a,
		     nilP = id}

-- stack algebra

data TypeDesc = INT | BOOL | UNIT | Fun TypeDesc Int | ForFun TypeDesc 

data Formal = Par String TypeDesc | FunPar String [Formal] TypeDesc
	
type Symtab = String -> (TypeDesc,Int,Int)      -- (td,depth,relAdr)

type ComStack   = Int -> Symtab -> Int -> Int    -> ([StackCom],Symtab,Int)
	       -- label            depth  relAdr    (code,st,relAdr)
type ExpStack   = Int -> Symtab -> Int           -> ([StackCom],TypeDesc)
	       -- label            depth    	    (code,td)
type FormsStack = Symtab -> Int -> Int           -> ([ComStack],Symtab,Int)
               --           depth  relAdr	    (commands,st,relAdr)
type ActsStack  = Int -> Symtab -> Int           -> ([StackCom],Int)
               -- label            depth            (code,actsLg)

javaStackP :: JavaLightP ComStack ComStack ExpStack ExpStack ExpStack ExpStack 
		         ExpStack ExpStack ExpStack FormsStack ActsStack 
javaStackP = JavaLightP {seq_       = seq_,
		         embed      = id,
		         block      = block, 
                         assign     = assign,
			 applyProc  = applyProc,
			 cond       = cond,
			 cond1      = cond1,
                         loop       = loop,
			 read_      = read_,
			 write_     = write_,
			 vardecl    = vardecl,
			 fundecl    = fundecl,
			 formals    = formals,
			 embedS     = id,
			 sum_       = id, 
			 plus       = apply2 Add,
			 minus      = apply2 Sub,
			 prod       = id,
		         times      = apply2 Mul,
		         div_       = apply2 Div,
			 embedI     = \i _ _ _ -> ([Push $ Con i],INT),
			 varInt     = var,
			 applyInt   = applyFun,
			 encloseS   = id, 
			 embedD     = id,
			 disjunct   = apply2 Or_,
			 embedC     = id,
			 conjunct   = apply2 And_, 
			 embedL     = id,
			 not_       = apply1 Inv,
			 atom       = apply2 . Cmp,
			 embedB     = \b _ _ _ -> ([Push $ Con $ mkInt b],BOOL),
		         varBool    = var,
			 applyBool  = applyFun,
			 encloseD   = id,
			 actuals    = actuals}
		     
 where seq_ :: ComStack -> ComStack -> ComStack
       seq_ c c' lab st dep adr = (code++code',st2,adr2)
                     where (code,st1,adr1) = c lab st dep adr
                           (code',st2,adr2) = c' (lab+length code) st1 dep adr1
       					   
       apply1 :: StackCom -> ExpStack -> ExpStack
       apply1 op e lab st dep = (fst (e lab st dep)++[op],INT)
	
       apply2 :: StackCom -> ExpStack -> ExpStack -> ExpStack
       apply2 op e e' lab st dep = (code++code'++[op],td)
                                 where (code,td) = e lab st dep
                                       code' = fst $ e' (lab+length code) st dep
					      
       block :: ComStack -> ComStack
       block c lab st dep adr = (code',st,adr)
		                where bodylab = lab+dep+3; dep' = dep+1
				      (code,_,local) = c bodylab st dep' dep'
				      code' = Move TOP STP:pushDisplay BA dep++
				              Move STP BA:
			      {- bodylab -}   code++replicate (local-dep') Pop++
					      Save BA:replicate dep' Pop
				      
       pushDisplay :: SymAdr -> Int -> [StackCom]
       pushDisplay reg dep = foldr push [Push reg] [0..dep-1]
       			     where push i code = Push (Dex reg i):code

       assign :: String -> ExpStack -> ComStack
       assign x e lab st dep adr = (fst (e lab st dep)++
       				    [Save $ Dex ba adrx,Pop],st,adr)
		                   where (_,declDep,adrx) = st x
					 ba = baseAdr declDep dep
		
       cond :: ExpStack -> ComStack -> ComStack -> ComStack
       cond e c c' lab st dep adr = (code++JumpF lab2:code1++Jump (Con exit):
       				     code2,st2,adr2)
	                           where (code,_) = e lab st dep
		                         lab1 = lab+length code+1
		                         (code1,st1,adr1) = c lab1 st dep adr
			                 lab2 = lab1+length code1+1
			                 (code2,st2,adr2) = c' lab2 st1 dep adr1
	                                 exit = lab2+length code2
		
       cond1 :: ExpStack -> ComStack -> ComStack
       cond1 e c lab st dep adr = (code++JumpF exit:code',st',adr')
		  	          where (code,_) = e lab st dep
		  	                lab' = lab+length code+1
		  	                (code',st',adr') = c lab' st dep adr
		  	                exit = lab'+length code'
		      
       loop :: ExpStack -> ComStack -> ComStack
       loop e c lab st dep adr = (code++JumpF exit:code'++[Jump $ Con lab],
       				  st',adr')
		  	         where (code,_) = e lab st dep
		  	               lab' = lab+length code+1
		  	               (code',st',adr') = c lab' st dep adr
		  	               exit = lab'+length code'+1
					
       read_ :: String -> ComStack
       read_ x _ st dep adr = ([Read $ Dex ba adrx],st,adr)
		              where (_,declDep,adrx) = st x
				    ba = baseAdr declDep dep
					    
       write_ :: ExpStack -> ComStack
       write_ e lab st dep adr = (fst (e lab st dep)++[Write,Pop],st,adr)
		
       vardecl :: String -> TypeDesc -> ComStack
       vardecl x td _ st dep adr = ([Push $ Con 0],update st x (td,dep,adr),
       				    adr+1)
				    
       fundecl :: String -> FormsStack -> TypeDesc -> ComStack -> ComStack 
       fundecl f pars td body lab st dep adr = (code',st1,adr+1)
		              where codelab = lab+2
		                    st1 = update st f (Fun td codelab,dep,adr)
				    dep' = dep+1
			            (parcode,st2,_) = pars st1 dep' $ -2
				    coms = foldl1 seq_ $ parcode++[body] 
				    bodylab = codelab+dep+2
				    (code,_,local) = coms bodylab st2 dep' dep'
				    retlab = Dex TOP $ -1
				    exit = bodylab+length code+local+1
				    code' = Push (Con 0):Jump (Con exit):
		             {- codelab -}  Move TOP BA:pushDisplay STP dep++
			     {- bodylab -}  code++replicate local Pop++
			   		    [Jump retlab]
			     {- exit -}
			                   
       formals :: [Formal] -> FormsStack
       formals pars st dep adr = foldl f ([],st,adr) pars 
            where f (cs,st,adr) (Par x td) = (cs,update st x (td,dep,adr'),adr')
	   				     where adr' = adr-1
	          f (cs,st,adr) (FunPar x@('@':g) pars td) = (cs++[c],st',adr')
		                where adr' = adr-3
		                      st' = update st x (ForFun td,dep,adr')
		                      c = fundecl g (formals pars) td $ assign g 
		                     	   $ applyFun x $ actuals $ map act pars
		                      act (Par x _) 	     = var x
		                      act (FunPar (_:g) _ _) = var g
					
       var :: String -> ExpStack
       var x _ st dep = case td of 
                             Fun _ codelab -> ([Push ba,Push $ Con codelab,
			  	                PushA $ Dex ba adr],td)
			     _ -> ([Push $ Dex ba adr],td)
	                where (td,declDep,adr) = st x
		              ba = baseAdr declDep dep

       applyFun :: String -> ActsStack -> ExpStack
       applyFun f pars lab st dep = 
            case td of Fun td codelab -> (code ba (Con codelab) $ Dex ba adr,td)
	               ForFun td      -> (code (Dex ba adr) (Dex ba $ adr+1)
	                                       $ Dex (Dex ba $ adr+2) 0,td) 
	    where (td,declDep,adr) = st f
	          (parcode,parLg) = pars lab st dep 
	          retlab = lab+length parcode+4
	          ba = baseAdr declDep dep
	          code ba codelab result = parcode++Push BA:Move ba STP:
					   Push (Con retlab):Jump codelab:
	                    {- retlab -}   Pop:Save BA:Pop:replicate parLg Pop++
			                   [Push result]
	       
       applyProc :: String -> ActsStack -> ComStack
       applyProc p = assign p . applyFun p
			         
       actuals :: [ExpStack] -> ActsStack
       actuals pars lab st dep = foldr f ([],0) pars
          where f e (code,parLg) = (code++code',parLg+case td of Fun _ _ -> 3
			                 		         _ -> 1)
		                   where (code',td) = e (lab+length code) st dep
				 		  
-- JavaLight+-compiler into the assembly language
		
typedesc :: Compiler m => Trans m TypeDesc
typedesc = csum [do string "Int"; return INT,
                 do string "Bool"; return BOOL]
                 
list :: Compiler m => Trans m a -> Trans m [a]
list comp = do tchar '('; csum [do tchar ')'; return [], nelist]
            where nelist = do a <- comp
                              csum [do tchar ','; as <- nelist; return $ a:as, 
			            do tchar ')'; return [a]]

compJava :: Compiler m => JavaLightP s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11
	                  -> Trans m s1
compJava alg = commands where
           alg' = derec alg
           commands = do c <- command
           		 csum [do cs <- commands; return $ seq_ alg c cs,
           		       return $ embed alg c]
           command = csum [do tstring "if"; e <- disjunctC; c <- command
			      csum [do tstring "else"; c' <- command
			     	       return $ cond alg e c c', 
			            return $ cond1 alg e c], 
		           do tstring "while"; e <- disjunctC; c <- command
		              return $ loop alg e c,
	   	           do tstring "read"; x <- tidentifier; tchar ';'
			      return $ read_ alg x,
	  	           do tstring "write"; e <- expC ';'
			      return $ write_ alg e,
	  	           do tchar '{'; cs <- commands; tchar '}'
			      return $ block alg cs,
			   do td <- token typedesc; x <- tidentifier
			      csum [do pars <- formalsC
			               tchar '{'; cs <- commands; tchar '}'
			               return $ fundecl alg x pars td cs,
			            do tchar ';'; return $ vardecl alg x td],
	  	           do x <- tidentifier
			      csum [do tchar '='; e <- expC ';'
			               return $ assign alg x e,
				    do pars <- formalsC
			               tchar '{'; cs <- commands; tchar '}'
			               return $ fundecl alg x pars UNIT cs,
			            do pars <- actualsC
			               return $ applyProc alg x pars]]
	   expC sym = csum [do e <- sumC; tchar sym; return $ embedS alg e,
	                    do e <- disjunctC; tchar sym; return $ embedD alg e]
           sumC = do e <- prodC; f <- sumsect; return $ sum' alg' e f
           sumsect = csum [do op <- csum $ map tchar "+-"
	                      e <- prodC; f <- sumsect
	                      return $ if op == '+' then plus' alg' e f
	                                            else minus' alg' e f,
	                   return $ nilS alg']
           prodC = do e <- factor; f <- prodsect; return $ prod' alg' e f
	   prodsect = csum [do op <- csum $ map tchar "*/"
	                       e <- factor; f <- prodsect
	                       return $ if op == '*' then times' alg' e f
	                                             else div' alg' e f,
	                    return $ nilP alg']
           factor = csum [do i <- tint; return $ embedI alg i,
		          do x <- tidentifier
			     csum [do pars <- actualsC
			    	      return $ applyInt alg x pars,
	                           do return $ varInt alg x],
			  do tchar '('; e <- sumC; tchar ')'
			     return $ encloseS alg e]
           disjunctC = do e <- conjunctC
           		  csum [do tstring "||"; e' <- disjunctC
           		           return $ disjunct alg e e',
           		  	return $ embedC alg e]
           conjunctC = do e <- literal
	                  csum [do tstring "&&"; e' <- conjunctC
	                           return $ conjunct alg e e',
	                  	return $ embedL alg e]
           literal = csum [do b <- tbool; return $ embedB alg b,
			   do tchar '!'; e <- literal; return $ not_ alg e, 
	              	   do e <- sumC; rel <- trelation; e' <- sumC
			      return $ atom alg rel e e',
			   do x <- tidentifier
			      csum [do pars <- actualsC
			      	       return $ applyBool alg x pars,
	                            do return $ varBool alg x],
			   do tchar '('; e <- disjunctC; tchar ')'
			      return $ encloseD alg e]
	   formal = csum [do td <- token typedesc; x <- tidentifier
	   		     csum [comp x td, return $ Par x td],
	   		  do x <- tidentifier; comp x UNIT]
	            where comp g td = do pars <- list formal
	  		                 return $ FunPar ('@':g) pars td
	   formalsC = do pars <- list formal; return $ formals alg pars
	   actualsC = do tchar '('
	                 pars <- csum [do tchar ')'; return [], comp]
	  		 return $ actuals alg pars
	              where comp = csum [do e <- expC ')'; return [e],
				         do e <- expC ','; es <- comp
				            return $ e:es]
           
java2stack :: String -> [Int] -> IO ()
java2stack file input = readFileAndDo file act where
               act str = case runC (compJava javaStackP) ((1,1),str) of 
        		      Left str -> putStrLn str
			      Right a -> continue a
               continue :: ComStack -> IO ()
	       continue a = do writeFile "javacode" $ showCode code
			       putStrLn $ "io = "++show (io $ execute code init)
		            where (code,_,_) = a 0 (const (INT,0,0)) 0 0
				  init = Jstate [] input 0 0 0
	     			      
showCode :: [StackCom] -> String
showCode = concat . zipWith addLab [0..] . map show

addLab :: Int -> String -> String
addLab n str = '\n':replicate (5-length lab) ' '++lab++": "++str
	       where lab = show n
					  
{- Examples					contents of the io stream

   Int x; read x; Int fact; fact=1; 
   while x>1 {fact=x*fact; x=x-1;} write fact;	[x] --> [x!]

   Int f(Int x) {if x<2 f=1; else f=x*f(x-1);} 		       
   Int x; read x; write f(x);			[x] --> [x!]

   f(Int x,Int fact) {if x<2 write fact; else f(x-1,x*fact)} 		       
   Int x; read x; f(x,1)			[x] --> [x!]
      
   Int f(Int x,Int g(Int x,Int y)) {if x<2 f=1; else f=g(x,f(x-1,g));}    
   Int g(Int x,Int y) {g=x*y;}				       
   Int x; read x; write f(x,g);			[x] --> [x!]           
   
   Int add(Int x,Int y) {if x==0 add=y; else add=add(x-1,y)+1;} 	
   Int x; Int y; read x; read y; 
   write add(x,y);	       			[x,y] --> [x+y]
   
   Int iter(Int f(Int x),Int x,Int n)
           {if n==0 iter = x; else iter = f(iter(f,x,n-1));}
   Int f(Int x) {f = x*5;} Int x; read x; Int n; read n; write iter(f,x,n);
   						[x,n] --> [x*5^n]

   Int f(Int x) {Int g(Int x) {if x<2 g=1; else g=x*f(x-1);} 
		 if x<2 f=1; else f=x+g(x-1);}         
   Int x; read x; write f(x);
    
   Int f(Int x,Bool b) {if x<2 || !b f=1; else f=x*f(x-1,b);}    
   Int x; read x; Bool b; read b;		[x,0] --> [1]
   write f(x,b);				[x,1] --> [x!]
    
   Int f(Int x,Bool b) {if x<2 || !b f=1; else f=x*f(x-1,b);}    
   Int x; read x; 				[x] -- x < 8  --> [x!]
   write f(x,x<8);				[x] -- x >= 8 --> [1]

   Int f(Int g(Int x),Int x) {f=g(g(x));} 			       
   Int h(Int x) {h=3*x;} 
   Int x; read x; write f(h,x);			[13] --> [117]

   Int f(Int g(Int x),Int x) {Int z() {z=g(x);} f=g(z());}
   Int h(Int x) {h=3*x;} 					
   Int x; read x; write f(h,x);			[13] --> [117]     
    
   Int f(Int g(Int x),Int x) {Int z(Int x) {z=g(x);} f=z(g(z(x)));}
   Int h(Int x) {h=3*x;} 
   Int x; read x; write f(h,x);                 [13] --> [351]         
    
   Int h(Int x) {h=3*x;} 
   Int f(Int g(Int x),Int x) {Int z(Int g(Int x)) {z=g(x);} f=h(g(z(h)));}
   Int x; read x; write f(h,x);			[13] --> [351]  
    
   Int f(Int x,Int g(Int x),Int y,Int z) {f=x+g(y)-z;}   	       
   Int h(Int x) {h=5+3*x;} 
   Int x; read x; write f(22,h,x+x,6);   	[13] --> [99]

   Int h(Int x) {h=x+x;} Int z; read z; 
   Int f(Int g(Int x),Int x) {Int y; y=11; f=x+h(25)+y+z;} 
   write f(h,33);				[13] --> [107]
   
   Int f(Int g(Int x),Int x,Int y,Bool b(Int x),Bool c) 		       
        {if b(x) f=2*g(x); else f=g(y);} 
   Int h(Int x) {h=10*x;} 
   Bool b(Int x) {b=x<=5;} 	    	        [5]  --> [100]
   Int x; read x; write f(h,x,x+3,b,x<=5); 	[13] --> [160]

   Int f(Int x,Int y) {if x>6 f=x-y; else f=x+y;} 	      
   Int x; read x;				[6] --> [61]
   Int y; y=55; write f(x,y);			[7] --> [-48]

   Int x; read x; 
   if x<1 {Int x; x=222;} else x=222;    	[-5] --> [-5]
   write x;					[5]  --> [222]
						
   Int n; read n; Int x; x=2; 			[n] --> [2^x | x <- [1..], 
   while x<n {write x; x=2*x;}                                 2^x < n]
						
   Int x; x=1; Int upb; read upb;
   map(Int f(Int x)) {while x<=upb {write x; x=x+1;} read x;
   		      while x<upb {write f(x); read x;} write f(x);}      
   Int f(Int x) {f=x*x;} map(f) 	        [upb] --> [1,4,9,16,...,upb*upb]
 						
   Int x; x=1; Int upb; read upb;
   map(f(Int x)) {while x<=upb {write x; x=x+1;} read x;
   		  while x<upb {f(x) read x;} f(x)}      
   f(Int x) {write x*x;} map(f) 	        [upb] --> [1,4,9,16,...,upb*upb]
   
   Bool x; read x; Bool y; read y; write x&&y;
   
   Int x; x=4; {Int x; x=5; {Int x; x=6; {Int x; x=7; write x;} write x;} 
   		write x;}
   write x;              			[] --> [7,6,5,4]
   
   Int f (Int g(Int h(Int x),Int x),Int h(Int x),Int x) {f=g(h,x+1);}          
   Int g (Int h(Int x),Int x) {g=h(x+1);}
   Int h (Int x) {h = x+1;}
   Int x; read x; write f(g,h,x+1);		[x] --> [x+4]
   
   f (Int g(Int h(Int x),Int x),Int h(Int x),Int x) {write g(h,x+1);}          
   Int g (Int h(Int x),Int x) {g=h(x+1);}
   Int h (Int x) {h = x+1;}
   Int x; read x; f(g,h,x+1)			[x] --> [x+4]
      
   f (g(h(Int x),Int x),h(Int x),Int x) {g(h,x+1)}          
   g (h(Int x),Int x) {h(x+1)}
   h (Int x) {write x+1;}
   Int x; read x; f(g,h,x+1)			[x] --> [x+4]

-}