import scala.collection.immutable.{Set => ImmSet,SortedMap,TreeMap,SortedSet,TreeSet}

import scala.util.parsing.combinator._ ;
import scala.util.parsing.input.Positional  ;
import scala.util.matching.Regex ;

/* Comparison utilities. */

object ComparisonUtilities {
  
  def compare2[A <: Ordered[A], B <: Ordered[B]] (a1 : A, b1 : B) (a2 : A, b2 : B) : Int = {
    val cmpA = a1 compare a2
    if (cmpA != 0)
      cmpA
    else
      b1 compare b2
  }
  
  def compare3[A <: Ordered[A], B <: Ordered[B], C <: Ordered[C]] (a1 : A, b1 : B , c1 : C) (a2 : A, b2 : B, c2 : C) : Int = {
    val cmpA = a1 compare a2
    if (cmpA != 0)
      cmpA
    else {
      val cmpB = b1 compare b2
      if (cmpB != 0)
        cmpB
      else
        c1 compare c2
    }
  }
  
  def compare4[A <: Ordered[A], B <: Ordered[B], C <: Ordered[C], D <: Ordered[D]] (a1 : A, b1 : B , c1 : C, d1 : D) (a2 : A, b2 : B, c2 : C, d2 : D) : Int = {
    val cmpA = a1 compare a2
    if (cmpA != 0)
      cmpA
    else {
      val cmpB = b1 compare b2
      if (cmpB != 0)
        cmpB
      else {
	val cmpC = c1 compare c2
	if (cmpC != 0)
	  cmpC
	else
          d1 compare d2
      }
    }
  }
  
  def compareLists[A <% Ordered[A]] (l1 : List[A], l2 : List[A]) : Int = (l1,l2) match {
    case (hdA :: tlA, hdB :: tlB) => {
      val cmpHD = hdA compare hdB
      if (cmpHD != 0)
        cmpHD
      else
        compareLists(tlA,tlB)
    }
    case (List(),List()) => 0 
    case (hd :: tl,List()) => 1    
    case (List(),hd :: tl) => -1
  }
}



/* S-Expressions. */

object SExp {
  var shouldNamesBeSymbols = true
  
  def apply(list : List[SExp]) : SExp = list match {
    case hd :: tl => :+:(hd,apply(tl))
    case Nil => SNil()
  }
  
  def apply(list : List[SExp], tombstone : SExp) : SExp = list match {
    case hd :: tl => :+:(hd,apply(tl,tombstone))
    case Nil => tombstone
  }
  
  def parseAllIn (filename : String) : SExp = {
    val input = scala.io.Source.fromFile(filename).mkString("")
    parseAll(input)
  }
  
  def parseAll (input : String) : SExp = {
    val p = new SExpParser
    p.parse(input)
  }
  
  private var maxSerialNumber = 0
  
  def allocateSerialNumber() : Long = {
    maxSerialNumber += 1
    maxSerialNumber
  }
}

abstract class SExp extends Positional {
  lazy val serialNumber : Long = SExp.allocateSerialNumber()
  
  def toString : String ;
  
  def toList : List[SExp] ;
  def toDottedList : (List[SExp],SExp) ;
  
  def isInteger : Boolean ;
  def isString : Boolean ;
  def isChar : Boolean ;
  def isBoolean : Boolean ;
  def isList : Boolean ;
  def isPair : Boolean ; 
  def isNull : Boolean ;
  def isSymbol : Boolean ;
  def isName : Boolean ;
}


final case class SInt(val value : BigInt) extends SExp {
  override def toString = value.toString

  def toList = throw new Exception("Cannot convert integer to list.")
  def toDottedList = (List(),this)

  def isInteger = true
  def isString = false
  def isChar = false
  def isBoolean = false
  def isList = false
  def isPair = false
  def isNull = false
  def isName = false
  def isSymbol = false
}


final case class SChar(val value : Char) extends SExp {
  override def toString = "#\\" + value.toString

  def toList = throw new Exception("Cannot convert integer to list.")
  def toDottedList = (List(),this)

  def isInteger = false
  def isString = false
  def isChar = true
  def isBoolean = false
  def isList = false
  def isPair = false
  def isNull = false
  def isName = false
  def isSymbol = false
}


final case class SText(val value : String) extends SExp {
  // TODO/FIXME: Escape the string value
  override def toString = "\"" + value + "\""

  def toList = throw new Exception("Cannot convert string to list.")
  def toDottedList = (List(),this)

  def isInteger = false
  def isString = true
  def isChar = false
  def isBoolean = false
  def isList = false
  def isPair = false
  def isNull = false
  def isName = false
  def isSymbol = false
}


case class SBoolean(val value : Boolean) extends SExp {
  override def toString = (if (value) { "#t" } else { "#f" })

  def toList = throw new Exception("Cannot convert Boolean to list.")
  def toDottedList = (List(),this)

  def isFalse = value

  def isInteger = false
  def isString = false
  def isChar = false
  def isBoolean = true
  def isList = false
  def isPair = false
  def isNull = false
  def isName = false
  def isSymbol = false  
}


abstract case class SSymbol (val string : String) extends SExp {
}


final case class SName(val s : String, val version : Int) extends SSymbol(s) with Ordered[SName] {
  def compare (that : SName) : Int = that match {
    case SName(s2,v2) => {
      val cmpString = s compare s2
      if (cmpString != 0)
        cmpString
      else
        version compare v2
    }
  }

  override def toString = 
    if (version == 0) {
      string
    } else {
      if (SExp.shouldNamesBeSymbols) 
        s + "$$" + version
      else
        "#name[" + string + " " + version + "]"
    }

  def toList = throw new Exception("Cannot convert symbol to list.")
  def toDottedList = (List(),this)

  def isInteger = false
  def isString = false
  def isChar = false
  def isBoolean = false
  def isList = false
  def isPair = false
  def isNull = false
  def isSymbol = true
  def isName = true

  override def equals (a : Any) = a match {
    case SName(s2,v2) => (s equals s2) && (version == v2)
    case _ => false
  }
}

final case class SNil() extends SExp {
  override def toString = "()"

  def toList = List()
  def toDottedList = (List(),this)

  def isInteger = false
  def isString = false
  def isChar = false
  def isBoolean = false
  def isList = true
  def isPair = false
  def isNull = true
  def isName = false
  def isSymbol = false
}

final case class :+:(var car : SExp, var cdr : SExp) extends SExp {
  override def toString = this.toDottedList match {
    case (l,SNil()) => "(" + (l mkString " ") + ")"
    case (l,end) => "(" + ((l mkString " ") + " . " + end) + ")"
  }

  def toList = car :: cdr.toList
  def toDottedList : (List[SExp],SExp) = {
    val (lst,end) = cdr.toDottedList
    return (car :: lst, end)
  }

  def isInteger = false
  def isString = false
  def isChar = false
  def isBoolean = false
  def isList = cdr.isList
  def isPair = true
  def isNull = false
  def isName = false
  def isSymbol = false
}


object SList {
  def apply(sx : SExp*) : SExp = 
    SExp(sx.toList)

  def unapplySeq(sx : SExp) : Option[List[SExp]] = {
    if (sx isList) 
      Some(sx toList)
    else
      None
  }
}


object SName {

  private val nameTable = scala.collection.mutable.HashMap[String,SName]()
  private val maxTable = scala.collection.mutable.HashMap[String,SName]()

  def from (string : String) : SName = {
    (nameTable get string) match {
      case Some(name) => name
      case None => {
        val name = SName(string,0)
        nameTable(string) = name
        name
      }
    }
  }

  def from (symbol : SSymbol) : SName = {
    from(symbol.string)
  }

  def gensym(string : String) : SName = {
    (maxTable get string) match {
      case Some(SName(_,v)) => {
        val name = SName(string,v+1)
        maxTable(string) = name
        name
      }
      case None => {
        val name = SName(string,1)
        maxTable(string) = name
        name        
      }
    }
  }

  def gensym(symbol : SSymbol) : SName = {
    gensym(symbol.string)
  }
}




object CommonSSymbols {

  val SQuote = SName.from("quote")
  
  val SCons = SName.from("cons")
  val SAppend = SName.from("cons")

  val SDefine = SName.from("define")

  val SLambda  = SName.from("lambda")

  val SLet     = SName.from("let")

  val SSetBang = SName.from("set!")
  val SVoid = SName.from("void")

  val SIf = SName.from("if")
  
  val SValues = SName.from("values")
  val SLetValues = SName.from("let-values")

}



class SExpParser extends RegexParsers {

  override def skipWhitespace = true 

  override protected val whiteSpace = new Regex("(\\s*([;][^\\r\\n]*)?)*")

  private def integer : Parser[SExp] = 
    regex(new Regex("-?[0-9]+")) ^^ { case s => SInt(Integer.parseInt(s)) }

  private def strue : Parser[SExp] =
    "#t" ^^ { case "#t" => SBoolean(true) }

  private def sfalse : Parser[SExp] =
    "#f" ^^ { case "#f" => SBoolean(false) }

  private def schar : Parser[SExp] =
    ("#\\" ~ regex(new Regex("[^\\r\\n\\t ]"))) ^^ { case "#\\" ~ c => SChar(c.charAt(0)) }

  private def symbol : Parser[SExp] = 
    regex(new Regex("([^.#; \\t\\r\n()',`\"][^; \\t\\r\\n()',`\"]*|[.][^; \\t\\r\\n()',`\"]+)")) ^^ { case s => SName.from(s) }

  private def text : Parser[SExp] =
    regex(new Regex("\"([^\"]|\\\\[\"])+\"")) ^^ { case s => SText(s.substring(1,s.length()-1)) }
  
