Release 0.13.0 (#15)

* Update stdlib reference

* Update stdlib reference

* Add Arbitrary for Maybe and Either

* Rename QuickCheck Result to Outcome

* Release 0.13.0

Data/List.juvix

@@ -12,13 +12,8 @@ rangeStep : Nat -> Nat -> List Nat
         | (suc n) xs := go n (n * step :: xs);
     in go n nil;
 
-unzipWith
-  : {A : Type}
-    -> {B : Type}
-    -> {C : Type}
-    -> (A -> B -> C)
-    -> List (Pair A B)
-    -> List C := map << uncurry;
+unzipWith : {A : Type} -> {B : Type} -> {C : Type} -> (A -> B -> C) -> List (Pair A B) -> List C :=
+  map << uncurry;
 
 range : Nat -> List Nat
   | n := rangeStep 1 n;

Data/Monoid.juvix

@@ -2,18 +2,10 @@ module Data.Monoid;
 
 import Stdlib.Prelude open;
 
-type Monoid (A : Type) :=
-  monoid : A -> (A -> A -> A) -> Monoid A;
+type Monoid (A : Type) := monoid : A -> (A -> A -> A) -> Monoid A;
 
-foldMap
-  : {A : Type}
-    -> {M : Type}
-    -> Monoid M
-    -> (A -> M)
-    -> List A
-    -> M
-  | (monoid mempty mappend) f :=
-    foldr (mappend << f) mempty;
+foldMap : {A : Type} -> {M : Type} -> Monoid M -> (A -> M) -> List A -> M
+  | (monoid mempty mappend) f := foldr (mappend << f) mempty;
 
 mconcat : {A : Type} -> Monoid A -> List A -> A
   | m xs := foldMap m id xs;

Data/Random.juvix

@@ -41,21 +41,17 @@ stdNext : StdGen -> Pair Nat StdGen
       s2 : Int := ofNat s2Nat;
       s3 : Int := ofNat s3Nat;
       k : Int := div s1 (ofNat 206);
-      s1' : Int :=
-        ofNat 157 * (s1 - k * ofNat 206) - k * ofNat 21;
+      s1' : Int := ofNat 157 * (s1 - k * ofNat 206) - k * ofNat 21;
       s1'' : Int := ite (s1' < ofNat 0) (s1' + ofNat 32363) s1';
       k' : Int := div s2 (ofNat 217);
-      s2' : Int :=
-        ofNat 146 * (s2 - k' * ofNat 217) - k' * ofNat 45;
+      s2' : Int := ofNat 146 * (s2 - k' * ofNat 217) - k' * ofNat 45;
       s2'' : Int := ite (s2' < ofNat 0) (s2' + ofNat 31727) s2';
       k'' : Int := div s3 (ofNat 222);
-      s3' : Int :=
-        ofNat 142 * (s3 - k' * ofNat 222) - k' * ofNat 133;
+      s3' : Int := ofNat 142 * (s3 - k' * ofNat 222) - k' * ofNat 133;
       s3'' : Int := ite (s2' < ofNat 0) (s2' + ofNat 31657) s3';
       z : Int := s1'' - s2'';
       z' : Int := ite (z > ofNat 706) (z - ofNat 32362) z;
-      z'' : Int :=
-        ite (z' < ofNat 1) (z' + ofNat 32362) (mod z (ofNat k1));
+      z'' : Int := ite (z' < ofNat 1) (z' + ofNat 32362) (mod z (ofNat k1));
     in toNat z'', stdGen (toNat s1'') (toNat s2'') (toNat s3'');
 
 stdSplit : StdGen -> Pair StdGen StdGen
@@ -65,18 +61,11 @@ stdSplit : StdGen -> Pair StdGen StdGen
       newS2 : Nat := ite (s2 == 1) k2 (sub s2 1);
       newS3 : Nat := ite (s3 == k3) 1 (s3 + 1);
       newG : StdGen := snd (stdNext g);
-      leftG : StdGen :=
-        stdGen newS1 (stdGenS2 newG) (stdGenS3 newG);
+      leftG : StdGen := stdGen newS1 (stdGenS2 newG) (stdGenS3 newG);
       rightG : StdGen := stdGen (stdGenS1 newG) newS2 newS3;
     in leftG, rightG;
 
-randNatAux
-  : StdGen
-    -> Nat
-    -> Nat
-    -> Nat
-    -> Pair Nat StdGen
-    -> Pair Nat StdGen
+randNatAux : StdGen -> Nat -> Nat -> Nat -> Pair Nat StdGen -> Pair Nat StdGen
   | g genLo genMag :=
     let
       terminating
@@ -98,8 +87,7 @@ randNat : StdGen -> Nat -> Nat -> Pair Nat StdGen
       q : Nat := 1000;
       k : Nat := sub hi lo + 1;
       tgtMag : Nat := k * q;
-      x : Pair Nat StdGen :=
-        randNatAux g genLo genMag tgtMag (0, g);
+      x : Pair Nat StdGen := randNatAux g genLo genMag tgtMag (0, g);
       v : Nat := fst x;
       g' : StdGen := snd x;
       v' : Nat := lo + mod v k;

Data/String.juvix

@@ -5,7 +5,6 @@ import Stdlib.Prelude open;
 import Data.Monoid as Monoid;
 
 intercalate : String → List String → String
-  | sep xs :=
-    Monoid.mconcat Monoid.string (intersperse sep xs);
+  | sep xs := Monoid.mconcat Monoid.string (intersperse sep xs);
 
 lines : List String -> String := intercalate "\n";

Example.juvix

@@ -8,79 +8,53 @@ import Data.String open;
 
 import Test.QuickCheckTest as QC;
 
-prop-reverseDoesNotChangeLength (xs : List Int) : Bool :=
-  length (reverse xs) == length xs;
+prop-reverseDoesNotChangeLength (xs : List Int) : Bool := length (reverse xs) == length xs;
 
-prop-reverseReverseIsIdentity (xs : List Int) : Bool :=
-  eqListInt xs (reverse (reverse xs));
+prop-reverseReverseIsIdentity (xs : List Int) : Bool := eqListInt xs (reverse (reverse xs));
 
 prop-tailLengthOneLess (xs : List Int) : Bool :=
-  null xs
-    || ofNat (length (tail xs)) == intSubNat (length xs) 1;
+  null 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);
+  case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs);
 
