Skip to content

Commit

Permalink
Fix issue in VC generation where refinement types were ignored (thanks
Browse files Browse the repository at this point in the history
  • Loading branch information
jad-hamza committed Feb 24, 2021
1 parent 58b58d7 commit dd0a383
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 26 deletions.
8 changes: 6 additions & 2 deletions core/src/main/scala/stainless/verification/TypeChecker.scala
Original file line number Diff line number Diff line change
Expand Up @@ -944,12 +944,15 @@ trait TypeChecker {

def vcFromContext(l: Seq[Variable], e: Expr): Expr = {
l.foldRight(e) { case (v, acc) =>
v match {
v.tpe match {
case LetEquality(e1: Variable, e2) =>
let(e1.toVal, e2, acc)
case Truth(t) =>
implies(t, acc)
case _ => acc
case RefinementType(vd, pred) =>
implies(renameVar(pred, vd.id, v.id), acc)
case _ =>
acc
}
}
}
Expand All @@ -958,6 +961,7 @@ trait TypeChecker {
v.tpe match {
case LetEquality(_, _) => true
case Truth(_) => true
case RefinementType(_, _) => true
case _ => false
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ object TypeCheckerContext {
def freshBindWithValue(vd: ValDef, e: Expr)(implicit opts: PrinterOptions, ctx: inox.Context): (TypingContext, Identifier) = {
val freshVd = vd.freshen
(
copy(termVariables = termVariables :+ freshVd.toVariable :+ Variable.fresh(letWitness, Equality(freshVd.toVariable,e))).setPos(this),
copy(termVariables = termVariables :+ freshVd.toVariable :+ Variable.fresh(letWitness, LetEquality(freshVd.toVariable,e))).setPos(this),
freshVd.id
)
}
Expand Down
25 changes: 2 additions & 23 deletions core/src/main/scala/stainless/verification/TypeCheckerUtils.scala
Original file line number Diff line number Diff line change
Expand Up @@ -53,23 +53,7 @@ object TypeCheckerUtils {
case _ => None
}

def unapply(v: Variable): Option[Expr] = v.tpe match {
case RefinementType(vd, e) if vd.tpe == UnitType() => Some(e)
case _ => None
}
}

// The type { u: Unit | e1 == e2 }
object Equality {
def apply(e1: Expr, e2: Expr) = {
val vd = ValDef.fresh("__u", UnitType())
RefinementType(vd, Equals(e1,e2))
}

def unapply(t: Type): Option[(Expr, Expr)] = t match {
case RefinementType(vd, Equals(e1,e2)) if vd.tpe == UnitType() => Some((e1,e2))
case _ => None
}
def unapply(v: Variable): Option[Expr] = unapply(v.tpe)
}

// The type { letWitness: Unit | e1 == e2 }
Expand All @@ -84,12 +68,7 @@ object TypeCheckerUtils {
case _ => None
}

def unapply(v: Variable): Option[(Variable, Expr)] = {
v.tpe match {
case RefinementType(vd, Equals(e1: Variable,e2)) if vd.tpe == UnitType() && v.id.name == letWitness => Some((e1, e2))
case _ => None
}
}
def unapply(v: Variable): Option[(Variable, Expr)] = unapply(v.tpe)
}

def renameVar(e: Expr, id1: Identifier, id2: Identifier): Expr = {
Expand Down

0 comments on commit dd0a383

Please sign in to comment.