First try at adding vectors

res/universal/res/adt/vector.pvl

@@ -0,0 +1,8 @@
+adt `vector`<T> {
+  pure T vector_loc(`vector`<T> v, int i);
+}
+
+    decreases;
+    requires 0 <= i;
+    requires i < 4;
+pure T v4loc<T>(`vector`<T> a, int i) = `vector`<T>.vector_loc(a, i);

src/col/vct/col/ast/Node.scala

@@ -129,6 +129,7 @@ final case class TOption[G](element: Type[G])(implicit val o: Origin = Diagnosti
 final case class TTuple[G](elements: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TTupleImpl[G]
 final case class TEither[G](left: Type[G], right: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TEitherImpl[G]
 final case class TMatrix[G](element: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TMatrixImpl[G]
+final case class TVector[G](element: Type[G], size: BigInt)(implicit val o: Origin = DiagnosticOrigin) extends CompositeType[G] with TVectorImpl[G]
 
 sealed trait PrimitiveType[G] extends Type[G] with PrimitiveTypeImpl[G]
 final case class TAny[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TAnyImpl[G]
@@ -417,6 +418,7 @@ final case class CoerceMapTuple[G](inner: Seq[Coercion[G]], sourceTypes: Seq[Typ
 final case class CoerceMapEither[G](inner: (Coercion[G], Coercion[G]), sourceTypes: (Type[G], Type[G]), targetTypes: (Type[G], Type[G]))(implicit val o: Origin) extends Coercion[G] with CoerceMapEitherImpl[G]
 final case class CoerceMapSeq[G](inner: Coercion[G], sourceSeqElement: Type[G], targetSeqElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapSeqImpl[G]
 final case class CoerceMapSet[G](inner: Coercion[G], sourceSetElement: Type[G], targetSetElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapSetImpl[G]
+final case class CoerceMapVector[G](inner: Coercion[G], sourceVectorElement: Type[G], targetVectorElement: Type[G], size: BigInt)(implicit val o: Origin) extends Coercion[G] with CoerceMapVectorImpl[G]
 final case class CoerceMapBag[G](inner: Coercion[G], sourceBagElement: Type[G], targetBagElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapBagImpl[G]
 final case class CoerceMapMatrix[G](inner: Coercion[G], sourceMatrixElement: Type[G], targetMatrixElement: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceMapMatrixImpl[G]
 final case class CoerceMapMap[G](inner: Coercion[G], sourceTypes: (Type[G], Type[G]), targetTypes: (Type[G], Type[G]))(implicit val o: Origin) extends Coercion[G] with CoerceMapMapImpl[G]
@@ -440,6 +442,7 @@ final case class LiteralSet[G](element: Type[G], values: Seq[Expr[G]])(implicit
 final case class LiteralBag[G](element: Type[G], values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with LiteralBagImpl[G]
 final case class LiteralTuple[G](ts: Seq[Type[G]], values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with LiteralTupleImpl[G]
 final case class LiteralMap[G](k: Type[G], v: Type[G], values: Seq[(Expr[G], Expr[G])])(implicit val o: Origin) extends Expr[G] with LiteralMapImpl[G]
+final case class LiteralVector[G](element: Type[G], values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with LiteralVectorImpl[G]
 final case class UntypedLiteralSeq[G](values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with UntypedLiteralSeqImpl[G]
 final case class UntypedLiteralSet[G](values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with UntypedLiteralSetImpl[G]
 final case class UntypedLiteralBag[G](values: Seq[Expr[G]])(implicit val o: Origin) extends Expr[G] with UntypedLiteralBagImpl[G]
@@ -646,6 +649,7 @@ final case class FreePointer[G](pointer: Expr[G])(val blame: Blame[PointerFreeEr
 final case class Old[G](expr: Expr[G], at: Option[Ref[G, LabelDecl[G]]])(val blame: Blame[LabelNotReached])(implicit val o: Origin) extends Expr[G] with OldImpl[G]
 final case class AmbiguousSubscript[G](collection: Expr[G], index: Expr[G])(val blame: Blame[FrontendSubscriptError])(implicit val o: Origin) extends Expr[G] with AmbiguousSubscriptImpl[G]
 final case class SeqSubscript[G](seq: Expr[G], index: Expr[G])(val blame: Blame[SeqBoundFailure])(implicit val o: Origin) extends Expr[G] with SeqSubscriptImpl[G]
+final case class VectorSubscript[G](seq: Expr[G], index: Expr[G])(val blame: Blame[VectorBoundFailure])(implicit val o: Origin) extends Expr[G] with VectorSubscriptImpl[G]
 final case class ArraySubscript[G](arr: Expr[G], index: Expr[G])(val blame: Blame[ArraySubscriptError])(implicit val o: Origin) extends Expr[G] with ArraySubscriptImpl[G]
 final case class PointerSubscript[G](pointer: Expr[G], index: Expr[G])(val blame: Blame[PointerSubscriptError])(implicit val o: Origin) extends Expr[G] with PointerSubscriptImpl[G]
 final case class Length[G](arr: Expr[G])(val blame: Blame[ArrayNull])(implicit val o: Origin) extends Expr[G] with LengthImpl[G]

src/col/vct/col/ast/expr/ambiguous/AmbiguousSubscriptImpl.scala

@@ -8,6 +8,7 @@ import vct.col.ast.ops.AmbiguousSubscriptOps
 
 trait AmbiguousSubscriptImpl[G] extends AmbiguousSubscriptOps[G] { this: AmbiguousSubscript[G] =>
   def isSeqOp: Boolean = CoercionUtils.getAnySeqCoercion(collection.t).isDefined
+  def isVectorOp: Boolean = CoercionUtils.getAnyVectorCoercion(collection.t).isDefined
   def isArrayOp: Boolean = CoercionUtils.getAnyArrayCoercion(collection.t).isDefined
   def isCArrayOp: Boolean = CoercionUtils.getAnyCArrayCoercion(collection.t).isDefined
   def isCPPArrayOp: Boolean = CoercionUtils.getAnyCPPArrayCoercion(collection.t).isDefined
@@ -16,6 +17,7 @@ trait AmbiguousSubscriptImpl[G] extends AmbiguousSubscriptOps[G] { this: Ambiguo
 
   override lazy val t: Type[G] =
     if (isSeqOp) collection.t.asSeq.get.element
+    else if (isVectorOp) collection.t.asVector.get.element
     else if (isArrayOp) collection.t.asArray.get.element
     else if (isCArrayOp) collection.t.asCArray.get.innerType
     else if (isCPPArrayOp) collection.t.asCPPArray.get.innerType

src/col/vct/col/ast/expr/literal/build/LiteralVectorImpl.scala

@@ -0,0 +1,13 @@
+package vct.col.ast.expr.literal.build
+
+import vct.col.ast.{LiteralVector, TVector, Type}
+import vct.col.print.{Ctx, Doc, Group, Precedence, Text}
+import vct.col.ast.ops.LiteralVectorOps
+
+trait LiteralVectorImpl[G] extends LiteralVectorOps[G] { this: LiteralVector[G] =>
+  override def t: Type[G] = TVector(element, values.size)
+
+  override def precedence: Int = Precedence.POSTFIX
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(Text("vector<") <> element <> "," <> values.size.toString <> ">{" <> Doc.args(values) <> "}")
+}

src/col/vct/col/ast/expr/op/collection/VectorSubscriptImpl.scala

@@ -0,0 +1,12 @@
+package vct.col.ast.expr.op.collection
+
+import vct.col.ast.{VectorSubscript, Type}
+import vct.col.print.{Ctx, Doc, Precedence, Group}
+import vct.col.ast.ops.VectorSubscriptOps
+
+trait VectorSubscriptImpl[G] extends VectorSubscriptOps[G] { this: VectorSubscript[G] =>
+  override def t: Type[G] = seq.t.asVector.get.element
+
+  override def precedence: Int = Precedence.POSTFIX
+  override def layout(implicit ctx: Ctx): Doc = Group(assoc(seq) <> "[" <> Doc.arg(index) <> "]")
+}

src/col/vct/col/ast/family/coercion/CoerceMapVectorImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.{CoerceMapVector, TVector}
+import vct.col.ast.ops.CoerceMapVectorOps
+
+trait CoerceMapVectorImpl[G] extends CoerceMapVectorOps[G] { this: CoerceMapVector[G] =>
+  override def target: TVector[G] = TVector(targetVectorElement, size)
+}

src/col/vct/col/ast/type/TSetImpl.scala

@@ -6,5 +6,5 @@ import vct.col.ast.ops.TSetOps
 
 trait TSetImpl[G] extends TSetOps[G] { this: TSet[G] =>
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("seq") <> open <> Doc.arg(element) <> close)
+    Group(Text("set") <> open <> Doc.arg(element) <> close)
 }

src/col/vct/col/ast/type/TVectorImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TVector
+import vct.col.ast.ops.TVectorOps
+import vct.col.print.{Ctx, Doc, Group, Text}
+
+trait TVectorImpl[G] extends TVectorOps[G] { this: TVector[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Group(Text("vector") <> open <> Doc.arg(element) <> "," <> size.toString <> close)
+}

src/col/vct/col/ast/type/typeclass/TypeImpl.scala

@@ -16,6 +16,7 @@ trait TypeImpl[G] extends TypeFamilyOps[G] { this: Type[G] =>
 
   def asSeq: Option[TSeq[G]] = CoercionUtils.getAnySeqCoercion(this).map(_._2)
   def asSet: Option[TSet[G]] = CoercionUtils.getAnySetCoercion(this).map(_._2)
+  def asVector: Option[TVector[G]] = CoercionUtils.getAnyVectorCoercion(this).map(_._2)
   def asBag: Option[TBag[G]] = CoercionUtils.getAnyBagCoercion(this).map(_._2)
   def asPointer: Option[TPointer[G]] = CoercionUtils.getAnyPointerCoercion(this).map(_._2)
   def asArray: Option[TArray[G]] = CoercionUtils.getAnyArrayCoercion(this).map(_._2)

src/col/vct/col/feature/FeatureRainbow.scala

@@ -486,6 +486,7 @@ class FeatureRainbow[G] {
     case node: LiteralSet[G] => SilverAxiomaticLibraryType
     case node: SeqMember[G] => SilverAxiomaticLibraryType
     case node: SeqSubscript[G] => SilverAxiomaticLibraryType
+    case node: VectorSubscript[G] => SilverAxiomaticLibraryType
     case node: SeqUpdate[G] => SilverAxiomaticLibraryType
     case node: SetIntersection[G] => SilverAxiomaticLibraryType
     case node: SetMember[G] => SilverAxiomaticLibraryType
@@ -502,6 +503,7 @@ class FeatureRainbow[G] {
     case node: TBag[G] => SilverAxiomaticLibraryType
     case node: TSeq[G] => SilverAxiomaticLibraryType
     case node: TSet[G] => SilverAxiomaticLibraryType
+    case node: TVector[G] => SilverAxiomaticLibraryType
 
     case node: SilverCurFieldPerm[G] => SilverSpecific
     case node: SilverCurPredPerm[G] => SilverSpecific

src/col/vct/col/origin/Blame.scala

@@ -409,6 +409,19 @@ case class SeqBoundExceedsLength(node: SeqSubscript[_]) extends SeqBoundFailure
   override def inlineDescWithSource(source: String): String = s"The index in `$source` may exceed the length of the sequence."
 }
 
+sealed trait VectorBoundFailure extends FrontendSubscriptError with BuiltinError
+case class VectorBoundNegative(node: VectorSubscript[_]) extends VectorBoundFailure with NodeVerificationFailure {
+  override def code: String = "vecIndexNegative"
+  override def descInContext: String = "The index in this vector subscript may be negative."
+  override def inlineDescWithSource(source: String): String = s"The index in `$source` may be negative."
+}
+case class VectorBoundExceedsLength(node: VectorSubscript[_]) extends VectorBoundFailure with NodeVerificationFailure {
+  override def code: String = "vecIndexExceedsLength"
+  override def descInContext: String = "The index in this vector subscript may exceed the length of the vector."
+  override def inlineDescWithSource(source: String): String = s"The index in `$source` may exceed the length of the vector."
+}
+
+
 sealed trait ForkFailure extends VerificationFailure
 case class ForkNull(node: Fork[_]) extends ForkFailure with NodeVerificationFailure {
   override def code: String = "forkNull"

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -340,6 +340,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
       case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
       case None => throw IncoercibleText(e, s"set")
     }
+  def vector(e: Expr[Pre]): (Expr[Pre], TVector[Pre]) =
+    CoercionUtils.getAnyVectorCoercion(e.t) match {
+      case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
+      case None => throw IncoercibleText(e, s"set")
+    }
   def bag(e: Expr[Pre]): (Expr[Pre], TBag[Pre]) =
     CoercionUtils.getAnyBagCoercion(e.t) match {
       case Some((coercion, t)) => (ApplyCoercion(e, coercion)(coercionOrigin(e)), t)
@@ -680,8 +685,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
         )
       case AmbiguousResult() => e
       case sub @ AmbiguousSubscript(collection, index) =>
-        firstOk(e, s"Expected collection to be a sequence, array, pointer or map, but got ${collection.t}.",
+        firstOk(e, s"Expected collection to be a sequence, vector, array, pointer or map, but got ${collection.t}.",
           AmbiguousSubscript(seq(collection)._1, int(index))(sub.blame),
+          AmbiguousSubscript(vector(collection)._1, int(index))(sub.blame),
           AmbiguousSubscript(array(collection)._1, int(index))(sub.blame),
           AmbiguousSubscript(pointer(collection)._1, int(index))(sub.blame),
           AmbiguousSubscript(map(collection)._1, coerce(index, map(collection)._2.key))(sub.blame),
@@ -905,6 +911,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
         LiteralSeq(element, values.map(coerce(_, element)))
       case LiteralSet(element, values) =>
         LiteralSet(element, values.map(coerce(_, element)))
+      case LiteralVector(element, values) =>
+        LiteralVector(element, values.map(coerce(_, element)))
       case LiteralTuple(ts, values) =>
         LiteralTuple(ts, values.zip(ts).map {
           case (v, t) => coerce(v, t)
@@ -1396,6 +1404,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends BaseCoercingRewrite
         VectorCompare(coerce(coercedLeft, seqType), coerce(coercedRight, seqType))
       case VectorRepeat(e) =>
         VectorRepeat(e)
+      case get @ VectorSubscript(xs, index) =>
+        VectorSubscript(vector(xs)._1, int(index))(get.blame)
       case VectorSum(indices, vec) =>
         VectorSum(coerce(indices, TSeq[Pre](TInt())), coerce(vec, TSeq[Pre](TRational())))
       case Void() =>

src/col/vct/col/typerules/CoercionUtils.scala

@@ -51,6 +51,8 @@ case object CoercionUtils {
         CoerceMapSeq(getAnyCoercion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget)
       case (TSet(innerSource), TSet(innerTarget)) =>
         CoerceMapSet(getPromotion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget)
+      case (TVector(innerSource, sizeSource), TVector(innerTarget, sizeTarget)) if sizeSource == sizeTarget =>
+        CoerceMapVector(getPromotion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget, sizeTarget)
       case (TBag(innerSource), TBag(innerTarget)) =>
         CoerceMapBag(getPromotion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget)
       case (TMatrix(innerSource), TMatrix(innerTarget)) =>
@@ -258,6 +260,13 @@ case object CoercionUtils {
     case _ => None
   }
 
+  def getAnyVectorCoercion[G](source: Type[G]): Option[(Coercion[G], TVector[G])] = source match {
+    case t: CPrimitiveType[G] => chainCCoercion(t, getAnyVectorCoercion)
+    case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyVectorCoercion)
+    case t: TVector[G] => Some((CoerceIdentity(source), t))
+    case _ => None
+  }
+
   def getAnyBagCoercion[G](source: Type[G]): Option[(Coercion[G], TBag[G])] = source match {
     case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBagCoercion)
     case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyBagCoercion)

src/col/vct/col/typerules/Types.scala

@@ -40,6 +40,8 @@ object Types {
       TSeq(leastCommonSuperType(left, right))
     case (TSet(left), TSet(right)) =>
       TSet(leastCommonSuperType(left, right))
+    case (TVector(left, sizeLeft), TVector(right, sizeRight)) if sizeLeft == sizeRight =>
+      TVector(leastCommonSuperType(left, right), sizeLeft)
     case (TBag(left), TBag(right)) =>
       TBag(leastCommonSuperType(left, right))
     case (TMatrix(left), TMatrix(right)) =>

src/main/vct/main/stages/Transformation.scala

@@ -280,6 +280,7 @@ case class SilverTransformation
     EnumToDomain,
     ImportArray.withArg(adtImporter),
     ImportPointer.withArg(adtImporter),
+    ImportVector.withArg(adtImporter),
     ImportMapCompat.withArg(adtImporter),
     ImportEither.withArg(adtImporter),
     ImportTuple.withArg(adtImporter),

src/parsers/antlr4/SpecLexer.g4

@@ -41,6 +41,7 @@ VAL_REF: 'ref';
 VAL_RATIONAL: 'rational';
 VAL_SEQ: 'seq';
 VAL_SET: 'set';
+VAL_VECTOR: 'vector';
 VAL_BAG: 'bag';
 VAL_POINTER: 'pointer';
 VAL_MAP: 'map';

src/parsers/antlr4/SpecParser.g4

@@ -3,6 +3,7 @@ parser grammar SpecParser;
 /**
  imported grammar rules
    langExpr
+   langConstInt
    langId
    langType
    langModifier
@@ -156,6 +157,7 @@ valMapPairs
 valPrimaryCollectionConstructor
  : 'seq' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralSeq
  | 'set' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralSet
+ | 'vector' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralVector
  | 'set' '<' langType '>' '{' langExpr '|' valSetCompSelectors ';' langExpr '}' # valSetComprehension
  | 'bag' '<' langType '>' '{' valExpressionList? '}' # valTypedLiteralBag
  | 'map' '<' langType ',' langType '>' '{' valMapPairs? '}' # valTypedLiteralMap
@@ -338,6 +340,7 @@ valType
  : ('resource' | 'process' | 'frac' | 'zfrac' | 'rational' | 'bool' | 'ref' | 'any' | 'nothing' | 'string') # valPrimaryType
  | 'seq' '<' langType '>' # valSeqType
  | 'set' '<' langType '>' # valSetType
+ | 'vector' '<' langType ',' langConstInt '>' # valVectorType
  | 'bag' '<' langType '>' # valBagType
  | 'option' '<' langType '>' # valOptionType
  | 'map' '<' langType ',' langType '>' # valMapType

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -1009,6 +1009,7 @@ case class PVLToCol[G](override val baseOrigin: Origin,
     }
     case ValSeqType(_, _, element, _) => TSeq(convert(element))
     case ValSetType(_, _, element, _) => TSet(convert(element))
+    case ValVectorType(_, _, element, _, size, _) => TVector(convert(element), convert(size))
     case ValBagType(_, _, element, _) => TBag(convert(element))
     case ValOptionType(_, _, element, _) => TOption(convert(element))
     case ValMapType(_, _, key, _, value, _) => TMap(convert(key), convert(value))
@@ -1041,6 +1042,7 @@ case class PVLToCol[G](override val baseOrigin: Origin,
   def convert(implicit e: ValPrimaryCollectionConstructorContext): Expr[G] = e match {
     case ValTypedLiteralSeq(_, _, t, _, _, exprs, _) => LiteralSeq(convert(t), exprs.map(convert(_)).getOrElse(Nil))
     case ValTypedLiteralSet(_, _, t, _, _, exprs, _) => LiteralSet(convert(t), exprs.map(convert(_)).getOrElse(Nil))
+    case ValTypedLiteralVector(_, _, t, _, _, exprs, _) => LiteralVector(convert(t), exprs.map(convert(_)).getOrElse(Nil))
     case ValSetComprehension(_, _, t, _, _, value, _, selectors, _, something, _) => ??(e)
     case ValTypedLiteralBag(_, _, t, _, _, exprs, _) => LiteralBag(convert(t), exprs.map(convert(_)).getOrElse(Nil))
     case ValTypedLiteralMap(_, _, key, _, value, _, _, pairs, _) => LiteralMap(convert(key), convert(value), pairs.map(convert(_)).getOrElse(Nil))

src/rewrite/vct/rewrite/Disambiguate.scala

@@ -105,6 +105,7 @@ case class Disambiguate[Pre <: Generation]() extends Rewriter[Pre] {
         else if(op.isMapOp) MapGet(dispatch(collection), dispatch(index))(op.blame)
         else if(op.isArrayOp) ArraySubscript(dispatch(collection), dispatch(index))(op.blame)
         else if(op.isSeqOp) SeqSubscript(dispatch(collection), dispatch(index))(op.blame)
+        else if(op.isVectorOp) VectorSubscript(dispatch(collection), dispatch(index))(op.blame)
         else throw Unreachable("AmbiguousSubscript must subscript a pointer, map, array, or seq because of the type check.")
       case op @ AmbiguousMember(x, xs) =>
         if(op.isMapOp) MapMember(dispatch(x), dispatch(xs))

src/rewrite/vct/rewrite/ParBlockEncoder.scala

@@ -223,6 +223,7 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] {
     case PointerSubscript(pointer, index) => combine(scanForAssignE(pointer), scanForAssignE(index))
     case ArraySubscript(pointer, index) => combine(scanForAssignE(pointer), scanForAssignE(index))
     case SeqSubscript(seq, index) => combine(scanForAssignE(seq), scanForAssignE(index))
+    case VectorSubscript(vec, index) => combine(scanForAssignE(vec), scanForAssignE(index))
     case _ => None
   }
 
@@ -231,6 +232,7 @@ case class ParBlockEncoder[Pre <: Generation]() extends Rewriter[Pre] {
     case ArraySubscript(arr, index) => combine(scanAssignTarget(arr), scanForAssignE(index))
     case PointerSubscript(pointer, index) => combine(scanAssignTarget(pointer), scanForAssignE(index))
     case SeqSubscript(seq, index) => combine(scanAssignTarget(seq), scanForAssignE(index))
+    case VectorSubscript(vec, index) => combine(scanAssignTarget(vec), scanForAssignE(index))
     case _ => None
   }