LARA

```package minijava.controlflow

trait PartialOrder {
type Elem
def leq(x : Elem, y : Elem) : Boolean // less than or equal
}
trait Lattice extends PartialOrder {
val top : Elem                        // universal set
val bottom : Elem                     // empty set
def join(x : Elem, y : Elem) : Elem   // union
def meet(x : Elem, y : Elem) : Elem   // intersection
}

// there should be more elegant definition--but make sure domain of results are correct
class PointwiseLattice[I,E,L <: Lattice{type Elem=E}](base : L, domain : Set[I])
extends Lattice
{
type Elem=Map[I,E]

def leq(x : Elem, y : Elem) : Boolean =  domain.forall(i => base.leq(x(i),y(i)))
val (top : Elem) = {
var res = Map[I,E]()
for (i <- domain)
res = res.update(i, base.top)
res
}
val (bottom : Elem) = {
var res = Map[I,E]()
for (i <- domain)
res = res.update(i, base.bottom)
res
}
def join(x : Elem, y : Elem) = {
var res = Map[I,E]()
for (i <- domain)
res = res.update(i, base.join(x(i),y(i)))
res
}
def meet(x : Elem, y : Elem) = {
var res = Map[I,E]()
for (i <- domain)
res = res.update(i, base.meet(x(i),y(i)))
res
}
}

object RangeLattice extends Lattice {
sealed abstract class Range
case object Empty extends Range // {}
case class Bounded(a : Int, b : Int) extends Range // [a,b]
{ assert (a <= b) }
case class LeftUnbounded(b : Int) extends Range // (-inf,b]
case class RightUnbounded(a : Int) extends Range // [a,+inf)
case object Full extends Range // (-inf,+inf)

type Elem = Range
def leq(x : Range, y : Range) = (x,y) match {
case (Empty,_) => true
case (_,Full) => true
case (Bounded(a1,b1),Bounded(a2,b2)) => (a2 <= a1 && b1 <= b2)
//  a2...a1...b1...b2
case (Bounded(a1,b1),LeftUnbounded(b2)) => (b1 <= b2)
case (Bounded(a1,b1),RightUnbounded(a2)) => (a2 <= a1)
case (LeftUnbounded(b1),LeftUnbounded(b2)) => (b1 <= b2)
case (RightUnbounded(a1),RightUnbounded(a2)) => (a2 <= a1)
case _ => false
}

val top = Full
val bottom = Empty

def join(x : Range, y : Range) = {
import Math.{min,max}
(x,y) match {
case (Empty,_) => y
case (_,Empty) => x
case (Full,_) => Full
case (_,Full) => Full
case (Bounded(a1,b1),Bounded(a2,b2)) =>
Bounded(min(a1,a2), max(b1,b2))
case (LeftUnbounded(b1),LeftUnbounded(b2)) =>
LeftUnbounded(max(b1,b2))
case (RightUnbounded(a1),RightUnbounded(a2)) =>
RightUnbounded(min(a1,a2))
case (LeftUnbounded(_),RightUnbounded(_)) => Full
case (RightUnbounded(_),LeftUnbounded(_)) => Full
case (Bounded(a1,b1),LeftUnbounded(b2)) =>
LeftUnbounded(max(b1,b2))
case (LeftUnbounded(b2),Bounded(a1,b1)) =>
LeftUnbounded(max(b1,b2))
case (Bounded(a1,b1),RightUnbounded(a2)) =>
RightUnbounded(min(a1,a2))
case (RightUnbounded(a2),Bounded(a1,b1)) =>
RightUnbounded(min(a1,a2))
}
}
def meet(x : Range, y : Range) = {
import Math.{min,max}
(x,y) match {
case (Empty,_) => Empty
case (_,Empty) => Empty
case (Full,_) => y
case (_,Full) => x
case (Bounded(a1,b1),Bounded(a2,b2)) => {
val a = max(a1,a2)
val b = min(b1,b2)
if (a <= b) Bounded(a,b) else Empty
}
case (LeftUnbounded(b1),LeftUnbounded(b2)) =>
LeftUnbounded(min(b1,b2))
}
}
}

object LatticeCombination {
def product(first : Lattice, second : Lattice) : Lattice = new Lattice {
type Elem = (first.Elem, second.Elem)
def leq(x : Elem, y : Elem) : Boolean =
first.leq(x._1,y._1) && second.leq(x._2,y._2)
val top = (first.top, second.top)
val bottom = (first.bottom, second.bottom)
def join(x : Elem, y : Elem) : Elem =
(first.join(x._1,y._1), second.join(x._2,y._2))
def meet(x : Elem, y : Elem) : Elem =
(first.meet(x._1,y._1), second.meet(x._2,y._2))
}

def mapPower[T](m : Map[T,Lattice]) : Lattice = new Lattice {
type Elem = Map[T,Any]
def leq(x : Elem, y : Elem) : Boolean = {
def leqAt(t:T, lat : Lattice) : Boolean = {
type e = lat.Elem
lat.leq(x(t).asInstanceOf[e],
y(t).asInstanceOf[e])
}
m.transform(leqAt).forall(_._2)
}
val (top : Elem) = {
def topAt(t : T, lat : Lattice) : Any = { lat.top }
m.transform(topAt)
}
val (bottom : Elem) = {
def bottomAt(t : T, lat : Lattice) : Any = { lat.bottom }
m.transform(bottomAt)
}
def join(x : Elem, y : Elem) = {
def joinAt(t : T, lat : Lattice) : Any = {
type e = lat.Elem
lat.join(x(t).asInstanceOf[e],
y(t).asInstanceOf[e])
}
m.transform(joinAt)
}
def meet(x : Elem, y : Elem) = {
def meetAt(t : T, lat : Lattice) : Any = {
type e = lat.Elem
lat.meet(x(t).asInstanceOf[e],
y(t).asInstanceOf[e])
}
m.transform(meetAt)
}
}
}```