TYPE

  VarSetLifted = lift(VarSet)


PROBLEM Faint_Variables

  direction  : backward
  carrier    : VarSetLifted
  init       : top
  init_start : allvars()
  combine    : glb

TRANSFER

  ASSIGN(v, e) =
      let faint <= @ in
         if (v ? faint) then
	   // if 'v' is faint, we don't care about the vars in the exp.
           lift(faint)
	 else
	   // but if it isn't, the vars in 'e' can't be faint
	   // either.
           lift(faint - variables(e))
         endif

  IF(e) =
      let faint <= @ in
        lift(faint - variables(e))
  
  WHILE(e) =
      let faint <= @ in
        lift(faint - variables(e))

  CALL(_, p, e) =
      let faint <= @ in
         if (p ? faint) then
	   // if 'p' is faint, we don't care about the vars in the
           // exp.  It's all assignments to a formal param. which
	   // wont get used anyway.
           lift(faint)
	 else
	   // but if it isn't, the vars in 'e' can't be faint
	   // either, 'cause the assign to the parameter.
           lift(faint - variables(e))
         endif

// FIXME: to do the stuff above, I need to move local variables all
// over the program, since I have found no way of distinguishing
// local from global variables.


SUPPORT

  allvars :: -> VarSetLifted
  allvars() = lift(vars)

  subExpressions :: Expression -> ExpressionSet
  subExpressions(expression) =
    case expType(expression) of
      "ARITH_BINARY" => subExpressions(expSubLeft(expression)) lub
                        subExpressions(expSubRight(expression));
      "ARITH_UNARY"  => subExpressions(expSub(expression));
      "BOOL_BINARY"  => subExpressions(expSubLeft(expression)) lub
                        subExpressions(expSubRight(expression));
      "BOOL_UNARY"   => subExpressions(expSub(expression));
      _              => {}; 
    endcase
    + expression

  variables :: Expression -> VarSet
  variables(expression) =
    { expVar(exp) | exp in subExpressions(expression);
                    expType(exp) = "VAR" }