-prop-mergeSumLengths
-  (xs : List Int) (ys : List Int) : Bool :=
+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));
+    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-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;
+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;
+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;
+  QC.mkTest "partition: recombination of the output equals the input" prop-partition;
 
-testDistributive : QC.Test :=
-  QC.mkTest
-    "all functions are distributive over +"
-    prop-distributive;
+testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" prop-distributive;
 
-reverseLengthTest : QC.Test :=
-  QC.mkTest
-    "reverse preserves length"
-    prop-reverseDoesNotChangeLength;
+reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
-  QC.mkTest
-    "reverse of reverse is identity"
-    prop-reverseReverseIsIdentity;
+  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;
+  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;
+  QC.mkTest "tail: length of output is one less than input unless empty" prop-tailLengthOneLess;
 
 main : IO :=
   readLn

Package.juvix

@@ -3,8 +3,9 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "quickcheck";
-     version := mkVersion 0 12 0;
-     dependencies := [github "anoma" "juvix-stdlib" "v0.4.0"];
-     main := just "Example.juvix"};
+  defaultPackage@?{
+    name := "quickcheck";
+    version := mkVersion 0 13 0;
+    dependencies := [github "anoma" "juvix-stdlib" "v0.5.0"];
+    main := just "Example.juvix"
+  };

Test/QuickCheck.juvix

@@ -5,22 +5,16 @@ import Data.List open;
 import Data.Monoid open;
 import Data.Random open;
 import Test.QuickCheck.Property open public;
-import Test.QuickCheck.Result open public;
+import Test.QuickCheck.Outcome open public;
 import Test.QuickCheck.Testable open public;
 
-quickcheck
-  {Predicate : Type}
-  {{Testable Predicate}}
-  : Nat -> Nat -> Predicate -> Result
+quickcheck {Predicate : Type} {{Testable Predicate}} : Nat -> Nat -> Predicate -> Outcome
   | attemptNum startSeed predicate :=
     let
-      seeds : List Nat :=
-        map (n in range attemptNum)
-          startSeed + n;
-      runOne (prop : Property) (nextSeed : Nat) : Result :=
+      seeds : List Nat := map (n in range attemptNum) startSeed + n;
+      runOne (prop : Property) (nextSeed : Nat) : Outcome :=
         let
-          result : Result := runProp prop (mkStdGen nextSeed);
+          result : Outcome := runProp prop (mkStdGen nextSeed);
         in overFailure result \ {f := f@Failure{seed := nextSeed}};
-      runAll (prop : Property) : Result :=
-        foldMap monoidResult (runOne prop) seeds;
+      runAll (prop : Property) : Outcome := foldMap monoidOutcome (runOne prop) seeds;
     in runAll (Testable.toProp predicate);

Test/QuickCheck/Arbitrary.juvix

@@ -9,12 +9,10 @@ import Test.QuickCheck.CoArbitrary open;
 trait
 type Arbitrary (A : Type) := mkArbitrary {gen : Gen A};
 
-runArb {A} {{Arbitrary A}} (rand : StdGen) : A :=
-  Gen.run Arbitrary.gen rand;
+runArb {A} {{Arbitrary A}} (rand : StdGen) : A := Gen.run Arbitrary.gen rand;
 
 instance
-arbitraryNat : Arbitrary Nat :=
-  mkArbitrary (mkGen \ {rand := fst (stdNext rand)});
+arbitraryNat : Arbitrary Nat := mkArbitrary (mkGen \ {rand := fst (stdNext rand)});
 
 instance
 arbitraryInt : Arbitrary Int :=