  private def nil : Parser[SExp] = 
    ("(" ~ ")") ^^ { case "(" ~ ")" => SNil() }

  private def sboolean : Parser[SExp] = strue | sfalse

  private def sxlist : Parser[SExp] = 
    ("(" ~ sexplist ~ ")") ^^ { case "(" ~ l ~ ")" => l }

  private def special : Parser[SExp] = 
    ("'"  ~ sexp) ^^ { case "'"  ~ sexp => SExp(List(CommonSSymbols.SQuote,sexp)) }
  
  private def sexp : Parser[SExp] = positioned(integer | sboolean | schar | text | symbol | special | nil |  sxlist)

  private def sexplist : Parser[SExp] = 
    rep(sexp) ~ (("." ~ sexp) ?) ^^
     { case sexps ~ Some("." ~ sexp) => SExp(sexps,sexp) 
       case sexps ~ None => SExp(sexps) }

  def parse (input : String) : SExp = parse(sexp,input).get

  def parseAll (input : String) : List[SExp] = parse(phrase(rep(sexp)),input).get
}



object SExpTests {

  def assert (test : => Boolean) {
    if (!test) {
      throw new Exception("Test failed!")
    }
  }

  def main (args : Array[String]) {

    import CommonSSymbols._ ;

    val p = new SExpParser

    if (args.length > 0) {

      val filename = args(0)

      // println("Testing s-expression parser on " + filename)

      val lines = scala.io.Source.fromFile(filename).mkString("")

      println(lines)

      val sexps = p.parseAll(lines)
      
      println(sexps) 
    }


    assert (p.parse(";; Math routines \n (foo)").toString
            ==
            "(foo)") ;

    assert (p.parse("3").toString
            ==
            "3") ;

    assert (p.parse("()").toString
            ==
            "()") ;

    assert (p.parse("foo").toString
            ==
            "foo") ;

    assert (p.parse("(3)").toString
            == 
            "(3)") ;

    assert (p.parse("( foo bar\n\n\t baz)").toString
            == 
            "(foo bar baz)") ;

    assert (p.parse("foo ;bar").toString
            == 
            "foo") ;

    assert (p.parse("(foo ;bar\n\n baz)").toString
            == 
            "(foo baz)") ;

    assert (p.parse("(foo )").toString
            == 
            "(foo)") ;

    assert (p.parse("(lambda)") match {
      case SList(SLet) => false
      case SList(SLambda) => true
    })

    
    //println("parseAll test:")
    //println(p.parseAll(";; Math routines \n (foo) (bar)").toString)

    assert (p.parseAll(";; Math routines \n ; test \n (foo) (bar) ; baz\n").toString
            ==
            "List((foo), (bar))") ;
            
  }

}



/* Syntax */


object Term {
  private var maxLabel : Int = 0

  def allocateLabel() : Int = {
    maxLabel += 1
    maxLabel
  }
}

object Exp {
  
}

abstract class Exp extends Ordered[Exp] {
  lazy val label = Term.allocateLabel()

  def isPure : Boolean ;
  def mustHalt : Boolean ;
  
  def isDuplicable : Boolean ;

  def isAtomic = isPure && mustHalt

  def free : ImmSet[SName] ;

  def compare (that : Exp) = this.label compare that.label
}

case class Halt() extends Exp {
  def isPure = true
  def mustHalt = true
  
  def isDuplicable = true
  
  def free = ImmSet()
}

abstract class AExp extends Exp {
  def isPure = true
  def mustHalt = true
}

case class Program(val exp : Exp) {
  lazy val label = Term.allocateLabel()
  
  override def toString = exp.toString
}

abstract class Formals {
  lazy val label = Term.allocateLabel()
  
  def formals : List[Formal] ;
  
  def :: (formal : Formal) : Formals ;

  def accepts (args : Arguments) : Boolean ;

  def bound : ImmSet[SName] ;
}

case class Formal(val name : SName) {
  lazy val label = Term.allocateLabel()
  
  override def toString = name.toString
}

case class VarFormals(rest : SName) extends Formals {
  override def toString = rest.toString
  def :: (formal : Formal) = MultiFormals(List(formal),rest)
  lazy val bound = ImmSet(rest)

  val formals = List()

  def accepts (args : Arguments) : Boolean = true
}

case class MultiFormals(val formals : List[Formal], rest : SName) extends Formals {
  override def toString = "(" + (formals mkString " ") + " . " + rest + ")"
  def :: (formal : Formal) = MultiFormals(formal :: formals, rest)
  lazy val bound = ImmSet(rest) ++ (formals map (_.name))
  
  def accepts (args : Arguments) : Boolean = {
    if (args.arguments.length < this.formals.length) 
      false
    else
      true
  }
}

case class ListFormals(val formals : List[Formal]) extends Formals {
  override def toString = "(" + (formals mkString " ") + ")"
  def :: (formal : Formal) = ListFormals(formal :: formals)
  lazy val bound = ImmSet() ++ (formals map (_.name))

  def accepts (args : Arguments) : Boolean = {
    if (args.arguments.length != this.formals.length) 
      false
    else
      true
  }
}



abstract class Arguments {
  lazy val label = Term.allocateLabel()
  def arguments : List[Argument] ;
  def :: (argument : Argument) : Arguments ;
  def free : ImmSet[SName] ;
}

object InternalPrimArguments extends ListArguments(List(Argument(Undefined())))

case class Argument(val ae : AExp) {
  lazy val label = Term.allocateLabel()
  override def toString = ae.toString
  lazy val free : ImmSet[SName] = ae.free
}

case class ListArguments(val arguments : List[Argument]) extends Arguments {
  override def toString = (arguments mkString " ")
  def :: (argument : Argument) : Arguments = 
    ListArguments(argument :: arguments)

  lazy val free = ImmSet() ++ (arguments flatMap (_.free))
}


// Core syntax:
case class Ref(val name : SName) extends AExp {
  override def toString = name.toString

  def isDuplicable = true 

  lazy val free : ImmSet[SName] = ImmSet(name)
}

abstract case class Lit(val sexp : SExp) extends AExp {

  lazy val free : ImmSet[SName] = ImmSet()
}

case class SelfLit(val value : SExp) extends Lit(value) {
  override def toString = sexp.toString

  def isDuplicable = true 
}

case class QuoteLit(val value : SExp) extends Lit(value) {
  override def toString = "(quote " +value.toString+ ")"
  
  def isDuplicable = value match {
    case _ : SSymbol => true
    case _ : SInt => true
    case _ : SNil => true
    case _ : SBoolean => true
    case _ : SChar => true
    case _ : SText => true
    case _ => false
  }
}

case class App(val fun : AExp, val args : Arguments) extends Exp {
  override def toString = "(" + fun + " " + args + ")"

  def this (fun : AExp, args : AExp*) = 
    this (fun,ListArguments(args.toList map (Argument(_))))

  def isPure = false
  def mustHalt = false

  def isDuplicable = false 

  lazy val free = fun.free ++ args.free
}

case class Lambda(val formals : Formals, val body : Exp) extends AExp {
  override def toString = "(lambda "+formals+" "+body+")"

  //def isPure = true // -- the expression, not the function itself.
  //def mustHalt = true // -- the expression, not the function itself.

  def isDuplicable = false 

  lazy val free = body.free -- formals.bound
}

case class ULambda(fs : Formals, b : Exp) extends Lambda(fs,b)

case class KLambda(fs : Formals, b : Exp) extends Lambda(fs,b)

case class If(val condition : AExp, ifTrue : Exp, ifFalse : Exp) extends Exp {
  override def toString = "(if " +condition +" "+ ifTrue +" "+ ifFalse + ")"

  def isPure = false
  def mustHalt = false

  def isDuplicable = false 

  lazy val free = condition.free ++ ifTrue.free ++ ifFalse.free
}

case class Set(val name : SName, val value : Exp) extends Exp {
  override def toString = "(set! "+name+" "+value+")"

  def isPure = false
  def mustHalt = value.mustHalt

  def isDuplicable = false 

  lazy val free = ImmSet(name) ++ value.free
}

case class Undefined() extends AExp {
  override def toString = "'undefined"

  override def isPure = true
  override def mustHalt = true

  def isDuplicable = true

  lazy val free : ImmSet[SName] = ImmSet()
}

case class Void() extends AExp {
  override def toString = "(void)"

  override def isPure = true
  override def mustHalt = true

  def isDuplicable = true

  lazy val free : ImmSet[SName] = ImmSet()
}


case class Binding (val name : SName, val value : Exp) {
  override def toString = "(" + name + " " + value + ")"
}

case class Let (val binding : Binding, val body : Exp) extends Exp {
  def isPure = false
  def mustHalt = false

  def isDuplicable = false 

  override def toString =
    "(let" + " ("+ binding +") " +body+")"

  lazy val free = ImmSet() ++ (binding.value.free) ++ (body.free -- (ImmSet() + binding.name))
}

object VoidExp {
  def apply() : Exp = new App(Ref(CommonSSymbols.SVoid))
}





/**
 A SSParser parses macro-expanded programs into an AST.
 */
class SSParser {
  
  import CommonSSymbols._ ;

  var expandQuotes = true ;

