TermEval.scala

import scala.collection.mutable.HashMap

class Term[Name]
case class Var[Name] (val x: Name) extends Term[Name]
case class App[Name] (val t1: Term[Name], val t2: Term[Name]) extends Term[Name]
case class Lam[Name] (val x: Name, t1: Term [Name]) extends Term[Name]


class FreeVars[Name](val instance: Term[Name]) {
  def freeVars: List[Name] = instance match {
    case Var(x) => List(x)
    case App(t1, t2) => t1.freeVars ++ t2.freeVars
    case Lam(x, t1) => t1.freeVars.filter(y => y != x)
  }
}
implicit def addFreeVars[Name](t: Term[Name]): FreeVars[Name] = new FreeVars(t)
implicit def noFreeVars[Name](f: FreeVars[Name]): Term[Name] = f.instance
assert( Var("x").freeVars == List("x") )
assert( Lam("x", App(Var("x"), Var("y"))).freeVars == List("y") )


trait Fresh[N] { 
  def fresh(): N
}

implicit val deBruijn = new Fresh[Int] {
  var counter: Int = 0;
  def fresh(): Int = {
    counter += 1;
    counter
  }
}

implicit val deBruijnStr = new Fresh[String] {
  var counter: Int = 0;
  def fresh(): String = {
    counter += 1;
    counter.toString
  }
}

class Subst[Name](val instance: Term[Name])(implicit F: Fresh[Name]) {
  def subst(n: Name, t: Term[Name]): Subst[Name] = {
    instance match {
      case v@Var(x) => {
        if (x == n) {
          t
        } else {
          v
        }
      }
      
      case App(t1, t2) => {
        App(t1.subst(n, t), t2.subst(n, t))
      }
      
      case l@Lam(x, t1) => {
        if (n == x) {
          l
        } else if (t.freeVars.contains(x)) {
          val f = F.fresh()
          Lam(f, t1.subst(x, Var(f)).subst(n, t))
        } else {
          Lam(x, t1.subst(n, t))
        }
      }
    }
  }
}
implicit def addSubst[Name: Fresh](t: Term[Name]): Subst[Name] = new Subst(t)
implicit def noSubst[Name: Fresh](s: Subst[Name]): Term[Name] = s.instance
assert( Var(0).subst(0, Var(1)).instance == Var(1) )
assert( Lam(0, Var(0)).subst(0, Var(1)).instance == Lam(0, Var(0)) )
assert( (Lam(0, App(Var(1), Var(0))).subst(1, Var(0)).instance match { case Lam(x, _) => x }) != 0 )
assert( (Lam(0, App(Var(1), Var(0))).subst(1, Var(0)).instance match { case Lam(_, App(t, _)) => t }) == Var(0) )


class Beta[Name](val instance: Lam[Name])(implicit F: Fresh[Name]) {
  def beta(t: Term[Name]): Term[Name] = {
    instance.t1.subst(instance.x, t)
  }
}
implicit def addBeta[Name](l: Lam[Name])(implicit F: Fresh[Name]): Beta[Name] = new Beta(l)
implicit def noBeta[Name](b: Beta[Name]): Lam[Name] = b.instance
assert(Lam(0, Var(0)).beta(Var(1)) == Var(1))
assert(Lam(0, App(Var(0), Var(2))).beta(Var(1)) == App(Var(1), Var(2)))

sealed abstract class dTerm[Name]
// Name gives position of hole
case class AppLeft[Name](val t: Term[Name]) extends dTerm[Name]
case class AppRight[Name](val t: Term[Name]) extends dTerm[Name]
case class LamRight[Name](val x: Name) extends dTerm[Name]
type TermPath[Name] = List[dTerm[Name]]

