Skip to content

Commit

Permalink
miniscala to DOT translation written in Scala
Browse files Browse the repository at this point in the history
  • Loading branch information
samuelgruetter committed May 28, 2016
1 parent eb3e454 commit 8a5ec8f
Show file tree
Hide file tree
Showing 4 changed files with 260 additions and 15 deletions.
32 changes: 32 additions & 0 deletions scala/miniscala1/src/main/scala/miniscala/DotTrees.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
package miniscala

object DotTrees {

sealed trait Vr
case class Var(name: String) extends Vr
case class VObj(selfName: String, ds: Seq[Dm]) extends Vr

sealed trait Ty
case object TBot extends Ty
case object TTop extends Ty
case class TFun(name: String, argName: String, argType: Ty, retType: Ty) extends Ty
case class TMem(name: String, lo: Ty, hi: Ty) extends Ty
//def TAlias(name: String, tp: Ty) = TMem(name, tp, tp)
case class TAlias(name: String, tp: Ty) extends Ty // syntactic sugar defined in DOT
case class TSel(qual: Vr, sel: String) extends Ty
case class TBind(selfName: String, tp: Ty) extends Ty
case class TAnd(tp1: Ty, tp2: Ty) extends Ty
case class TOr(tp1: Ty, tp2: Ty) extends Ty

sealed trait Tm
case class TmVar(v: Vr) extends Tm
case class TmApp(t1: Tm, l: String, t2: Tm) extends Tm

sealed trait Dm
case class DFun(name: String, argName: String, argType: Ty, retType: Ty, body: Tm) extends Dm
case class DTy(name: String, tp: Ty) extends Dm

def Let(x: String, t1: Tm, tp1: Ty, t2: Tm, tp2: Ty): Tm = {
TmApp(TmVar(VObj("_unusedSelf", Seq(DFun("call", x, tp1, tp2, t2)))), "call", t1)
}
}
3 changes: 3 additions & 0 deletions scala/miniscala1/src/main/scala/miniscala/Main.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,5 +12,8 @@ object Main {
val s: String = LnMiniscalaToCoq.printTrm(t2)
println(s)
println()
val t3: DotTrees.Tm = MiniScalaToDot.translateProg(t1)
println(t3)
println()
}
}
157 changes: 157 additions & 0 deletions scala/miniscala1/src/main/scala/miniscala/MiniScalaToDot.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,157 @@
package miniscala

import miniscala.{MiniScalaTrees => ms}
import miniscala.{DotTrees => dot}