  def parseExp(sexp : SExp) : Exp = {
    // DEBUG
    // println("parsing exp: " + sexp)
    
    sexp match {
      
      // Literals:
      case _ : SInt => SelfLit(sexp)
      case c : SChar => SelfLit(c)
      case t : SText => SelfLit(t)
      case b : SBoolean => SelfLit(b)
      case n : SName => Ref(n)
      case SQuote :+: sexp :+: SNil() => {
        QuoteLit(sexp)
      }
      
      // Functions:
      case SLambda :+: formals :+: body :+: SNil() => 
        Lambda(parseFormals(formals), parseExp(body))
      
      // Side effects and sequencing:
      case SSetBang :+: (name : SName) :+: value :+: SNil() =>
        Set(name,parseExp(value))
      
      // Conditionals:
      case SIf :+: condition :+: ifTrue :+: ifFalse :+: SNil() =>
        If(parseAExp(condition), parseExp(ifTrue), parseExp(ifFalse))
	  
      // Binding forms:
      case SLet :+: binding :+: body :+: SNil() =>
        Let(parseBinding(binding),parseExp(body))
      
      // Applications:
      case fun :+: args => 
        App(parseAExp(fun), parseArguments(args))
    }
  }
  
  def parseAExp(sexp : SExp) : AExp = {
    // DEBUG
    // println("parsing aexp: " + sexp)

    
    sexp match {
      
      // Literals:
      case _ : SInt => SelfLit(sexp)
      case c : SChar => SelfLit(c)
      case t : SText => SelfLit(t)
      case b : SBoolean => SelfLit(b)
      case n : SName => Ref(n)
      case SQuote :+: sexp :+: SNil() => {
        QuoteLit(sexp)
      }
      
      // Functions:
      case SLambda :+: formals :+: body :+: SNil() => 
        Lambda(parseFormals(formals), parseExp(body))
    }
  }
  
  def parseFormals(sxl : SExp) : Formals = {
    if (sxl.isList) {
      val names = sxl.toList
      ListFormals(names map ((n : SExp) => Formal(n.asInstanceOf[SName])))
    } else if (sxl.isPair) {
      val (names,rest) = sxl.toDottedList
      if (names isEmpty)
        VarFormals(rest.asInstanceOf[SName])
      else
        MultiFormals(names map ((n : SExp) => Formal(n.asInstanceOf[SName])), rest.asInstanceOf[SName])
    } else if (sxl.isName) {
      VarFormals(sxl.asInstanceOf[SName])
    } else {
      throw new Exception("Unhandled case for formals")
    }
  }

  def parseArguments(sxl : SExp) : Arguments = {
    ListArguments(sxl.toList map (x => Argument(parseAExp(x))))
  }

  def parseBinding(binding : SExp) = {
    binding match {
      case SList(SList(name : SName, value : SExp)) => Binding(name,parseExp(value))
    }
  }

  def parseProgram (sx : SExp) : Program = {
    Program(parseExp(sx))
  }

}



object SSParser {

  def apply (sexp : SExp) : Program = {
    val p = new SSParser
    p.parseProgram(sexp)
  }

}




object SSParserTests {
  def assert (test : => Boolean) {
    if (!test) {
      throw new Exception("Test failed!")
    }
  }
  
  
  def main (args : Array[String]) {

    val sxp = new SExpParser
    val p = new SSParser

    if (args.length > 0) {

      val filename = args(0)

      System.err.println("Testing RnRSParser on " + filename)

      val lines = scala.io.Source.fromFile(filename).mkString("")

      // println(lines)

      val sexp = sxp.parse(lines)
      
      val ast = p.parseProgram(sexp)

      println (ast)
    }

    //val prog = "(define (f x) x) (define v (f 10))"
    val prog = "(let ((f (lambda (x) x))) (let ((v (f 10))) v))"

    val sprog = sxp.parse(prog)

    val ast = p.parseProgram(sprog)

    // println(ast)

    ()
  }
}



/* Small-step abstract interpretation */


/**
 A state in a small-step abstract interpretation.
 
*/
case class CoreState(val exp : Exp, val bEnv : BEnv, val rp : ReturnPtr, val t : Time) extends Ordered[CoreState] {
  override def compare (that : CoreState) = 
    that match {
      case CoreState(exp2, bEnv2, rp2, t2) => ComparisonUtilities.compare4 (exp,bEnv,rp.asInstanceOf[Addr],t) (exp2,bEnv2,rp2.asInstanceOf[Addr],t2)
      //case _ => -1
    }
  
  override def equals (that : Any) = that match {
    case that : CoreState => (this compare that) == 0
    case _ => false
  }
}

case class State(val core : CoreState, val store : Store) {
  /*
  override def equals (that : Any) = that match {
    case that : State => (this compare that) == 0
    case _ => false
  }
  */
}

trait SmallStepAbstractInterpretation {
  def atomEval (bEnv : BEnv, store : Store) (exp : Exp) : D = exp match {
    case Lit(SBoolean(value)) => new SortedSetD() + BooleanValue(value)
    case _ : Lit => new SortedSetD()
    case Undefined() => new SortedSetD()
    case Ref(name) => {
      val addr = bEnv(name)
      (store get addr) match {
        case Some(d) => d
        case None => {
          throw new Exception("could not find address: " + addr)
        }
      }
    }
    case Void() => new SortedSetD()
    case lam : Lambda => {
      new SortedSetD() + Clo(lam,bEnv)
    }
  }
  
  def testState (lst : List[CoreState]) = {
    var calls : List[Pair[SName,D]] = List()
    for(state <- lst) {
      state match {
	case CoreState(exp @ App(Ref(f), args),bEnv,rp,t) =>
	  calls = (f, atomEval(bEnv, globalStore) (Ref(f).asInstanceOf[Exp])) :: calls
	case _ => {}
      }
    }
    var map = new listing()
    for(Pair(f, d) <- calls) {
      map = map + (f, d)
    }
    
    val lists = map.toList
    var count = 0
    for(Pair(f,d) <- lists) {
      val labels =
	for(Clo(lam,_) <- d.toList) yield {
	  lam.label
	}
      if(labels.length == 1)
	count = count + 1
    }
    
    count
  }
  
  def initialState : State ;
  def next (state : State) : List[State] ;
  
  var count = 0 
  var globalStore : Store = null
  
  def runWithGlobalStore () {
    // seen records the last generation store seen with this flat.
    val seen = scala.collection.mutable.HashMap[CoreState,Long]()
    var visited = scala.collection.mutable.Set[CoreState]()
    var currentGeneration : Long = 1
    
    val init = initialState
    var todo = List(init)
    
    globalStore = init.store
    var timeout = -1
    
    while (!todo.isEmpty && timeout != 0) {
      var newState = todo.head
      todo = todo.tail
      
      val core = newState.core
      val store = newState.store
      
      val lastSeenGeneration : Long = seen.getOrElse(core,0)
      
      /*if (currentGeneration <= lastSeenGeneration) {
        // println("Current generation: " + currentGeneration) // DEBUG
        // println("Last generation: " + lastSeenGeneration) // DEBUG
        // println("Not a new state: " + newState) // DEBUG
	}
	*/
	
      if (currentGeneration > lastSeenGeneration) {
        // globalStore changed since we last saw this flat.
        if (timeout > 0)
          timeout -= 1
	
	visited = visited + newState.core
	
        count += 1
	
        // Install the global store:
        newState = new State(newState.core, globalStore)
	
        //println("State:\n" + newState + "\n")
	
        // Explore successors:
        val succs = next(newState)
	
        // Mark this state as being seen with the current generation.
        seen(newState.core) = currentGeneration
	
        // Check each successor for change:
        for (succ <- succs) {
          var store = succ.store
          if (!store.clst.isEmpty) {
            // Something changed!
	    
            // Bump up the current store generation:
            currentGeneration += 1
            // Apply store changes to the global store:
            globalStore = store.changes(globalStore, "k")
	    //println("HERE+++++++++++++++" + globalStore) // DEBUG
          }
        }
        todo = todo ++ succs
      }
    }
    
    if (timeout == 0)
      println("Timeout reached")

    println("States explored: " + count)
    println("Unique states explored: " + visited.size)
    //println("State list: " + (for(s <- visited.toList) yield { s.toString + "\n\t" }))
    println("Found " + testState(visited.toList) + " possible places for inlining")
  }
}



/* Flow analyses */

trait Frame extends Value {
  def isObjectLocation = false ;
  def isProcedure = false;
  
  def localCompareFrame (that : Value) : Int ;
  
  def localCompare (that : Value) : Int = {
    val thisClass = this.getClass() 
    val thatClass = that.getClass()
    val cmp = thisClass.getName() compare thatClass.getName()
    if (cmp != 0)
      cmp
    else
      localCompareFrame(that)
  }
}

case class RFrame(val v : SName, e : Exp, rho : BEnv, rp : ReturnPtr) extends Frame {
  def localCompareFrame (that : Value) : Int = {
    that match {
      case RFrame(v2,e2,rho2,rp2) => ComparisonUtilities.compare4 (v, e, rho, rp.asInstanceOf[Addr]) (v2, e2, rho2, rp2.asInstanceOf[Addr])
    }
  }
}

trait Addr extends Ordered[Addr] {
  
  def localCompare (that : Addr) : Int ;

  def compare (that : Addr) : Int = {
    val thisClass = this.getClass() 
    val thatClass = that.getClass()
    val cmp = thisClass.getName() compare thatClass.getName()
    if (cmp != 0)
      cmp
    else
      localCompare(that)
  }
}

trait ObjectLocation extends Value {
  def isProcedure = false
  def isObjectLocation = true
  def objectType : SName ;
}

case class ConsLocation(time : Time) extends ObjectLocation {
  def localCompare (that : Value) : Int = that match {
    case ConsLocation(thatTime) => time compare thatTime
  }

  val objectType = SName.from("cons")
}

