From 29edc0838a3bfab1a71c75dbd80c547b7c827ee9 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 13:26:49 +0200 Subject: [PATCH 1/9] use traits in list functions --- Stdlib/Data/List/Base.juvix | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 4a8f069d..768585d1 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/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 + | (x :: xs) (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 (y :: ys)) + (y :: merge (x :: 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; From c96a24646bf6c73772d4923cb9ece22527a52973 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 13:41:57 +0200 Subject: [PATCH 2/9] fix merge --- Stdlib/Data/List/Base.juvix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 768585d1..dd78501b 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -101,11 +101,11 @@ splitAt {A} : Nat → List A → List A × List A --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering. terminating merge {A} {{Ord A}} : List A → List A → List A - | (x :: xs) (y :: ys) := + | xs@(x :: xs') ys@(y :: ys') := if (isLT (Ord.cmp x y)) - (x :: merge xs (y :: ys)) - (y :: merge (x :: xs) ys) + (x :: merge xs' ys) + (y :: merge xs ys') | nil ys := ys | xs nil := xs; From a2f7bdd031be7d46bb9bc1d31f53cd087eb9dbe0 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 13:55:54 +0200 Subject: [PATCH 3/9] update test --- test/Test.juvix | 21 --------------------- test/Test/Arb.juvix | 26 +++++++++++--------------- test/juvix.yaml | 2 +- 3 files changed, 12 insertions(+), 37 deletions(-) diff --git a/test/Test.juvix b/test/Test.juvix index 748a12ec..fa772616 100644 --- a/test/Test.juvix +++ b/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; diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix index 5980356f..81a0d4e3 100644 --- a/test/Test/Arb.juvix +++ b/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); diff --git a/test/juvix.yaml b/test/juvix.yaml index 31618b1e..b109baac 100644 --- a/test/juvix.yaml +++ b/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 From ad27db542e0b220e117dec22f11ed6de78892f72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Fri, 22 Sep 2023 14:13:24 +0200 Subject: [PATCH 4/9] Update test/juvix.yaml Co-authored-by: Paul Cadman --- test/juvix.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/juvix.yaml b/test/juvix.yaml index b109baac..1c229e06 100644 --- a/test/juvix.yaml +++ b/test/juvix.yaml @@ -2,7 +2,7 @@ dependencies: - ../ - git: url: https://github.com/anoma/juvix-quickcheck.git - ref: main + ref: v0.7.0 name: quickcheck name: stdlib-test version: 0.0.0 From 5ba76985c57f07ad77c95f6e9a64459dcc7959cf Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 16:02:31 +0200 Subject: [PATCH 5/9] fix --- test/Test.juvix | 2 +- test/Test/Arb.juvix | 15 --------------- 2 files changed, 1 insertion(+), 16 deletions(-) diff --git a/test/Test.juvix b/test/Test.juvix index fa772616..f768e0ba 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -44,7 +44,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); + Nat.== length (merge xs ys); prop-partition : List Int -> (Int -> Bool) -> Bool | xs p := diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix index 81a0d4e3..49852305 100644 --- a/test/Test/Arb.juvix +++ b/test/Test/Arb.juvix @@ -21,18 +21,3 @@ arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A) r2 : StdGen := snd rSplit; in Gen.run g r1 :: randList r2 n; in randList rand size}); - ---- Generate an arbitrary rectangular matrix -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); - in runArb rand2}); - ---argumentMatrixInt : Argument (List (List Int)) := --- argument showListI (arbitraryMatrix arbitraryInt); From 93342aa0a5d4b73f9dcd18261f8d69b2a97770a9 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 17:30:46 +0200 Subject: [PATCH 6/9] fix test --- test/Test.juvix | 40 +++++++++++++++++++++------------------- test/Test/Arb.juvix | 13 +++++++++++++ test/juvix.yaml | 2 +- 3 files changed, 35 insertions(+), 20 deletions(-) diff --git a/test/Test.juvix b/test/Test.juvix index f768e0ba..df828761 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -138,87 +138,89 @@ sortTest : String -> (List Int -> List Int) -> QC.Test | sortName sort := QC.mkTest ("sort properties: " ++str sortName) - (prop-sort sort); + (QC.mkFun (prop-sort sort)); dropTest : QC.Test := QC.mkTest "drop properties" - prop-drop; + (QC.mkFun \ { a := QC.mkFun \ { b := prop-drop a b }}); snocTest : QC.Test := QC.mkTest "snoc properties" - prop-snoc; + (QC.mkFun \ { a := QC.mkFun \ { b := prop-snoc a b }}); zipTest : QC.Test := QC.mkTest "zip properties" - prop-zip; + (QC.mkFun \ { a := QC.mkFun \ { b := prop-zip a b }}); zipWithTest : QC.Test := QC.mkTest "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 "equal Nats compare to EQ" - prop-equal-compare-to-eq; + (QC.mkFun prop-equal-compare-to-eq); gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" - prop-gcd-bad; + (QC.mkFun \ { a := QC.mkFun \ { b := prop-gcd-bad a b }}); partitionTest : QC.Test := QC.mkTest "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 "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 "reverse preserves length" - prop-reverseDoesNotChangeLength; + (QC.mkFun prop-reverseDoesNotChangeLength); reverseReverseIdTest : QC.Test := QC.mkTest "reverse of reverse is identity" - prop-reverseReverseIsIdentity; + (QC.mkFun prop-reverseReverseIsIdentity); splitAtRecombineTest : QC.Test := QC.mkTest "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 "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 "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 "tail: length of output is one less than input unless empty" - prop-tailLengthOneLess; + (QC.mkFun prop-tailLengthOneLess); transposeMatrixIdTest : QC.Test := QC.mkTest + {{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 {{showListI}} {{QC.arbitraryMatrix}}}} "transpose: transpose swaps dimensions" - prop-transposeMatrixDimensions; + (QC.mkFun prop-transposeMatrixDimensions); main : IO := readLn @@ -238,8 +240,8 @@ main : IO := :: zipWithTest :: snocTest :: dropTest - :: sortTest "mergeSort" (mergeSort ordIntI) - :: sortTest "quickSort" (quickSort ordIntI) + :: sortTest "mergeSort" mergeSort + :: sortTest "quickSort" quickSort :: transposeMatrixIdTest :: transposeMatrixDimentionsTest :: nil)}; diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix index 49852305..68d25f45 100644 --- a/test/Test/Arb.juvix +++ b/test/Test/Arb.juvix @@ -21,3 +21,16 @@ arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A) r2 : StdGen := snd rSplit; in Gen.run g r1 :: randList r2 n; in randList rand size}); + +--- Generate an arbitrary rectangular matrix +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}); diff --git a/test/juvix.yaml b/test/juvix.yaml index 1c229e06..e993e545 100644 --- a/test/juvix.yaml +++ b/test/juvix.yaml @@ -2,7 +2,7 @@ dependencies: - ../ - git: url: https://github.com/anoma/juvix-quickcheck.git - ref: v0.7.0 + ref: 23c12c794bb425bd475a372ac0350feaf74eaf34 name: quickcheck name: stdlib-test version: 0.0.0 From 749ea1f2466af709deddda0992fb1bd9bb6ba0d4 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 18:04:40 +0200 Subject: [PATCH 7/9] fix formatting --- Stdlib/Data/List/Base.juvix | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index dd78501b..47acb4f2 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -203,15 +203,15 @@ mergeSort {A} {{Ord A}} (l : List A) : List A := --- ascending order using the QuickSort algorithm. terminating 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; + 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 From 21864b09d26d1af3f7ff0ce44c3ac46fc466d434 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 22 Sep 2023 18:49:38 +0200 Subject: [PATCH 8/9] fix formatting --- test/Test.juvix | 37 +++++++++++++++++++++++++------------ test/Test/Arb.juvix | 26 ++++++++++++++------------ 2 files changed, 39 insertions(+), 24 deletions(-) diff --git a/test/Test.juvix b/test/Test.juvix index df828761..587611f3 100644 --- a/test/Test.juvix +++ b/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 xs ys); + length xs Nat.+ length ys Nat.== length (merge xs ys); prop-partition : List Int -> (Int -> Bool) -> Bool | xs p := @@ -143,22 +142,28 @@ sortTest : String -> (List Int -> List Int) -> QC.Test dropTest : QC.Test := QC.mkTest "drop properties" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-drop a b }}); + (QC.mkFun \ {a := QC.mkFun \ {b := prop-drop a b}}); snocTest : QC.Test := QC.mkTest "snoc properties" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-snoc a b }}); + (QC.mkFun \ {a := QC.mkFun \ {b := prop-snoc a b}}); zipTest : QC.Test := QC.mkTest "zip properties" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-zip a b }}); + (QC.mkFun \ {a := QC.mkFun \ {b := prop-zip a b}}); zipWithTest : QC.Test := QC.mkTest "zipWith properties" - (QC.mkFun \ { a := QC.mkFun \ { b := QC.mkFun \ { c := prop-zipWith (\ {x := QC.Fun.fun (QC.Fun.fun a x)}) b c }}}); + (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 @@ -168,17 +173,22 @@ equalCompareToEqTest : QC.Test := gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-gcd-bad a b }}); + (QC.mkFun \ {a := QC.mkFun \ {b := prop-gcd-bad a b}}); partitionTest : QC.Test := QC.mkTest "partition: recombination of the output equals the input" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-partition a (QC.Fun.fun b)}}); + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-partition a (QC.Fun.fun b)}}); testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" - (QC.mkFun \ { a := QC.mkFun \ { b := QC.mkFun \ { c := prop-distributive a b (QC.Fun.fun c) }}}); + (QC.mkFun + \ {a := + QC.mkFun + \ {b := + QC.mkFun \ {c := prop-distributive a b (QC.Fun.fun c)}}}); reverseLengthTest : QC.Test := QC.mkTest @@ -193,17 +203,20 @@ reverseReverseIdTest : QC.Test := splitAtRecombineTest : QC.Test := QC.mkTest "splitAt: recombination of the output is equal to the input list" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-splitAtRecombine a b }}); + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-splitAtRecombine a b}}); splitAtLengthTest : QC.Test := QC.mkTest "splitAt: Check lengths of output if the input Nat is greater than the length of the input list" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-splitAtLength a b }}); + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-splitAtLength a b}}); mergeSumLengthsTest : QC.Test := QC.mkTest "merge: sum of the lengths of input lists is equal to the length of output list" - (QC.mkFun \ { a := QC.mkFun \ { b := prop-mergeSumLengths a b }}); + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-mergeSumLengths a b}}); tailLengthOneLessTest : QC.Test := QC.mkTest diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix index 68d25f45..cf9f3966 100644 --- a/test/Test/Arb.juvix +++ b/test/Test/Arb.juvix @@ -6,7 +6,8 @@ import Test.QuickCheck.Arbitrary open; import Test.QuickCheck.Gen open; import Data.Random open; -arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A) +arbitrarySizedList {A} (size : Nat) + : Arbitrary A -> Arbitrary (List A) | (mkArbitrary g) := mkArbitrary (mkGen @@ -23,14 +24,15 @@ arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A) in randList rand size}); --- Generate an arbitrary rectangular matrix -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}); +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}); From fcdb5c650b501d48e5406406cc6bee9b120bd80d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 25 Sep 2023 08:49:16 +0100 Subject: [PATCH 9/9] Use tag ref for test/quickcheck dependency --- test/juvix.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/juvix.yaml b/test/juvix.yaml index e993e545..414a0c9f 100644 --- a/test/juvix.yaml +++ b/test/juvix.yaml @@ -2,7 +2,7 @@ dependencies: - ../ - git: url: https://github.com/anoma/juvix-quickcheck.git - ref: 23c12c794bb425bd475a372ac0350feaf74eaf34 + ref: v0.7.1 name: quickcheck name: stdlib-test version: 0.0.0