Update list functions to use traits

Stdlib/Data/List/Base.juvix

@@ -8,7 +8,6 @@ import Stdlib.Data.Nat.Base open;
 import Stdlib.Data.Maybe.Base open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Data.Product.Base open;
-import Stdlib.Trait.Ord open;
 
 syntax operator :: cons;
 --- Inductive list.
@@ -100,14 +99,15 @@ splitAt {A} : Nat → List A → List A × List A
     case splitAt m xs of {l1, l2 := x :: l1, l2};
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
-merge {A} : Ord A → List A → List A → List A
-  | o@(mkOrd cmp) (x :: xs) (y :: ys) :=
+terminating
+merge {A} {{Ord A}} : List A → List A → List A
+  | xs@(x :: xs') ys@(y :: ys') :=
     if
-      (isLT (cmp x y))
-      (x :: merge o xs (y :: ys))
-      (y :: merge o (x :: xs) ys)
-  | _ nil ys := ys
-  | _ xs nil := xs;
+      (isLT (Ord.cmp x y))
+      (x :: merge xs' ys)
+      (y :: merge xs ys')
+  | nil ys := ys
+  | xs nil := xs;
 
 --- 𝒪(𝓃). Returns a tuple where the first component has the items that
 --- satisfy the predicate and the second component has the elements that don't.
@@ -184,7 +184,7 @@ zip {A B} : List A -> List B -> List (A × B)
 
 --- 𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort
 --- algorithm.
-mergeSort {A} (o : Ord A) (l : List A) : List A :=
+mergeSort {A} {{Ord A}} (l : List A) : List A :=
   let
     terminating
     go : Nat -> List A -> List A
@@ -196,21 +196,20 @@ mergeSort {A} (o : Ord A) (l : List A) : List A :=
           splitXs : List A × List A := splitAt len' xs;
           left : List A := fst splitXs;
           right : List A := snd splitXs;
-        in merge o (go len' left) (go (sub len len') right);
+        in merge (go len' left) (go (sub len len') right);
   in go (length l) l;
 
 --- On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in
 --- ascending order using the QuickSort algorithm.
 terminating
-quickSort {A} : Ord A → List A → List A
-  | (mkOrd cmp) :=
+quickSort {A} {{Ord A}} : List A → List A :=
     let
       terminating
       go : List A → List A
         | nil := nil
         | xs@(_ :: nil) := xs
         | (x :: xs) :=
-          case partition (isGT ∘ cmp x) xs of {l1, l2 :=
+          case partition (isGT ∘ Ord.cmp x) xs of {l1, l2 :=
             go l1 ++ x :: go l2};
     in go;
 

test/Test.juvix

@@ -137,107 +137,86 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool
 sortTest : String -> (List Int -> List Int) -> QC.Test
   | sortName sort :=
     QC.mkTest
-      (QC.testableFunction QC.argumentListInt QC.testableBool)
       ("sort properties: " ++str sortName)
       (prop-sort sort);
 
 dropTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction
-      QC.argumentNat
-      (QC.testableFunction QC.argumentListInt QC.testableBool))
     "drop properties"
     prop-drop;
 
 snocTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction
-      QC.argumentListInt
-      (QC.testableFunction QC.argumentInt QC.testableBool))
     "snoc properties"
     prop-snoc;
 
 zipTest : QC.Test :=
   QC.mkTest
-    QC.testableListIntListInt
     "zip properties"
     prop-zip;
 
 zipWithTest : QC.Test :=
   QC.mkTest
-    QC.testableHofIntIntListIntListInt
     "zipWith properties"
     prop-zipWith;
 
 equalCompareToEqTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction QC.argumentNat QC.testableBool)
     "equal Nats compare to EQ"
     prop-equal-compare-to-eq;
 
 gcdNoCoprimeTest : QC.Test :=
   QC.mkTest
-    QC.testableBinaryInt
     "no integers are coprime"
     prop-gcd-bad;
 
 partitionTest : QC.Test :=
   QC.mkTest