case class FieldAddr(baseAddr : ObjectLocation, field : SName) extends Addr {
  def localCompare (that : Addr) : Int = {
    that match {
      case FieldAddr(ba2,field2) => ComparisonUtilities.compare2 (baseAddr.asInstanceOf[Value],field) (ba2.asInstanceOf[Value],field2)
    }
  }
}


trait BEnv extends Ordered[BEnv] {
  def apply(name : SName) : Addr ;
  
  override def equals (that : Any) = that match {
    case thatBEnv : BEnv => (this compare thatBEnv) == 0
    case _ => false
  }
  
  def update(name : SName, addr : Addr) : BEnv ;
}

case class MapBind (val name : SName, val time : Time) extends Addr {
  def localCompare (that : Addr) : Int = that match {
    case MapBind(thatName,thatTime) => ComparisonUtilities.compare2 (this.name,this.time) (thatName,thatTime)
  }
}

case class MapBEnv (val map : SortedMap[String,Addr]) extends BEnv {
  def apply (name : SName) = map(name.s)
  def succ (m : Int, l : Int) = throw new Exception("Not appropriate in this context.")
  
  def compare (that : BEnv) = that match {
    case MapBEnv(thatMap) => ComparisonUtilities.compareLists (this.map.toList,thatMap.toList)
  }
  
  def update (name : SName, addr : Addr) : BEnv = 
    MapBEnv(map(name.s) = addr)
    
}

trait Time extends Ordered[Time] {
  def succ (k : Int, call : Int) : Time ;
}

abstract class Store (val clst : List[StoreUpdate]) {
  def apply(addr : Addr) : D = (this get addr) match {
    case Some(d) => d
    case None => throw new Exception("Could not find " + addr)
  }
  def getOrElse(addr : Addr, default : D) : D = (this get addr) match {
    case Some(d) => d
    case None => default
  }
  def get(addr : Addr) : Option[D] ;


  def wt (that : Store) : Boolean ;

  /**
   Weak update.
   */
  def + (addr : Addr, d : D) : Store ;

  /**
   Strong update if safe; weak update otherwise.
   */
  def update (addr : Addr, d : D) : Store ;
  
  def changes(s : Store, analysis : String) : Store ;
}

trait Value extends Ordered[Value] {
  def isProcedure : Boolean ;
  def isObjectLocation : Boolean ;

  protected def localCompare(that : Value) : Int ;

  def compare (that : Value) : Int = {
    val thisClassName = this.getClass().getName()
    val thatClassName = that.getClass().getName()
    val cmp = thisClassName compare thatClassName
    if (cmp != 0)
      cmp
    else
      this.localCompare(that)
  }
  
  override def equals (that : Any) : Boolean = that match {
    case that : Value => (this compare that) == 0
    case _ => false
  }
}

case class BooleanValue(val value : Boolean) extends Value {
  override def toString = if (value) { "#t" } else { "#f" }

  def localCompare (that : Value) : Int = that match {
    case BooleanValue(value2) => value compare value2
  }
  
  def isProcedure = false
  def isObjectLocation = false
}


case class PrimValue(val name : String) extends Value {
  def localCompare (that : Value) : Int = that match {
    case PrimValue(name2 : String) => name compare name2
  }

  def isProcedure = true
  def isObjectLocation = false
}


case class Clo(val lam : Lambda, val bEnv : BEnv) extends Value {
  def localCompare (that : Value) : Int = that match {
    case Clo(lam2,bEnv2) => ComparisonUtilities.compare2 (lam.asInstanceOf[Exp],bEnv) (lam2.asInstanceOf[Exp],bEnv2)
  }

  def isProcedure = true 
  def isObjectLocation = false
}

trait D extends Ordered[D] {
  def isPure = true
  def mustHalt = true
  
  def isDuplicable = true
  
  def free = ImmSet()
    
  def + (value : Value) : D ;
  def join (that : D) : D ;
  def wt (that : D) : Boolean ;
  def toList : List[Value] ;
  
  def compare (that : D) : Int = {
    val thisClassName = this.getClass().getName()
    val thatClassName = that.getClass().getName()
    val cmp = thisClassName compare thatClassName
    if (cmp != 0)
      cmp
    else
      this.localCompare(that)
  }
  
  def localCompare(that : D) : Int ;
}






/* Generics components */

case class StoreUpdate (val isStrong : Boolean, val addr : Addr, val d : D) {
  override def toString = ("(" + addr + ", " + d + ")")
  
  def apply(store : Store, analysis : String) : Store = {
    store match {
      case MapStore(map, changes) => 
        if (isStrong)
          new MapStore (map(addr) = d, List())
        else
	  if(analysis == "k")
            new MapStore (map + Pair(addr, d), List())
	  else
	    map get addr match {
	      case Some(existingD) => new MapStore(map(addr) = d join existingD, List())
	      case None => new MapStore(map(addr) = d, List())
	    }
    }
  }
}

case class MapStore(val map : SortedMap[Addr,D], override val clst : List[StoreUpdate]) extends Store(clst) {
  def this () = this(TreeMap(), List())

  def get(addr : Addr) : Option[D] = map get addr

  def wt (that : Store) = that match {
    case _ => throw new Exception("Unknown store type")
  }

  /**
   Weak update.
   */
  def + (addr : Addr, d : D) : MapStore = {
    map get addr match {
      case Some(existingD) => {
	new MapStore(map(addr) = d join existingD, StoreUpdate(false, addr, d) :: clst)
      }
      case None => new MapStore(map(addr) = d, StoreUpdate(false, addr, d) :: clst)
    }
  }

  /**
   A simple store does not contain enough information to determine whether a strong update is safe or not, so
   this operation always performs a weak update.
   */
  def update (addr : Addr, d : D) : Store = {
    // We don't have enough information to do a strong update, so we fall back to a weak update.
    this + (addr,d)
  }
  
  def changes (s : Store, analysis : String) : Store = {
    changes(s, clst, analysis)
  }
  
  def changes (s : Store, lst : List[StoreUpdate], analysis : String) : Store = {
    lst match {
      case hd :: tl => hd((changes(s, tl, analysis)), analysis)
      case Nil => s
    }
  }
  
  def compare (that : MapStore) : Int = {
    this.toString compare that.toString
  }
  
  override def toString = "\n " +  (map mkString "\n ")
}


case class SortedSetD (val set : SortedSet[Value]) extends D {
  def this () = this (TreeSet())
  
  def localCompare (that : D) : Int = {
    var lt = false
    var gt = false
    if ( this wt that )
      lt = true
    if (that wt this)
      gt = true
    
    (lt,gt) match {
      case (true,true) => 0
      case (false,true) => 1
      case (true,false) => -1
      case (false,false) => -1
    }
  }
  
  def + (value : Value) : D = SortedSetD(set + value)
  
  def join (that : D) = SortedSetD(set ++ that.toList)

  def wt (that : D) : Boolean = {
    that match {
      case SortedSetD(set2) => set subsetOf set2
    }
  }

  def toList = set.toList

  override def toString = "{" + (set mkString ",") + "}"
}


case class KTime(val last : List[Int]) extends Time {
  def compare (that : Time) =  that match {
    case KTime(last2) => ComparisonUtilities.compareLists (last,last2)
  }
  def succ (k : Int, call : Int) : KTime = KTime((call :: last) take k)
}


case object UniTime extends Time {
  def compare (that : Time) = 
    if (this eq that)
      0
    else
      -1

  def succ (k : Int, call : Int) : Time = this
}

case class PrimAddr(val name : SName) extends Addr {
  def localCompare (that : Addr) : Int = that match {
    case PrimAddr(thatName) => this.name compare thatName
  }
}

case class ReturnPtr(val exp : Exp) extends Addr {
  def localCompare (that : Addr) : Int = that match {
    case ReturnPtr(thatExp) => this.exp compare thatExp
  }
}

/* SS primitives */
object SSPrimitives {

  def list = List("*","-","+","/",
                  "quotient","gcd","modulo",
                  "<","=",">",
                  "odd?","even?",
                  "not",
                  "cons","car","cdr",
                  "newline","display",
                  "error", "halt",
		  "square")

}

class Parameters(val values : List[D]) {

  def this () = this(List())

  def apply(position : Int) : D = values(position)

  def :: (d : D) : Parameters =
    new Parameters(d :: values)
}


class KCFA_ANF(exp : Exp, bEnv0 : BEnv, t0 : Time, store0 : Store, botD : D) extends SmallStepAbstractInterpretation {
  
  var k : Int = 0

  val bEnv1 = SSPrimitives.list.foldRight (bEnv0) ((name,bEnv) => bEnv(SName.from(name)) = PrimAddr(SName.from(name)))
  
  val storex = SSPrimitives.list.foldRight (store0) ((name,store) => store(bEnv1(SName.from(name))) = botD + PrimValue(name))
  
  val rp1 = ReturnPtr(Ref(SName.from("halt")))
  
  val topFrame = new RFrame(SName.from("final"), Halt(), bEnv1, rp1)
  
  val wrapper = new StoreUpdate(false, rp1, botD + topFrame)
  
  val store1 = wrapper(storex, "k")
  
  override def atomEval (bEnv : BEnv, store : Store) (exp : Exp) : D = exp match {
    case Lit(SBoolean(value)) => botD + BooleanValue(value)
    case _ : Lit => botD
    case Undefined() => botD
    case Ref(name) => {
      val addr = bEnv(name)
      (store get addr) match {
        case Some(d) => d
        case None => {
          throw new Exception("could not find address: " + addr)
        }
      }
    }
    case Void() => botD
    case lam : Lambda => {
      botD + Clo(lam,bEnv)
    }
  }

  def inject (exp : Exp) : State = {
    State(CoreState(exp,bEnv1,rp1,t0),store1)
  }
  
