Example.juvix

module Example;

import Stdlib.Prelude open;
import Stdlib.Extra.Gcd open;

import Data.List open;
import Data.String open;

import Test.QuickCheckTest as QC;

prop-reverseDoesNotChangeLength (xs : List Int) : Bool :=
  length (reverse xs) == length xs;

prop-reverseReverseIsIdentity (xs : List Int) : Bool :=
  eqListInt xs (reverse (reverse xs));

prop-tailLengthOneLess (xs : List Int) : Bool :=
  isEmpty xs || ofNat (length (tail xs)) == intSubNat (length xs) 1;

prop-splitAtRecombine (n : Nat) (xs : List Int) : Bool :=
  case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs);

prop-mergeSumLengths (xs : List Int) (ys : List Int) : Bool :=
  length xs + length ys == length (merge {{ordIntI}} xs ys);

prop-partition (xs : List Int) (p : Int -> Bool) : Bool :=
  case partition p xs of
    lhs, rhs :=
      all p lhs
        && not (any p rhs)
        && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));

prop-distributive (a : Int) (b : Int) (f : Int -> Int) : Bool :=
  f (a + b) == f a + f b;

prop-add-sub (a : Int) (b : Int) : Bool := a == a + b - b;

prop-add-sub-bad (a : Int) (b : Int) : Bool := a == ofNat 2;

prop-gcd-bad (a : Int) (b : Int) : Bool := gcd a b > ofNat 1;

gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" prop-gcd-bad;

partitionTest : QC.Test :=
  QC.mkTest
    "partition: recombination of the output equals the input"
    prop-partition;

testDistributive : QC.Test :=
  QC.mkTest "all functions are distributive over +" prop-distributive;

reverseLengthTest : QC.Test :=
  QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength;

reverseReverseIdTest : QC.Test :=
  QC.mkTest "reverse of reverse is identity" prop-reverseReverseIsIdentity;

splitAtRecombineTest : QC.Test :=
  QC.mkTest
    "splitAt: recombination of the output is equal to the input list"
    prop-splitAtRecombine;

mergeSumLengthsTest : QC.Test :=
  QC.mkTest
    "merge: sum of the lengths of input lists is equal to the length of output list"
    prop-mergeSumLengths;

tailLengthOneLessTest : QC.Test :=
  QC.mkTest
    "tail: length of output is one less than input unless empty"
    prop-tailLengthOneLess;

main : IO :=
  readLn
    \{seed :=
      QC.runTestsIO
        100
        (stringToNat seed)
        [
          partitionTest;
          reverseLengthTest;
          reverseReverseIdTest;
          splitAtRecombineTest;
          mergeSumLengthsTest;
          tailLengthOneLessTest;
        ]};