migration

fp-principles/huffman-coding/Huffman.scala

@@ -90,7 +90,7 @@ object Huffman {
     def times(chars: List[Char]): List[(Char, BigInt)] = {
       require(!chars.isEmpty)
       val distinctList = distinct(chars, List())
-      distinctList zip distinctList.map(elem => chars.count(e => e == elem))
+      distinctList.zip(distinctList.map(elem => chars.count(e => e == elem)))
     }.ensuring(res => listEqu(distinct(chars, List()), distinct(chars, List()).map(elem => chars.count(e => e == elem)))
                      && distinct(chars, List()).content == chars.content)
 
@@ -109,7 +109,7 @@ object Huffman {
     def listEqu(list: List[Char], zipWith: List[BigInt]): Boolean = {
       require(list.size == zipWith.size)
       decreases(list)
-      (list zip zipWith).map(elem => elem._1) == list because {
+      (list.zip(zipWith)).map(elem => elem._1) == list because {
         if (list.isEmpty) true
         else listEqu(list.tail, zipWith.tail)
       }
@@ -318,7 +318,7 @@ object Huffman {
    * into a sequence of bits.
    */
     def encode(tree: CodeTree)(text: List[Char]): List[Boolean] = {
-      require(text.content subsetOf tree.chars)
+      require(text.content.subsetOf(tree.chars))
       text.flatMap(elem => encodeChar(tree, elem))
     }
 

fp-principles/object-oriented-sets/TweetSet.scala

@@ -182,7 +182,7 @@ case class NonEmpty(elem: Tweet, left: TweetSet, right: TweetSet) extends TweetS
 
       // this lemma shows that the size of remove(elem) is strictly smaller than this.size
       assert(unionSize(left,right))
-      if(p(elem)) remove(elem).filterAcc(p, acc incl elem)
+      if(p(elem)) remove(elem).filterAcc(p, acc.incl(elem))
       else remove(elem).filterAcc(p, acc)
     }
 
@@ -216,7 +216,7 @@ case class NonEmpty(elem: Tweet, left: TweetSet, right: TweetSet) extends TweetS
       if (x.text < elem.text) new NonEmpty(elem, left.incl(x), right)
       else if (elem.text < x.text) new NonEmpty(elem, left, right.incl(x))
       else this
-    }.ensuring(res => (res contains x))
+    }.ensuring(res => (res.contains(x)))
 
     override def remove(tw: Tweet): TweetSet = {
       decreases((this, 0))
@@ -243,7 +243,7 @@ case class NonEmpty(elem: Tweet, left: TweetSet, right: TweetSet) extends TweetS
     override def union(that: TweetSet): TweetSet = {
       decreases((this, 0))
 
-      left union (right union (that incl elem))
+      left.union(right.union(that.incl(elem)))
     }
 
     override def size: BigInt = {
@@ -280,43 +280,43 @@ object TweetSetLemmas {
     decreases(s)
     s match {
       case Empty() =>
-        (s incl e).size <= s.size + 1
+        (s.incl(e)).size <= s.size + 1
       case NonEmpty(elem, left, right) =>
         // FIXME: change these to assertions when they are no longer simplified for postconditions
         inclSize(left, e) &&
         inclSize(right, e) &&
-        (s incl e).size <= s.size + 1
+        (s.incl(e)).size <= s.size + 1
     }
   }.holds
 
   def unionSize(s1: TweetSet, s2: TweetSet): Boolean = {
     decreases(s1)
     s1 match {
       case Empty() =>
-        (s1 union s2).size <= s1.size + s2.size
+        (s1.union(s2)).size <= s1.size + s2.size
       case NonEmpty(elem, left, right) =>
         // FIXME: change these to assertions when they are no longer simplified for postconditions
-        unionSize(left, right union (s2 incl elem)) &&
-        unionSize(right, s2 incl elem) &&
+        unionSize(left, right.union(s2.incl(elem))) &&
+        unionSize(right, s2.incl(elem)) &&
         inclSize(s2, elem) &&
-        (s1 union s2).size <= s1.size + s2.size
+        (s1.union(s2)).size <= s1.size + s2.size
     }
   }.holds
 
   def removeSize(s: TweetSet, e: Tweet): Boolean = {
     decreases(s)
     s match {
       case Empty() =>
-        (s.contains(e) && (s remove e).size <= s.size - 1) ||
-        (!s.contains(e) && (s remove e).size <= s.size)
+        (s.contains(e) && (s.remove(e)).size <= s.size - 1) ||
+        (!s.contains(e) && (s.remove(e)).size <= s.size)
       case NonEmpty(elem, left, right) =>
         // FIXME: change these to assertions when they are no longer simplified for postconditions
         removeSize(left, e) &&
         removeSize(right, e) &&
         unionSize(left,right) &&
         (
-          (s.contains(e) && (s remove e).size <= s.size - 1) ||
-          (!s.contains(e) && (s remove e).size <= s.size)
+          (s.contains(e) && (s.remove(e)).size <= s.size - 1) ||
+          (!s.contains(e) && (s.remove(e)).size <= s.size)
         )
     }
   }.holds
@@ -383,7 +383,7 @@ object TweetSetLemmas {
         check(inclForall(right, elem, p))
     }
 
-    (s incl elem).forall(p)
+    (s.incl(elem)).forall(p)
   }.holds
 
   def inclIsSearchTree(s: TweetSet, elem: Tweet): Boolean = {
@@ -392,20 +392,20 @@ object TweetSetLemmas {
 
     s match {
       case Empty() =>
-        check((s incl elem).isSearchTree)
+        check((s.incl(elem)).isSearchTree)
       case NonEmpty(e, left, right) =>
         if (elem.text < e.text) {
           check(inclIsSearchTree(left, elem))
           check(inclForall(left, elem, smallerThan(e)))
-          check((s incl elem).isSearchTree)
+          check((s.incl(elem)).isSearchTree)
         } else if (elem.text > e.text) {
           check(inclIsSearchTree(right, elem))
           check(inclForall(right, elem, greaterThan(e)))
-          check((s incl elem).isSearchTree)
+          check((s.incl(elem)).isSearchTree)
         }
     }
 
-    (s incl elem).isSearchTree
+    (s.incl(elem)).isSearchTree
   }.holds
 
   def unionForall(s1: TweetSet, s2: TweetSet, p: Tweet => Boolean): Boolean = {
@@ -416,11 +416,11 @@ object TweetSetLemmas {
       case Empty() => ()
       case NonEmpty(elem, left, right) =>
         check(inclForall(s2, elem, p))
-        check(unionForall(right, s2 incl elem, p))
-        check(unionForall(left, right union (s2 incl elem), p))
+        check(unionForall(right, s2.incl(elem), p))
+        check(unionForall(left, right.union(s2.incl(elem)), p))
     }
 
-    (s1 union s2).forall(p)
+    (s1.union(s2)).forall(p)
   }.holds
 
   def unionIsSearchTree(s1: TweetSet, s2: TweetSet): Boolean = {
@@ -431,11 +431,11 @@ object TweetSetLemmas {
       case Empty() => ()
       case NonEmpty(elem, left, right) =>
         check(inclIsSearchTree(s2, elem))
-        check(unionIsSearchTree(right, s2 incl elem))
-        check(unionIsSearchTree(left, right union (s2 incl elem)))
+        check(unionIsSearchTree(right, s2.incl(elem)))
+        check(unionIsSearchTree(left, right.union(s2 `incl` elem)))
     }
 
-    (s1 union s2).isSearchTree
+    (s1.union(s2)).isSearchTree
   }.holds
 
   def removeForall(s: TweetSet, p: Tweet => Boolean, elem: Tweet): Boolean = {

qoi/verified/decoder.scala

@@ -647,7 +647,7 @@ object decoder {
     require(readH == h.toInt)
     require(readChan.toLong == chan)
 
-    val SomeMut(DecodedResult(decodedPixels, ww, hh, cchan)) = decode(bytes, until)
+    val SomeMut(DecodedResult(decodedPixels, ww, hh, cchan)) = decode(bytes, until): @unchecked
     val initIndex = Array.fill(64)(0)
     val initPixels = Array.fill(w.toInt * h.toInt * chan.toInt)(0: Byte)
     val initPx = Pixel.fromRgba(0, 0, 0, 255.toByte)

qoi/verified/encoder.scala

@@ -128,7 +128,7 @@ object encoder {
       }
 
       decoder.decodeLemma(outPos + Padding)
-      val SomeMut(decoder.DecodedResult(actuallyDecoded, ww, hh, cchan)) = decoder.decode(bytes, outPos + Padding)
+      val SomeMut(decoder.DecodedResult(actuallyDecoded, ww, hh, cchan)) = decoder.decode(bytes, outPos + Padding): @unchecked
       check(ww == w)
       check(hh == h)
       check(cchan == chan)
@@ -494,7 +494,7 @@ object encoder {
           assert(rhs2 == rhs1)
           assert(lhs2 <= rhs2)
           val lhs3 = chan * (outPos1 - HeaderSize + chan + 1)
-          assert((lhs3 <= lhs2) because (chan >= 3 && outPos1 <= outPos0 + 2))
+          assert((lhs3 <= lhs2) `because` (chan >= 3 && outPos1 <= outPos0 + 2))
           assert(lhs3 <= rhs2)
           check(positionsIneqInv(0, outPos1 + chan + 1, pxPos + chan))
         }
@@ -520,7 +520,7 @@ object encoder {
           } else trivial
         })
 
-        assert((outPos2 <= bytes.length - Padding) because (bytes.length == maxSize))
+        assert((outPos2 <= bytes.length - Padding).because(bytes.length == maxSize))
         check(positionsIneqInv(0, outPos1, pxPos))
         // Precond 6 slow (~40s)
         check(encodeNoRunProp(indexPre, index, bytes, outPos1, outPos2))
@@ -550,7 +550,7 @@ object encoder {
           val lhs3 = chan * (outPos0 - HeaderSize + run0 * chan + chan + 1)
           assert(lhs3 <= rhs2)
           val lhs4 = chan * (outPos1 - HeaderSize)
-          assert((lhs4 <= lhs3) because (chan >= 3 && outPos1 <= outPos0 + 2 && run0 >= 0))
+          assert((lhs4 <= lhs3).because(chan >= 3 && outPos1 <= outPos0 + 2 && run0 >= 0))
           assert(lhs4 <= rhs2)
           check(positionsIneqInv(run1, outPos1, pxPos + chan))
         } else {
@@ -573,7 +573,7 @@ object encoder {
           val lhs4 = chan * ((outPos1 - HeaderSize) + chan * (run0 + 1))
           assert(lhs4 == lhs3)
           assert(lhs4 <= rhs2)
-          check(positionsIneqInv(run1, outPos1, pxPos + chan) because (run1 == run0 + 1))
+          check(positionsIneqInv(run1, outPos1, pxPos + chan).because(run1 == run0 + 1))
         }
 
         check(rangesInv(index.length, bytes.length, run1, outPos1, pxPos))
@@ -583,7 +583,7 @@ object encoder {
     }
     assert(HeaderSize <= outPos2 && outPos2 <= maxSize - Padding)
     assert((px != pxPrev) ==> (outPos1 < outPos2))
-    assert((outPos2 <= bytes.length - Padding) because (bytes.length == maxSize))
+    assert((outPos2 <= bytes.length - Padding).because(bytes.length == maxSize))
     assert(runUpd.reset ==> updateRunProp(bytes, run0, outPos0, runUpd))
     assert((px != pxPrev) ==> encodeNoRunProp(indexPre, index, bytes, outPos1, outPos2))
 
@@ -1383,7 +1383,7 @@ object encoder {
     assert(b1Bytes1 == b1Bytes2)
     assert((b1Bytes1 & Mask2) == OpRun)
     check(res1 == res2)
-    check((outPos0 < bytes2.length - Padding) because (bytes.length == bytes2.length))
+    check((outPos0 < bytes2.length - Padding).because(bytes.length == bytes2.length))
   }.ensuring(_ => updateRunProp(bytes2, run0, outPos0, ru))
 
   @ghost
@@ -1434,7 +1434,7 @@ object encoder {
     assert(arraysEq(pixels, decPixels, pxPos, pxPos + chan))
     arraysEqCombinedLemma2(pixels, decPixels, 0, pxPos, pxPos + chan)
     assert(arraysEq(pixels, decPixels, 0, pxPos + chan))
-    check(arraysEq(pixels, decPixels, 0, decIter.pxPos) because (decIter.pxPos == pxPos + chan))
+    check(arraysEq(pixels, decPixels, 0, decIter.pxPos).because(decIter.pxPos == pxPos + chan))
 
     GhostDecoded(freshCopy(decIndex), freshCopy(decPixels), decIter.inPos, decIter.pxPos)
   }.ensuring { newDecoded =>

system-f/Reduction.scala

@@ -70,7 +70,7 @@ object Reduction {
           case App(t1p, t2p) if reducesTo(t1, t1p).isDefined && t2 == t2p  => Some[ReductionRule](App1Congruence)
           case App(t1p, t2p) if t1 == t1p && reducesTo(t2, t2p).isDefined => Some[ReductionRule](App2Congruence)
           case _ => None[ReductionRule]()
-        }) orElse (t1 match {
+        }).orElse(t1 match {
           case Abs(_, body) if absSubstitution(body, t2) == tp => Some[ReductionRule](AbsAppReduction)
           case _ => None[ReductionRule]()
         })
@@ -79,7 +79,7 @@ object Reduction {
         (tp match {
           case Fix(fp) if reducesTo(f, fp).isDefined => Some[ReductionRule](FixCongruence)
           case _ => None[ReductionRule]()
-        }) orElse (f match {
+        }).orElse(f match {
           case Abs(_, body) if absSubstitution(body, t) == tp => Some[ReductionRule](AbsFixReduction)
           case _ => None[ReductionRule]()
         })
@@ -94,7 +94,7 @@ object Reduction {
         (tp match {
           case TApp(termp, typp) if reducesTo(term, termp).isDefined && typ == typp => Some[ReductionRule](TAppCongruence)
           case _ => None[ReductionRule]()
-        }) orElse (term match {
+        }).orElse(term match {
           case TAbs(body) if tabsSubstitution(body, typ) == tp => Some[ReductionRule](TAbsTappReduction)
           case _ => None[ReductionRule]()
         })
@@ -191,7 +191,7 @@ object ReductionProperties {
     require(reducesTo(t, tp).get == AbsAppReduction)
 
     assert(t.isInstanceOf[App])
-    val App(t1, _) = t
+    val App(t1, _) = t: @unchecked
     assert(t1.isInstanceOf[Abs])
   }.ensuring(
     t.isInstanceOf[App] && t.asInstanceOf[App].t1.isInstanceOf[Abs] &&
@@ -221,7 +221,7 @@ object ReductionProperties {
     require(reducesTo(t, tp).get == AbsFixReduction)
 
     assert(t.isInstanceOf[Fix])
-    val Fix(f) = t
+    val Fix(f) = t: @unchecked
     assert(f.isInstanceOf[Abs])
   }.ensuring(
     t.isInstanceOf[Fix] && t.asInstanceOf[Fix].t.isInstanceOf[Abs] &&
@@ -253,7 +253,7 @@ object ReductionProperties {
     require(reducesTo(t, tp).get == TAbsTappReduction)
 
     assert(t.isInstanceOf[TApp])
-    val TApp(body, _) = t
+    val TApp(body, _) = t: @unchecked
     assert(body.isInstanceOf[TAbs])
   }.ensuring(
     t.isInstanceOf[TApp] && t.asInstanceOf[TApp].t.isInstanceOf[TAbs] &&

system-f/Transformations.scala

@@ -1010,7 +1010,7 @@ object TransformationsProperties {
       require(if(d < 0) !hasFreeVariablesIn(env, c, -d) else true)
       require(0 <= j && j < env.length)
 
-      val Cons(h, t) = env
+      val Cons(h, t) = env: @unchecked
 
       if(j == 0) {
       }

system-f/Typing.scala

@@ -470,7 +470,7 @@ object TypingProperties {
 
         termAndEnvNegativeShiftValidityImplyTypeNegativeShiftValidity(btd, s, c)
         assert(btd.t.isInstanceOf[UniversalType])
-        val UniversalType(bodyTyp) = btd.t
+        val UniversalType(bodyTyp) = btd.t: @unchecked
 
         TypeTrProp.boundRangeShift(typArg, 1, 0, c, -s)
         assert(!TypeTr.shift(typArg, 1, 0).hasFreeVariablesIn(c + 1, -s))
@@ -553,7 +553,7 @@ object TypingProperties {
         val btdp = shiftAllTypes(btd, s, c)
 
         assert(btd.t.isInstanceOf[UniversalType])
-        val UniversalType(bodyTyp) = btd.t
+        val UniversalType(bodyTyp) = btd.t: @unchecked
 
         universalSubstitutionShiftCommutativity(bodyTyp, typeArg, s, c)
 
@@ -771,7 +771,7 @@ object TypingProperties {
         val btdp = preservationUnderTypeSubst(btd, j, styp)
         val argTypep = TypeTr.substitute(argType, j, styp)
         assert(btdp.t.isInstanceOf[UniversalType])
-        val UniversalType(bodyType) = btd.t
+        val UniversalType(bodyType) = btd.t: @unchecked
         universalSubstitutionSubstitutionCommutativity(bodyType, argType, j, styp)
         TAppDerivation(newEnv, newTyp, TApp(btdp.term, argTypep), btdp)
       }
@@ -790,7 +790,7 @@ object TypingProperties {
     require(absTd.ter.argType == argTd.t)
     require(absTd.t == ArrowType(argTd.t, typ))
 
-    val Abs(argType, _) = absTd.term
+    val Abs(argType, _) = absTd.term: @unchecked
 
     val sd0 = argTd
     val sd1 = insertTypeInEnv(Nil(), argType, sd0.env, sd0)
@@ -849,7 +849,7 @@ object TypingProperties {
     require(reducesTo(td.term, reduced).isDefined)
     decreases(td)
 
-    val Some(rule) = reducesTo(td.term, reduced)
+    val Some(rule) = reducesTo(td.term, reduced): @unchecked
 
     td match {
       case AbsDerivation(env, typ, t@Abs(argType, body), btd) => {
@@ -864,7 +864,7 @@ object TypingProperties {
         assert(btd.env == argType :: td.env)
         assert(btdp.env == btd.env)
         assert(typ.isInstanceOf[ArrowType])
-        val ArrowType(t1, t2) = typ
+        val ArrowType(t1, t2) = typ: @unchecked
         assert(t1 == argType)
         assert(t2 == btdp.t)
         assert(tp == Abs(argType, btdp.term))