@@ 0,0 1,371 @@
+;;; Copyright 2023 The Plunder Authors
+;;; Use of this source code is governed by a BSD-style license that can be
+;;; found in the LICENSE file.
+
+### quickcheck <- pq
+
+/+ splitmix [mkSMGen nextWord64 splitSMGen]
+/+ prelude
+
+(**debug m v)#=v
+
+; uncomment to get debug output
+;(**debug m v)#=(trk m v)
+
+# datatype (Result a)
+* OK
+ * good : Int ; {good} is the number successful tests
+ * drop : Int ; {drop} is the number discards
+* FAIL
+ * gen : StdGen ; {gen} is the generator (for replay)
+ * size : Int ; The {size} (for replay)
+ * good : Int ; {good} is the number of successful tests
+ * drop : Int ; {drop} is the number discards
+ * fail : a ; {fail} is the failing value (shrunk)
+* GAVE_UP
+ * good : Int ; {good} is the number of successful tests
+ * drop : Int ; {drop} is the number discards
+
+* # typedef (Gen a) (StdGen > Int > a)
+* # typedef (Shrink a) (a > List a)
+* # typedef PropResult (Opt Bit)
+
+# record Args
+| ARGS
+* replay : Opt (StdGen, Int)
+* maxSuccess : Int
+* maxDiscardRatio : Int
+* maxSize : Int
+* maxShrinks : Int
+
+> Args
+= stdArgs (ARGS NONE 100 100 100 10000)
+
+# record State
+| STATE
+* successCount : Int
+* totalDiscardCount : Int
+* recentDiscardCount : Int
+
+; infix 4 ===
+; (===) :: Eq a => a -> a -> PropResult
+; x === y = SOME (x == y)
+
+; infix 4 =/=
+; (=/=) :: Eq a => a -> a -> PropResult
+; x =/= y = SOME (x /= y)
+
+> (a -> Bit) > a > PropResult
+(prop1 fun x)=(SOME | fun x)
+
+> (a > b > Bit) > a > b > PropResult
+(prop2 fun x y)=(SOME | fun x y)
+
+> PropResult
+discardRes=NONE
+
+> a > a > PropResult
+= qcEql | prop2 eql
+
+> a > a > PropResult
+= qcNeq | prop2 neq
+
+> Bit > PropResult
+qcIs=SOME
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; quickCheck
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(roundTo n m)=(mul (div n m) m)
+
+> StdGen
+> Args
+> Gen a
+> Shrink a
+> (a -> PropResult)
+> Result a
+= (quickCheck sgSeed args gen shrink prop)
+;
+@ stInit | STATE 0 0 0
+@ sgInit | maybeCase (getReplay args) sgSeed idx-0
+;
+@ (at0 f s n d)
+ | if (and (eql 0 n) (eql 0 d))
+ | s
+ | else
+ | f n d
+;
+@ (computeSize_ n d)
+ @ msz (getMaxSize args)
+ @ msc (getMaxSuccess args)
+ ;; e.g. with maxSuccess = 250, maxSize = 100, goes like this:
+ ;; 0, 1, 2, ..., 99, 0, 1, 2, ..., 99, 0, 2, 4, ..., 98.
+ @ tst
+ | lte (add (roundTo n msz) msz) msc
+ | gte n msc
+ | eql 0 (mod msc msz)
+ | if tst
+ | min msz
+ | add
+ | mod n msz
+ | div d 10
+ | else
+ | min msz
+ | div | mul
+ | mod n msz
+ | msz
+ | add
+ | mod (getMaxSuccess args) msz
+ | div d 10
+;
+@ computeSize
+ # datacase (getReplay args)
+ * NONE | computeSize_
+ * (SOME [_ s]) | at0 computeSize_ s
+;
+@ (runShrinks count lastGood shrinks)
+ # datacase shrinks
+ * NIL
+ | lastGood
+ * (CONS v nextShrinks)
+ | if (debug ["shrink: " v] (prop v == SOME FALSE))
+ | runShrinks (inc count) v (shrink v)
+ | else
+ | runShrinks count lastGood nextShrinks
+;
+@ (go st sg)
+ | if (gte (getSuccessCount st) (getMaxSuccess args))
+ | OK getSuccessCount-st getTotalDiscardCount-st
+ | if | gte (getTotalDiscardCount st)
+ | mul (getMaxDiscardRatio args) (getMaxSuccess args)
+ | GAVE_UP getSuccessCount-st getTotalDiscardCount-st
+ @ sg2,sg1 | splitSMGen sg
+ @ size | computeSize getSuccessCount-st getRecentDiscardCount-st
+ @ v | gen sg2 size
+ # datacase (debug ["go: " v] (prop v))
+ * (SOME res)
+ | if res
+ | go (setSuccessCount (inc | getSuccessCount st) st) sg1
+ | FAIL sgInit size getSuccessCount-st getTotalDiscardCount-st
+ | runShrinks 0 v (shrink v)
+ * NONE
+ ^ (go _ sg1)
+ | setTotalDiscardCount (add 1 getTotalDiscardCount-st)
+ | setRecentDiscardCount (add 1 getRecentDiscardCount-st)
+ | st
+;
+| go stInit sgInit
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Gen
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+> Gen a
+> (a -> Gen b)
+> Gen b
+= (bindGen m k r n)
+@ [r1 r2] | splitSMGen r
+| k (m r1 n) r2 n
+
+> a > Gen a
+(pureGen x r n)=x
+
+> (Int -> Gen a) > Gen a
+(sized f r n)=(f n r n)
+
+> Gen Int
+getSize=(sized pureGen)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; generators
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+> Gen W64
+(genU64 r n)=(fst | nextWord64 r)
+
+> W64 > W64 > Gen W64
+= (chooseW64 lo hi r n)
+@ val (fst (nextWord64 r))
+| add lo (mod val (sub hi lo))
+
+> Gen a > Gen b > Gen (a, b)
+= (gen2 genA genB)
+: vA <- bindGen genA
+: vB <- bindGen genB
+| pureGen (vA, vB)
+
+> Int > Gen a > Gen (List a)
+= (genListLen len gen)
+| if (lte len 0)
+ | pureGen ~[]
+: v <- bindGen gen
+: vs <- bindGen (genListLen (sub len 1) gen)
+| pureGen (v :: vs)
+
+> Int > Gen a > Gen (List a)
+= (genListLenMax maxLen gen)
+: len <- bindGen genU64
+@ len | mod len maxLen
+| genListLen len gen
+
+> Gen a > Gen (List a)
+= (genList gen)
+: n <- sized
+: k <- bindGen (chooseW64 0 n)
+| genListLen k gen
+
+= (fmapGen f gen)
+& (r n)
+| f (gen r n)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; shrinkers
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; shrink lists should be in *ascending* order. we try the smallest first. if
+;; the prop passes, we keep going "up" the list.
+
+> (a -> List a)
+> (b -> List b)
+> (a, b)
+> List (a, b)
+= (shrink2 shrA shrB (x, y))
+| listWeld
+ | listMap (x_ & x_,y) (shrA x)
+| listMap (y_ & x,y_) (shrB y)
+
+> Integral a > a > [a]
+= (shrinkU64 x)
+| listNub
+| listTakeWhile (gth x)
+^ (0 :: _)
+| listMap (sub x)
+| listDrop 1 (listIterate v&(div v 2) x)
+
+> Bit > List Bit
+(shrinkBool b)=(if b ~[FALSE] ~[])
+
+> (a > List a) > List a > List (List a)
+= (shrinkList shr xs)
+@ n
+ | listLen xs
+@ (shrinkOne xs)
+ # datacase xs
+ * NIL | NIL
+ * (CONS x xs)
+ | listWeld
+ | listMap x&(x::xs) (shr x)
+ | listMap xs&(x::xs) (shrinkOne xs)
+@ (removes k n xs)
+ @ xs1 | listTake k xs
+ @ xs2 | listDrop k xs
+ | if (gth k n) | NIL
+ | if (listIsEmpty xs2) | ~[NIL]
+ ^ (xs2 :: listMap (listWeld xs1) _)
+ | removes k (sub n k) xs2
+| listWeld
+ | listCat
+ | listMap k&(removes k n xs)
+ | listTakeWhile (v&(gth v 0))
+ | listIterate (v&(div v 2)) n
+| shrinkOne xs
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; test helpers / pretty-printers
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+= (showResult name seed result)
+# datacase result
+* (OK passed dropped)
+ `
+ | $(TAPE name 0) SUCCESS
+ ## =passed $(WORD showNat-passed 0)
+ ## =dropped $(WORD showNat-dropped 0)
+* (FAIL gen size passed dropped failed)
+ `
+ | $(TAPE name 0) FAILURE
+ | =parameters
+ ## =seed $(WORD showNat-seed 0)
+ ## =stdgen $(EMBD gen)
+ ## =size $(WORD showNat-size 0)
+ ## =passed $(WORD showNat-passed 0)
+ ## =dropped $(WORD showNat-dropped 0)
+ | {counter example:}
+ | $(EMBD failed)
+* (GAVE_UP passed dropped)
+ `
+ | $(TAPE name 0) GAVE UP
+ ## =passed $(WORD showNat-passed 0)
+ ## =dropped $(WORD showNat-dropped 0)
+
+= (qc_exec1 seed name prop [gen shrink] isExpectedResult)
+@ sg | mkSMGen seed
+@ result | quickCheck sg stdArgs gen shrink prop
+@ resultRex | showResult name seed result
+| ifNot (isExpectedResult result) resultRex
+| trk resultRex 1
+
+= (resultIsOk result)
+# datacase result
+* (OK _ _) | TRUE
+* _ | FALSE
+
+= (resultIsFail result)
+# datacase result
+* (FAIL _ _ _ _ _) | TRUE
+* _ | FALSE
+
+(qc1_pass seed name prop arb)=(qc_exec1 seed name prop arb resultIsOk)
+(qc1_fail seed name prop arb)=(qc_exec1 seed name prop arb resultIsFail)
+
+= (qc2_pass seed name fun [genA shrinkA] [genB shrinkB])
+@ genAB | gen2 genA genB
+@ shrinkAB | shrink2 shrinkA shrinkB
+@ fun | uncurry fun
+| qc1_pass seed name fun [genAB shrinkAB]
+
+= (qc2_fail seed name fun [genA shrinkA] [genB shrinkB])
+@ genAB | gen2 genA genB
+@ shrinkAB | shrink2 shrinkA shrinkB
+@ fun | uncurry fun
+| qc1_fail seed name fun [genAB shrinkAB]
+
+= arbU64 | (genU64, shrinkU64)
+= arbU64List | (genList genU64, shrinkList shrinkU64)
+
+= (isList x)
+^ (isZero x || _)
+| (isRow x && (len x == 2) && isList (snd x))
+
+= (isW64 x) | lte x wMax64
+= (isW32 x) | lte x wMax32
+= (isListOf ck x) | (isList x && listAll ck x)
+= (subNeg x y) | eql (iSub64 x y) | iNeg64 (iSub64 y x)
+= (revRev ls) | eql ls | listRev (listRev ls)
+= (palindrome ls) | eql ls | listRev ls
+
+!! qc1_pass 42 'w64 is a w64' (prop1 isW64) arbU64
+!! qc1_pass 42 'w64 is not 0' (prop1 neq-0) arbU64
+!! qc1_fail 42 'w64 is a w32' (prop1 isW32) arbU64
+!! qc1_pass 42 'list is list' (prop1 isList) arbU64List
+!! qc1_pass 42 'list is list' (prop1 isListOf-isW64) arbU64List
+!! qc1_fail 42 'palindrome' (prop1 palindrome) arbU64List
+!! qc2_fail 42 'eq pair' (prop2 eql) arbU64 arbU64
+!! qc1_pass 42 'sub neg' (prop2 subNeg) arbU64
+!! qc1_pass 42 'rev rev' (prop1 revRev) arbU64List
+
+^-^
+^-^ ARGS
+^-^ prop1 prop2 discardRes qcEql qcNeq qcIs
+^-^ quickCheck
+^-^ bindGen pureGen sized getSize
+^-^ genU64 chooseW64 gen2 genListLen genListLenMax genList fmapGen
+^-^ shrink2 shrinkU64 shrinkBool shrinkList
+^-^ qc1_pass qc1_fail qc2_pass
+^-^