Skip to content

Commit

Permalink
Resolve some type errors
Browse files Browse the repository at this point in the history
  • Loading branch information
bobismijnnaam committed Jun 21, 2023
1 parent b6b69b4 commit deee303
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 2 deletions.
2 changes: 1 addition & 1 deletion src/col/vct/col/ast/Node.scala
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ final case class Branch[G](branches: Seq[(Expr[G], Statement[G])])(implicit val
final case class IndetBranch[G](branches: Seq[Statement[G]])(implicit val o: Origin) extends CompositeStatement[G] with IndetBranchImpl[G]
final case class Switch[G](expr: Expr[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with SwitchImpl[G]
final case class Loop[G](init: Statement[G], cond: Expr[G], update: Statement[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with LoopImpl[G]
final case class RangedFor[G](binder: Variable[G], from: Expr[G], to: Expr[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with LoopImpl[G]
final case class RangedFor[G](binder: Variable[G], from: Expr[G], to: Expr[G], contract: LoopContract[G], body: Statement[G])(implicit val o: Origin) extends CompositeStatement[G]
final case class TryCatchFinally[G](body: Statement[G], after: Statement[G], catches: Seq[CatchClause[G]])(implicit val o: Origin) extends CompositeStatement[G] with TryCatchFinallyImpl[G]
final case class Synchronized[G](obj: Expr[G], body: Statement[G])(val blame: Blame[LockRegionFailure])(implicit val o: Origin) extends CompositeStatement[G] with SynchronizedImpl[G]
final case class ParInvariant[G](decl: ParInvariantDecl[G], inv: Expr[G], content: Statement[G])(val blame: Blame[ParInvariantNotEstablished])(implicit val o: Origin) extends CompositeStatement[G] with ParInvariantImpl[G]
Expand Down
2 changes: 1 addition & 1 deletion src/parsers/vct/parsers/transform/PVLToCol.scala
Original file line number Diff line number Diff line change
Expand Up @@ -348,7 +348,7 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val
case PvlRangedFor(contract, _, _, Iter0(t, name, _, from, _, to), _, body) =>
withContract(contract, contract =>
Scope(Nil, RangedFor(
LocalDecl(new Variable(convert(t))(origin(name)))(origin(name)),
new Variable(convert(t))(origin(name)),
convert(from), convert(to),
contract.consumeLoopContract(stat),
convert(body))))
Expand Down
16 changes: 16 additions & 0 deletions src/rewrite/vct/rewrite/EncodeRangedFor.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
package vct.col.rewrite

import vct.col.ast.{Statement, RangedFor}
import vct.col.util.AstBuildHelpers.const

case object EncodeRangedFor extends RewriterBuilder {
override def key: String = "encodeRangedFor"
override def desc: String = "Encodes ranged for as a regular for loop"
}

case class EncodeRangedFor[Pre <: Generation]() extends Rewriter[Pre] {
override def dispatch(stat: Statement[Pre]): Statement[Post] = stat match {
// case RangedFor(v, from, to, contract, body) => ???
case stat => rewriteDefault(stat)
}
}

0 comments on commit deee303

Please sign in to comment.