Skip to content
Snippets Groups Projects
Commit 119a8648 authored by Régis Blanc's avatar Régis Blanc
Browse files

I am thinking we should lift the precondition of enclosing function as well..

parent ad5b8539
No related branches found
No related tags found
No related merge requests found
......@@ -84,12 +84,21 @@ object ImperativeCodeElimination extends Pass {
val whileFunBaseCase = (if(whileFunVars.size == 1) whileFunVars.head.toVariable else Tuple(whileFunVars.map(_.toVariable))).setType(whileFunReturnType)
val whileFunBody = IfExpr(whileFunCond, whileFunRecursiveCall, whileFunBaseCase).setType(whileFunReturnType)
whileFunDef.body = Some(whileFunBody)
val trivialPostcondition: Option[Expr] = Some(Not(replace(whileFunVars.map(id => (id.toVariable, ResultVariable())).toMap, whileFunCond)))
val resVar = ResultVariable().setType(whileFunReturnType)
val whileFunVars2ResultVars: Map[Expr, Expr] =
if(whileFunVars.size == 1)
Map(whileFunVars.head.toVariable -> resVar)
else
whileFunVars.zipWithIndex.map{ case (v, i) => (v.toVariable, TupleSelect(resVar, i+1).setType(v.getType)) }.toMap
val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(v => (v.toVariable, modifiedVars2WhileFunVars(v.toVariable))).toMap
val trivialPostcondition: Option[Expr] = Some(Not(replace(whileFunVars2ResultVars, whileFunCond)))
val invariantPrecondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2WhileFunVars, expr))
whileFunDef.precondition = invariantPrecondition
whileFunDef.postcondition = trivialPostcondition.map(expr =>
And(expr, invariantPrecondition match {
case Some(e) => replace(whileFunVars.map(id => (id.toVariable, ResultVariable())).toMap, e)
case Some(e) => replace(modifiedVars2ResultVars, e)
case None => BooleanLiteral(true)
}))
......
......@@ -55,14 +55,12 @@ object UnitElimination extends Pass {
Tuple(newArgs.map(removeUnit)).setType(TupleType(newTpes))
}
case ts@TupleSelect(t, index) => {
println("Select Tuple: " + ts)
val TupleType(tpes) = t.getType
val selectionType = tpes(index-1)
val (_, newIndex) = tpes.zipWithIndex.foldLeft((0,-1)){
case ((nbUnit, newIndex), (tpe, i)) =>
if(i == index-1) (nbUnit, index - nbUnit) else (if(tpe == UnitType) nbUnit + 1 else nbUnit, newIndex)
}
println("new index = " + newIndex)
TupleSelect(removeUnit(t), newIndex).setType(selectionType)
}
case Let(id, e, b) => {
......
......@@ -27,6 +27,7 @@ object Trees {
def getInvariant: Expr = invariant.get
def setInvariant(inv: Expr): Expr = { invariant = Some(inv); this }
def setInvariant(inv: Option[Expr]): Expr = { invariant = inv; this }
}
......@@ -429,7 +430,7 @@ object Trees {
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
case Concat(t1,t2) => Some((t1,t2,Concat))
case ListAt(t1,t2) => Some((t1,t2,ListAt))
case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.getInvariant)))
case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant)))
case _ => None
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment