Skip to content

Commit

Permalink
Show crazy compile error
Browse files Browse the repository at this point in the history 
Scalac does not inline type aliases enough before type inference:

[error] /Users/pgiarrusso/Documents/Research/Sorgenti/ilc-scala-sbt/src/main/scala/ilc/feature/let/ANormalForm.scala:383: type mismatch;
[error]  found   : PartialFunction[AddCaches2.this.mySyntax.Term,AddCaches2.this.mySyntax.Term]
[error]  required: AddCaches2.this.mySyntax.=?>:[T,AddCaches2.this.mySyntax.Term]
[error]     (which expands to)  PartialFunction[T,AddCaches2.this.mySyntax.Term]
[error]     or(descendAbsRule orElse descendLetRule(intermediateResults))(descendAtom(intermediateResults))
[error]                       ^

As mentioned in src/main/scala/ilc/feature/let/Traversals.scala, you can
work this around by inlining the type alias: this will make everything
compile.

Warning: If after that you undo the change, everything will still
compile (under SBT, and sometimes in Eclipse) because SBT's compilation
manager, when computing the interface of a file, *does* inline type
aliases correctly.
  • Loading branch information
@Blaisorblade
Blaisorblade committed Jul 6, 2014
1 parent bf18349 commit bea1580
Show file tree
Hide file tree
Showing 5 changed files with 271 additions and 273 deletions.
2 changes: 1 addition & 1 deletion src/main/scala/ilc/TypeChecking.scala
View file
Expand Up @@ -5,5 +5,5 @@ object TypeChecking extends utils.BooleanFlag {
* Define this to false to disable some internal typechecking checks, which might be useful
* for chaotic prototyping.
*/
val value = true
val value = false
}
147 changes: 135 additions & 12 deletions src/main/scala/ilc/feature/let/ANormalForm.scala
View file
Expand Up @@ -287,18 +287,8 @@ trait AddCaches extends ANormalFormStateful {
//normalT,
Nil)
}

def transformVar(varName: Name, fstT: Type): Var =
Var(transformName{ name =>
if (name endsWith "Tot") {
//XXX AAARGH
name
//new Exception().printStackTrace()
} else {
name + "Tot"
}
}(varName), fstT)
def transformVar(v: Var): Var = transformVar(v.getName, v.getType)
def transformVar(v: Var): Var = ???
def transformVar(varName: Name, fstT: Type): Var = ???

//XXX: what about primitives? In the paper, you can distinguish them
//statically, here you typically can't.
Expand All @@ -315,3 +305,136 @@ trait AddCaches extends ANormalFormStateful {
Let(variable, project(1) ! varTot, body))
}
}