object MiniScalaToDot {

def translateProg(t: ms.Trm): dot.Tm = trTrm(Nil, t)._2

// Why also typechecking during translation?
// - enforce nominality
// - get type T2 in expressions translated to "let x = t1 in t2" for
// "(new { def call(x: T1): T2 = t2 }).call(t1)" (DOT requires explicit return type T2)

type Ctx = List[(String, ms.Typ)]
def lookupVar(name: String, ctx: Ctx): ms.Typ = ctx.find(_._1 == name) match {
case Some((_, tp)) => tp
case None => sys.error(s"$name not found in context\n${ctx.mkString("\n")}")
}

def lookupDef(name: String, defs: Seq[ms.Def]): ms.Def = defs.find(_.name == name).get

def checkConforms(actual: ms.Typ, expected: ms.Typ): Unit = {
if (actual != expected) sys.error(s"expected $expected but found $actual")
}

def lookupClass(p: ms.Pth, ctx: Ctx): ms.TypOfCls = p match {
case ms.PthVar(name) => lookupVar(name, ctx).asInstanceOf[ms.TypOfCls]
case ms.PthSel(prefix, sel) =>
val ms.TypCls(q) = lookupVar(prefix, ctx)
val ms.TypOfCls(z0, ds0) = lookupClass(q, ctx)
val ms.DefClass(_, z, ds) = lookupDef(sel, ds0)
ms.TypOfCls(z, ds.map(_.subst(z0, prefix)))
}

val unit = dot.TmVar(dot.VObj("_", Seq()))

def trTyp(t: ms.Pth): dot.Ty = t match {
case ms.PthVar(name) => dot.TSel(dot.Var(name), "C")
case ms.PthSel(prefix, sel) => dot.TSel(dot.Var(prefix), "C_" + sel)
}

def trCtorRef(c: ms.Pth): dot.Tm = c match {
case ms.PthVar(name) => dot.TmApp(dot.TmVar(dot.Var(name)), "new", unit)
case ms.PthSel(prefix, sel) => dot.TmApp(dot.TmVar(dot.Var(prefix)), "new_" + sel, unit)
}

def trTypOfDef(d: ms.Def, outerSelfRef: String): (dot.Ty, dot.Ty) = d match {
case ms.DefClass(name, selfName, defs) =>
val defsType = trTypOfDefs(defs, selfName)
val tpmem = dot.TAlias("C_" + name, dot.TBind(selfName, defsType))
val defmem = dot.TFun("new_" + name, "_dummy", dot.TTop, dot.TSel(dot.Var(outerSelfRef), "C_" + name))
(tpmem, defmem)
case ms.DefDef(name, argName, argTp, retTp, body) =>
val ms.TypCls(argTpPth) = argTp
val ms.TypCls(retTpPth) = retTp
(dot.TFun(name, argName, trTyp(argTpPth), trTyp(retTpPth)), dot.TTop)
case ms.DefVal(name, tp, rhs) => sys.error("not yet supported")
}

def trTypOfDefs(ds: Seq[ms.Def], outerSelfRef: String): dot.Ty = if (ds.isEmpty) {
dot.TTop
} else {
val (t1, t2) = trTypOfDef(ds.head, outerSelfRef)
dot.TAnd(t1, dot.TAnd(t2, trTypOfDefs(ds.tail, outerSelfRef)))
}

// returns Seq of length 1 or 2
def trDef(ctx: Ctx, d: ms.Def, outerSelfRef: String): Seq[dot.Dm] = d match {
case ms.DefClass(name, selfName, defs) =>
val ctx2 = (selfName, ms.TypCls(ms.PthSel(outerSelfRef, name))) :: ctx
val defsType = trTypOfDefs(defs, selfName)
val tpdef = dot.DTy("C_" + name, dot.TBind(selfName, defsType))
val defdef = dot.DFun("new_" + name, "_dummy", dot.TTop, dot.TSel(dot.Var(outerSelfRef), "C_" + name),
dot.TmVar(dot.VObj(selfName, trDefs(ctx2, defs, selfName)))
)
Seq(tpdef, defdef)
case ms.DefDef(name, argName, argTp, retTp, body) =>
val (actualRetTp, body2) = trTrm((argName, argTp) :: ctx, body)
checkConforms(actualRetTp, retTp)
val ms.TypCls(argTpPth) = argTp
val ms.TypCls(retTpPth) = retTp
Seq(dot.DFun(name, argName, trTyp(argTpPth), trTyp(retTpPth), body2))
case ms.DefVal(name, tp, rhs) => sys.error("not yet supported")
}

def trDefs(ctx: Ctx, ds: Seq[ms.Def], outerSelfRef: String): Seq[dot.Dm] = if (ds.isEmpty) {
Seq()
} else {
trDef(ctx, ds.head, outerSelfRef) ++ trDefs(ctx, ds.tail, outerSelfRef)
}

def trTrm(ctx: Ctx, t: ms.Trm): (ms.Typ, dot.Tm) = t match {
case ms.Var(name) => (lookupVar(name, ctx), dot.TmVar(dot.Var(name)))

// TODO notin FV checks
case ms.App(ms.Var(x1), label, ms.Var(x2)) =>
val ms.TypCls(p1) = lookupVar(x1, ctx)
val ms.TypCls(p2) = lookupVar(x2, ctx)
val ms.TypOfCls(z, ds) = lookupClass(p1, ctx)
val ms.DefDef(_, argName, argTyp, retTyp, _) = lookupDef(label, ds).subst(z, x1)
checkConforms(ms.TypCls(p2), argTyp)
(retTyp.subst(argName, x2), dot.TmApp(dot.TmVar(dot.Var(x1)), label, dot.TmVar(dot.Var(x2))))
case ms.App(ms.Var(x1), label, t2) =>
val ms.TypCls(p1) = lookupVar(x1, ctx)
val (tp2, t2a) = trTrm(ctx, t2)
val ms.TypOfCls(z, ds) = lookupClass(p1, ctx)
val ms.DefDef(_, argName, argTyp, retTyp, _) = lookupDef(label, ds).subst(z, x1)
checkConforms(tp2, argTyp)
(retTyp, dot.TmApp(dot.TmVar(dot.Var(x1)), label, t2a))
case ms.App(t1, label, ms.Var(x2)) =>
val (ms.TypCls(p1), t1a) = trTrm(ctx, t1)
val ms.TypCls(p2) = lookupVar(x2, ctx)
val ms.TypOfCls(z, ds) = lookupClass(p1, ctx)
val ms.DefDef(_, argName, argTyp, retTyp, _) = lookupDef(label, ds)
checkConforms(ms.TypCls(p2), argTyp)
(retTyp.subst(argName, x2), dot.TmApp(t1a, label, dot.TmVar(dot.Var(x2))))
case ms.App(t1, label, t2) =>
val (ms.TypCls(p1), t1a) = trTrm(ctx, t1)
val (tp2, t2a) = trTrm(ctx, t2)
val ms.TypOfCls(z, ds) = lookupClass(p1, ctx)
val ms.DefDef(_, argName, argTyp, retTyp, _) = lookupDef(label, ds)
checkConforms(tp2, argTyp)
(retTyp, dot.TmApp(t1a, label, t2a))

case ms.New(cls) =>
val _ = lookupClass(cls, ctx)
(ms.TypCls(cls), trCtorRef(cls))

case ms.Block(ms.DefVal(name, tp1, t1), t2) =>
val (actualTp1, t1a) = trTrm(ctx, t1)
checkConforms(actualTp1, tp1)
val ctx2 = (name, tp1) :: ctx
val (tp2, t2a) = trTrm(ctx2, t2) // NOTE: here we get the type t2a, that's why we need to do typechecking
val ms.TypCls(tp1Pth) = tp1
val ms.TypCls(tp2Pth) = tp2
(tp2, dot.Let(name, t1a, trTyp(tp1Pth), t2a, trTyp(tp2Pth)))
case ms.Block(ms.DefClass(name, selfName, defs), t2) =>
val ctx2 = (name, ms.TypOfCls(selfName, defs)) :: ctx
val ctx3 = (selfName, ms.TypCls(ms.PthVar(name))) :: ctx2
val defs2 = trDefs(ctx3, defs, selfName)
val defsTp = trTypOfDefs(defs, selfName)
val (tp2, t2a) = trTrm(ctx2, t2)
val ms.TypCls(tp2Pth) = tp2
val obj = dot.VObj("_self", Seq(
dot.DTy("C", dot.TBind(selfName, defsTp)),
dot.DFun("new", "_dummy", dot.TTop, dot.TSel(dot.Var("_self"), "C"), dot.TmVar(dot.VObj(selfName, defs2)))
))
val objTp = dot.TBind("_self", dot.TAnd(
dot.TAlias("C", dot.TBind(selfName, defsTp)),
dot.TFun("new", "_dummy", dot.TTop, dot.TSel(dot.Var("_self"), "C"))
))
(tp2, dot.Let(name, dot.TmVar(obj), objTp, t2a, trTyp(tp2Pth)))
case ms.Block(ms.DefDef(name, argName, argTyp, retTyp, body), expr) => sys.error("not yet supported")
}

}
83 changes: 68 additions & 15 deletions scala/miniscala1/src/main/scala/miniscala/MiniScalaTrees.scala
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,35 @@ import scala.collection.immutable.Seq
*/
object MiniScalaTrees {

sealed trait Pth
case class PthVar(name: String) extends Pth
case class PthSel(prefix: String /*not (yet) Pth!*/, sel: String) extends Pth
sealed trait Pth {
def subst(from: String, to: String): Pth
}
case class PthVar(name: String) extends Pth {
def subst(from: String, to: String): PthVar = if (name == from) PthVar(to) else PthVar(name)
}
case class PthSel(prefix: String /*not (yet) Pth!*/, sel: String) extends Pth {
def subst(from: String, to: String): PthSel = if (prefix == from) PthSel(to, sel) else PthSel(prefix, sel)
}

sealed trait Trm
case class Var(name: String) extends Trm
case class App(receiver: Trm, label: String, arg: Trm) extends Trm
case class New(cls: Pth) extends Trm
case class Block(stat: Stat, ret: Trm) extends Trm
sealed trait Trm {
def subst(from: String, to: String): Trm
}
case class Var(name: String) extends Trm {
def subst(from: String, to: String): Var = if (name == from) Var(to) else Var(name)
}
case class App(receiver: Trm, label: String, arg: Trm) extends Trm {
def subst(from: String, to: String) = App(receiver.subst(from, to), label, arg.subst(from, to))
}
case class New(cls: Pth) extends Trm {
def subst(from: String, to: String) = New(cls.subst(from, to))
}
case class Block(stat: Stat, ret: Trm) extends Trm {
def subst(from: String, to: String): Block = if (stat.name == from) {
Block(stat, ret) // TODO what about var in type of DefVal?
} else {
Block(stat.subst(from, to), ret.subst(from, to))
}
}
object Block {
def apply(stats: Seq[Stat], ret: Trm): Trm = stats.foldRight(ret)((stat, oldRet) => Block(stat, oldRet))
}
Expand All @@ -28,13 +48,46 @@ object MiniScalaTrees {

sealed trait Def {
def name: String
def subst(from: String, to: String): Def
}
case class DefVal(name: String, typ: Typ, rhs: Trm) extends Def {
def subst(from: String, to: String): DefVal = {
DefVal(name, typ.subst(from, to), rhs.subst(from, to))
}
}
case class DefDef(name: String, argName: String, argTyp: Typ, retTyp: Typ, body: Trm) extends Def {
def subst(from: String, to: String): DefDef = if (argName == from ) {
DefDef(name, argName, argTyp.subst(from, to), retTyp, body)
} else {
DefDef(name, argName, argTyp.subst(from, to), retTyp.subst(from, to), body.subst(from, to))
}
}
case class DefClass(name: String, selfName: String, defs: Seq[Def]) extends Def {
def subst(from: String, to: String): DefClass = if (selfName == from) {
DefClass(name, selfName, defs)
} else {
DefClass(name, selfName, defs.map(_.subst(from, to)))
}
}
case class DefVal(name: String, typ: Typ, rhs: Trm) extends Def
case class DefDef(name: String, argName: String, argTyp: Typ, retTyp: Typ, body: Trm) extends Def
case class DefClass(name: String, selfName: String, defs: Seq[Def]) extends Def

sealed trait Typ
case class TypCls(ref: Pth) extends Typ
case class TypMtd(argName: String, argTyp: Typ, retTyp: Typ) extends Typ
case class TypOfCls(selfName: String, members: Seq[Def]) extends Typ
sealed trait Typ {
def subst(from: String, to: String): Typ
}
case class TypCls(ref: Pth) extends Typ {
def subst(from: String, to: String): Typ = TypCls(ref.subst(from, to))
}
case class TypMtd(argName: String, argTyp: Typ, retTyp: Typ) extends Typ {
def subst(from: String, to: String): Typ = if (argName == from) {
TypMtd(argName, argTyp.subst(from, to), retTyp)
} else {
TypMtd(argName, argTyp.subst(from, to), retTyp.subst(from, to))
}
}
case class TypOfCls(selfName: String, members: Seq[Def]) extends Typ {
def subst(from: String, to: String): TypOfCls = if (selfName == from) {
TypOfCls(selfName, members)
} else {
TypOfCls(selfName, members.map(_.subst(from, to)))
}
}
}

0 comments on commit 8a5ec8f

Please sign in to comment.