From deee303bec23d775d8d0f40a86241a2eb46f1f1a Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Wed, 21 Jun 2023 17:13:35 +0200 Subject: [PATCH] Resolve some type errors --- src/col/vct/col/ast/Node.scala | 2 +- src/parsers/vct/parsers/transform/PVLToCol.scala | 2 +- src/rewrite/vct/rewrite/EncodeRangedFor.scala | 16 ++++++++++++++++ 3 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 src/rewrite/vct/rewrite/EncodeRangedFor.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 912f534c39..73fcefc29b 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -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] diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index b5e09a46e8..6a4a0fa754 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -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)))) diff --git a/src/rewrite/vct/rewrite/EncodeRangedFor.scala b/src/rewrite/vct/rewrite/EncodeRangedFor.scala new file mode 100644 index 0000000000..ff1725cd5c --- /dev/null +++ b/src/rewrite/vct/rewrite/EncodeRangedFor.scala @@ -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) + } +}