Update list functions to use traits (#82)

Co-authored-by: Paul Cadman <[email protected]>

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,23 +196,22 @@ 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) :=
-    let
-      terminating
-      go : List A → List A
-        | nil := nil
-        | xs@(_ :: nil) := xs
-        | (x :: xs) :=
-          case partition (isGT ∘ cmp x) xs of {l1, l2 :=
-            go l1 ++ x :: go l2};
-    in go;
+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 ∘ Ord.cmp x) xs of {l1, l2 :=
+          go l1 ++ x :: go l2};
+  in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
 catMaybes {A} : List (Maybe A) -> List A

test/Test.juvix

@@ -43,8 +43,7 @@ prop-splitAtLength : Nat -> List Int -> Bool
 
 prop-mergeSumLengths : List Int -> List Int -> Bool
   | xs ys :=
-    length xs Nat.+ length ys
-      Nat.== length (merge ordIntI xs ys);
+    length xs Nat.+ length ys Nat.== length (merge xs ys);
 
 prop-partition : List Int -> (Int -> Bool) -> Bool
   | xs p :=
@@ -137,109 +136,104 @@ 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);
+      (QC.mkFun (prop-sort sort));
 
 dropTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction
-      QC.argumentNat
-      (QC.testableFunction QC.argumentListInt QC.testableBool))
     "drop properties"
-    prop-drop;
+    (QC.mkFun \ {a := QC.mkFun \ {b := prop-drop a b}});
 
 snocTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction
-      QC.argumentListInt
-      (QC.testableFunction QC.argumentInt QC.testableBool))
     "snoc properties"
-    prop-snoc;
+    (QC.mkFun \ {a := QC.mkFun \ {b := prop-snoc a b}});
 
 zipTest : QC.Test :=
   QC.mkTest
-    QC.testableListIntListInt
     "zip properties"
-    prop-zip;
+    (QC.mkFun \ {a := QC.mkFun \ {b := prop-zip a b}});
 
 zipWithTest : QC.Test :=
   QC.mkTest
-    QC.testableHofIntIntListIntListInt
     "zipWith properties"
-    prop-zipWith;
+    (QC.mkFun
+      \ {a :=
+        QC.mkFun
+          \ {b :=
+            QC.mkFun
+              \ {c :=
+                prop-zipWith \ {x := QC.Fun.fun (QC.Fun.fun a x)} b c}}});
 
 equalCompareToEqTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction QC.argumentNat QC.testableBool)
     "equal Nats compare to EQ"
-    prop-equal-compare-to-eq;
+    (QC.mkFun prop-equal-compare-to-eq);
 
 gcdNoCoprimeTest : QC.Test :=
   QC.mkTest
-    QC.testableBinaryInt
     "no integers are coprime"
-    prop-gcd-bad;
+    (QC.mkFun \ {a := QC.mkFun \ {b := prop-gcd-bad a b}});
 
 partitionTest : QC.Test :=
   QC.mkTest
-    QC.testableListIntHofIntBool
     "partition: recombination of the output equals the input"
-    prop-partition;
+    (QC.mkFun
+      \ {a := QC.mkFun \ {b := prop-partition a (QC.Fun.fun b)}});
 
 testDistributive : QC.Test :=
   QC.mkTest
-    QC.testableIntIntHofIntInt
     "all functions are distributive over +"
-    prop-distributive;
+    (QC.mkFun
+      \ {a :=
+        QC.mkFun
+          \ {b :=
+            QC.mkFun \ {c := prop-distributive a b (QC.Fun.fun c)}}});
 
 reverseLengthTest : QC.Test :=
   QC.mkTest
-    QC.testableListInt
     "reverse preserves length"
-    prop-reverseDoesNotChangeLength;
+    (QC.mkFun prop-reverseDoesNotChangeLength);
 
 reverseReverseIdTest : QC.Test :=
   QC.mkTest
-    QC.testableListInt
     "reverse of reverse is identity"
-    prop-reverseReverseIsIdentity;
+    (QC.mkFun prop-reverseReverseIsIdentity);
 
 splitAtRecombineTest : QC.Test :=
   QC.mkTest
-    QC.testableNatListInt
     "splitAt: recombination of the output is equal to the input list"
-    prop-splitAtRecombine;
+    (QC.mkFun
+      \ {a := QC.mkFun \ {b := prop-splitAtRecombine a b}});
 
 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;
+    (QC.mkFun
+      \ {a := QC.mkFun \ {b := prop-splitAtLength a b}});
 
 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;
+    (QC.mkFun
+      \ {a := QC.mkFun \ {b := prop-mergeSumLengths a b}});
 
 tailLengthOneLessTest : QC.Test :=
   QC.mkTest
-    QC.testableListInt
     "tail: length of output is one less than input unless empty"
-    prop-tailLengthOneLess;
+    (QC.mkFun prop-tailLengthOneLess);
 
 transposeMatrixIdTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction QC.argumentMatrixInt QC.testableBool)
+    {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}}
     "transpose: recrangular matrix has property transpose . transpose = id"
-    prop-transposeMatrixId;
+    (QC.mkFun prop-transposeMatrixId);
 
 transposeMatrixDimentionsTest : QC.Test :=
   QC.mkTest
-    (QC.testableFunction QC.argumentMatrixInt QC.testableBool)
+    {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}}
     "transpose: transpose swaps dimensions"
-    prop-transposeMatrixDimensions;
+    (QC.mkFun prop-transposeMatrixDimensions);
 
 main : IO :=
   readLn
@@ -259,8 +253,8 @@ main : IO :=
           :: zipWithTest
           :: snocTest
           :: dropTest
-          :: sortTest "mergeSort" (mergeSort ordIntI)
-          :: sortTest "quickSort" (quickSort ordIntI)
+          :: sortTest "mergeSort" mergeSort
+          :: sortTest "quickSort" quickSort
           :: transposeMatrixIdTest
           :: transposeMatrixDimentionsTest
           :: nil)};

test/Test/Arb.juvix

@@ -6,11 +6,11 @@ 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 +20,19 @@ 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
-        \ {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});
-
-argumentMatrixInt : Argument (List (List Int)) :=
-  argument showListI (arbitraryMatrix arbitraryInt);
+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});

test/juvix.yaml

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