From 8a5ec8ff6fdafcdec40ad9c27d7c8a0f36f32cdd Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Sat, 28 May 2016 17:23:07 +0200 Subject: [PATCH] miniscala to DOT translation written in Scala --- .../src/main/scala/miniscala/DotTrees.scala | 32 ++++ .../src/main/scala/miniscala/Main.scala | 3 + .../main/scala/miniscala/MiniScalaToDot.scala | 157 ++++++++++++++++++ .../main/scala/miniscala/MiniScalaTrees.scala | 83 +++++++-- 4 files changed, 260 insertions(+), 15 deletions(-) create mode 100644 scala/miniscala1/src/main/scala/miniscala/DotTrees.scala create mode 100644 scala/miniscala1/src/main/scala/miniscala/MiniScalaToDot.scala diff --git a/scala/miniscala1/src/main/scala/miniscala/DotTrees.scala b/scala/miniscala1/src/main/scala/miniscala/DotTrees.scala new file mode 100644 index 0000000..cba8877 --- /dev/null +++ b/scala/miniscala1/src/main/scala/miniscala/DotTrees.scala @@ -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) + } +} diff --git a/scala/miniscala1/src/main/scala/miniscala/Main.scala b/scala/miniscala1/src/main/scala/miniscala/Main.scala index d04f529..486440d 100644 --- a/scala/miniscala1/src/main/scala/miniscala/Main.scala +++ b/scala/miniscala1/src/main/scala/miniscala/Main.scala @@ -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() } } diff --git a/scala/miniscala1/src/main/scala/miniscala/MiniScalaToDot.scala b/scala/miniscala1/src/main/scala/miniscala/MiniScalaToDot.scala new file mode 100644 index 0000000..fccc767 --- /dev/null +++ b/scala/miniscala1/src/main/scala/miniscala/MiniScalaToDot.scala @@ -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") + } + +} diff --git a/scala/miniscala1/src/main/scala/miniscala/MiniScalaTrees.scala b/scala/miniscala1/src/main/scala/miniscala/MiniScalaTrees.scala index 815bca9..fabd07c 100644 --- a/scala/miniscala1/src/main/scala/miniscala/MiniScalaTrees.scala +++ b/scala/miniscala1/src/main/scala/miniscala/MiniScalaTrees.scala @@ -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)) } @@ -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))) + } + } }