  lazy val initialState = inject(exp)
  
  def tick (call : Exp, t : Time) : Time = t.succ(k,call.label)
  
  def evalArgs (args : Arguments, bEnv : BEnv, store : Store) : Parameters = {
    args match {
      case ListArguments(arglist) => evalArgs (new Parameters()) (arglist,bEnv,store)
    }
  }

  def evalArgs (parameters : Parameters) (arglist : List[Argument], bEnv : BEnv, store : Store) : Parameters = {
    arglist match {
      case Nil => parameters
      case hd :: tl => {
        val p = evalArgs (parameters) (tl,bEnv,store)
        hd match {
          case Argument(exp) => (atomEval (bEnv,store) (exp)) :: p
        }
      }
    }
  }
  
  
  private def applyProcedure (args : Arguments, params : Parameters, store : Store, rp : ReturnPtr, newTime : Time) (proc : Value) : List[State] = {
    proc match {
      
      case Clo(lam @ Lambda(VarFormals(name),body),bEnv2) if !(body.free contains name)  => {
        List(State(CoreState(body,bEnv2,rp,newTime),store))
      }
      
      case Clo(lam @ Lambda(formals,body),bEnv2) if formals accepts args => {
        
        var newStore = store 
        var newBEnv = bEnv2
        
        // Bind arguments:
        for ((Formal(name),d) <- formals.formals zip params.values) {
          // TODO: Un-hard-code the MapBind; factor into alloc
          newBEnv = (newBEnv(name) = MapBind(name,newTime))
          newStore += (newBEnv(name), d)
        }
        
        if (formals.formals.length < params.values.length) {
          // Stuff the rest into a list.
          val remainder = params.values.drop(formals.formals.length)
          throw new Exception("Mismatched Arguments: " + formals + " : " + params)
        }
        
        List(State(CoreState(body,newBEnv,rp,newTime),newStore))
      }
      
      
      case PrimValue("*"|"+"|"-"|"/"|"quotient"|"gcd"|"modulo"|"<"|"="|">"|"odd?"|"even?"|"display"|"newline"|"not"|"square") => {
	val frames = store (rp)
	for (frame <- frames.toList if frame.isInstanceOf[Frame]) yield {
	  frame match {
	    case RFrame(v,e,rho,rp2) => {
	      val rv = botD
              val addr = MapBind(v, newTime)
              var newStore = store
	      var newBEnv = rho
              newBEnv = newBEnv update (v, addr)
	      newStore += (addr, rv)
	      State(CoreState(e,newBEnv,rp2,newTime),newStore)
	    }
	  }
	}
      }
      
      case PrimValue("cons") => {
        if (params.values.length != 2)
          List()
        else {
          val loc = ConsLocation(newTime)
          val carD = params(0)
          var cdrD = params(1)
          val carAddr = FieldAddr(loc,SName.from("car"))
          val cdrAddr = FieldAddr(loc,SName.from("cdr"))
          var newStore = store
          newStore += (carAddr, carD)
          newStore += (cdrAddr, cdrD)
	  val frames = store (rp)
	  for (frame <- frames.toList if frame.isInstanceOf[Frame]) yield {
	    frame match {
	      case RFrame(v,e,rho,rp2) => {
		val rv = botD
		val addr = MapBind(v, newTime)
		var newBEnv = rho
		newBEnv = newBEnv update (v, addr)
		newStore += (addr, rv)
		State(CoreState(e,newBEnv,rp2,newTime),newStore)
	      }
	    }
	  }
        }
      }
      
      case PrimValue(field @ ("car"|"cdr")) => {
        if (params.values.length == 1) {
          val cellLocs = params(0)
	  val frames = store (rp)
          val states : List[State] =
            for (cellLoc <- cellLocs.toList if cellLoc.isObjectLocation;
		 frame <- frames.toList if frame.isInstanceOf[Frame]) yield {
              val loc = cellLoc.asInstanceOf[ObjectLocation]
	      frame match {
		case RFrame(v,e,rho,rp2) => {
		  val rv = store.getOrElse(FieldAddr(loc,SName.from(field)),botD)
		  val addr = MapBind(v, newTime)
		  var newStore = store
		  var newBEnv = rho
		  newBEnv = newBEnv update (v, addr)
		  newStore += (addr, rv)
		  State(CoreState(e,newBEnv,rp2,newTime),newStore)
		}
	      }
	    }
          states
        } else {
          List()
        }
      }
      
      case PrimValue("error") => List()
    }
  }
  
  def next (state : State) : List[State] = {
    state match {
      
      case State(CoreState(exp @ App(f,args),bEnv,rp,t),store) => {
        val procs = atomEval (bEnv,store) (f)
        val params = evalArgs (args,bEnv,store)
        val newTime = tick(exp,t)
        for (procValue <- procs.toList if procValue.isProcedure; 
             succ <- applyProcedure (args,params,store,rp,newTime) (procValue)) yield {
          succ
        }
      }

      case State(CoreState(exp @ If(condition,ifTrue,ifFalse),bEnv,rp,t),store) => {
        for (call <- List(ifTrue,ifFalse)) yield {
          val newTime = tick (exp,t)
          State(CoreState(call,bEnv,rp,newTime),store)
        }
      }
      
      // Return expression
      case State(CoreState(ae @ (_ : AExp),bEnv,rp,t),store) => {
	//println("Return: " + ae.toString)  //DEBUG
	val frames = store (rp)
	val newTime = tick(ae, t)
	for (frame <- frames.toList if frame.isInstanceOf[Frame]) yield {
	  frame match {
	    case RFrame(v,e,rho,rp2) => {
	      val rv = atomEval(bEnv, store) (ae)
              val addr = MapBind(v, newTime)
              var newStore = store
	      var newBEnv = rho
              newBEnv = newBEnv update (v, addr)
	      newStore += (addr, rv)
	      State(CoreState(e,newBEnv,rp2,newTime),newStore)
	    }
	  }
	}
      }
      
      case State(CoreState(exp @ Let(Binding(name, value), body), bEnv, rp, t), store) => {
	val frame = RFrame(name,body,bEnv,rp)
	val newTime = tick(exp, t)
	val addr = ReturnPtr(exp)
	var newStore = store
        newStore = newStore + (addr, botD + frame)
	//println("Frame: " + newStore(addr))  // DEBUG
	//println("First: " + store) // DEBUG
	//println("Changed: " + newStore.clst) // DEBUG
	List(State(CoreState(value,bEnv,addr,newTime),newStore))
      }
      
      case State(CoreState(exp @ Set(name,value), bEnv, rp, t), store) => {
	val frame = RFrame(name,Void(),bEnv,rp)
	val newTime = tick(exp, t)
	val addr = ReturnPtr(exp)
	var newStore = store
	newStore += (addr, botD + frame)
	List(State(CoreState(value,bEnv,addr,newTime),newStore))
      }
      
      case State(CoreState(exp @ Halt(), bEnv, rp, t), store) => {
	List()
      }
      
      case _ => throw new Exception("unhandled state: " + state)
      
    }
  }

}



/*
 * PDCFA
 */
case class PDFrame(val v : SName, e : Exp, rho : BEnv) extends Frame {
  def localCompareFrame (that : Value) : Int = {
    that match {
      case PDFrame(v2,e2,rho2) => ComparisonUtilities.compare3 (v, e, rho) (v2, e2, rho2)
    }
  }
}

trait Label extends Ordered[Label] {
  def isEpsilon : Boolean ;
  def isPush : Boolean ;
  def isPop : Boolean ;

  def localCompare(that : Label) : Int ;
  
  def compare (that : Label) : Int = {
    val thisClass = this.getClass() 
    val thatClass = that.getClass()
    val cmp = thisClass.getName() compare thatClass.getName()
    if (cmp != 0)
      cmp
    else
      localCompare(that)
  }
}

case class Epsilon() extends Label {
  def isEpsilon = true
  def isPush = false
  def isPop = false
  
  def localCompare(that : Label) : Int = {
    that match {
      case Epsilon() => 0
      case _ => -1
    }
  }
}

case class Push(val frame : Frame) extends Label {
  def isEpsilon = false
  def isPush = true
  def isPop = false
  
  def localCompare(that : Label) : Int = {
    that match {
      case Push(f2) => frame compare f2 
      case _ => -1
    }
  }
}

case class Pop(val frame : Frame) extends Label {
  def isEpsilon = false
  def isPush = false
  def isPop = true
  
  def localCompare(that : Label) : Int = {
    that match {
      case Pop(f2) => frame compare f2 
      case _ => -1
    }
  }
}

//new state needing to be expanded
// trait Expander {
//   def toExpand : Boolean ;
// }

// case class Done(val s : CoreState, val e : Edge) extends Expander {
//   def toExpand = false
// }

// case class Expand(val state : CoreState, val frame : Frame) extends Expander {
//   def toExpand = true
// }

trait Edge extends Ordered[Edge] {
  def compare (that : Edge) : Int ;
}

//already expanded edge
case class FullEdge(val s : CoreState, l : Label) extends Edge {
  def compare (that : Edge) : Int = {
    that match {
      case FullEdge(s2, l2) => ComparisonUtilities.compare2 (s, l) (s2, l2)
      case _ => -1
    }
  }
}

//placeholder for where pops can go
case class PopEdgeEm() extends Edge {
  def compare (that : Edge) : Int = {
    that match {
      case PopEdgeEm() => 0
      case _ => -1
    }
  }
}

case class EdgeSet (set : SortedSet[Edge]) {
  def this () = this (TreeSet())
  
  def + (e : Edge) : EdgeSet = EdgeSet(set + e)
  
  def join (that : EdgeSet) = EdgeSet(set ++ that.toList)
  
  def toList = set.toList

  override def toString = "{" + (set mkString ",") + "}"
}

