Commit 0832dbb5 authored by André Pacak's avatar André Pacak
Browse files

ctxfusion and error collection

parent 146a730e
package itypes.compiler
import itypes.Context
import itypes.lang.TypeLang._
import itypes.compiler.Util._
trait CollectErrorsTrans extends Context {
def reportStuck: Seq[String]
def genPropagateRules: Boolean
def apply(spec: Spec): Spec = {
initJudgmentDeclarations(spec)
val reportStuckDecls = spec.judgs.filter { j => reportStuck.contains(j.name) }
val errorDecls = reportStuckDecls.map(deriveDecl)
val rules = spec.rules.flatMap(newError) ++
spec.rules.flatMap(propagate) ++
spec.rules.flatMap(retainSliced) ++
spec.rules.flatMap(retainNormal)
Spec(spec.name, spec.judgs ++ errorDecls, rules)
}
def deriveDecl(decl: JudgmentDeclaration): JudgmentDeclaration = {
val inputParams = selectAtIndices(decl.params, inputIndices(decl))
val errorParam = (StringSort, Out, "")
JudgmentDeclaration(nameOfEpsilon(decl), "", inputParams :+ errorParam, Map())
}
def nameOfEpsilon(decl: JudgmentDeclaration): String = s"epsilon_${decl.name}"
def propagate(rule: Rule): Seq[Rule] = {
if (reportStuck.contains(rule.conc.name)) {
val concDecl = lookupJudgment(rule.conc.name)
val reportStuckPrems = rule.prems.collect { case ji: JudgmentInstance if (reportStuck.contains(ji.name)) => ji }
reportStuckPrems.map { prem =>
val inputs = inputMetaterms(rule.conc)(this)
val gensym = new Gensym(metavars(rule)(this).map(_.name))
val msgVar = MetaVar(gensym.fresh("msg"))
val conc = JudgmentInstance(nameOfEpsilon(concDecl), inputs :+ msgVar)
val premDecl = lookupJudgment(prem.name)
val prevPrems = rule.prems.take(rule.prems.indexOf(prem))
val prems = prevPrems :+ JudgmentInstance(nameOfEpsilon(premDecl), inputMetaterms(prem)(this) :+ msgVar)
Rule(s"epsilon_${rule.name}", prems, conc)
}
} else Seq()
}
def newError(rule: Rule): Seq[Rule] = {
if (reportStuck.contains(rule.conc.name)) {
val concDecl = lookupJudgment(rule.conc.name)
val isErrorSource = (x: Instance) => isFallible(x) && !isIgnoreStuck(concDecl, x)
val fallible = rule.prems.filter(isErrorSource)
fallible.map { prem =>
val inputs = inputMetaterms(rule.conc)(this)
val msg = deriveErrorMsg(prem)
val conc = JudgmentInstance(nameOfEpsilon(concDecl), inputs :+ StringVal(msg))
val prevPrems = rule.prems.take(rule.prems.indexOf(prem))
val prems = prevPrems :+ genNegation(prem)
Rule(s"epsilon_${rule.name}", prems, conc)
}
} else Seq()
}
// what cannot fail?
def isFallible(inst: Instance): Boolean = inst match {
case JudgmentInstance(name, args) => true
case Lookup(map, k, v) => true
case Eq(lhs, rhs) => true
case Neq(lhs, rhs) => true
case Match(t, pat) => true
case Undef(t) => true
case Not(inst) => true
case LatticeMemberCall(res) => true
}
def isIgnoreStuck(decl: JudgmentDeclaration, inst: Instance): Boolean =
if (decl.name.startsWith("phi") || decl.name.startsWith("pi")) {
true
} else inst match {
case JudgmentInstance(name, _) => name.startsWith("pi")
case _ => false
}
def deriveErrorMsg(inst: Instance): String = inst match {
case JudgmentInstance(name, args) => s"Judgment ${name} failed"
case Lookup(map, k, v) => s"Lookup of ${k.prettyprint} in ${map.prettyprint} failed"
case Eq(lhs, rhs) => s"Equality check of ${lhs.prettyprint} and ${rhs.prettyprint} failed"
case Neq(lhs, rhs) => s"Inequality check of ${lhs.prettyprint} and ${rhs.prettyprint} failed"
case Match(t, pat) => s"Pattern match of ${t.prettyprint} to ${pat.prettyprint} failed"
case Undef(t) => s"Undef check of ${t.prettyprint} failed"
case Not(inst) => s"Negation of ${inst.prettyprint("")} failed"
case LatticeMemberCall(res) => s"Lattice member call ${res.prettyprint} failed"
}
def genNegation(inst: Instance): Instance = inst match {
case Eq(lhs, rhs) => Neq(lhs, rhs)
case Neq(lhs, rhs) => Eq(lhs, rhs)
case Not(inst) => inst
case _ => Not(inst)
}
def retainSliced(rule: Rule): Option[Rule] = {
if (reportStuck.contains(rule.conc.name)) {
val outputs = outputMetaterms(rule.conc)(this)
val prems = slice(rule.prems, outputs)(this)
Some(Rule(rule.name, prems, rule.conc))
}
else None
}
def retainNormal(rule: Rule): Option[Rule] = {
if (!reportStuck.contains(rule.conc.name)) Some(rule)
else None
}
}
package itypes.compiler
import itypes.Context
import itypes.lang.TypeLang._
import itypes.compiler.Util._
trait CtxFusionTrans extends Context {
def apply(spec: Spec): Spec = {
initJudgmentDeclarations(spec)
val mapOutputDecls = spec.judgs.filter { _.params.exists { p => p._2 == Out && p._1.isInstanceOf[MapSort]} }
val phiDecls = mapOutputDecls.map(deriveDecl)
val mapOutputRules = spec.rules.filter { rule =>
val concDecl = lookupJudgment(rule.conc.name)
mapOutputDecls.contains(concDecl)
}
val phiRules = mapOutputRules.flatMap(derivePhiRules)
val replacedRules = spec.rules.map(replace)
Spec(spec.name, phiDecls ++ spec.judgs, replacedRules ++ phiRules)
}
def deriveDecl(decl: JudgmentDeclaration): JudgmentDeclaration = {
val name = nameOfPhiDecl(decl)
val inputParams = decl.params.filter { _._2 == In }
val MapSort(keySort, valSort) = decl.params.find { _._2 == Out }.get._1
JudgmentDeclaration(name, "", inputParams ++ Seq((keySort, In, ""), (valSort, Out, "")), Map())
}
def nameOfPhiDecl(decl: JudgmentDeclaration): String = s"phi_${decl.name}"
def derivePhiRules(rule: Rule): Set[Rule] = {
var nextStep = Set(init(rule))
var finalRules = Set[Rule]()
while (nextStep.nonEmpty) {
val xxx = nextStep.flatMap(bound) ++ nextStep.flatMap(delegate)
nextStep = nextStep.flatMap(unfold)
finalRules ++= xxx
}
finalRules
}
def init(r: Rule): Rule = {
val decl = lookupJudgment(r.conc.name)
val inputArgs = selectAtIndices(r.conc.args, inputIndices(decl))
val outputArg = selectAtIndices(r.conc.args, outputIndices(decl)).head
val usedvars = metavars(r)(this)
val gensym = new Gensym(usedvars.map(_.name))
val keyMetaVar = MetaVar(gensym.fresh("key"))
val valMetaVar = MetaVar(gensym.fresh("val"))
val conc = JudgmentInstance(nameOfPhiDecl(decl), inputArgs ++ Seq(keyMetaVar, valMetaVar))
val prems = r.prems :+ Lookup(outputArg, keyMetaVar, valMetaVar)
Rule(nameOfPhiDecl(decl), prems, conc)
}
def unfold(rule: Rule): Option[Rule] = {
val outerBind = collectOuterBind(rule.prems)
outerBind.flatMap { bind =>
val key = rule.conc.args.reverse(1)
val prems = Seq(Neq(bind.args.head, key), Lookup(bind.args.last, key, rule.conc.args.last))
Some(Rule(rule.name + "_unfold", rule.prems.dropRight(1) ++ prems, rule.conc))
}
}
def bound(rule: Rule): Option[Rule] = {
val outerBind = collectOuterBind(rule.prems)
outerBind.flatMap { bind =>
val prems = Seq(Eq(bind.args.head, rule.conc.args.reverse(1)), Eq(bind.args(1), rule.conc.args.last))
Some(Rule(rule.name + "_bound", rule.prems.dropRight(1) ++ prems, rule.conc))
}
}
def collectOuterBind(prems: Seq[Instance]): Option[Node] = {
prems.flatMap { prem =>
val metas = metaterms(prem)
metas.filter {
case Node("Bind", _) => true
case _ => false
}
}
}.headOption.asInstanceOf[Option[Node]]
def delegate(rule: Rule): Option[Rule] = {
// the premises of the rule are n premises and the last premise is a lookup instance
// TODO implement more sophisticated check
// transformation is not applicable if the map passed to lookup is bind
rule.prems.last match {
case Lookup(Node("Bind", _), _, _) => return None
case _ => // do nothing
}
val lookup = rule.prems.last.asInstanceOf[Lookup]
val outputOfLookup = lookup.v
val keyOfLookup = lookup.k
val mapDeterminingPrem = determiningPrem(rule.prems, lookup.map)
mapDeterminingPrem.flatMap { prem =>
val phiInstance = phiForPi(prem, keyOfLookup, outputOfLookup)
val prems = rule.prems.dropRight(1) :+ phiInstance
Some(Rule(rule.name, prems, rule.conc))
}
}
def replace(rule: Rule): Rule = {
// replace lookups with appropriate phis
val newPrems = rule.prems.map {
case l@Lookup(map, key, value) =>
determiningPrem(rule.prems, map) match {
case Some(prem) => phiForPi(prem, key, value)
case None => l
}
case prem => prem
}
Rule(rule.name, newPrems, rule.conc)
}
def phiForPi(pi: JudgmentInstance, key: Metaterm, value: Metaterm): JudgmentInstance = {
val premDecl = lookupJudgment(pi.name)
val inputs = selectAtIndices(pi.args, inputIndices(premDecl))
JudgmentInstance(nameOfPhiDecl(premDecl), inputs ++ Seq(key, value))
}
// implement better tracking
def determiningPrem(prems: Seq[Instance], trg: Metaterm): Option[JudgmentInstance] = prems.collectFirst {
case ji@JudgmentInstance(n, _) =>
val decl = lookupJudgment(n)
val output = outputIndices(decl)
decl.params(output.head)._1 match {
case _: MapSort => ji
}
}
}
......@@ -5,7 +5,7 @@ import itypes.lang.TypeLang._
object Util {
def slice(ins: Seq[Instance], criteria: Seq[Metaterm])(implicit ctx: Context): Seq[Instance] = {
var seen = criteria.toSet
var seen = criteria.toSet ++ criteria.flatMap(metavars)
var collected = Seq[Instance]()
ins.reverse.foreach { i =>
val outputMetaVars = outputMetaterms(i).flatMap(metavars)
......
......@@ -6,10 +6,21 @@ case class ConstrSig(name: String, sort: Sort, params: Seq[Sort])
object TypeLang {
case class Spec(name: String, judgs: Seq[JudgmentDeclaration], rules: Seq[Rule])
case class Spec(name: String, judgs: Seq[JudgmentDeclaration], rules: Seq[Rule]) {
def prettyprint(): String = {
s"Specification $name\n${judgs.map(_.prettyprint(" ")).mkString("\n\n")}\n\n${rules.map(_.prettyprint(" ")).mkString("\n\n")}"
}
}
// TODO functional deps are currently implicit
case class JudgmentDeclaration(name: String, pre: String = "", params: Seq[(Sort, Mode, String)], coFuns: Map[Seq[Int], Int] = Map())
case class JudgmentDeclaration(name: String, pre: String = "", params: Seq[(Sort, Mode, String)], coFuns: Map[Seq[Int], Int] = Map()) {
def prettyprint(implicit indent: String): String = {
val stringParams = params.map { case (sort, mode, _) =>
s"${sort}: ${mode}"
}
s"$indent$name(${stringParams.mkString(", ")})"
}
}
sealed trait Sort
case object StringSort extends Sort
......@@ -25,34 +36,84 @@ object TypeLang {
case object In extends Mode
case object Out extends Mode
case class Rule(name: String, prems: Seq[Instance], conc: JudgmentInstance)
sealed trait Instance
case class JudgmentInstance(name: String, args: Seq[Metaterm]) extends Instance
case class Rule(name: String, prems: Seq[Instance], conc: JudgmentInstance) {
def prettyprint(implicit indent: String): String = {
s"${indent}rule $name\n${prems.map(_.prettyprint(indent + " ")).mkString("\n")}\n${indent}------------------------------------\n${conc.prettyprint(indent + " ")}"
}
}
sealed trait Instance {
def prettyprint(implicit indent: String): String
}
case class JudgmentInstance(name: String, args: Seq[Metaterm]) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"$indent$name(${args.map(_.prettyprint).mkString(", ")})"
}
}
// we have a special instance for lookup because we do not support type parameters for judgments (only for lookup)
case class Lookup(map: Metaterm, k: Metaterm, v: Metaterm) extends Instance
case class Eq(lhs: Metaterm, rhs: Metaterm) extends Instance
case class Neq(lhs: Metaterm, rhs: Metaterm) extends Instance
case class Match(t: Metaterm, pat: Metaterm) extends Instance
case class Undef(t: Metaterm) extends Instance
case class Not(inst: JudgmentInstance) extends Instance
case class LatticeMemberCall(res: Metaterm) extends Instance
sealed trait Metaterm
case class StringVal(s: String) extends Metaterm
case class MetaVar(name: String) extends Metaterm
case class Parent(t: Metaterm) extends Metaterm
case class Named(name: String, t: Metaterm) extends Metaterm
case class Node(name: String, args: Seq[Metaterm]) extends Metaterm
case object Wildcard extends Metaterm
case class Lookup(map: Metaterm, k: Metaterm, v: Metaterm) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"${indent}lookup(${Seq(map, k, v).map(_.prettyprint).mkString(", ")})"
}
}
case class Eq(lhs: Metaterm, rhs: Metaterm) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"$indent${lhs.prettyprint} == ${rhs.prettyprint}"
}
}
case class Neq(lhs: Metaterm, rhs: Metaterm) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"$indent${lhs.prettyprint} != ${rhs.prettyprint}"
}
}
case class Match(t: Metaterm, pat: Metaterm) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"$indent${t.prettyprint} match ${pat.prettyprint}"
}
}
case class Undef(t: Metaterm) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"${indent}undef ${t.prettyprint}"
}
}
case class Not(inst: Instance) extends Instance {
override def prettyprint(implicit indent: String): String = {
s"${indent}not ${inst.prettyprint}"
}
}
case class LatticeMemberCall(res: Metaterm) extends Instance {
override def prettyprint(implicit indent: String): String = throw new IllegalArgumentException("NOTSUPPORTED")
}
sealed trait Metaterm {
def prettyprint: String
}
case class StringVal(s: String) extends Metaterm {
override def prettyprint: String = "\"" + s +"\""
}
case class MetaVar(name: String) extends Metaterm {
override def prettyprint: String = name
}
case class Parent(t: Metaterm) extends Metaterm {
override def prettyprint: String = s"parent(${t.prettyprint})"
}
case class Named(name: String, t: Metaterm) extends Metaterm {
override def prettyprint: String = s"$name: ${t.prettyprint}"
}
case class Node(name: String, args: Seq[Metaterm]) extends Metaterm {
override def prettyprint: String = s"$name(${args.map(_.prettyprint).mkString(", ")})"
}
case object Wildcard extends Metaterm {
override def prettyprint: String = "_"
}
// TODO two options
sealed trait MapNode extends Metaterm
case object Empty extends MapNode
case class Bind(key: Metaterm, value: Metaterm, rest: MapNode) extends MapNode
// sealed trait MapNode extends Metaterm
// case object Empty extends MapNode
// case class Bind(key: Metaterm, value: Metaterm, rest: MapNode) extends MapNode
val empty: Node = Node("itypes.lang.TypeLang.Empty", Seq())
def bind(k: Metaterm, v: Metaterm, rest: Metaterm): Node = Node("itypes.lang.TypeLang.Bind", Seq(k, v, rest))
......
......@@ -2,49 +2,38 @@ package itypes.compiler
import itypes.lang.TypeLang._
import itypes.testspecs.CoFunTransSTLC
import itypes.testspecs.OriginalSTLC._
import itypes.testspecs.STLC._
import itypes.testspecs.STLCLanguageModel._
import itypes.util.TransformationTestUtil
import org.scalatest.funsuite.AnyFunSuite
class CoFunTransTest extends AnyFunSuite {
val ctxlessTypeOfDecl = JudgmentDeclaration("typeOf", "", Seq((termSort, In, ""), (typeSort, Out, "")), Map())
def selectRules(spec: Spec, name: String): Seq[Rule] = {
val trans = new CoFunTrans {}
val transformedSpec = trans.apply(spec)
transformedSpec.rules.filter(_.name == name)
}
def selectDeclaration(spec: Spec, name: String): JudgmentDeclaration = {
val trans = new CoFunTrans {}
val transformedSpec = trans.apply(spec)
transformedSpec.judgs.find(_.name == name).get
}
test("Judgment declaration does not change when no co-functional dependencies") {
assertResult(ctxlessTypeOfDecl)(new CoFunTrans{}.updateDecl(ctxlessTypeOfDecl))
val containsRules: (Spec, Seq[Rule]) => Boolean =
TransformationTestUtil.containsRules(new CoFunTrans {}.apply)
val containsDeclarations: (Spec, Seq[JudgmentDeclaration]) => Boolean =
TransformationTestUtil.containsDeclarations(new CoFunTrans {}.apply)
test("Judgment declaration does not change when no co-functional dependencies are declared") {
val ctxlessTypeOfDecl = JudgmentDeclaration("typeOf", "", Seq((termSort, In, ""), (typeSort, Out, "")), Map())
assert(containsDeclarations(Spec("Test", Seq(ctxlessTypeOfDecl), Seq()), Seq(ctxlessTypeOfDecl)))
}
test("Generate new judgment declarations for co-functional dependencies") {
assertResult(Seq(CoFunTransSTLC.piTypeOf))(new CoFunTrans{}.deriveDecl(typeOf))
assert(containsDeclarations(CoFunTransSTLC.spec, Seq(CoFunTransSTLC.piTypeOf)))
}
test("Alter judgment having co-functional dependency") {
assertResult(CoFunTransSTLC.typeOf)(new CoFunTrans{}.updateDecl(typeOf))
assert(containsDeclarations(CoFunTransSTLC.spec, Seq(CoFunTransSTLC.typeOf)))
}
test("Generate new rule for target of co-functional dependency") {
assertResult(Seq(CoFunTransSTLC.piTypeOfApp1, CoFunTransSTLC.piTypeOfApp2))(selectRules(spec, "pi_typeOf_0_T-App"))
assertResult(Seq(CoFunTransSTLC.piTypeOfLam))(selectRules(spec, "pi_typeOf_0_T-Lam"))
assert(containsRules(spec, Seq(CoFunTransSTLC.piTypeOfApp1, CoFunTransSTLC.piTypeOfApp2, CoFunTransSTLC.piTypeOfLam)))
}
test("Alter rules for target of co-functional dependency") {
assertResult(Seq(CoFunTransSTLC.tApp))(selectRules(spec, "T-App"))
assert(containsRules(spec, Seq(CoFunTransSTLC.tApp)))
assertResult(Seq(CoFunTransSTLC.tLam))(selectRules(spec, "T-Lam"))
assert(containsRules(spec, Seq(CoFunTransSTLC.tLam)))
}
}
package itypes.compiler
import itypes.lang.TypeLang._
import itypes.testspecs.{CoFunTransSTLC, CollectErrorsTransSTLC, CtxFusionTransSTLC, STLC}
import itypes.util.TransformationTestUtil
import org.scalatest.funsuite.AnyFunSuite
class CollectErrorsTransTest extends AnyFunSuite {
val containsRules: (Spec, Seq[Rule]) => Boolean =
TransformationTestUtil.containsRules(new CollectErrorsTrans {
override def reportStuck: Seq[String] = Seq("typeOf")
override def genPropagateRules: Boolean = true
} .apply)
val containsDeclarations: (Spec, Seq[JudgmentDeclaration]) => Boolean =
TransformationTestUtil.containsDeclarations(new CollectErrorsTrans {
override def reportStuck: Seq[String] = Seq("typeOf")
override def genPropagateRules: Boolean = true
} .apply)
test("Generate new judgment declarations for report stuck marked judgments") {
assert(containsDeclarations(CtxFusionTransSTLC.spec, Seq(CollectErrorsTransSTLC.epsilonTypeOf)))
}
test("Retain old judgment judgments") {
assert(containsDeclarations(CtxFusionTransSTLC.spec, Seq(CollectErrorsTransSTLC.typeOf, CollectErrorsTransSTLC.piTypeOf, CollectErrorsTransSTLC.phiTypeOf)))
}
test("Generate new error rules for rules that have reportstuck marked conclusion") {
assert(containsRules(CtxFusionTransSTLC.spec, Seq(
CollectErrorsTransSTLC.epsilonApp1,
CollectErrorsTransSTLC.epsilonApp2,
CollectErrorsTransSTLC.epsilonApp3,
CollectErrorsTransSTLC.epsilonLam,
CollectErrorsTransSTLC.epsilonVar)))
}
test("Generate error propagation rules for rules that have reportstuck marked conclusion") {
assert(containsRules(CtxFusionTransSTLC.spec, Seq(
CollectErrorsTransSTLC.epsilonLamPropagate,
CollectErrorsTransSTLC.epsilonAppPropagate1,
CollectErrorsTransSTLC.epsilonAppPropagate2)))
}
test("Update old rules that have reportstuck marked conclusion") {
assert(containsRules(CtxFusionTransSTLC.spec, Seq(
CollectErrorsTransSTLC.tApp,
CollectErrorsTransSTLC.tLam,
CollectErrorsTransSTLC.tVar)))
}
}
package itypes.compiler
import itypes.lang.TypeLang._
import itypes.testspecs.CoFunTransSTLC._
import itypes.testspecs.CtxFusionTransSTLC
import itypes.util.TransformationTestUtil
import org.scalatest.funsuite.AnyFunSuite
class CtxFusionTransTest extends AnyFunSuite {
val containsRules: (Spec, Seq[Rule]) => Boolean =
TransformationTestUtil.containsRules(new CtxFusionTrans {}.apply)
val containsDeclarations: (Spec, Seq[JudgmentDeclaration]) => Boolean =
TransformationTestUtil.containsDeclarations(new CtxFusionTrans {}.apply)
test("Generate new judgment declaration for map producing judgments") {
assert(containsDeclarations(spec, Seq(CtxFusionTransSTLC.phiTypeOf)))
}
test("Generate new rules for phi judgment") {
assert(containsRules(spec, Seq(CtxFusionTransSTLC.phiApp1, CtxFusionTransSTLC.phiApp2, CtxFusionTransSTLC.phiLamNext, CtxFusionTransSTLC.phiLamBound)))
}
test("replace lookup with phi") {
assert(containsRules(spec, Seq(CtxFusionTransSTLC.tVar)))
}
}
package itypes.compiler
import itypes.lang.TypeLang._
import itypes.testspecs.OriginalSTLC._
import itypes.testspecs.STLC._
import itypes.testspecs.STLCLanguageModel._
import org.scalatest.funsuite.AnyFunSuite
......
package itypes.testspecs
import itypes.lang.TypeLang._