-    QC.testableListIntHofIntBool
     "partition: recombination of the output equals the input"
     prop-partition;
 
 testDistributive : QC.Test :=
   QC.mkTest
-    QC.testableIntIntHofIntInt
     "all functions are distributive over +"
     prop-distributive;
 
 reverseLengthTest : QC.Test :=
   QC.mkTest
-    QC.testableListInt
     "reverse preserves length"
     prop-reverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
   QC.mkTest
-    QC.testableListInt
     "reverse of reverse is identity"
     prop-reverseReverseIsIdentity;
 
 splitAtRecombineTest : QC.Test :=
   QC.mkTest
-    QC.testableNatListInt
     "splitAt: recombination of the output is equal to the input list"
     prop-splitAtRecombine;
 
 splitAtLengthTest : QC.Test :=
   QC.mkTest
-    QC.testableNatListInt
     "splitAt: Check lengths of output if the input Nat is greater than the length of the input list"
     prop-splitAtLength;
 
 mergeSumLengthsTest : QC.Test :=
   QC.mkTest
-    QC.testableListIntListInt
     "merge: sum of the lengths of input lists is equal to the length of output list"
     prop-mergeSumLengths;
 
 tailLengthOneLessTest : QC.Test :=
   QC.mkTest
-    QC.testableListInt
     "tail: length of output is one less than input unless empty"
     prop-tailLengthOneLess;
 
 transposeMatrixIdTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction QC.argumentMatrixInt QC.testableBool)
     "transpose: recrangular matrix has property transpose . transpose = id"
     prop-transposeMatrixId;
 
 transposeMatrixDimentionsTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction QC.argumentMatrixInt QC.testableBool)
     "transpose: transpose swaps dimensions"
     prop-transposeMatrixDimensions;
 

test/Test/Arb.juvix

@@ -6,11 +6,10 @@ import Test.QuickCheck.Arbitrary open;
 import Test.QuickCheck.Gen open;
 import Data.Random open;
 
-arbitrarySizedList
-  : {A : Type} -> Nat -> Arbitrary A -> Arbitrary (List A)
-  | {A} size (arbitrary g) :=
-    arbitrary
-      (gen
+arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A)
+  | (mkArbitrary g) :=
+    mkArbitrary
+      (mkGen
         \ {rand :=
           let
             randList : StdGen -> Nat -> List A
@@ -20,23 +19,20 @@ arbitrarySizedList
                   rSplit : StdGen × StdGen := stdSplit r;
                   r1 : StdGen := fst rSplit;
                   r2 : StdGen := snd rSplit;
-                in runGen g r1 :: randList r2 n;
+                in Gen.run g r1 :: randList r2 n;
           in randList rand size});
 
 --- Generate an arbitrary rectangular matrix
-arbitraryMatrix
-  : {A : Type} -> Arbitrary A -> Arbitrary (List (List A))
-  | {A} arbA :=
-    arbitrary
-      (gen
+arbitraryMatrix {A} (arbA : Arbitrary A) : Arbitrary (List (List A)) :=
+    mkArbitrary
+      (mkGen
         \ {rand :=
           let
             randSplit : StdGen × StdGen := stdSplit rand;
             rand1 : StdGen := fst randSplit;
             rand2 : StdGen := snd randSplit;
             cols : Nat := fst (randNat rand1 1 10);
-            arbRow : Arbitrary (List A) := arbitrarySizedList cols arbA;
-          in runArb (arbitraryList arbRow) rand2});
+          in runArb rand2});
 
-argumentMatrixInt : Argument (List (List Int)) :=
-  argument showListI (arbitraryMatrix arbitraryInt);
+--argumentMatrixInt : Argument (List (List Int)) :=
+--  argument showListI (arbitraryMatrix arbitraryInt);

test/juvix.yaml

@@ -2,7 +2,7 @@ dependencies:
 - ../
 - git:
     url: https://github.com/anoma/juvix-quickcheck.git
-    ref: update-for-0.5.0
+    ref: main
     name: quickcheck
 name: stdlib-test
 version: 0.0.0