From 59ee46d06f02590e5ca423c1be0e0bc7b77aaec9 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 23 Aug 2024 11:40:34 +0200 Subject: [PATCH] migration --- fp-principles/huffman-coding/Huffman.scala | 6 +-- .../object-oriented-sets/TweetSet.scala | 48 +++++++++---------- qoi/verified/decoder.scala | 2 +- qoi/verified/encoder.scala | 16 +++---- system-f/Reduction.scala | 12 ++--- system-f/Transformations.scala | 2 +- system-f/Typing.scala | 12 ++--- 7 files changed, 49 insertions(+), 49 deletions(-) diff --git a/fp-principles/huffman-coding/Huffman.scala b/fp-principles/huffman-coding/Huffman.scala index d602878d..a4aa74d8 100644 --- a/fp-principles/huffman-coding/Huffman.scala +++ b/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)) } diff --git a/fp-principles/object-oriented-sets/TweetSet.scala b/fp-principles/object-oriented-sets/TweetSet.scala index f4c9e5ef..e420ac9a 100644 --- a/fp-principles/object-oriented-sets/TweetSet.scala +++ b/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,12 +280,12 @@ 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 @@ -293,13 +293,13 @@ object TweetSetLemmas { 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 @@ -307,16 +307,16 @@ object TweetSetLemmas { 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 = { diff --git a/qoi/verified/decoder.scala b/qoi/verified/decoder.scala index ce8d0766..06b8143e 100644 --- a/qoi/verified/decoder.scala +++ b/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) diff --git a/qoi/verified/encoder.scala b/qoi/verified/encoder.scala index b95ab9b3..8a5d70f5 100644 --- a/qoi/verified/encoder.scala +++ b/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 => diff --git a/system-f/Reduction.scala b/system-f/Reduction.scala index f4a87235..4dda267c 100644 --- a/system-f/Reduction.scala +++ b/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] && diff --git a/system-f/Transformations.scala b/system-f/Transformations.scala index 532339bf..8888585f 100644 --- a/system-f/Transformations.scala +++ b/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) { } diff --git a/system-f/Typing.scala b/system-f/Typing.scala index ed9ce2e7..c0c872b4 100644 --- a/system-f/Typing.scala +++ b/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))