case class CoreStateSet (set : SortedSet[CoreState]) {
  def this () = this (TreeSet())
  
  def + (s : CoreState) : CoreStateSet = CoreStateSet(set + s)
  
  def join (that : CoreStateSet) = CoreStateSet(set ++ that.toList)
  
  def toList = set.toList
  
  override def toString = "{" + (set mkString ",") + "}"
}

trait Graph {
  def apply (s : CoreState) : EdgeSet ;
  
  def add (s : CoreState, e : Edge) : Graph ;
  
  def getOrElse (s : CoreState, default : EdgeSet) : EdgeSet ;
  
  def get (s : CoreState) : Option[EdgeSet] ;
  
}

case class MapGraph(map : SortedMap[CoreState,EdgeSet]) extends Graph {
  def this () = this (TreeMap())
  
  def apply (s : CoreState) : EdgeSet = {
    this getOrElse (s, EdgeSet(TreeSet()))
  }
  
  def getOrElse (s : CoreState, default : EdgeSet) : EdgeSet = (this get s) match {
    case Some(d) => d
    case None => default
  }
  
  def get (s : CoreState) : Option[EdgeSet] = map get s
  
  def add (s : CoreState, e : Edge) : Graph = {
    map get s match {
      case Some(existingSet) => new MapGraph(map(s) = existingSet + e)
      case None => new MapGraph(map(s) = EdgeSet(TreeSet()) + e)
    }
  }
  
  override def toString = "\n " +  (map mkString "\n ")
}

trait RGraph {
  def apply (s : CoreState) : CoreStateSet ;
  
  def add (s : CoreState, s2 : CoreState) : RGraph ;
  
  def getOrElse (s : CoreState, default : CoreStateSet) : CoreStateSet ;
  
  def get (s : CoreState) : Option[CoreStateSet] ;
}

case class MapRGraph (map : SortedMap[CoreState,CoreStateSet]) extends RGraph {
  def this () = this (TreeMap())
  
  def apply (s : CoreState) : CoreStateSet = {
    //println("++++++++++" + map.toList + "\n" + s) // DEBUG
    this getOrElse (s, CoreStateSet(TreeSet()) + s)
  }
  
  def getOrElse (s : CoreState, default : CoreStateSet) : CoreStateSet = (this get s) match {
    case Some(d) => d + s
    case None => default
  }
  
  def get (s : CoreState) : Option[CoreStateSet] = map get s
  
  def add (s : CoreState, s2 : CoreState) : RGraph = {
    map get s match {
      case Some(existingSet) => MapRGraph(map(s) = existingSet + s2)
      case None => MapRGraph(map(s) = CoreStateSet(TreeSet()) + s2)
    }
  }
  
  override def toString = "\n " +  (map mkString "\n ")
}


case class RDSG(val in : RGraph, val out : RGraph) {
  def this () = this (new MapRGraph(), new MapRGraph())
  
  override def toString : String  = "RDSG(" + out.toString + ")"
  
  def apply (s1 : CoreState, s2 : CoreState) : Boolean = {
    (s1 == s2
     ||
     (out(s1).toList contains s2))
  }
  
  //finds transitive closure
  def add (s1 : CoreState, s2 : CoreState) : RDSG = {
    if(this (s1, s2))
      this
    else {
      var singleAdds : List[Pair[CoreState, CoreState]] = List((s1,s2))
      singleAdds ++= in(s1).toList map (s => (s, s2))
      singleAdds ++= out(s2).toList map (s => (s1, s))
      val connections = for (s <- in(s1).toList; ss <- out(s2).toList) yield {
	(s, ss)
      }
      singleAdds ++= connections
      
      this singleAddList(singleAdds)
    }
  }
  
  //adds list of edges transitively
  def addList (lst : List[Pair[CoreState,CoreState]]) : RDSG = {
    lst match {
      case (s1, s2) :: tl => (this add (s1, s2)) addList (tl)
      case Nil => this
    }
  }
  
  //finds transitive closure and returns list of new edges needed to make transitive closure
  def report (s1 : CoreState, s2 : CoreState) : List[Pair[CoreState, CoreState]] = {
    if(this (s1, s2))
      List((s1, s2))
    else {
      var singleAdds : List[Pair[CoreState, CoreState]] = List((s1,s2))
      singleAdds ++= in(s1).toList map (s => (s, s2))
      singleAdds ++= out(s2).toList map (s => (s1, s))
      val connections = for (s <- in(s1).toList; ss <- out(s2).toList) yield {
	(s, ss)
      }
      singleAdds = singleAdds union connections
      if (singleAdds contains (s1, s2))
	singleAdds
      else
	singleAdds + (s1, s2)
    }
  }
  
  //adds list of edges transitively and returns list of edges 
  def reportList (lst : List[Pair[CoreState,CoreState]]) : List[Pair[CoreState, CoreState]] = {
    lst match {
      case (s1, s2) :: tl => ((this add (s1, s2)) reportList tl) ++ (this report (s1, s2))
      case Nil => List()
    }
  }
  
  //returns list of edges not in RDSG
  def checkList(lst : List[Pair[CoreState,CoreState]]) : List[Pair[CoreState,CoreState]] = {
    lst match {
      case (s1, s2) :: tl => 
	val remainder = checkList(tl)
        if (this (s1, s2))
	  remainder
        else
	  (s1, s2) :: remainder
      case Nil => Nil
    }
  }
  
  //does not find transitive closure
  def singleAdd (s1 : CoreState, s2 : CoreState) : RDSG = {
    //println("-----------" + (new RDSG (in add (s2, s1), out add (s1, s2))) (s1, s2)) // DEBUG
    new RDSG (in add (s2, s1), out add (s1, s2))
  }
  
  def singleAddList (lst : List[Pair[CoreState,CoreState]]) : RDSG = {
    lst match {
      case (s1, s2) :: tl => (this singleAdd (s1, s2)) singleAddList (tl)
      case Nil => this
    }
  }
}

case class DSG(val in : Graph, val out : Graph, val trans : RDSG) {
  def this () = this (new MapGraph(), new MapGraph(), new RDSG())
  
  override def toString : String  = "DSG(" + out.toString + ",\n\t" + trans.toString + ")"

  def apply (s1 : CoreState, e : Edge) : Boolean = {
    out(s1).toList contains e
  }
  
  //finds all previously known push-pop pairs
  def findEpsilonsFromPairs(epsilons : ImmSet[Pair[CoreState, CoreState]], trans : RDSG) : ImmSet[Pair[CoreState, CoreState]] = {
    val currentEpsilons = ImmSet() ++ (trans reportList epsilons.toList)
    var otherEpsilons = for((s1, s2) <- currentEpsilons;
			    FullEdge(s, Push(f)) <- in(s1).toList;
			    FullEdge(ss, Pop(ff)) <- out(s2).toList;
			    if((f compare ff) == 0))
			yield { (s, ss) }
    var newEpsilons = currentEpsilons ++ otherEpsilons
    if(newEpsilons != currentEpsilons)
      findEpsilonsFromPairs(newEpsilons, trans)
    else
      newEpsilons
  }
  
  //finds all new epsilons for a list of new epsilons:
  def findAllEpsilons(epsilons : ImmSet[Pair[CoreState, CoreState]], trans : RDSG) : List[Pair[CoreState, CoreState]] = {
    val currentEpsilons = findEpsilonsFromPairs(ImmSet() ++ (trans reportList epsilons.toList), trans)
    if(epsilons != currentEpsilons)
      findAllEpsilons(currentEpsilons, trans)
    else
      epsilons.toList
  }
  
  //finds push-pop transitive closure
  def add (s1 : CoreState, e : Edge) : Pair[DSG,ImmSet[CoreState]] = {
    var ans : ImmSet[CoreState] = e match {
      case FullEdge(s2, l) => ImmSet() + s2
      case _ => ImmSet()
    }
    if (this (s1, e))
      (this, ans)
    else {
      var newTrans : RDSG = null
      var newEpsilons : List[Pair[CoreState,CoreState]] = null
      e match {
	case PopEdgeEm() => (this singleAdd(s1, e), ans)
	case FullEdge(s2, l) => {
	  l match {
	    case Epsilon() => {
	      newEpsilons = findAllEpsilons(ImmSet((s1, s2)), trans)
	      newTrans = trans addList newEpsilons
 	      (DSG(in add (s2, FullEdge(s1, Epsilon())),
		   out add (s1, FullEdge(s2, Epsilon())),
		   newTrans),
	       ans ++ impliedEdges(newEpsilons))
	    }
	    case Push(f) => {
	      var newPopList =
		ImmSet() ++ (for (ss <- trans.out(s2).toList;
				  PopEdgeEm() <- out(ss).toList)
			     yield {
			       ss
			     })
	      newEpsilons =
		for (ss <- trans.out(s2).toList;
		     FullEdge(sss, Pop(ff)) <- out(ss).toList;
		     if((f compare ff) == 0))
		yield {
		  (s1, sss)
		}
	      newEpsilons = findAllEpsilons(ImmSet() ++ newEpsilons, trans)
	      newTrans = trans addList newEpsilons
 	      (DSG(in add (s2, FullEdge(s1, Push(f))),
		   out add (s1, FullEdge(s2, Push(f))),
		   newTrans),
	       ans ++ newPopList ++ impliedEdges(newEpsilons))
	    }
	    case Pop(f) => {
	      newEpsilons =
		for (s <- trans.in(s1).toList;
		     FullEdge(p, Push(ff)) <- in(s).toList;
		     if((f compare ff) == 0))
		yield {
		  (p, s2)
		}
	      newEpsilons = findAllEpsilons(ImmSet() ++ newEpsilons, trans)
	      newTrans = trans addList newEpsilons
 	      (DSG(in add (s2, FullEdge(s1, Pop(f))),
		   out add (s1, FullEdge(s2, Pop(f))),
		   newTrans),
	       ans ++ impliedEdges(newEpsilons))
	    }
	  }
	}
      }
    }
  }
  
  //returns frames that can be on top at given state
  def pushedFrames(state : CoreState) : List[Frame] = {
    for (s <- trans.in(state).toList;
	 FullEdge(p, Push(f)) <- in(s).toList) yield { f }
  }
  
  //finds new edges (pops) implied by given new epsilon edges
  def impliedEdges(epsilons : List[Pair[CoreState, CoreState]]) : ImmSet[CoreState] = { 
    epsilons match {
      case (s1, s2) :: tl => impliedEdges(tl) ++ impliedSingle(s1, s2)
      case Nil => ImmSet()
    }
  }
  
  //finds new pops given a new epsilon edge
  def impliedSingle(s1 : CoreState, s2 : CoreState) = {
    if(trans (s1, s2))
      ImmSet()
    else {
      ImmSet() ++ (for (FullEdge(s, Push(f)) <- in(s1).toList;
			PopEdgeEm() <- out(s2).toList)
		   yield {
		     s2
		   })
    }
  }
  
  //adds list of singleAdds
  def singleAddList (lst : List[Pair[CoreState,Edge]]) : DSG = {
    lst match {
      case (s, e) :: tl => (this singleAdd (s, e)) singleAddList (tl)
      case Nil => this
    }
  }

  //adds only to in and out
  def singleAdd (s1 : CoreState, e : Edge) : DSG = {
    e match {
      case PopEdgeEm() => DSG (in, out add (s1, PopEdgeEm()), trans)
      case FullEdge(s2, l) => DSG (in add (s2, FullEdge(s1, l)), out add (s1, FullEdge(s2, l)), trans)
    }
  }
}

