Update for compatibility with Juvix 0.6.3 (#14)

* Replace Product with Pair

* Fix reference to stdlib

* Update to latest stdlib

* Update stdlib, if -> ite

Data/List.juvix

@@ -17,8 +17,8 @@ unzipWith
     -> {B : Type}
     -> {C : Type}
     -> (A -> B -> C)
-    -> List (A × B)
-    -> List C := map ∘ uncurry;
+    -> List (Pair A B)
+    -> List C := map << uncurry;
 
 range : Nat -> List Nat
   | n := rangeStep 1 n;

Data/Monoid.juvix

@@ -12,7 +12,8 @@ foldMap
     -> (A -> M)
     -> List A
     -> M
-  | (monoid mempty mappend) f := foldr (mappend ∘ f) mempty;
+  | (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

@@ -32,9 +32,9 @@ mkStdGen : Nat -> StdGen
       s3 : Nat := mod q2 k3;
     in stdGen (s1 + 1) (s2 + 1) (s3 + 1);
 
-stdRange : Nat × Nat := 1, k1;
+stdRange : Pair Nat Nat := 1, k1;
 
-stdNext : StdGen -> Nat × StdGen
+stdNext : StdGen -> Pair Nat StdGen
   | (stdGen s1Nat s2Nat s3Nat) :=
     let
       s1 : Int := ofNat s1Nat;
@@ -43,27 +43,27 @@ stdNext : StdGen -> Nat × StdGen
       k : Int := div s1 (ofNat 206);
       s1' : Int :=
         ofNat 157 * (s1 - k * ofNat 206) - k * ofNat 21;
-      s1'' : Int := if (s1' < ofNat 0) (s1' + ofNat 32363) s1';
+      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 := if (s2' < ofNat 0) (s2' + ofNat 31727) s2';
+      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 := if (s2' < ofNat 0) (s2' + ofNat 31657) s3';
+      s3'' : Int := ite (s2' < ofNat 0) (s2' + ofNat 31657) s3';
       z : Int := s1'' - s2'';
-      z' : Int := if (z > ofNat 706) (z - ofNat 32362) z;
+      z' : Int := ite (z > ofNat 706) (z - ofNat 32362) z;
       z'' : Int :=
-        if (z' < ofNat 1) (z' + ofNat 32362) (mod z (ofNat k1));
+        ite (z' < ofNat 1) (z' + ofNat 32362) (mod z (ofNat k1));
     in toNat z'', stdGen (toNat s1'') (toNat s2'') (toNat s3'');
 
-stdSplit : StdGen -> StdGen × StdGen
+stdSplit : StdGen -> Pair StdGen StdGen
   | g@(stdGen s1 s2 s3) :=
     let
-      newS1 : Nat := if (s1 == k1) 1 (s1 + 1);
-      newS2 : Nat := if (s2 == 1) k2 (sub s2 1);
-      newS3 : Nat := if (s3 == k3) 1 (s3 + 1);
+      newS1 : Nat := ite (s1 == k1) 1 (s1 + 1);
+      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);
@@ -75,21 +75,21 @@ randNatAux
     -> Nat
     -> Nat
     -> Nat
-    -> Nat × StdGen
-    -> Nat × StdGen
+    -> Pair Nat StdGen
+    -> Pair Nat StdGen
   | g genLo genMag :=
     let
       terminating
-      go : Nat -> Nat × StdGen -> Nat × StdGen
+      go : Nat -> Pair Nat StdGen -> Pair Nat StdGen
         | zero p@(v, g) := p
         | r'@(suc _) (v, g) :=
           let
-            n : Nat × StdGen := stdNext g;
+            n : Pair Nat StdGen := stdNext g;
             v' : Nat := v * genMag + sub (fst n) genLo;
           in go (div r' (sub genMag 1)) (v', snd n);
     in go;
 
-randNat : StdGen -> Nat -> Nat -> Nat × StdGen
+randNat : StdGen -> Nat -> Nat -> Pair Nat StdGen
   | g lo hi :=
     let
       genLo : Nat := fst stdRange;
@@ -98,27 +98,28 @@ randNat : StdGen -> Nat -> Nat -> Nat × StdGen
       q : Nat := 1000;
       k : Nat := sub hi lo + 1;
       tgtMag : Nat := k * q;
-      x : 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;
     in v', g';
 
-randBool : StdGen -> Bool × StdGen
+randBool : StdGen -> Pair Bool StdGen
   | g :=
     let
-      x : Nat × StdGen := randNat g 0 1;
+      x : Pair Nat StdGen := randNat g 0 1;
       b : Bool := fst x == 1;
     in b, snd x;
 
 run : Nat -> StdGen -> IO
   | zero _ := printString ""
   | (suc n) g :=
     let
-      next : Nat × StdGen := randNat g 0 100;
+      next : Pair Nat StdGen := randNat g 0 100;
       b : Nat := fst next;
       g' : StdGen := snd next;
-    in printNatLn b >> run n g';
+    in printNatLn b >>> run n g';
 
 main : IO :=
   let

Example.juvix

@@ -19,21 +19,19 @@ prop-tailLengthOneLess (xs : List Int) : Bool :=
     || 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 :=
   length xs + length ys == length (merge {{ordIntI}} xs ys);
 
 prop-partition (xs : List Int) (p : Int -> Bool) : Bool :=
-  case partition p xs of {
+  case partition p xs of
     lhs, rhs :=
       all p lhs
         && not (any p rhs)
-        && eqListInt (sortInt xs) (sortInt (lhs ++ rhs))
-  };
+        && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
 
 prop-distributive
   (a : Int) (b : Int) (f : Int -> Int) : Bool :=

Package.juvix

@@ -5,6 +5,6 @@ import PackageDescription.V2 open;
 package : Package :=
   defaultPackage
     {name := "quickcheck";
-     version := mkVersion 0 11 0;
-     dependencies := [github "anoma" "juvix-stdlib" "v0.3.0"];
+     version := mkVersion 0 12 0;
+     dependencies := [github "anoma" "juvix-stdlib" "v0.4.0"];
      main := just "Example.juvix"};

Test/QuickCheck/Arbitrary.juvix

@@ -22,10 +22,10 @@ arbitraryInt : Arbitrary Int :=
     (mkGen
       \ {rand :=
         let
-          runRand : Nat × StdGen := stdNext rand;
+          runRand : Pair Nat StdGen := stdNext rand;
           n : Nat := fst runRand;
           isPos : Bool := fst (randBool (snd runRand));
-        in if isPos (ofNat n) (negSuc n)});
+        in ite isPos (ofNat n) (negSuc n)});
 
 instance
 arbitraryBool : Arbitrary Bool :=