trait AddCaches2 {
outer =>

val mySyntax: Syntax with IsAtomic with products.SyntaxSugar with unit.Syntax with Traversals
val aNormalizer = new ANormalFormStateful {
lazy val mySyntax: outer.mySyntax.type = outer.mySyntax
override val partialApplicationsAreSpecial = false
}
protected val freshGen = new FreshGen {
//This must be lazy because at this time mySyntax is not initialized yet.
lazy val syntax: mySyntax.type = mySyntax
}
import mySyntax._
import aNormalizer._
import freshGen._

def addCaches: Term => Term =
etaExpandPrimitives andThen aNormalizeTerm andThen extendReturns

def etaExpandPrimitives: Term => Term = everywhere { orIdentity {
case v: Var => v
case primitive if isAtomic(primitive) =>
@annotation.tailrec def getArgsRev(typ: Type, acc: List[Type] = Nil): List[Type] = typ match {
case s =>: t =>
getArgsRev(t, s :: acc)
case _ => acc
}
val vars = getArgsRev(primitive.getType).reverse map (fresh("eta", _))
vars.foldRight(vars.foldLeft(primitive)(App))(Abs)
}}

//This needs to be invoked for each abs node, to reset the list of intermediate results for that scope.
//That's similar to A-normalization.
def extendReturns: Term => Term = descendAbsLetAtom(Nil)

/* We implement an abstract machine traversing a structure specified by this grammar
* (courtesy of A-normalization):
*
* exp ::= atom | let var = appOrAbs in exp | abs
* app ::= atom atom
* app ::= app atom [if partialApplicationsAreSpecial]
* abs ::= lambda name . exp
* appOrAbs ::= app | abs
* atom ::= name | primitive
*
* Thanks to etaExpandPrimitives, primitives are fully eta-expanded, so non-nullary ones can only appear inside lambdas.
* This means that the operator of an application can't be a primitive - except in those eta-expansion.
* Instead of
* app ::= atom atom
* we have
* app ::= name atom
*/

//XXX also prove that the resulting term is (at least dynamically) type-safe.
//We should even manage to get static type-safety still easily.
//The complicated thing to type is that a function and its derivative share
//the type of "cache", but this is not yet visible here, and that's only needed
//when we want to pack different functions together...
//NO: consider f g, f h, where g and h are different functions with the same
//type. They'll get different types now! But this requires only let-polymorphism.

//Resulting term produces a tuple.
//Proof: by invariant on descendAbsLetAtom
def descendExp = descendAbsLetAtom(Nil)
//Resulting term produces a tuple.
//Proof: by inspection of tupleVars.
def descendAtom(intermediateResults: List[Var]) = { (t: Term) =>
assert(isAtomic(t))
tupleVars(intermediateResults)(t)
}

//Resulting term produces a tuple.
//Proof: by invariant on descendAbsRule and descendLetRule and descendAtom
def descendAbsLetAtom(intermediateResults: List[Var]): Term => Term =
or(descendAbsRule orElse descendLetRule(intermediateResults))(descendAtom(intermediateResults))

//Resulting term produces a tuple.
//Proof: by induction & invariant on descendExp
def descendAbsRule: Term =?>: Term = {
case Abs(v, body) =>
Abs(v, descendExp(body))
}

def transformVar(varName: Name, fstT: Type): Var =
Var(transformName{ name =>
if (name endsWith "Tot") {
//XXX AAARGH
throw new Exception()//.printStackTrace()
//name
} else {
name + "Tot"
}
}(varName), fstT)
def transformVar(v: Var): Var = transformVar(v.getName, v.getType)

//Resulting term produces a tuple.
//Proof: by induction on descendAbsLetAtom, which is always called through
//transformedBody.
def descendLetRule(intermediateResults: List[Var]): Term =?>: Term = {
case Let(v, exp, body) =>
def transformedBody(newVar: Var) = descendAbsLetAtom(newVar :: intermediateResults)(body)
exp match {
case App(fun: Var, arg) if isAtomic(arg) =>
case class UnknownType() extends Type
val varTot = fresh(transformVar(v.getName, ProductType(v.getType, UnknownType())))
//Is this application still type-safe?
//fun's return is correctly tupled, and its argument is not tupled
//because it's bound by the output of descendLetRule
Let(varTot, App(fun, arg),
Let(v, Proj1 ! varTot, transformedBody(varTot)))

case _: App => exp
case _: Abs =>
Let(v, descendAbsRule(exp), transformedBody(v))
}
}

def tupleVars(intermediateResults: List[Var]): Term =?>: Term = {
case t =>
//XXX: Liu does use unary tuples instead! Hmm... well, in fact using unit is an encoding of them
//with nested pairs... right? No, with nested pairs the base case is the pair of the last two vars.
//That's one reason why project has to be so complicated...
val rest =
if (intermediateResults.isEmpty)
UnitTerm :: Nil
else
intermediateResults
(t :: intermediateResults foldLeft (tuple(intermediateResults.length + 1))) {
_ ! _
}
}
}
89 changes: 34 additions & 55 deletions src/main/scala/ilc/feature/let/ANormalFormTest.sc
View file
Expand Up @@ -18,7 +18,7 @@ object ANormalFormTest {
//| with ilc.feature.let.BetaReduction with ilc.feature.let.Pretty with ilc.feat
//| ure.inference.LetSyntaxSugar{val aNormalizer: ilc.feature.let.ANormalFormSta
//| teful{val mySyntax: ilc.feature.let.ANormalFormTest.<refinement>.type}} = il
//| c.feature.let.ANormalFormTest$$anonfun$main$1$$anon$1@746ab811
//| c.feature.let.ANormalFormTest$$anonfun$main$1$$anon$1@7b1c661c
//Both work, but the output is different.

//def tests(v: Bacchus with feature.let.ANormalFormStateful with integers.ImplicitSyntaxSugar with inference.LetInference
Expand Down Expand Up @@ -51,8 +51,10 @@ object ANormalFormTest {
x))
*/
val test2 =
let('x, let('y, 20: Term)('y))('x) //> test2 : ilc.feature.let.ANormalFormTest.v.UntypedTerm = ULet(x,ULet(y,UMon
//| omorphicConstant(LiteralInt(20)),UVar(y)),UVar(x))
let('x, let('y, (PlusInt ! (20: Term) ! (30: Term)): Term)('y))('x)
//> test2 : ilc.feature.let.ANormalFormTest.v.UntypedTerm = ULet(x,ULet(y,UMon
//| omorphicConstant(App(App(PlusInt,LiteralInt(20)),LiteralInt(30))),UVar(y)),
//| UVar(x))
/*
(define t3
'(let ([x (if #t 1 2)])
Expand Down Expand Up @@ -120,65 +122,42 @@ object ANormalFormTest {
//| x;
//| a_1;
//| a_2 =
//| id_i
//| id_i2lit
//| LiteralInt(3);
//| a_3 =
//| id
//| apply
//| id_i
//| a_2;
//| a_3"
"\n" + pretty(normalize(aNormalizeTerm(test1))) //> res2: String = "
//| LiteralInt(3)"
"\n" + pretty(aNormalizeTerm(normalize(test1))) //> res3: String = "
//| LiteralInt(3)"
"\n" + pretty(test2) //> res4: String = "
//| x =
//| y =
//| LiteralInt(20);
//| y;
//| x"
"\n" + pretty(aNormalizeTerm(test2)) //> res5: String = "
//| LiteralInt(20)"
"\n" + pretty(normalize(aNormalizeTerm(test2))) //> res6: String = "
//| LiteralInt(20)"
"\n" + pretty(aNormalizeTerm(normalize(test2))) //> res7: String = "
//| LiteralInt(20)"
"\n" + pretty(test3) //> res8: String = "
//| x =
//| IfThenElse(ℤ)
//| True
//| (λunit.
//| LiteralInt(1))
//| (λunit.
//| LiteralInt(2));
//| x"
"\n" + pretty(aNormalizeTerm(test3)) //> res9: String = "
//| a_7 =
//| λunit.
//| LiteralInt(1);
//| a_8 =
//| λunit.
//| LiteralInt(2);
//| a_9 =
//| IfThenElse(ℤ)
//| True
//| a_7
//| a_8;
//| a_9"
"\n" + pretty(aNormalizeTerm(normalize(test3))) //> res10: String = "
//| a_10 =
//| λunit_1.
//| LiteralInt(1);
//| a_11 =
//| λunit_2.
//| LiteralInt(2);
//| a_12 =
//| IfThenElse(ℤ)
//| True
//| a_10
//| a_11;
//| a_12"
"\n" + pretty(normalize(aNormalizeTerm(test1))) //> ilc.feature.base.TypeError: Type error: Variable id_i2lit not available in
//| context Map(id -> FunVal(<function1>,Var(x,(ℤ → ℤ) → ℤ → ℤ),t
//| rue), id_i -> FunVal(<function1>,Var(x,ℤ),true), apply -> FunVal(<functio
//| n1>,Var(f,ℤ → ℤ),false)), ill-scoped term
//| at ilc.feature.let.BetaReduction$Normalize$.eval(BetaReduction.scala:196
//| )
//| at ilc.feature.let.BetaReduction$Normalize$.eval(BetaReduction.scala:192
//| )
//| at ilc.feature.let.BetaReduction$Normalize$.eval(BetaReduction.scala:168
//| )
//| at ilc.feature.let.BetaReduction$Normalize$$anonfun$eval$1.apply(BetaRed
//| uction.scala:166)
//| at ilc.feature.let.BetaReduction$Normalize$$anonfun$eval$1.apply(BetaRed
//| uction.scala:166)
//| at ilc.feature.let.BetaReduction$Normalize$.ilc$feature$let$BetaReductio
//| n$Normalize$$findFun$1(BetaReduction.scala:176)
//| at ilc.feature.let.BetaReduction$Normalize$.eval(BetaReduction.scala:192
//| )
//| at ilc.feature.let.BetaReduction$Normali
//| Output exceeds cutoff limit.
"\n" + pretty(aNormalizeTerm(normalize(test1)))
"\n" + pretty(test2)
"\n" + pretty(aNormalizeTerm(test2))
"\n" + pretty(normalize(aNormalizeTerm(test2)))
"\n" + pretty(aNormalizeTerm(normalize(test2)))
"\n" + pretty(test3)
"\n" + pretty(aNormalizeTerm(test3))
"\n" + pretty(aNormalizeTerm(normalize(test3)))
//"\n" + pretty(addCaches(test3))
//"\n" + pretty(addCaches(test1))
//}
Expand Down

0 comments on commit bea1580

Please sign in to comment.