/*
trait SmallStepAbstractPushDownInterpretation {
}
*/

trait SmallStepAbstractPushDownInterpretation {
  def atomEval (bEnv : BEnv, store : Store) (exp : Exp) : D = exp match {
    case Lit(SBoolean(value)) => new SortedSetD() + BooleanValue(value)
    case _ : Lit => new SortedSetD()
    case Undefined() => new SortedSetD()
    case Ref(name) => {
      val addr = bEnv(name)
      (store get addr) match {
        case Some(d) => d
        case None => {
          throw new Exception("could not find address: " + addr)
        }
      }
    }
    case Void() => new SortedSetD()
    case lam : Lambda => {
      new SortedSetD() + Clo(lam,bEnv)
    }
  }
  
  //counts number of inlining possibilities
  def testState (lst : List[CoreState]) = {
    var calls : List[Pair[SName,D]] = List()
    for(state <- lst) {
      state match {
	case CoreState(exp @ App(Ref(f), args),bEnv,rp,t) =>
	  calls = (f, atomEval(bEnv, globalStore) (Ref(f).asInstanceOf[Exp])) :: calls
	case _ => {}
      }
    }
    var map = new listing()
    for(Pair(f, d) <- calls) {
      map = map + (f, d)
    }
    
    val lists = map.toList
    var count = 0
    for(Pair(f,d) <- lists) {
      val labels =
	for(Clo(lam,_) <- d.toList) yield {
	  lam.label
	}
      if(labels.length == 1)
	count = count + 1
    }
    
    count
  }
  
  def initialState : State ;
  def next (state : State) : ImmSet[State] ;
  
  var count = 0 
  var globalStore : Store = null
  
  var globalDSG : DSG = null
  
  def runWithGlobalStore () {
    // seen records the last generation store seen with this flat.
    val seen = scala.collection.mutable.HashMap[CoreState,Long]()
    var visited = scala.collection.mutable.Set[CoreState]()
    var currentGeneration : Long = 1
    
    val init = initialState
    var todo = List(init.core)
    
    globalStore = init.store
    globalDSG = new DSG()
    var timeout = -1
    
    while (!todo.isEmpty && timeout != 0) {
      var core = todo.head
      todo = todo.tail
      
      val lastSeenGeneration : Long = seen.getOrElse(core,0)
      
      /*if (currentGeneration <= lastSeenGeneration) {
        // println("Current generation: " + currentGeneration) // DEBUG
        // println("Last generation: " + lastSeenGeneration) // DEBUG
        // println("Not a new state: " + newState) // DEBUG
	}
	*/
	
      if (currentGeneration > lastSeenGeneration) {
        // globalStore changed since we last saw this flat.
        if (timeout > 0)
          timeout -= 1
	
	visited = visited + core
	
        count += 1
	
	// println(count)
	
        // Install the global store:
	var newState = new State(core, globalStore)
	
        //println("State:\n" + newState + "\n")
	
        // Explore successors:
        val succs = next(newState)
	
        // Mark this state as being seen with the current generation.
        seen(newState.core) = currentGeneration
	
	var newStore = globalStore
	
        // Check each successor for change:
        for (succ <- succs) {
	  
          var store = succ.store
          
	  if (!store.clst.isEmpty) {
            // Something changed!
            
            // Apply store changes to a temporary store:
            newStore = store.changes(new MapStore(newStore.asInstanceOf[MapStore].map, List()), "pd")
	    
	  }
        }
	
	if(! (globalStore.asInstanceOf[MapStore].toString == newStore.asInstanceOf[MapStore].toString)) {
          // Bump up the current store generation:
	  // println(globalStore.asInstanceOf[MapStore].toString + "\n\n\n" +newStore.asInstanceOf[MapStore].toString)
          currentGeneration += 1
	  globalStore = newStore
	  
	}
	
	val succCores = for(succ <- succs) yield { succ.core }
	
        todo = todo ++ succCores
      }
    }
    
    if (timeout == 0)
      println("Timeout reached")

    println("States explored: " + count)
    println("Unique states explored: " + visited.size)
    // println("State list: " + (for(s <- visited.toList) yield { s.toString + "\n\t" }))
    // println("store: " + globalStore.toString) 
    // println("DSG: " + globalDSG.toString) 
    // println("State list: " + visited)
    println("Found " + testState(visited.toList) + " possible places for inlining")
  }
}
  
class PDCFA_ANF(exp : Exp, bEnv0 : BEnv, t0 : Time, store0 : Store, botD : D) extends SmallStepAbstractPushDownInterpretation {
  
  var k : Int = 0
  
  val bEnv1 = SSPrimitives.list.foldRight (bEnv0) ((name,bEnv) => bEnv(SName.from(name)) = PrimAddr(SName.from(name)))
  
  val store1 = SSPrimitives.list.foldRight (store0) ((name,store) => store(bEnv1(SName.from(name))) = botD + PrimValue(name))
  
  val rp1 = ReturnPtr(Ref(SName.from("halt")))
  
  override def atomEval (bEnv : BEnv, store : Store) (exp : Exp) : D = exp match {
    case Lit(SBoolean(value)) => botD + BooleanValue(value)
    case _ : Lit => botD
    case Undefined() => botD
    case Ref(name) => {
      val addr = bEnv(name)
      (store get addr) match {
        case Some(d) => d
        case None => {
          throw new Exception("could not find address: " + addr)
        }
      }
    }
    case Void() => botD
    case lam : Lambda => {
      botD + Clo(lam,bEnv)
    }
  }

  def inject (exp : Exp) : State = {
    State(CoreState(exp,bEnv1,rp1,t0),store1)
  }
  
  lazy val initialState = inject(exp)
  
  def tick (call : Exp, t : Time) : Time = t.succ(k,call.label)
  
  def pushedFrames(state : CoreState, dsg : DSG) : List[Frame] = {
    dsg pushedFrames state
  }

  def evalArgs (args : Arguments, bEnv : BEnv, store : Store) : Parameters = {
    args match {
      case ListArguments(arglist) => evalArgs (new Parameters()) (arglist,bEnv,store)
    }
  }