case class TermZipperBoundsException(val message: String) extends Exception
case class TermZipper[Name](val path: TermPath[Name], val sub: Term[Name]) {
  def up(): TermZipper[Name] = {
    path match {
      case List() => throw TermZipperBoundsException("Already at the top.")
      case AppLeft(t)::tail => TermZipper(tail, App(sub, t))
      case AppRight(t)::tail => TermZipper(tail, App(t, sub))
      case LamRight(x)::tail => TermZipper(tail, Lam(x, sub))
    }
  }
  def down(): TermZipper[Name] = {
    sub match {
      case Var(_) => throw TermZipperBoundsException("Already at the bottom.")
      case App(t1, t2) => TermZipper(path ++ List(AppLeft(t2)), t1)
      case Lam(x, t) => TermZipper(path ++ List(LamRight(x)), t)
    }
  }
  def left(): TermZipper[Name] = {
    path match {
      case AppRight(t)::tail => TermZipper(AppLeft(sub)::tail, t)
      case _ => throw TermZipperBoundsException("Already at the left.")
    }
  }
  def right(): TermZipper[Name] = {
    path match {
      case AppLeft(t)::tail => TermZipper(AppRight(sub)::tail, t)
      case _ => throw TermZipperBoundsException("Already at the right.")
    }
  }
}
object TermZipper {
  def apply[Name](t: Term[Name]): TermZipper[Name] = TermZipper(List(), t)
}
implicit def addZipper[Name](t: Term[Name]): TermZipper[Name] = TermZipper(t)
assert( App(Var(0), Var(1)).down == TermZipper(List(AppLeft(Var(1))), Var(0)) )
assert( TermZipper(List(AppLeft(Var(1))), Var(0)).right == TermZipper(List(AppRight(Var(0))), Var(1)) )
assert( TermZipper(List(AppLeft(Var(1))), Var(0)).up == TermZipper(App(Var(0), Var(1))) )
assert( TermZipper(List(AppRight(Var(0))), Var(1)).up == addZipper(App(Var(0), Var(1))) )
assert( TermZipper(List(LamRight(0)), Var(0)).up == addZipper(Lam(0, Var(0))) )

class Eval[Name](val instance: TermZipper[Name])(implicit F: Fresh[Name]) {
  def eval[Return](k: TermZipper[Name] => Return, m: HashMap[String, TermZipper[Name] => Return]): Return = {
    m += (("session://" + instance.path.mkString("/") + "/" + instance.sub.toString, k))
    instance.sub match {
      case Var(_) => k(instance)
      case Lam(_, _) => k(instance)
      case App(Var(_), _) => k(instance)
      case App(l@Lam(_, _), t) => TermZipper(instance.path, l.beta(t)).eval(k, m)
      case App(a@App(_, _), t1) => {
        TermZipper(instance.path ++ List(AppLeft(t1)), a).eval(
            (t: TermZipper[Name]) => TermZipper(instance.path, App(t.sub, t1)).eval(k, m),
            m)
      }
    }
  }
  def eval[Return](k: TermZipper[Name] => Return): Return = eval(k, new HashMap[String, TermZipper[Name] => Return])
}
implicit def addEval[Name](t: TermZipper[Name])(implicit F: Fresh[Name]): Eval[Name] = new Eval(t)
implicit def noEval[Name](e: Eval[Name]): TermZipper[Name] = e.instance
implicit def addEvalChain[Name](t: Term[Name])(implicit F: Fresh[Name]): Eval[Name] = new Eval(addZipper(t))

App(App(Lam(0, Lam(1, Var(0))), Var(1)), Var(2)).eval((t: TermZipper[Int]) => assert(t == addZipper(Var(1))))
App(Var(0), Var(1)).eval((t: TermZipper[Int]) => assert(t == addZipper(App(Var(0), Var(1)))))

val kmap = new HashMap[String, TermZipper[Int] => Unit]

App(App(Lam(0, Lam(1, Var(0))), Var(1)), Var(2)).eval((t: TermZipper[Int]) => assert(t == addZipper(Var(1))), kmap)
assert(
  (try {
    kmap("session://AppLeft(Var(2))/App(Lam(0,Lam(1,Var(0))),Var(1))")(Lam(19, Var(19))) 
  } catch {
    case _: AssertionError => "passed" 
  }) == "passed"
)