Skip to content

Commit

Permalink
Update for Juvix v0.6.0 (#11)
Browse files Browse the repository at this point in the history
* Update the juvix-stdlib

* Format the project

* Update stdlib and format
  • Loading branch information
paulcadman authored Mar 1, 2024
1 parent 37ddfcf commit dc0d389
Show file tree
Hide file tree
Showing 8 changed files with 40 additions and 21 deletions.
9 changes: 5 additions & 4 deletions Example.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ prop-splitAtRecombine (n : Nat) (xs : List Int) : Bool :=
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 :=
Expand All @@ -35,8 +35,9 @@ prop-partition (xs : List Int) (p : Int -> Bool) : Bool :=
&& 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;

Expand Down
7 changes: 4 additions & 3 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
JUVIX_CMD=juvix

all: run-quickcheck

build/Random: Data/Random.juvix
juvix compile Data/Random.juvix -o build/Random
${JUVIX_CMD} compile Data/Random.juvix -o build/Random

build/Example: $(wildcard ./**/*.juvix) Example.juvix
@mkdir -p build
juvix compile Example.juvix -o build/Example
${JUVIX_CMD} compile Example.juvix -o build/Example

.PHONY: run-random
run-random: build/Random
Expand All @@ -22,7 +23,7 @@ clean-build:

.PHONY: clean-deps
clean-deps:
juvix clean
${JUVIX_CMD} clean

.PHONY: clean
clean: clean-deps clean-build
7 changes: 3 additions & 4 deletions Package.juvix
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
module Package;

import Stdlib.Prelude open;
import PackageDescription.V1 open;
import PackageDescription.V2 open;

package : Package :=
defaultPackage
{name := "quickcheck";
version := mkVersion 0 9 0;
dependencies := [github "anoma" "juvix-stdlib" "v0.0.1"];
version := mkVersion 0 10 0;
dependencies := [github "anoma" "juvix-stdlib" "v0.2.0"];
main := just "Example.juvix"};
4 changes: 3 additions & 1 deletion Test/QuickCheck.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ import Test.QuickCheck.Property open public;
import Test.QuickCheck.Result open public;
import Test.QuickCheck.Testable open public;

quickcheck {Predicate : Type} {{Testable Predicate}}
quickcheck
{Predicate : Type}
{{Testable Predicate}}
: Nat -> Nat -> Predicate -> Result
| attemptNum startSeed predicate :=
let
Expand Down
5 changes: 4 additions & 1 deletion Test/QuickCheck/Arbitrary.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,10 @@ arbitraryList {A} {{Arbitrary A}} : Arbitrary (List A) :=
in randList rand2 len});

instance
arbitraryFunction {A B} {{CoArbitrary A}} {{Arbitrary B}}
arbitraryFunction
{A B}
{{CoArbitrary A}}
{{Arbitrary B}}
: Arbitrary (A -> B) :=
mkArbitrary
(promote (CoArbitrary.coarbitrary Arbitrary.gen));
16 changes: 12 additions & 4 deletions Test/QuickCheck/Testable.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,12 @@ trait
type Testable (A : Type) :=
mkTestable {toProp : A -> Property};

forAll {A T : Type} {{Show A}} {{Arbitrary A}} {{Testable
T}} : (A -> T) -> Property
forAll
{A T : Type}
{{Show A}}
{{Arbitrary A}}
{{Testable T}}
: (A -> T) -> Property
| prop :=
mkProperty
(mkGen
Expand Down Expand Up @@ -47,8 +51,12 @@ testableBool : Testable Bool :=
in mkTestable \ {b := Testable.toProp (toResult b)};

instance
testableFunction {A T} {{Show A}} {{Arbitrary A}} {{Testable
T}} : Testable (A -> T) := mkTestable \ {f := forAll f};
testableFunction
{A T}
{{Show A}}
{{Arbitrary A}}
{{Testable T}}
: Testable (A -> T) := mkTestable \ {f := forAll f};

instance
showableFunction {A B : Type} : Show (A -> B) :=
Expand Down
7 changes: 5 additions & 2 deletions Test/QuickCheckTest.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,11 @@ type Test :=
property : Property
};

mkTest {Predicate : Type} {{Testable
Predicate}} (name : String) (predicate : Predicate)
mkTest
{Predicate : Type}
{{Testable Predicate}}
(name : String)
(predicate : Predicate)
: Test := test name (Testable.toProp predicate);

type TestResult :=
Expand Down
6 changes: 4 additions & 2 deletions juvix.lock.yaml
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
# This file was autogenerated by Juvix version 0.5.4.
# This file was autogenerated by Juvix version 0.6.0.
# Do not edit this file manually.

version: 2
checksum: beb38798792b395019addc1f9636e981c2bde42b9b6fdc2ac6b7a455509a4ae5
dependencies:
- git:
name: anoma_juvix-stdlib
ref: f68b0614ad695eaa13ead42f3466e0a78219f826
ref: e2efe4e6fe8e8bf1766050a7fa7ad8ff4e8c69fc
url: https://github.com/anoma/juvix-stdlib
dependencies: []

0 comments on commit dc0d389

Please sign in to comment.