  def evalArgs (parameters : Parameters) (arglist : List[Argument], bEnv : BEnv, store : Store) : Parameters = {
    arglist match {
      case Nil => parameters
      case hd :: tl => {
        val p = evalArgs (parameters) (tl,bEnv,store)
        hd match {
          case Argument(exp) => (atomEval (bEnv,store) (exp)) :: p
        }
      }
    }
  }
  
  
  private def applyProcedure (state : State, args : Arguments, params : Parameters, store : Store, newTime : Time) (proc : Value) : ImmSet[State] = {
    
    proc match {
      
      // evaluate closure
      case Clo(lam @ Lambda(VarFormals(name),body),bEnv2) if !(body.free contains name)  => {
	val (newDSG, newStates) = globalDSG add(state.core,
				  FullEdge(CoreState(body,bEnv2,rp1,newTime),
					   Epsilon()))
	globalDSG = newDSG
	for(c <- newStates) yield { State(c, store) }
      }
      
      // evaluate closure
      case Clo(lam @ Lambda(formals,body),bEnv2) if formals accepts args => {
	var newStore = store 
        var newBEnv = bEnv2
        
        // Bind arguments:
        for ((Formal(name),d) <- formals.formals zip params.values) {
          // TODO: Un-hard-code the MapBind; factor into alloc
          newBEnv = (newBEnv(name) = MapBind(name,newTime))
          newStore += (newBEnv(name), d)
        }
        
        if (formals.formals.length < params.values.length) {
          // Stuff the rest into a list.
          val remainder = params.values.drop(formals.formals.length)
          throw new Exception("Mismatched Arguments: " + formals + " : " + params)
        }
        
        val (newDSG, newStates) = globalDSG add (state.core,
						 FullEdge(CoreState(body,newBEnv,rp1,newTime),
							  Epsilon()))
	globalDSG = newDSG
	for(c <- newStates) yield { State(c, newStore) }
      }
      
      // evaluate primative
      case PrimValue("*"|"+"|"-"|"/"|"quotient"|"gcd"|"modulo"|"<"|"="|">"|"odd?"|"even?"|"display"|"newline"|"not") => {
        val (newDSG, newStates) = globalDSG add (state.core,
						 FullEdge(CoreState(Void(),state.core.bEnv,rp1,newTime),
							  Epsilon()))
	globalDSG = newDSG
	for(c <- newStates) yield { State(c, store) }
      }
      
      // evaluate cons
      case PrimValue("cons") => {
        if (params.values.length != 2)
          ImmSet()
        else {
          val loc = ConsLocation(newTime)
          val carD = params(0)
          var cdrD = params(1)
          val carAddr = FieldAddr(loc,SName.from("car"))
          val cdrAddr = FieldAddr(loc,SName.from("cdr"))
          var newStore = store
          newStore += (carAddr, carD)
          newStore += (cdrAddr, cdrD)
	  var newStates : ImmSet[State] = ImmSet()
          val rv = botD + loc
          val frames = pushedFrames(state.core, globalDSG)
          for (frame <- frames.toList if frame.isInstanceOf[Frame]) {
            frame match {
              case PDFrame(v,e,rho) => {
		var newBEnv = rho
                val addr = MapBind(v, newTime)
		newBEnv = newBEnv update (v, addr)
                newStore += (addr, rv)
		
		val (newDSG, newStates2) = globalDSG add (state.core,
							  FullEdge(CoreState(e,newBEnv,rp1,newTime),
								   Pop(frame)))
		globalDSG = newDSG
		newStates = newStates ++ (for(c <- newStates2) yield { State(c, newStore) })
              }
            }
          }
	  newStates
        }
      }
      
      // evaluate car or cdr
      case PrimValue(field @ ("car"|"cdr")) => {
        if (params.values.length == 1) {
          val cellLocs = params(0)
          val frames = pushedFrames(state.core, globalDSG)
	  var newStates : ImmSet[State] = ImmSet()
          for (cellLoc <- cellLocs.toList if cellLoc.isObjectLocation;
               frame <- frames.toList if frame.isInstanceOf[Frame]) {
            val loc = cellLoc.asInstanceOf[ObjectLocation]
            val fieldValue = store.getOrElse(FieldAddr(loc,SName.from("cons")),botD)
            frame match {
              case PDFrame(v,e,rho) => {
                val rv = botD join fieldValue//.asInstanceOf[Value]                           
                val addr = MapBind(v, newTime)
                var newBEnv = rho
                var newStore = store
                newBEnv = newBEnv update (v, addr)
                newStore += (addr, rv)
		
		val (newDSG, newStates2) = globalDSG add (state.core,
							  FullEdge(CoreState(e,newBEnv,rp1,newTime),
								   Pop(frame)))
		globalDSG = newDSG
		newStates ++= (for(c <- newStates2) yield { State(c, newStore) })
	      }
            }
          }
	  newStates
        } else {
         ImmSet()
        }
      }
      
      case PrimValue("error") => ImmSet()
    }
  }
  
  def next (state : State) : ImmSet[State] = {
    state match {
      // tail-call state
      case State(CoreState(exp @ App(f,args),bEnv,rp1,t),store) => {
        val procs = atomEval (bEnv,store) (f)
        val params = evalArgs (args,bEnv,store)
        val newTime = tick(exp,t)
        ImmSet() ++ (for (procValue <- procs.toList if procValue.isProcedure; 
			  succ <- applyProcedure (state,args,params,store,newTime) (procValue)) yield {
			    succ
			  })
      }
      
      // conditional state
      case State(CoreState(exp @ If(condition,ifTrue,ifFalse),bEnv,rp1,t),store) => {
	var newStates : ImmSet[State] = ImmSet()
        for (call <- List(ifTrue,ifFalse)) {
          val newTime = tick (exp,t)
	  
	  val (newDSG, newStates2) = globalDSG add (state.core,
						    FullEdge(CoreState(call,bEnv,rp1,newTime),
								   Epsilon()))
	  globalDSG = newDSG
	  newStates ++= (for(c <- newStates2) yield { State(c, store) })
	}
	newStates
      }
      
      // return state
      case State(CoreState(ae @ (_ : AExp),bEnv,rp1,t),store) => {
	// println("Return: " + ae.toString)  //DEBUG
	var newStates : ImmSet[State] = ImmSet()
	val frames = pushedFrames(state.core, globalDSG)
	val rv = atomEval(bEnv, store) (ae)
	for (frame <- frames.toList if frame.isInstanceOf[Frame]) {
          frame match {
	    case PDFrame(v,e,rho) => {
              val addr = MapBind(v, state.core.t)
              var newBEnv = rho
              var newStore = store
              newBEnv = newBEnv update (v, addr)
              newStore += (addr, rv)
	      
	      val (newDSG, newStates2) = globalDSG add (state.core,
							FullEdge(CoreState(e,newBEnv,rp1,state.core.t),
								 Pop(frame)))
	      globalDSG = newDSG
	      newStates ++= (for(c <- newStates2) yield { State(c, newStore) })
	    }
          }
        }
	newStates
      }
      
      // nontail-call state
      case State(CoreState(exp @ Let(Binding(name, value), body), bEnv, rp1, t), store) => {
	val frame = PDFrame(name,body,bEnv)
	val newTime = tick(exp, t)
	
	val (newDSG, newStates) = globalDSG add (state.core,
						 FullEdge(CoreState(value,bEnv,rp1,newTime),
							  Push(frame)))
	globalDSG = newDSG
	ImmSet() ++ (for(c <- newStates) yield { State(c, store) })
      }
      
      // set state (push)
      case State(CoreState(exp @ Set(name,value), bEnv, rp1, t), store) => {
	val frame = PDFrame(name,Void(),bEnv)
	val newTime = tick(exp, t)

	val (newDSG, newStates) = globalDSG add (state.core,
						 FullEdge(CoreState(value,bEnv,rp1,newTime),
							  Push(frame)))
	globalDSG = newDSG
	for(c <- newStates) yield { State(c, store) }
      }
      
      // end state
      case State(CoreState(exp @ Halt(), bEnv, rp1, t), store) => {
	ImmSet()
      }
      
      case _ => throw new Exception("unhandled state: " + state)
      
    }
  }


}



class CFAOptions {
  var file : String = null ;
  var k = 0
  var analysis = "k"
}


object CFAOptions {

  def parse(args : List[String], opts : CFAOptions) : Unit = args match {
    case List() => {}
    case "--k" :: k :: rest => { 
      opts.k = Integer.parseInt(k)
      parse(rest,opts)
    }
    
    case "--analysis" :: a :: rest => { 
      opts.analysis = a
      parse(rest,opts)
    }

    case fileName :: rest => {
      opts.file = fileName ;
      parse(rest,opts)
    }

  }

  def parse(args : Array[String]) : CFAOptions = {
    val opts = new CFAOptions
    parse(args.toList,opts)
    opts
  }
}


object RunCFA {

  def main (args : Array[String]) {

    val opts = CFAOptions.parse(args)

    if (opts.file == null) {
      System.err.println ("Please specify a filename.")
      return 
    }

    val filename = opts.file
    System.err.print("Parsing s-expressions...")
    val sexps = SExp.parseAllIn(filename)
    System.err.println("done")
    
    System.err.print("Bulding AST...")
    val ast = SSParser(sexps)
    System.err.println("done") 
    
    System.out.println("Input program:")
    System.out.println(ast)
    System.out.println("\n")

    opts.analysis match {
      case "k" => { 
	val CFA = new KCFA_ANF(ast.exp,new MapBEnv(TreeMap()), KTime(List()), new MapStore(), new SortedSetD())
	CFA.k = opts.k
	CFA.runWithGlobalStore()
      }
      case "pd" => { 
	val CFA = new PDCFA_ANF(ast.exp,new MapBEnv(TreeMap()), KTime(List()), new MapStore(), new SortedSetD())
	CFA.k = opts.k
	CFA.runWithGlobalStore()
      }
    }
    
    ()
  }
}


case class listing (val map : SortedMap[SName,D], val botD : D) {
  def this () = this(TreeMap(), new SortedSetD())
  def this (map : SortedMap[SName,D]) = this(map, new SortedSetD())
  
  def apply(addr : SName) : D = (this get addr) match {
    case Some(d) => d
    case None => throw new Exception("Could not find " + addr)
  }
  
  def getOrElse(addr : SName, default : D) : D = (this get addr) match {
    case Some(d) => d
    case None => default
  }
  
  def get(addr : SName) : Option[D] = map get addr

  def wt (that : listing) = {
    var test = true
    for( (addr, d1) <- map if test == true)
      that get addr match {
	case Some(d2) => test = d1 wt d2
	case None => test = d1 wt botD
      }
  }
  
  def + (addr : SName, d : D) : listing = {
    map get addr match {
      case Some(existingD) => new listing(map(addr) = d join existingD)
      case None => new listing(map(addr) = d)
    }
  }
  
  def update (addr : SName, d : D) : listing = {
    // We don't have enough information to do a strong update, so we fall back to a weak update.
    this + (addr,d)
  }
  
  def toList = map.toList
  
  override def toString = "\n " +  (map mkString "\n ")
}