TYPE
  prod = Var * Var
  prodset = set(prod)
  State   = lift( prodset)

PROBLEM copy_propagation

  direction  : forward
  carrier    : State
  init       : top
  init_start : lift({})
  combine    : glb


TRANSFER

// in assignments calculate the new value of the variable and add it to the state
  ASSIGN(variable, expression) = 
      let VarCopies <= @ in
        lift(trans(VarCopies - kill(variable) 
                             + gen(variable, expression))
	     )

  CALL(_, param, expression), call_edge = 
     let VarCopies <= @ in
        if (expType(expression) = "VAR" )
        then lift(trans(VarCopies+{(param,expVar(expression))}))
        else @ 
        endif
	   
  CALL(_, param, exp), local_edge = top
//* 28: */  
  END(_, param) =
      let VarCopies <= @ in
        lift(VarCopies - {(x,param)|x in vars}
                       - {(param,x)|x in vars})
/* 40: */  SUPPORT
  kill :: Var -> prodset
  kill(variable) = {(variable,x)|x in vars} + {(x,variable)|x in vars}

  gen :: Var * Expression -> prodset
  gen(variable, expression) = 
    if expType(expression) = "VAR" then
       {(variable,expVar(expression))}
     else
       {}
     endif

  // Dette kommer til at virke, omend det ikke er en fuld transitiv 
  // lukning (kun et skridt videre i kæden). Det er fordi nye led kun
  // kan tilføjes bag i en kæde. Hvis det skulle være sammen koblingen 
  // af to kæder skulle x og y være i hver sin kæde ved x:=y, men al 
  // information om x slettes jo ved en tildeling x:=y.
  trans :: prodset -> prodset
  trans(VarCopies) = {(x,z)| (x,y) in VarCopies; (y,z) in VarCopies} 
		     + VarCopies 
		     - {(x,x)|x in vars}