@@ -28,8 +26,7 @@ arbitraryInt : Arbitrary Int :=
         in ite isPos (ofNat n) (negSuc n)});
 
 instance
-arbitraryBool : Arbitrary Bool :=
-  mkArbitrary (mkGen \ {rand := fst (randBool rand)});
+arbitraryBool : Arbitrary Bool := mkArbitrary (mkGen \ {rand := fst (randBool rand)});
 
 instance
 arbitraryList {A} {{Arbitrary A}} : Arbitrary (List A) :=
@@ -52,10 +49,33 @@ arbitraryList {A} {{Arbitrary A}} : Arbitrary (List A) :=
         in randList rand2 len});
 
 instance
-arbitraryFunction
-  {A B}
-  {{CoArbitrary A}}
-  {{Arbitrary B}}
-  : Arbitrary (A -> B) :=
+arbitraryFunction {A B} {{CoArbitrary A}} {{Arbitrary B}} : Arbitrary (A -> B) :=
+  mkArbitrary (promote (CoArbitrary.coarbitrary Arbitrary.gen));
+
+instance
+arbitraryMaybe {A} {{Arbitrary A}} : Arbitrary (Maybe A) :=
   mkArbitrary
-    (promote (CoArbitrary.coarbitrary Arbitrary.gen));
+    (mkGen
+      \ {rand :=
+        let
+          randSplit : Pair StdGen StdGen := stdSplit rand;
+          rand1 : StdGen := fst randSplit;
+          rand2 : StdGen := snd randSplit;
+          mkJust : Bool := fst (randBool rand1);
+        in if
+          | mkJust := Gen.run Arbitrary.gen rand2 |> just
+          | else := nothing});
+
+instance
+arbitraryResult {A B} {{Arbitrary A}} {{Arbitrary B}} : Arbitrary (Result A B) :=
+  mkArbitrary
+    (mkGen
+      \ {rand :=
+        let
+          randSplit : Pair StdGen StdGen := stdSplit rand;
+          rand1 : StdGen := fst randSplit;
+          rand2 : StdGen := snd randSplit;
+          mkError : Bool := fst (randBool rand1);
+        in if
+          | mkError := Gen.run Arbitrary.gen rand2 |> error
+          | else := Gen.run Arbitrary.gen rand2 |> ok});

Test/QuickCheck/CoArbitrary.juvix

@@ -6,11 +6,7 @@ import Test.QuickCheck.Gen open;
 
 -- | A perturbation of a generator associated with a type B
 trait
-type CoArbitrary (A : Type) :=
-  mkCoarbitrary {coarbitrary : {B : Type}
-    -> Gen B
-    -> A
-    -> Gen B};
+type CoArbitrary (A : Type) := mkCoarbitrary {coarbitrary : {B : Type} -> Gen B -> A -> Gen B};
 
 binaryDigits : Nat -> List Nat
   | n :=
@@ -29,22 +25,14 @@ perturb : Int -> StdGen -> StdGen
             splitG : Pair StdGen StdGen := stdSplit g;
           in ite b (snd splitG) (fst splitG);
       terminating
-      digitsParity : List Bool :=
-        map (x in binaryDigits (abs n))
-          x == 0;
-    in for (rand := vary
-           (n < ofNat 0)
-           rand0) (b in digitsParity)
+      digitsParity : List Bool := map (x in binaryDigits (abs n)) x == 0;
+    in for (rand := vary (n < ofNat 0) rand0) (b in digitsParity)
          vary b rand;
 
 instance
 coarbitraryInt : CoArbitrary Int :=
-  mkCoarbitrary
-    \ {g n := mkGen \ {rand := Gen.run g (perturb n rand)}};
+  mkCoarbitrary \ {g n := mkGen \ {rand := Gen.run g (perturb n rand)}};
 
 instance
 coarbitraryListInt : CoArbitrary (List Int) :=
-  mkCoarbitrary
-    \ {g xs :=
-      mkGen
-        \ {rand := Gen.run g (foldr perturb (perturb 0 rand) xs)}};
+  mkCoarbitrary \ {g xs := mkGen \ {rand := Gen.run g (foldr perturb (perturb 0 rand) xs)}};

Test/QuickCheck/Gen.juvix

@@ -1,10 +1,8 @@
 module Test.QuickCheck.Gen;
 
-import
-Data.Random open;
+import Data.Random open;
 
 --- A generator of values of type A
 type Gen (A : Type) := mkGen {run : StdGen -> A};
 
-promote {A B} (f : A -> Gen B) : Gen (A -> B) :=
-  mkGen \ {rand a := Gen.run (f a) rand};
+promote {A B} (f : A -> Gen B) : Gen (A -> B) := mkGen \ {rand a := Gen.run (f a) rand};