@@ -37,15 +37,15 @@ arbitraryList {A} {{Arbitrary A}} : Arbitrary (List A) :=
     (mkGen
       \ {rand :=
         let
-          randSplit : StdGen × StdGen := stdSplit rand;
+          randSplit : Pair StdGen StdGen := stdSplit rand;
           rand1 : StdGen := fst randSplit;
           rand2 : StdGen := snd randSplit;
           len : Nat := fst (randNat rand1 0 10);
           randList : StdGen -> Nat -> List A
             | _ zero := nil
             | r (suc n) :=
               let
-                rSplit : StdGen × StdGen := stdSplit r;
+                rSplit : Pair StdGen StdGen := stdSplit r;
                 r1 : StdGen := fst rSplit;
                 r2 : StdGen := snd rSplit;
               in Gen.run Arbitrary.gen r1 :: randList r2 n;

Test/QuickCheck/CoArbitrary.juvix

@@ -17,7 +17,7 @@ binaryDigits : Nat -> List Nat
     let
       terminating
       go : Nat -> List Nat
-        | n := if (n == 0) nil (mod n 2 :: go (div n 2));
+        | n := ite (n == 0) nil (mod n 2 :: go (div n 2));
     in reverse (go n);
 
 perturb : Int -> StdGen -> StdGen
@@ -26,8 +26,8 @@ perturb : Int -> StdGen -> StdGen
       vary : Bool -> StdGen -> StdGen
         | b g :=
           let
-            splitG : StdGen × StdGen := stdSplit g;
-          in if b (snd splitG) (fst splitG);
+            splitG : Pair StdGen StdGen := stdSplit g;
+          in ite b (snd splitG) (fst splitG);
       terminating
       digitsParity : List Bool :=
         map (x in binaryDigits (abs n))

Test/QuickCheck/Gen.juvix

@@ -1,6 +1,7 @@
 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};

Test/QuickCheck/Result.juvix

@@ -44,4 +44,4 @@ overFailure : Result -> (Failure -> Failure) -> Result
   | (failure x) f := failure (f x);
 
 allSuccess : List Result -> Bool :=
-  isSuccess ∘ foldMap monoidResult id;
+  isSuccess << foldMap monoidResult id;

Test/QuickCheck/Testable.juvix

@@ -24,7 +24,7 @@ forAll
       (mkGen
         \ {rand :=
           let
-            srand : StdGen × StdGen := stdSplit rand;
+            srand : Pair StdGen StdGen := stdSplit rand;
             rand1 : StdGen := fst srand;
             rand2 : StdGen := snd srand;
             arg : A := Gen.run Arbitrary.gen rand1;
@@ -47,7 +47,7 @@ instance
 testableBool : Testable Bool :=
   let
     toResult : Bool -> Result
-      | b := if b success (failure (mkFailure 0 nil));
+      | b := ite b success (failure (mkFailure 0 nil));
   in mkTestable \ {b := Testable.toProp (toResult b)};
 
 instance

Test/QuickCheckTest.juvix

@@ -55,7 +55,7 @@ runTestsIO : Nat -> Nat -> List Test -> IO
       results : List TestResult :=
         runTests attemptNum startSeed ts;
     in printStringLn (lines (map showTestResult results))
-      >> if
+      >>> ite
         (allTestSuccess results)
         (printStringLn "All tests passed")
         (Fail.failwith "Test failed");

juvix.lock.yaml

@@ -1,11 +1,11 @@
-# This file was autogenerated by Juvix version 0.6.2.
+# This file was autogenerated by Juvix version 0.6.3.
 # Do not edit this file manually.
 
 version: 2
-checksum: e08a891c59e8056374e088c49ec9e7c7f45d95d21f5685ee37e09d87f5580614
+checksum: c075caa88ab9043a8d5bc5324401e27c67922a3004807c82b031b002e5336c6a
 dependencies:
 - git:
     name: anoma_juvix-stdlib
-    ref: 73ecbc57738f4bde6f4f39636436ba38504b33f6
+    ref: 89a5960fb8a29291e9271986b98ca7b1edf4031b
     url: https://github.com/anoma/juvix-stdlib
   dependencies: []