From ff351799c068e7b3e23dd903547d228dc30aff5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Fri, 11 Oct 2024 19:09:50 +0200 Subject: [PATCH] Update the coding style according to the guidelines (#126) * Depends on #125 --------- Co-authored-by: Paul Cadman --- Stdlib/Cairo/Ec.juvix | 108 ++++---- Stdlib/Cairo/Poseidon.juvix | 4 +- Stdlib/Data/BinaryTree.juvix | 18 +- Stdlib/Data/Bool.juvix | 41 +-- Stdlib/Data/Bool/Base.juvix | 8 +- Stdlib/Data/Byte.juvix | 2 +- Stdlib/Data/Int/Base.juvix | 14 +- Stdlib/Data/Int/Ord.juvix | 8 +- Stdlib/Data/List.juvix | 27 +- Stdlib/Data/List/Base.juvix | 167 ++++++------ Stdlib/Data/Map.juvix | 46 ++-- Stdlib/Data/Maybe.juvix | 54 ++-- Stdlib/Data/Maybe/Base.juvix | 21 +- Stdlib/Data/Nat/Ord.juvix | 22 +- Stdlib/Data/Pair.juvix | 29 ++- Stdlib/Data/Pair/Base.juvix | 31 +-- Stdlib/Data/Queue/Base.juvix | 58 +++-- Stdlib/Data/Range.juvix | 20 +- Stdlib/Data/Result.juvix | 53 ++-- Stdlib/Data/Result/Base.juvix | 78 +++--- Stdlib/Data/Set/AVL.juvix | 274 +++++++++++--------- Stdlib/Data/String/Base.juvix | 4 +- Stdlib/Data/String/Ord.juvix | 2 +- Stdlib/Data/Tree.juvix | 34 +-- Stdlib/Data/UnbalancedSet.juvix | 76 +++--- Stdlib/Data/Unit.juvix | 22 +- Stdlib/Debug/Fail.juvix | 4 +- Stdlib/Debug/Trace.juvix | 2 +- Stdlib/Extra/Gcd.juvix | 11 +- Stdlib/Function.juvix | 25 +- Stdlib/System/IO/Base.juvix | 2 +- Stdlib/System/IO/Bool.juvix | 2 +- Stdlib/System/IO/Int.juvix | 2 +- Stdlib/System/IO/Nat.juvix | 2 +- Stdlib/System/IO/String.juvix | 4 +- Stdlib/Trait/Applicative.juvix | 16 +- Stdlib/Trait/Eq.juvix | 2 +- Stdlib/Trait/Foldable/Monomorphic.juvix | 34 +-- Stdlib/Trait/Foldable/Polymorphic.juvix | 26 +- Stdlib/Trait/Functor/Monomorphic.juvix | 21 +- Stdlib/Trait/Functor/Polymorphic.juvix | 10 +- Stdlib/Trait/Monad.juvix | 10 +- Stdlib/Trait/Ord.juvix | 58 +++-- Stdlib/Trait/Ord/Eq.juvix | 2 +- test/Package.juvix | 4 +- test/Test.juvix | 322 ++++++++++++------------ test/Test/AVL.juvix | 56 ++--- test/Test/Arb.juvix | 31 +-- test/Test/Map.juvix | 4 +- test/Test/Queue.juvix | 4 +- test/Test/UnbalancedSet.juvix | 6 +- test/juvix.lock.yaml | 10 +- 52 files changed, 1038 insertions(+), 853 deletions(-) diff --git a/Stdlib/Cairo/Ec.juvix b/Stdlib/Cairo/Ec.juvix index fcf44b71..a3de922d 100644 --- a/Stdlib/Cairo/Ec.juvix +++ b/Stdlib/Cairo/Ec.juvix @@ -8,6 +8,7 @@ module Stdlib.Cairo.Ec; import Stdlib.Data.Field open; import Stdlib.Data.Bool open; +import Stdlib.Data.Pair open; module StarkCurve; ALPHA : Field := 1; @@ -37,77 +38,80 @@ module Internal; end; --- Checks if an EC point is on the STARK curve. -isOnCurve : Point -> Bool - | (mkPoint x y) := - if - | y == 0 := x == 0 - | else := y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA; - ---- Doubles a valid point p (computes p + p) on the elliptic curve. -double : Point -> Point - | p@(mkPoint x y) := - if - | y == 0 := p - | else := - let - slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y); - r_x := slope * slope - x - x; - r_y := slope * (x - r_x) - y; - in mkPoint@?{ - x := r_x; - y := r_y - }; +isOnCurve (point : Point) : Bool := + case point of + mkPoint x y := + if + | y == 0 := x == 0 + | else := y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA; + +--- Doubles a valid `point` (computes point + point) on the elliptic curve. +double (point : Point) : Point := + case point of + mkPoint x y := + if + | y == 0 := point + | else := + let + slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y); + r_x := slope * slope - x - x; + r_y := slope * (x - r_x) - y; + in mkPoint@?{ + x := r_x; + y := r_y + }; --- Adds two valid points on the EC. -add : Point -> Point -> Point - | p@(mkPoint x1 y1) q@(mkPoint x2 y2) := - if - | y1 == 0 := q - | y2 == 0 := p - | x1 == x2 := - if - | y1 == y2 := double p - | else := mkPoint 0 0 - | else := - let - slope := (y1 - y2) / (x1 - x2); - r_x := slope * slope - x1 - x2; - r_y := slope * (x1 - r_x) - y1; - in mkPoint r_x r_y; - ---- Subtracts a point from another on the EC. -sub (p q : Point) : Point := add p q@Point{y := 0 - y}; - ---- Computes p + m * q on the elliptic curve. +add (point1 point2 : Point) : Point := + case point1, point2 of + mkPoint x1 y1, mkPoint x2 y2 := + if + | y1 == 0 := point2 + | y2 == 0 := point1 + | x1 == x2 := + if + | y1 == y2 := double point1 + | else := mkPoint 0 0 + | else := + let + slope := (y1 - y2) / (x1 - x2); + r_x := slope * slope - x1 - x2; + r_y := slope * (x1 - r_x) - y1; + in mkPoint r_x r_y; + +--- Subtracts point2 from point1 on the EC. +sub (point1 point2 : Point) : Point := add point1 point2@Point{y := 0 - y}; + +--- Computes point1 + alpha * point2 on the elliptic curve. --- Because the EC operation builtin cannot handle inputs where additions of points with the same x --- coordinate arise during the computation, this function adds and subtracts a nondeterministic --- point s to the computation, so that regardless of input, the probability that such additions --- arise will become negligibly small. --- The precise computation is therefore: ---- ((p + s) + m * q) - s ---- so that the inputs to the builtin itself are (p + s), m, and q. +--- ((point1 + s) + alpha * point2) - s +--- so that the inputs to the builtin itself are (point1 + s), alpha, and point2. --- --- Arguments: ---- p - an EC point. ---- m - the multiplication coefficient of q (a field element). ---- q - an EC point. +--- point1 - an EC point. +--- alpha - the multiplication coefficient of point2 (a field element). +--- point2 - an EC point. --- --- Returns: ---- p + m * q. +--- point1 + alpha * point2. --- --- Assumptions: ---- p and q are valid points on the curve. -addMul (p : Point) (m : Field) (q : Point) : Point := +--- point1 and point2 are valid points on the curve. +addMul (point1 : Point) (alpha : Field) (point2 : Point) : Point := if - | Point.y q == 0 := p + | Point.y point2 == 0 := point1 | else := let s : Point := Internal.randomEcPoint; - r : Point := Internal.ecOp (add p s) m q; + r : Point := Internal.ecOp (add point1 s) alpha point2; in sub r s; ---- Computes m * p on the elliptic curve. -mul (m : Field) (p : Point) : Point := addMul (mkPoint 0 0) m p; +--- Computes alpha * point on the elliptic curve. +mul (alpha : Field) (point : Point) : Point := addMul (mkPoint 0 0) alpha point; module Operators; import Stdlib.Data.Fixity open; diff --git a/Stdlib/Cairo/Poseidon.juvix b/Stdlib/Cairo/Poseidon.juvix index a025b2eb..ebaded3d 100644 --- a/Stdlib/Cairo/Poseidon.juvix +++ b/Stdlib/Cairo/Poseidon.juvix @@ -27,11 +27,11 @@ poseidonHash2 (x y : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseido --- Hashes n elements and retrieves a single field element output. {-# eval: false #-} -poseidonHashList (lst : List Field) : Field := +poseidonHashList (list : List Field) : Field := let go (acc : PoseidonState) : List Field -> PoseidonState | [] := poseidonHash acc@PoseidonState{s0 := s0 + 1} | [x] := poseidonHash acc@PoseidonState{ s0 := s0 + x; s1 := s1 + 1 } | (x1 :: x2 :: xs) := go (poseidonHash acc@PoseidonState{ s0 := s0 + x1; s1 := s1 + x2 }) xs; - in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst); + in PoseidonState.s0 (go (mkPoseidonState 0 0 0) list); diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix index e5876a06..6a70de9b 100644 --- a/Stdlib/Data/BinaryTree.juvix +++ b/Stdlib/Data/BinaryTree.juvix @@ -4,17 +4,21 @@ import Stdlib.Data.Nat open; import Stdlib.Data.List open; type BinaryTree (A : Type) := - | leaf : BinaryTree A - | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A; + | leaf + | node { + left : BinaryTree A; + element : A; + right : BinaryTree A + }; ---- fold a tree in depth first order -fold {A B} (f : A -> B -> B -> B) (acc : B) : BinaryTree A -> B := +--- fold a tree in depth-first order +fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B := let go (acc : B) : BinaryTree A -> B | leaf := acc | (node l a r) := f a (go acc l) (go acc r); - in go acc; + in go acc tree; -length : {A : Type} -> BinaryTree A -> Nat := fold λ {_ l r := 1 + l + r} 0; +length {A} (tree : BinaryTree A) : Nat := fold \ {_ l r := 1 + l + r} 0 tree; -to-list : {A : Type} -> BinaryTree A -> List A := fold λ {e ls rs := e :: ls ++ rs} nil; +toList {A} (tree : BinaryTree A) : List A := fold \ {e ls rs := e :: ls ++ rs} nil tree; diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix index bfc5d891..6aa14b87 100644 --- a/Stdlib/Data/Bool.juvix +++ b/Stdlib/Data/Bool.juvix @@ -1,6 +1,8 @@ module Stdlib.Data.Bool; import Stdlib.Data.Bool.Base open public; +import Stdlib.Data.Pair.Base open; +import Stdlib.Data.String.Base open; import Stdlib.Trait.Eq open; import Stdlib.Trait.Ord open; import Stdlib.Trait.Show open; @@ -8,28 +10,31 @@ import Stdlib.Trait.Show open; {-# specialize: true, inline: case #-} instance boolEqI : Eq Bool := - mkEq - λ { - | true true := true - | false false := true - | _ _ := false - }; + mkEq@{ + eq (x y : Bool) : Bool := + case x, y of + | true, true := true + | false, false := true + | _ := false + }; {-# specialize: true, inline: case #-} instance boolOrdI : Ord Bool := - mkOrd - λ { - | false false := EQ - | false true := LT - | true false := GT - | true true := EQ - }; + mkOrd@{ + cmp (x y : Bool) : Ordering := + case x, y of + | false, false := Equal + | false, true := LessThan + | true, false := GreaterThan + | true, true := Equal + }; instance showBoolI : Show Bool := - mkShow - λ { - | true := "true" - | false := "false" - }; + mkShow@{ + show (x : Bool) : String := + if + | x := "true" + | else := "false" + }; diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix index d266726d..75fe8a63 100644 --- a/Stdlib/Data/Bool/Base.juvix +++ b/Stdlib/Data/Bool/Base.juvix @@ -5,7 +5,7 @@ import Stdlib.Data.Fixity open; --- Logical negation. {-# isabelle-function: {name: "\\"} #-} -not : Bool → Bool +not : Bool -> Bool | true := false | false := true; @@ -13,7 +13,7 @@ syntax operator || logical; --- Logical disjunction. Evaluated lazily. Cannot be partially applied builtin bool-or -|| : Bool → Bool → Bool +|| : Bool -> Bool -> Bool | true _ := true | false a := a; @@ -21,13 +21,13 @@ syntax operator && logical; --- Logical conjunction. Evaluated lazily. Cannot be partially applied. builtin bool-and -&& : Bool → Bool → Bool +&& : Bool -> Bool -> Bool | true a := a | false _ := false; --- Returns the first argument if ;true;, otherwise it returns the second argument. Evaluated lazily. Cannot be partially applied. builtin bool-if -ite : {A : Type} → Bool → A → A → A +ite : {A : Type} -> Bool -> A -> A -> A | true a _ := a | false _ b := b; diff --git a/Stdlib/Data/Byte.juvix b/Stdlib/Data/Byte.juvix index 89cfab6c..99bb444c 100644 --- a/Stdlib/Data/Byte.juvix +++ b/Stdlib/Data/Byte.juvix @@ -17,7 +17,7 @@ eqByteI : Eq Byte := mkEq (Byte.==); instance showByteI : Show Byte := mkShow@{ - show := Byte.toNat >> Show.show + show (x : Byte) : String := Show.show (Byte.toNat x) }; {-# specialize: true, inline: case #-} diff --git a/Stdlib/Data/Int/Base.juvix b/Stdlib/Data/Int/Base.juvix index f3cb68d2..bfc4fcd5 100644 --- a/Stdlib/Data/Int/Base.juvix +++ b/Stdlib/Data/Int/Base.juvix @@ -16,9 +16,10 @@ type Int := negSuc Nat; --- Converts an ;Int; to a ;Nat;. If the ;Int; is negative, it returns ;zero;. -toNat : Int -> Nat - | (ofNat n) := n - | (negSuc _) := zero; +toNat (int : Int) : Nat := + case int of + | ofNat n := n + | negSuc _ := zero; --- Non-negative predicate for ;Int;s. builtin int-nonneg @@ -88,6 +89,7 @@ mod : Int -> Int -> Int | (negSuc m) (negSuc n) := negNat (Nat.mod (suc m) (suc n)); --- Absolute value -abs : Int -> Nat - | (ofNat n) := n - | (negSuc n) := suc n; +abs (int : Int) : Nat := + case int of + | ofNat n := n + | negSuc n := suc n; diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix index 31fdf058..cf51476b 100644 --- a/Stdlib/Data/Int/Ord.juvix +++ b/Stdlib/Data/Int/Ord.juvix @@ -4,7 +4,7 @@ import Stdlib.Data.Fixity open; import Stdlib.Data.Int.Base open; import Stdlib.Data.Bool.Base open; -import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering}; +import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering}; import Stdlib.Data.Nat.Base as Nat; import Stdlib.Data.Nat.Ord as Nat; @@ -49,9 +49,9 @@ syntax operator >= comparison; {-# inline: true #-} compare (m n : Int) : Ordering := if - | m == n := EQ - | m < n := LT - | else := GT; + | m == n := Equal + | m < n := LessThan + | else := GreaterThan; --- Returns the smallest ;Int;. min (x y : Int) : Int := ite (x < y) x y; diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index e31a7b06..6596def2 100644 --- a/Stdlib/Data/List.juvix +++ b/Stdlib/Data/List.juvix @@ -27,18 +27,20 @@ eqListI {A} {{Eq A}} : Eq (List A) := | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false; in mkEq go; +isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool := isElement (Eq.eq) elem list; + instance ordListI {A} {{Ord A}} : Ord (List A) := let go : List A -> List A -> Ordering - | nil nil := EQ - | nil _ := LT - | _ nil := GT + | nil nil := Equal + | nil _ := LessThan + | _ nil := GreaterThan | (x :: xs) (y :: ys) := case Ord.cmp x y of - | LT := LT - | GT := GT - | EQ := go xs ys; + | LessThan := LessThan + | GreaterThan := GreaterThan + | Equal := go xs ys; in mkOrd go; instance @@ -47,11 +49,12 @@ showListI {A} {{Show A}} : Show (List A) := go : List A -> String | nil := "nil" | (x :: xs) := Show.show x ++str " :: " ++str go xs; - in mkShow - λ { - | nil := "nil" - | s := "(" ++str go s ++str ")" - }; + in mkShow@{ + show (list : List A) : String := + case list of + | nil := "nil" + | s := "(" ++str go s ++str ")" + }; {-# specialize: true, inline: case #-} instance @@ -80,7 +83,7 @@ instance applicativeListI : Applicative List := mkApplicative@{ pure {A} (a : A) : List A := [a]; - ap {A B} : List (A -> B) -> List A -> List B + ap {A B} : (listOfFuns : List (A -> B)) -> (listOfAs : List A) -> List B | [] _ := [] | (f :: fs) l := map f l ++ ap fs l }; diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index d472078f..e900074f 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -9,63 +9,63 @@ import Stdlib.Data.Maybe.Base open; import Stdlib.Trait.Ord open; import Stdlib.Data.Pair.Base open; ---- 𝒪(𝓃). Returns ;true; if the given ---- object is in the ;List;. +--- 𝒪(𝓃). Returns ;true; if the given object elem is in the ;List;. {-# specialize: [1] #-} -elem {A} (eq : A → A → Bool) (s : A) : List A → Bool +isElement {A} (eq : A -> A -> Bool) (elem : A) : (list : List A) -> Bool | nil := false - | (x :: xs) := eq s x || elem eq s xs; + | (x :: xs) := eq elem x || isElement eq elem xs; --- 𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or ---- nothing if there's no such element. +--- nothing if there is no such element. {-# specialize: [1] #-} -find {A} (predicate : A → Bool) : List A → Maybe A +find {A} (predicate : A -> Bool) : (list : List A) -> Maybe A | nil := nothing | (x :: xs) := if | predicate x := just x | else := find predicate xs; ---- Right-associative fold. -{-# specialize: [1] #-} -liftFoldr {A B} (f : A → B → B) (z : B) : List A → B - | nil := z - | (h :: hs) := f h (liftFoldr f z hs); - syntax iterator listRfor {init := 1; range := 1}; {-# specialize: [1] #-} -listRfor {A B} (f : B → A → B) (acc : B) : List A → B +listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> B | nil := acc - | (x :: xs) := f (listRfor f acc xs) x; + | (x :: xs) := fun (listRfor fun acc xs) x; + +--- Right-associative fold. +{-# specialize: [1] #-} +liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : B := listRfor (flip fun) acc list; --- Left-associative and tail-recursive fold. {-# specialize: [1] #-} -listFoldl {A B} (f : B → A → B) (z : B) : List A → B - | nil := z - | (h :: hs) := listFoldl f (f z h) hs; +listFoldl {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> B + | nil := acc + | (h :: hs) := listFoldl fun (fun acc h) hs; syntax iterator listFor {init := 1; range := 1}; {-# inline: 0, isabelle-function: {name: "foldl"} #-} -listFor : {A B : Type} → (B → A → B) → B → List A → B := listFoldl; +listFor : {A B : Type} -> (B -> A -> B) -> B -> List A -> B := listFoldl; syntax iterator listMap {init := 0; range := 1}; --- 𝒪(𝓃). Maps a function over each element of a ;List;. {-# specialize: [1] #-} -listMap {A B} (f : A → B) : List A → List B +listMap {A B} (fun : A -> B) : (list : List A) -> List B | nil := nil - | (h :: hs) := f h :: listMap f hs; + | (h :: hs) := fun h :: listMap fun hs; syntax iterator filter {init := 0; range := 1}; --- 𝒪(𝓃). Filters a ;List; according to a given predicate, i.e., --- keeps the elements for which the given predicate returns ;true;. {-# specialize: [1] #-} -filter {A} (f : A → Bool) : List A → List A +filter {A} (predicate : A -> Bool) : (list : List A) -> List A | nil := nil - | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs); + | (h :: hs) := + if + | predicate h := h :: filter predicate hs + | else := filter predicate hs; --- 𝒪(𝓃). Returns the length of the ;List;. length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc}; @@ -74,24 +74,25 @@ length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc}; {-# isabelle-function: {name: "rev"} #-} reverse {A} (l : List A) : List A := listFor (acc := nil) (x in l) {x :: acc}; ---- Returns a ;List; of length n where every element is the given value. -replicate {A} : Nat → A → List A +--- Returns a ;List; of length resultLength where every element is the given value. +replicate {A} : (resultLength : Nat) -> (value : A) -> List A | zero _ := nil | (suc n) x := x :: replicate n x; ---- Takes the first n elements of a ;List;. -take {A} : Nat → List A → List A +--- Takes the first elemsNum elements of a ;List;. +take {A} : (elemsNum : Nat) -> (list : List A) -> List A | (suc n) (x :: xs) := x :: take n xs | _ _ := nil; ---- Drops the first n elements of a ;List;. -drop {A} : Nat → List A → List A +--- Drops the first elemsNum elements of a ;List;. +drop {A} : (elemsNum : Nat) -> (list : List A) -> List A | (suc n) (x :: xs) := drop n xs | _ xs := xs; ---- 𝒪(𝓃). splitAt n xs returns a tuple where first element is xs ---- prefix of length n and second element is the remainder of the ;List;. -splitAt {A} : Nat → List A → Pair (List A) (List A) +--- 𝒪(𝓃). Returns a tuple where first element is the +--- prefix of the given list of length prefixLength and second element is the +--- remainder of the ;List;. +splitAt {A} : (prefixLength : Nat) -> (list : List A) -> Pair (List A) (List A) | _ nil := nil, nil | zero xs := nil, xs | (suc zero) (x :: xs) := x :: nil, xs @@ -99,92 +100,108 @@ splitAt {A} : Nat → List A → Pair (List A) (List A) --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering. terminating -merge {A} {{Ord A}} : List A → List A → List A - | xs@(x :: xs') ys@(y :: ys') := - if - | isLT (Ord.cmp x y) := x :: merge xs' ys - | else := y :: merge xs ys' - | nil ys := ys - | xs nil := xs; +merge {A} {{Ord A}} (list1 list2 : List A) : List A := + case list1, list2 of + | xs@(x :: xs'), ys@(y :: ys') := + if + | x < y := x :: merge xs' ys + | else := 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. -partition {A} (f : A → Bool) : List A → Pair (List A) (List A) +partition {A} (predicate : A → Bool) : (list : List A) -> Pair (List A) (List A) | nil := nil, nil - | (x :: xs) := case partition f xs of l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2); + | (x :: xs) := + case partition predicate xs of + l1, l2 := + if + | predicate x := x :: l1, l2 + | else := l1, x :: l2; syntax operator ++ cons; --- Concatenates two ;List;s. -++ : {A : Type} → List A → List A → List A +++ : {A : Type} -> (list1 : List A) -> (list2 : List A) -> List A | nil ys := ys | (x :: xs) ys := x :: xs ++ ys; --- 𝒪(𝓃). Append an element. -snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil; +snoc {A} (list : List A) (elem : A) : List A := list ++ elem :: nil; --- Concatenates a ;List; of ;List;s. {-# isabelle-function: {name: "concat"} #-} -flatten : {A : Type} → List (List A) → List A := listFoldl (++) nil; +flatten {A} (listOfLists : List (List A)) : List A := listFoldl (++) nil listOfLists; ---- 𝒪(𝓃). Inserts the given element before every element in the given ;List;. -prependToAll {A} (sep : A) : List A → List A +--- 𝒪(𝓃). Inserts the given separator before every element in the given ;List;. +prependToAll {A} (separator : A) : (list : List A) -> List A | nil := nil - | (x :: xs) := sep :: x :: prependToAll sep xs; + | (x :: xs) := separator :: x :: prependToAll separator xs; ---- 𝒪(𝓃). Inserts the given element inbetween every two elements in the given ;List;. -intersperse {A} (sep : A) : List A → List A - | nil := nil - | (x :: xs) := x :: prependToAll sep xs; +--- 𝒪(𝓃). Inserts the given separator inbetween every two elements in the given ;List;. +intersperse {A} (separator : A) (list : List A) : List A := + case list of + | nil := nil + | x :: xs := x :: prependToAll separator xs; --- 𝒪(1). Drops the first element of a ;List;. {-# isabelle-function: {name: "tl"} #-} -tail {A} : List A → List A - | (_ :: xs) := xs - | nil := nil; +tail {A} (list : List A) : List A := + case list of + | _ :: xs := xs + | nil := nil; -head {A} (a : A) : List A -> A - | (x :: _) := x - | nil := a; +head {A} (defaultValue : A) (list : List A) : A := + case list of + | x :: _ := x + | nil := defaultValue; syntax iterator any {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate. {-# specialize: [1] #-} -any {A} (f : A → Bool) : List A → Bool +any {A} (predicate : A -> Bool) : (list : List A) -> Bool | nil := false - | (x :: xs) := ite (f x) true (any f xs); + | (x :: xs) := + if + | predicate x := true + | else := any predicate xs; syntax iterator all {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if all elements of the ;List; satisfy the predicate. {-# specialize: [1] #-} -all {A} (f : A -> Bool) : List A -> Bool +all {A} (predicate : A -> Bool) : (list : List A) -> Bool | nil := true - | (x :: xs) := ite (f x) (all f xs) false; + | (x :: xs) := + if + | predicate x := all predicate xs + | else := false; --- 𝒪(1). Returns ;true; if the ;List; is empty. -null {A} : List A → Bool - | nil := true - | _ := false; +null {A} (list : List A) : Bool := + case list of + | nil := true + | _ := false; --- 𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function --- to each pair of elements from the input lists. {-# specialize: [1] #-} -zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List C +zipWith {A B C} (fun : A -> B -> C) : (listA : List A) -> (listB : List B) -> List C | nil _ := nil | _ nil := nil - | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys; + | (x :: xs) (y :: ys) := fun x y :: zipWith fun xs ys; --- 𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists. -zip {A B} : List A -> List B -> List (Pair A B) +zip {A B} : (listA : List A) -> (listB : List B) -> List (Pair A B) | nil _ := nil | _ nil := nil | (x :: xs) (y :: ys) := (x, y) :: zip xs ys; --- 𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort --- algorithm. -mergeSort {A} {{Ord A}} (l : List A) : List A := +mergeSort {A} {{Ord A}} (list : List A) : List A := let terminating go : Nat -> List A -> List A @@ -197,22 +214,22 @@ mergeSort {A} {{Ord A}} (l : List A) : List A := left : List A := fst splitXs; right : List A := snd splitXs; in merge (go len' left) (go (sub len len') right); - in go (length l) l; + in go (length list) list; --- 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 := +quickSort {A} {{Ord A}} (list : List A) : List A := let terminating - go : List A → List A + go : List A -> List A | nil := nil | xs@(_ :: nil) := xs - | (x :: xs) := case partition (Ord.cmp x >> isGT) xs of l1, l2 := go l1 ++ x :: go l2; - in go; + | (x :: xs) := case partition \ {y := y < x} xs of l1, l2 := go l1 ++ x :: go l2; + in go list; --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;. -catMaybes {A} : List (Maybe A) -> List A +catMaybes {A} : (listOfMaybes : List (Maybe A)) -> List A | nil := nil | (just h :: hs) := h :: catMaybes hs | (nothing :: hs) := catMaybes hs; @@ -221,10 +238,10 @@ syntax iterator concatMap {init := 0; range := 1}; --- Applies a function to every item on a ;List; and concatenates the result. --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list. -concatMap {A B} (f : A -> List B) : List A -> List B := listMap f >> flatten; +concatMap {A B} (fun : A -> List B) (list : List A) : List B := flatten (listMap fun list); --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix. -transpose {A} : List (List A) -> List (List A) +transpose {A} : (listOfLists : List (List A)) -> List (List A) | nil := nil | (xs :: nil) := listMap λ {x := x :: nil} xs | (xs :: xss) := zipWith (::) xs (transpose xss); diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix index eb3995e3..841a030e 100644 --- a/Stdlib/Data/Map.juvix +++ b/Stdlib/Data/Map.juvix @@ -19,32 +19,44 @@ open AVL using {AVLTree}; import Stdlib.Data.BinaryTree as Tree; -type Binding A B := binding A B; +type Binding Key Value := + mkBinding { + key : Key; + value : Value + }; -key {A B} : Binding A B -> A - | (binding a _) := a; +key {Key Value} (binding : Binding Key Value) : Key := Binding.key binding; -value {A B} : Binding A B -> B - | (binding _ b) := b; +value {Key Value} (binding : Binding Key Value) : Value := Binding.value binding; -toPair {A B} : Binding A B -> Pair A B - | (binding a b) := a, b; +toPair {Key Value} (binding : Binding Key Value) : Pair Key Value := key binding, value binding; instance -bindingKeyOrdering {A B} {{Ord A}} : Ord (Binding A B) := - mkOrd λ {b1 b2 := Ord.cmp (key b1) (key b2)}; +bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) := + mkOrd@{ + cmp (b1 b2 : Binding Key Value) : Ordering := Ord.cmp (key b1) (key b2) + }; -type Map A B := mkMap (AVLTree (Binding A B)); +type Map Key Value := mkMap (AVLTree (Binding Key Value)); -empty {A B} : Map A B := mkMap AVL.empty; +empty {Key Value} : Map Key Value := mkMap AVL.empty; {-# specialize: [1, f] #-} -insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B) : Map A B -> Map A B - | (mkMap s) := - let - f' : Binding A B -> Binding A B -> Binding A B - | (binding a b1) (binding _ b2) := binding a (f b1 b2); - in mkMap (Set.insertWith f' (binding k v) s); +insertWith + {Key Value} + {{Ord Key}} + (fun : Value -> Value -> Value) + (key : Key) + (value : Value) + (map : Map Key Value) + : Map Key Value := + case map of + mkMap tree := + let + fun' (binding1 binding2 : Binding Key Value) : Binding Key Value := + case binding1, binding2 of mkBinding a b1, mkBinding _ b2 := mkBinding a (fun b1 b2); + binding := mkBinding key value; + in mkMap (Set.insertWith fun' binding tree); insert {A B : Type} {{Ord A}} : A -> B -> Map A B -> Map A B := insertWith λ {old new := new}; diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix index 095171ad..d02e565f 100644 --- a/Stdlib/Data/Maybe.juvix +++ b/Stdlib/Data/Maybe.juvix @@ -11,35 +11,39 @@ import Stdlib.Trait.Monad open; import Stdlib.Data.Bool.Base open; import Stdlib.Data.String.Base open; +import Stdlib.Data.Pair.Base open; {-# specialize: true, inline: case #-} instance eqMaybeI {A} {{Eq A}} : Eq (Maybe A) := - mkEq - λ { - | nothing nothing := true - | (just a1) (just a2) := Eq.eq a1 a2 - | _ _ := false - }; + mkEq@{ + eq (m1 m2 : Maybe A) : Bool := + case m1, m2 of + | nothing, nothing := true + | just a1, just a2 := Eq.eq a1 a2 + | _ := false + }; instance showMaybeI {A} {{Show A}} : Show (Maybe A) := - mkShow - λ { - | nothing := "nothing" - | (just a) := "just " ++str Show.show a - }; + mkShow@{ + show (m : Maybe A) : String := + case m of + | nothing := "nothing" + | just a := "just " ++str Show.show a + }; {-# specialize: true, inline: case #-} instance ordMaybeI {A} {{Ord A}} : Ord (Maybe A) := - mkOrd - λ { - | nothing nothing := EQ - | (just a1) (just a2) := Ord.cmp a1 a2 - | nothing (just _) := LT - | (just _) nothing := GT - }; + mkOrd@{ + cmp (m1 m2 : Maybe A) : Ordering := + case m1, m2 of + | nothing, nothing := Equal + | just a1, just a2 := Ord.cmp a1 a2 + | nothing, just _ := LessThan + | just _, nothing := GreaterThan + }; {-# specialize: true, inline: case #-} instance @@ -58,15 +62,17 @@ instance applicativeMaybeI : Applicative Maybe := mkApplicative@{ pure := just; - ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B - | (just f) (just x) := just (f x) - | _ _ := nothing + ap {A B} (listOfFuns : Maybe (A -> B)) (list : Maybe A) : Maybe B := + case listOfFuns, list of + | just f, just x := just (f x) + | _, _ := nothing }; instance monadMaybeI : Monad Maybe := mkMonad@{ - bind {A B} : Maybe A -> (A -> Maybe B) -> Maybe B - | nothing _ := nothing - | (just a) f := f a + bind {A B} (maybe : Maybe A) (fun : A -> Maybe B) : Maybe B := + case maybe of + | nothing := nothing + | just a := fun a }; diff --git a/Stdlib/Data/Maybe/Base.juvix b/Stdlib/Data/Maybe/Base.juvix index 390226d3..a35c60c1 100644 --- a/Stdlib/Data/Maybe/Base.juvix +++ b/Stdlib/Data/Maybe/Base.juvix @@ -5,17 +5,20 @@ import Juvix.Builtin.V1.Bool open; --- Extracts the value from a ;Maybe; if present, else returns the given value. {-# inline: true #-} -fromMaybe {A} (a : A) : Maybe A → A - | nothing := a - | (just a) := a; +fromMaybe {A} (defaultValue : A) (maybeValue : Maybe A) : A := + case maybeValue of + | nothing := defaultValue + | just a := a; --- Applies a function to the value from a ;Maybe; if present, else returns the --- given value. {-# inline: true, isabelle-function: {name: "case_option"} #-} -maybe {A B} (b : B) (f : A → B) : Maybe A → B - | nothing := b - | (just a) := f a; +maybe {A B} (defaultValue : B) (fun : A -> B) (maybeValue : Maybe A) : B := + case maybeValue of + | nothing := defaultValue + | just a := fun a; -isJust {A} : Maybe A -> Bool - | nothing := false - | (just _) := true; +isJust {A} (maybeValue : Maybe A) : Bool := + case maybeValue of + | nothing := false + | just _ := true; diff --git a/Stdlib/Data/Nat/Ord.juvix b/Stdlib/Data/Nat/Ord.juvix index c97c6290..61b439f8 100644 --- a/Stdlib/Data/Nat/Ord.juvix +++ b/Stdlib/Data/Nat/Ord.juvix @@ -3,14 +3,14 @@ module Stdlib.Data.Nat.Ord; import Stdlib.Data.Fixity open; import Stdlib.Data.Nat.Base open; -import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering}; +import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering}; import Stdlib.Data.Bool.Base open; syntax operator == comparison; --- Tests for equality. builtin nat-eq -== : Nat → Nat → Bool +== : Nat -> Nat -> Bool | zero zero := true | zero _ := false | _ zero := false @@ -25,7 +25,7 @@ syntax operator <= comparison; --- Returns ;true; iff the first element is less than or equal to the second. builtin nat-le -<= : Nat → Nat → Bool +<= : Nat -> Nat -> Bool | zero _ := true | _ zero := false | (suc n) (suc m) := n <= m; @@ -50,12 +50,18 @@ syntax operator >= comparison; {-# inline: true #-} compare (n m : Nat) : Ordering := if - | n == m := EQ - | n < m := LT - | else := GT; + | n == m := Equal + | n < m := LessThan + | else := GreaterThan; --- Returns the smaller ;Nat;. -min (x y : Nat) : Nat := ite (x < y) x y; +min (x y : Nat) : Nat := + if + | x < y := x + | else := y; --- Returns the larger ;Nat;. -max (x y : Nat) : Nat := ite (x > y) x y; +max (x y : Nat) : Nat := + if + | x > y := x + | else := y; diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix index 6ddf5275..feb2a550 100644 --- a/Stdlib/Data/Pair.juvix +++ b/Stdlib/Data/Pair.juvix @@ -11,20 +11,29 @@ import Stdlib.Trait.Show open; {-# specialize: true, inline: case #-} instance eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B) - | {{mkEq eq-a}} {{mkEq eq-b}} := mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2}; + | {{mkEq eqA}} {{mkEq eqB}} := + mkEq@{ + eq (p1 p2 : Pair A B) : Bool := case p1, p2 of (a1, b1), a2, b2 := eqA a1 a2 && eqB b1 b2 + }; {-# specialize: true, inline: case #-} instance ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B) - | {{mkOrd cmp-a}} {{mkOrd cmp-b}} := - mkOrd - λ {(a1, b1) (a2, b2) := - case cmp-a a1 a2 of - | LT := LT - | GT := GT - | EQ := cmp-b b1 b2}; + | {{mkOrd cmpA}} {{mkOrd cmpB}} := + mkOrd@{ + cmp (p1 p2 : Pair A B) : Ordering := + case p1, p2 of + (a1, b1), a2, b2 := + case cmpA a1 a2 of + | LessThan := LessThan + | GreaterThan := GreaterThan + | Equal := cmpB b1 b2 + }; instance showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B) - | {{mkShow show-a}} {{mkShow show-b}} := - mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"}; + | {{mkShow showA}} {{mkShow showB}} := + mkShow@{ + show (p : Pair A B) : String := + case p of a, b := "(" ++str showA a ++str " , " ++str showB b ++str ")" + }; diff --git a/Stdlib/Data/Pair/Base.juvix b/Stdlib/Data/Pair/Base.juvix index 07ea8405..39a41eeb 100644 --- a/Stdlib/Data/Pair/Base.juvix +++ b/Stdlib/Data/Pair/Base.juvix @@ -8,33 +8,26 @@ syntax operator , pair; builtin pair type Pair (A B : Type) := , : A → B → Pair A B; ---- Converts a function of two arguments to a function with a product argument. -uncurry {A B C} (f : A -> B -> C) : Pair A B -> C - | (a, b) := f a b; +--- Converts a function f of two arguments to a function with a product argument. +uncurry {A B C} (f : A -> B -> C) (pair : Pair A B) : C := case pair of a, b := f a b; ---- Converts a function with a product argument to a function of two arguments. +--- Converts a function f with a product argument to a function of two arguments. curry {A B C} (f : Pair A B -> C) (a : A) (b : B) : C := f (a, b); --- Projects the first component of a tuple. -fst {A B} : Pair A B → A - | (a, _) := a; +fst {A B} (pair : Pair A B) : A := case pair of a, _ := a; --- Projects the second component of a tuple. -snd {A B} : Pair A B → B - | (_, b) := b; +snd {A B} (pair : Pair A B) : B := case pair of _, b := b; --- Swaps the components of a tuple. -swap {A B} : Pair A B → Pair B A - | (a, b) := b, a; +swap {A B} (pair : Pair A B) : Pair B A := case pair of a, b := b, a; ---- Applies a function to the first component. -first {A B A'} (f : A → A') : Pair A B → Pair A' B - | (a, b) := f a, b; +--- Applies a function f to the first component. +first {A B A'} (f : A -> A') (pair : Pair A B) : Pair A' B := case pair of a, b := f a, b; ---- Applies a function to the second component. -second {A B B'} (f : B → B') : Pair A B → Pair A B' - | (a, b) := a, f b; +--- Applies a function f to the second component. +second {A B B'} (f : B -> B') (pair : Pair A B) : Pair A B' := case pair of a, b := a, f b; ---- Applies a function to both components. -both {A B} (f : A → B) : Pair A A → Pair B B - | (a, b) := f a, f b; +--- Applies a function f to both components. +both {A B} (f : A -> B) (pair : Pair A A) : Pair B B := case pair of a, b := f a, f b; diff --git a/Stdlib/Data/Queue/Base.juvix b/Stdlib/Data/Queue/Base.juvix index 1b715f38..b6085e95 100644 --- a/Stdlib/Data/Queue/Base.juvix +++ b/Stdlib/Data/Queue/Base.juvix @@ -18,58 +18,66 @@ import Stdlib.Function open; import Stdlib.Trait.Foldable open; --- A first-in-first-out data structure -type Queue (A : Type) := queue (List A) (List A); +type Queue (A : Type) := + mkQueue { + front : List A; + back : List A + }; --- 𝒪(1). The empty ;Queue;. -empty {A} : Queue A := queue nil nil; +empty {A} : Queue A := mkQueue nil nil; --- 𝒪(1). Returns ;true; when the ;Queue; has no elements. -isEmpty {A} : Queue A -> Bool - | (queue nil nil) := true - | _ := false; +isEmpty {A} (queue : Queue A) : Bool := + case queue of + | mkQueue nil nil := true + | _ := false; --- 𝒪(1). Returns first element of the ;Queue;, if any. -head {A} : Queue A -> Maybe A - | (queue nil _) := nothing - | (queue (x :: _) _) := just x; +head {A} (queue : Queue A) : Maybe A := + case queue of + | mkQueue nil _ := nothing + | mkQueue (x :: _) _ := just x; --- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty -- then returns ;nothing;. -tail {A} : Queue A -> Maybe (Queue A) - | (queue nil _) := nothing - | (queue (_ :: front) back) := just (queue front back); +tail {A} (queue : Queue A) : Maybe (Queue A) := + case queue of + | mkQueue nil _ := nothing + | mkQueue (_ :: front) back := just (mkQueue front back); --- 𝒪(n) worst-case, but 𝒪(1) amortized {-# inline: true #-} -check {A} : Queue A -> Queue A - | (queue nil back) := queue (reverse back) nil - | q := q; +check {A} (queue : Queue A) : Queue A := + case queue of + | mkQueue nil back := mkQueue (reverse back) nil + | q := q; --- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the -- rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;. -pop {A} : Queue A -> Maybe (Pair A (Queue A)) - | (queue nil _) := nothing - | (queue (x :: front) back) := just (x, check (queue front back)); +pop {A} (queue : Queue A) : Maybe (Pair A (Queue A)) := + case queue of + | mkQueue nil _ := nothing + | mkQueue (x :: front) back := just (x, check (mkQueue front back)); --- 𝒪(1). Adds an element to the end of the ;Queue;. -push {A} (x : A) : Queue A -> Queue A - | (queue front back) := check (queue front (x :: back)); +push {A} (x : A) (queue : Queue A) : Queue A := + case queue of mkQueue front back := check (mkQueue front (x :: back)); --- 𝒪(n). Adds a list of elements to the end of the ;Queue;. -pushMany {A} (xs : List A) (q : Queue A) : Queue A := for (acc := q) (x in xs) push x acc; +pushMany {A} (list : List A) (queue : Queue A) : Queue A := + for (acc := queue) (x in list) {push x acc}; --- 𝒪(n). Build a ;Queue; from a ;List;. -fromList {A} (xs : List A) : Queue A := pushMany xs empty; +fromList {A} (list : List A) : Queue A := pushMany list empty; --- toList: O(n). Returns a ;List; of the elements in the ;Queue;. --- The elements are in the same order as they appear in the ;Queue; --- (i.e. the first element of the ;Queue; is the first element of the ;List;). -toList {A} : Queue A -> List A - | (queue front back) := front ++ reverse back; +toList {A} (queue : Queue A) : List A := case queue of mkQueue front back := front ++ reverse back; --- 𝒪(n). Returns the number of elements in the ;Queue;. -size {A} : Queue A -> Nat - | (queue front back) := length front + length back; +size {A} (queue : Queue A) : Nat := case queue of mkQueue front back := length front + length back; instance eqQueueI {A} {{Eq A}} : Eq (Queue A) := mkEq ((==) on toList); diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix index b70ad273..f847cea5 100644 --- a/Stdlib/Data/Range.juvix +++ b/Stdlib/Data/Range.juvix @@ -25,13 +25,13 @@ syntax operator to range; --- `x to y` is the range [x..y] {-# inline: always #-} -to {N} {{Natural N}} (l h : N) : Range N := mkRange l h; +to {N} {{Natural N}} (low high : N) : Range N := mkRange low high; syntax operator step step; --- `x to y step s` is the range [x, x + s, ..., y] {-# inline: always #-} -step {N} (r : Range N) (s : N) : StepRange N := mkStepRange r s; +step {N} (range : Range N) (stp : N) : StepRange N := mkStepRange range stp; -- This instance assumes that `low <= high`. {-# specialize: true, inline: case #-} @@ -39,7 +39,7 @@ instance foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N := mkFoldable@{ {-# specialize: [1, 3] #-} - for {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B + for {B : Type} (f : B -> N -> B) (initialValue : B) : Range N -> B | (mkRange low high) := let {-# specialize-by: [f, high] #-} @@ -48,16 +48,16 @@ foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N := if | next == high := f acc next | else := go (f acc next) (next + 1); - in go ini low; + in go initialValue low; {-# specialize: [1, 3] #-} - rfor {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B + rfor {B : Type} (f : B -> N -> B) (initialValue : B) : Range N -> B | (mkRange low high) := let {-# specialize-by: [f, high] #-} terminating go (next : N) : B := if - | next == high := f ini next + | next == high := f initialValue next | else := f (go (next + 1)) next; in go low }; @@ -68,7 +68,7 @@ instance foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N := mkFoldable@{ {-# specialize: [1, 3] #-} - for {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B + for {B : Type} (f : B -> N -> B) (initialValue : B) : StepRange N -> B | (mkStepRange (mkRange low high) step) := let {-# specialize-by: [f, high, step] #-} @@ -77,9 +77,9 @@ foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N := if | next > high := acc | else := go (f acc next) (next + step); - in go ini low; + in go initialValue low; {-# specialize: [1, 3] #-} - rfor {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B + rfor {B : Type} (f : B -> N -> B) (initialValue : B) : StepRange N -> B | (mkStepRange (mkRange low high) step) := let {-# specialize-by: [f, high, step] #-} @@ -87,6 +87,6 @@ foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N := go (next : N) : B := if | next <= high := f (go (next + step)) next - | else := ini; + | else := initialValue; in go low }; diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix index 98b301f6..59430367 100644 --- a/Stdlib/Data/Result.juvix +++ b/Stdlib/Data/Result.juvix @@ -3,6 +3,7 @@ module Stdlib.Data.Result; import Stdlib.Data.Result.Base open public; import Stdlib.Data.Bool.Base open; import Stdlib.Data.String.Base open; +import Stdlib.Data.Pair.Base open; import Stdlib.Trait.Eq open; import Stdlib.Trait.Ord open; @@ -11,59 +12,63 @@ import Stdlib.Trait open; {-# specialize: true, inline: case #-} instance -ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) := +ordResultI {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) := mkOrd@{ - cmp : Result A B -> Result A B -> Ordering - | (error a1) (error a2) := Ord.cmp a1 a2 - | (ok b1) (ok b2) := Ord.cmp b1 b2 - | (error _) (ok _) := LT - | (ok _) (error _) := GT + cmp (result1 result2 : Result Error Value) : Ordering := + case result1, result2 of + | error a1, error a2 := Ord.cmp a1 a2 + | ok b1, ok b2 := Ord.cmp b1 b2 + | error _, ok _ := LessThan + | ok _, error _ := GreaterThan }; {-# specialize: true, inline: case #-} instance -eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) := +eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) := mkEq@{ - eq : Result A B -> Result A B -> Bool - | (error a1) (error a2) := a1 == a2 - | (ok b1) (ok b2) := b1 == b2 - | _ _ := false + eq (result1 result2 : Result Error Value) : Bool := + case result1, result2 of + | error a1, error a2 := a1 == a2 + | ok b1, ok b2 := b1 == b2 + | _, _ := false }; instance -showResultI {A B} {{Show A}} {{Show B}} : Show (Result A B) := +showResultI {Error Value} {{Show Error}} {{Show Value}} : Show (Result Error Value) := mkShow@{ - show : Result A B -> String + show : Result Error Value -> String | (error x) := "Error (" ++str Show.show x ++str ")" | (ok x) := "Ok (" ++str Show.show x ++str ")" }; {-# specialize: true, inline: case #-} instance -functorResultI {err} : Functor (Result err) := +functorResultI {Error} : Functor (Result Error) := mkFunctor@{ map := mapOk }; {-# specialize: true, inline: true #-} instance -monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res := +monomorphicFunctorResultI {Error Value} : Monomorphic.Functor (Result Error Value) Value := fromPolymorphicFunctor; instance -applicativeResultI {err} : Applicative (Result err) := +applicativeResultI {Error} : Applicative (Result Error) := mkApplicative@{ pure := ok; - ap {A B} : Result err (A -> B) -> Result err A -> Result err B - | (ok f) (ok x) := ok (f x) - | (ok _) (error e) := error e - | (error e) _ := error e + ap {A B} (resultFun : Result Error (A -> B)) (result : Result Error A) : Result Error B := + case resultFun, result of + | ok f, ok x := ok (f x) + | ok _, error e := error e + | error e, _ := error e }; instance -monadResultI {err} : Monad (Result err) := +monadResultI {Error} : Monad (Result Error) := mkMonad@{ - bind {A B} : Result err A -> (A -> Result err B) -> Result err B - | (error e) _ := error e - | (ok a) f := f a + bind {A B} (result : Result Error A) (fun : A -> Result Error B) : Result Error B := + case result of + | error e := error e + | ok a := fun a }; diff --git a/Stdlib/Data/Result/Base.juvix b/Stdlib/Data/Result/Base.juvix index b0a65c65..3d98ffe3 100644 --- a/Stdlib/Data/Result/Base.juvix +++ b/Stdlib/Data/Result/Base.juvix @@ -6,46 +6,68 @@ import Stdlib.Function open; --- The Result type represents either a success with a value of `ok` or an error --- with value `error`. -type Result E A := - | error E - | ok A; +type Result Error Value := + | error Error + | ok Value; --- Apply the onError function if the value is ;error; or apply the --- onOk function if the value is ;ok;. -handleResult {E A B} (onError : E -> B) (onOk : A -> B) : Result E A -> B - | (error a) := onError a - | (ok a) := onOk a; +{-# inline: true #-} +handleResult + {Error Value1 Value2} + (onError : Error -> Value2) + (onOk : Value1 -> Value2) + (result : Result Error Value1) + : Value2 := + case result of + | error a := onError a + | ok a := onOk a; ---- Apply a function to the ;error; value of a Result. -mapError {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A := handleResult (f >> error) ok; +--- Apply a function f to the ;error; value of a Result. +mapError + {Value Error1 Error2} + (f : Error1 -> Error2) + (result : Result Error1 Value) + : Result Error2 Value := handleResult (f >> error) ok result; ---- Apply a function to the ;ok; value of a Result. -mapOk {E A C} (f : A -> C) : Result E A -> Result E C := handleResult error (f >> ok); +--- Apply a function f to the ;ok; value of a Result. +mapOk + {Error Value1 Value2} + (f : Value1 -> Value2) + (result : Result Error Value1) + : Result Error Value2 := handleResult error (f >> ok) result; --- Return ;true; if the value is an ;error;, otherwise ;false;. -isError {E A} : Result E A -> Bool - | (error _) := true - | (ok _) := false; +isError {Error Value} (result : Result Error Value) : Bool := + case result of + | error _ := true + | ok _ := false; --- Return ;true; if the value is ;ok;, otherwise ;false;. -isOk {E A} : Result E A -> Bool - | (error _) := false - | (ok _) := true; +isOk {Error Value} (result : Result Error Value) : Bool := + case result of + | error _ := false + | ok _ := true; ---- Return the contents of an ;error; value, otherwise return a default. -fromError {E A} (default : E) : Result E A -> E - | (error a) := a - | (ok _) := default; +--- Return the contents of an ;error; value, otherwise return defaultError. +fromError {Error Value} (defaultError : Error) (result : Result Error Value) : Error := + case result of + | error a := a + | ok _ := defaultError; ---- Return the contents of an ;ok; value, otherwise return a default. -fromOk {E A} (default : A) : Result E A -> A - | (error _) := default - | (ok b) := b; +--- Return the contents of an ;ok; value, otherwise return defaultValue. +fromOk {Error Value} (defaultValue : Value) (result : Result Error Value) : Value := + case result of + | error _ := defaultValue + | ok b := b; --- Convert a Result to a Maybe. An ;error; value becomes `nothing`. -resultToMaybe {E A} : Result E A -> Maybe A := handleResult (const nothing) just; +resultToMaybe {Error Value} (result : Result Error Value) : Maybe Value := + handleResult (const nothing) just result; --- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`. -maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A - | nothing := error defaultError - | (just x) := ok x; +maybeToResult + {Error Value} (defaultError : Error) (maybeValue : Maybe Value) : Result Error Value := + case maybeValue of + | nothing := error defaultError + | just x := ok x; diff --git a/Stdlib/Data/Set/AVL.juvix b/Stdlib/Data/Set/AVL.juvix index 988bd507..a4b37d8b 100644 --- a/Stdlib/Data/Set/AVL.juvix +++ b/Stdlib/Data/Set/AVL.juvix @@ -14,7 +14,7 @@ import Stdlib.Data.Nat open; import Stdlib.Data.Int open; import Stdlib.Data.Bool open; import Stdlib.Data.Pair open; -import Stdlib.Data.List open; +import Stdlib.Data.List open hiding {isMember}; import Stdlib.Data.String open; import Stdlib.Trait.Foldable open; import Stdlib.Function open; @@ -24,138 +24,168 @@ type AVLTree (A : Type) := | --- An empty AVL tree. empty | --- A node of an AVL tree. - node A Nat (AVLTree A) (AVLTree A); + node { + element : A; + height : Nat; + left : AVLTree A; + right : AVLTree A + }; --- 𝒪(1) Retrieves the height of an ;AVLTree;. The height is the distance from --- the root to the deepest child. -height {A} : AVLTree A -> Nat - | empty := 0 - | (node _ h _ _) := h; +height {A} (tree : AVLTree A) : Nat := + case tree of + | empty := 0 + | node@{height} := height; type BalanceFactor := - | --- Left children is higher. + | --- Left child is higher. LeanLeft | --- Equal heights of children. LeanNone - | --- Right children is higher. + | --- Right child is higher. LeanRight; -{-# inline: true #-} -diffFactor {A} : AVLTree A -> Int - | empty := 0 - | (node _ _ left right) := intSubNat (height right) (height left); +diffFactor {A} (tree : AVLTree A) : Int := + case tree of + | empty := 0 + | node@{left; right} := intSubNat (height right) (height left); ---- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree ---- minus the height of the left subtree. {-# inline: true #-} -balanceFactor {A} (t : AVLTree A) : BalanceFactor := +balanceFactor' {A} (left right : AVLTree A) : BalanceFactor := let - diff : Int := diffFactor t; + h1 := height left; + h2 := height right; in if - | 0 < diff := LeanRight - | diff < 0 := LeanLeft + | h1 < h2 := LeanRight + | h2 < h1 := LeanLeft | else := LeanNone; +--- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree +--- minus the height of the left subtree. +balanceFactor {A} (tree : AVLTree A) : BalanceFactor := + -- We avoid `diffFactor` here for efficiency. + case tree of + | empty := LeanNone + | node@{left; right} := balanceFactor' left right; + --- 𝒪(1). Helper function for creating a node. -mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A) : AVLTree A := - node val (1 + max (height l) (height r)) l r; +mkNode {A} (value : A) (left : AVLTree A) (right : AVLTree A) : AVLTree A := + node value (1 + max (height left) (height right)) left right; --- 𝒪(1). Left rotation. -rotateLeft {A} : AVLTree A -> AVLTree A - | (node x _ a (node z _ b c)) := mknode z (mknode x a b) c - | n := n; +rotateLeft {A} (tree : AVLTree A) : AVLTree A := + case tree of + | node x _ a (node z _ b c) := mkNode z (mkNode x a b) c + | n := n; --- 𝒪(1). Right rotation. -rotateRight {A} : AVLTree A -> AVLTree A - | (node z _ (node y _ x t3) t4) := mknode y x (mknode z t3 t4) - | n := n; +rotateRight {A} (tree : AVLTree A) : AVLTree A := + case tree of + | node z _ (node y _ x t3) t4 := mkNode y x (mkNode z t3 t4) + | n := n; --- 𝒪(1). Applies local rotations if needed. -balance : {A : Type} -> AVLTree A -> AVLTree A - | empty := empty - | n@(node x h l r) := - let - factor : BalanceFactor := balanceFactor n; - in case factor of - | LeanRight := - case balanceFactor r of { - | LeanLeft := rotateLeft (mknode x l (rotateRight r)) - | _ := rotateLeft n - } - | LeanLeft := - case balanceFactor l of { - | LeanRight := rotateRight (mknode x (rotateLeft l) r) - | _ := rotateRight n - } - | LeanNone := n; +balance {A} (tree : AVLTree A) : AVLTree A := + case tree of + | empty := empty + | node@{element; height; left; right} := + case balanceFactor' left right of + | LeanRight := + case balanceFactor right of { + | LeanLeft := rotateLeft (mkNode element left (rotateRight right)) + | _ := rotateLeft tree + } + | LeanLeft := + case balanceFactor left of { + | LeanRight := rotateRight (mkNode element (rotateLeft left) right) + | _ := rotateRight tree + } + | LeanNone := tree; --- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function. ---- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2 -lookupWith {A K} {{o : Ord K}} (f : A -> K) (x : K) : AVLTree A -> Maybe A := +--- Ord A, Ord K and fun must be compatible. i.e cmp_k (fun a1) (fun a2) == cmp_a a1 a2 +{-# specialize: [1, 2] #-} +lookupWith {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (tree : AVLTree A) : Maybe A := let - {-# specialize-by: [o, f] #-} + {-# specialize-by: [order, fun] #-} go : AVLTree A -> Maybe A | empty := nothing - | m@(node y h l r) := - case Ord.cmp x (f y) of - | LT := go l - | GT := go r - | EQ := just y; - in go; + | node@{element; left; right} := + case Ord.cmp elem (fun element) of + | LessThan := go left + | GreaterThan := go right + | Equal := just element; + in go tree; --- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;. {-# specialize: [1] #-} -member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool := lookupWith id x >> isJust; +lookup {A} {{Ord A}} (elem : A) (tree : AVLTree A) : Maybe A := lookupWith id elem tree; ---- 𝒪(log 𝓃). Inserts an element into and ;AVLTree; using a function to +--- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;. +isMember {A} {{Ord A}} (elem : A) (tree : AVLTree A) : Bool := isJust (lookupWith id elem tree); + +--- 𝒪(log 𝓃). Inserts an element elem into and ;AVLTree; using a function to --- deduplicate entries. --- ---- Assumption: Given a1 == a2 then f a1 a2 == a1 == a2 +--- Assumption: If a1 == a2 then fun a1 a2 == a1 == a2 --- where == comes from Ord a. -insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A) : AVLTree A -> AVLTree A := +{-# specialize: [1, 2] #-} +insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (tree : AVLTree A) : AVLTree A := let - {-# specialize-by: [o, f] #-} + {-# specialize-by: [order, fun] #-} go : AVLTree A -> AVLTree A - | empty := mknode x empty empty - | m@(node y h l r) := - case Ord.cmp x y of - | LT := balance (mknode y (go l) r) - | GT := balance (mknode y l (go r)) - | EQ := node (f y x) h l r; - in go; + | empty := mkNode elem empty empty + | node@{element; height; left; right} := + case Ord.cmp elem element of + | LessThan := balance (mkNode element (go left) right) + | GreaterThan := balance (mkNode element left (go right)) + | Equal := node (fun element elem) height left right; + in go tree; --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;. -insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A := insertWith (flip const); +insert {A} {{Ord A}} (elem : A) (tree : AVLTree A) : AVLTree A := insertWith (flip const) elem tree; + +--- 𝒪(log 𝓃). Removes the minimum element from an ;AVLTree;. +{-# specialize: [1] #-} +deleteMin {A} {{Ord A}} : (tree : AVLTree A) -> Maybe (Pair A (AVLTree A)) + | empty := nothing + | node@{element; left; right} := + case deleteMin left of + | nothing := just (element, right) + | just (element', left') := just (element', mkNode element left' right); --- 𝒪(log 𝓃). Removes an element from an ;AVLTree; based on a projected comparison value. --- ---- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2) -deleteWith {A B} {{o : Ord A}} {{po : Ord B}} (p : A -> B) (x : B) : AVLTree A -> AVLTree A := +--- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (fun a1 == fun a2) == (a1 == a2) +{-# specialize: [1, 2, 3] #-} +deleteWith + {A B} + {{orderA : Ord A}} + {{orderB : Ord B}} + (fun : A -> B) + (elem : B) + (tree : AVLTree A) + : AVLTree A := let - {-# specialize-by: [o, po, p] #-} - deleteMin : AVLTree A -> Maybe (Pair A (AVLTree A)) - | empty := nothing - | (node v _ l r) := - case deleteMin l of - | nothing := just (v, r) - | just (m, l') := just (m, mknode v l' r); - {-# specialize-by: [o, po, p] #-} + {-# specialize-by: [orderA, orderB, fun] #-} go : AVLTree A -> AVLTree A | empty := empty - | (node y h l r) := - case Ord.cmp x (p y) of - | LT := balance (mknode y (go l) r) - | GT := balance (mknode y l (go r)) - | EQ := - case l of - | empty := r + | node@{element; left; right} := + case Ord.cmp elem (fun element) of + | LessThan := balance (mkNode element (go left) right) + | GreaterThan := balance (mkNode element left (go right)) + | Equal := + case left of + | empty := right | _ := - case deleteMin r of - | nothing := l - | just (minRight, r') := balance (mknode minRight l r'); - in go; + case deleteMin right of + | nothing := left + | just (minRight, right') := balance (mkNode minRight left right'); + in go tree; --- 𝒪(log 𝓃). Removes an element from an ;AVLTree;. +{-# specialize: [1] #-} delete {A} {{o : Ord A}} : A -> AVLTree A -> AVLTree A := deleteWith id; --- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;. @@ -172,73 +202,78 @@ lookupMax {A} : AVLTree A -> Maybe A | (node _ _ l empty) := lookupMax l | (node _ _ _ r) := lookupMax r; ---- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;. +--- 𝒪(𝒹 log 𝓃). Deletes elements from an ;AVLTree;. {-# specialize: [1] #-} deleteMany {A} {{Ord A}} : List A -> AVLTree A -> AVLTree A := deleteManyWith id; ---- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree; based on a projected comparison value. +--- 𝒪(𝒹 log 𝓃). Deletes elements from an ;AVLTree; based on a projected comparison value. --- ---- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2) -{-# specialize: [2] #-} -deleteManyWith {A B} {{Ord A}} {{Ord B}} (p : A -> B) (d : List B) (t : AVLTree A) : AVLTree A := - for (acc := t) (x in d) - deleteWith p x acc; +--- Assumption: Ord A and Ord B are compatible, i.e., for a1 a2 in A, we have (fun a1 == fun a2) == (a1 == a2) +{-# specialize: [1, 2] #-} +deleteManyWith + {A B} {{Ord A}} {{Ord B}} (fun : A -> B) (toDelete : List B) (tree : AVLTree A) : AVLTree A := + for (acc := tree) (x in toDelete) {deleteWith fun x acc}; --- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that --- every two children do not differ on height by more than 1. -isBalanced {A} : AVLTree A -> Bool +isBalanced {A} : (tree : AVLTree A) -> Bool | empty := true - | n@(node _ _ l r) := isBalanced l && isBalanced r && abs (diffFactor n) <= 1; + | tree@node@{left; right} := isBalanced left && isBalanced right && abs (diffFactor tree) <= 1; --- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;. {-# specialize: [1] #-} -fromList {A} {{Ord A}} (l : List A) : AVLTree A := for (acc := empty) (x in l) insert x acc; +fromList {A} {{Ord A}} (list : List A) : AVLTree A := for (acc := empty) (x in list) {insert x acc}; --- 𝒪(𝓃). Returns the number of elements of an ;AVLTree;. size {A} : AVLTree A -> Nat | empty := 0 - | (node _ _ l r) := 1 + size l + size r; + | node@{left; right} := 1 + size left + size right; ---- 𝒪(𝓃). Returns the elements of an ;AVLTree; in ascending order. +-- TODO: Implement this tail-recursively with an accumulator. Then it will be O(n). +--- 𝒪(n log n). Returns the elements of an ;AVLTree; in ascending order. toList {A} : AVLTree A -> List A | empty := nil - | (node x _ l r) := toList l ++ (x :: nil) ++ toList r; + | node@{element; left; right} := toList left ++ (element :: nil) ++ toList right; ---- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of both ;AVLTree;s. +-- TODO: avoid conversion to list. +--- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of both ;AVLTree;s. intersection {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := - toList s1 |> filter \ {x := member? x s2} |> fromList; + toList s1 |> filter \ {x := isMember x s2} |> fromList; ---- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of the first but not the second ;AVLTree;. +-- TODO: avoid conversion to list. +--- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of the first but not the second ;AVLTree;. difference {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := - toList s1 |> filter \ {x := not (member? x s2)} |> fromList; + toList s1 |> filter \ {x := not (isMember x s2)} |> fromList; ---- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of either the first or second ;AVLTree;. +-- TODO: avoid conversion to list. +--- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of either the first or second ;AVLTree;. union {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := fromList (toList s1 ++ toList s2); ---- 𝒪(𝓃). Formats the tree in a debug friendly format. -prettyDebug {A} {{Show A}} : AVLTree A -> String := +--- Formats the tree in a debug friendly format. +prettyDebug {A} {{Show A}} (tree : AVLTree A) : String := let go : AVLTree A -> String | empty := "_" - | n@(node v h l r) := + | tree@node@{element; left; right} := "(" - ++str go l + ++str go left ++str " h" - ++str Show.show (diffFactor n) + ++str Show.show (diffFactor tree) ++str " " - ++str Show.show v + ++str Show.show element ++str " " - ++str go r + ++str go right ++str ")"; - in go; + in go tree; --- 𝒪(𝓃). -toTree {A} : AVLTree A -> Maybe (Tree A) +toTree {A} : (tree : AVLTree A) -> Maybe (Tree A) | empty := nothing - | (node v _ l r) := just (Tree.node v (catMaybes (toTree l :: toTree r :: nil))); + | node@{element; left; right} := + just (Tree.node element (catMaybes (toTree left :: toTree right :: nil))); --- Returns the textual representation of an ;AVLTree;. -pretty {A} {{Show A}} : AVLTree A -> String := toTree >> maybe "empty" Tree.treeToString; +pretty {A} {{Show A}} (tree : AVLTree A) : String := maybe "empty" Tree.treeToString (toTree tree); -- TODO: remove toList instance @@ -248,16 +283,17 @@ eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) := mkEq ((==) on toList); instance ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) := mkOrd (Ord.cmp on toList); +-- TODO: remove toList {-# specialize: true, inline: case #-} instance polymorphicFoldableAVLTreeI : Polymorphic.Foldable AVLTree := Polymorphic.mkFoldable@{ - for {A B} (f : B -> A -> B) (acc : B) : AVLTree A -> B := - toList >> Polymorphic.Foldable.for f acc; - rfor {A B} (f : B → A → B) (acc : B) : AVLTree A -> B := - toList >> Polymorphic.Foldable.rfor f acc + for {A B} (f : B -> A -> B) (acc : B) (tree : AVLTree A) : B := + Polymorphic.Foldable.for f acc (toList tree); + rfor {A B} (f : B → A → B) (acc : B) (tree : AVLTree A) : B := + Polymorphic.Foldable.rfor f acc (toList tree) }; {-# specialize: true, inline: true #-} instance -foldableVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable; +foldableAVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable; diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix index ed81c3b2..a55090fc 100644 --- a/Stdlib/Data/String/Base.juvix +++ b/Stdlib/Data/String/Base.juvix @@ -6,7 +6,7 @@ import Stdlib.Function open; import Stdlib.Data.Fixity open; --- Concatenates a ;List; of ;String;s. -concatStr : List String -> String := listFoldl (++str) ""; +concatStr (string : List String) : String := listFoldl (++str) "" string; --- Joins a ;List; of ;String;s with "\n". -unlines : List String -> String := intersperse "\n" >> concatStr; +unlines (list : List String) : String := concatStr (intersperse "\n" list); diff --git a/Stdlib/Data/String/Ord.juvix b/Stdlib/Data/String/Ord.juvix index 474795ec..af56de05 100644 --- a/Stdlib/Data/String/Ord.juvix +++ b/Stdlib/Data/String/Ord.juvix @@ -8,4 +8,4 @@ import Stdlib.Data.Bool open; syntax operator == comparison; --- Equality for ;String;s. builtin string-eq -axiom == : String → String → Bool; +axiom == : String -> String -> Bool; diff --git a/Stdlib/Data/Tree.juvix b/Stdlib/Data/Tree.juvix index c5e943f5..3756df8e 100644 --- a/Stdlib/Data/Tree.juvix +++ b/Stdlib/Data/Tree.juvix @@ -10,22 +10,26 @@ import Stdlib.Function open; Forest (A : Type) : Type := List (Tree A); --- N-Ary tree. -positive -type Tree (A : Type) := node A (List (Tree A)); - -shift (first other : String) (xs : List String) : List String := - zipWith (++str) (first :: replicate (length xs) other) xs; +type Tree (A : Type) := + node { + element : A; + children : List (Tree A) + }; terminating -draw {A} {{Show A}} : Tree A -> List String - | (node v cs) := Show.show v :: drawForest cs; +draw {A} {{Show A}} (tree : Tree A) : List String := + Show.show (Tree.element tree) :: drawForest (Tree.children tree); terminating -drawForest {A} {{Show A}} : Forest A -> List String - | [] := [] - | [h] := "|" :: shift "`- " " " (draw h) - | (h :: hs) := "|" :: shift "+- " "| " (draw h) ++ drawForest hs; - -treeToString {A} {{Show A}} : Tree A -> String := draw >> unlines; - -forestToString {A} {{Show A}} : Forest A -> String := drawForest >> unlines; +drawForest {A} {{Show A}} (forest : Forest A) : List String := + let + shift (first other : String) (xs : List String) : List String := + zipWith (++str) (first :: replicate (length xs) other) xs; + in case forest of + | [] := [] + | [h] := "|" :: shift "`- " " " (draw h) + | h :: hs := "|" :: shift "+- " "| " (draw h) ++ drawForest hs; + +treeToString {A} {{Show A}} (tree : Tree A) : String := unlines (draw tree); + +forestToString {A} {{Show A}} (forest : Forest A) : String := unlines (drawForest forest); diff --git a/Stdlib/Data/UnbalancedSet.juvix b/Stdlib/Data/UnbalancedSet.juvix index db420594..f1af8245 100644 --- a/Stdlib/Data/UnbalancedSet.juvix +++ b/Stdlib/Data/UnbalancedSet.juvix @@ -7,40 +7,46 @@ import Stdlib.Trait.Ord as Ord open using {Ord; mkOrd; module Ord}; import Stdlib.Data.BinaryTree as Tree; open Tree using {BinaryTree; leaf; node}; -type UnbalancedSet (A : Type) := unbalancedSet : Ord A -> BinaryTree A -> UnbalancedSet A; - -empty {A} {{o : Ord A}} : UnbalancedSet A := unbalancedSet o leaf; - -member? {A} (x : A) : UnbalancedSet A -> Bool - | (unbalancedSet o@(mkOrd cmp) t) := - let - go : BinaryTree A -> Bool - | leaf := false - | (node l y r) := - case cmp x y of - | Ord.LT := go l - | Ord.GT := go r - | Ord.EQ := true; - in go t; - -insert {A} (x : A) : UnbalancedSet A -> UnbalancedSet A - | (unbalancedSet o@(mkOrd cmp) t) := - let - go : BinaryTree A -> BinaryTree A - | leaf := node leaf x leaf - | n@(node l y r) := - case cmp x y of - | Ord.LT := node (go l) y r - | Ord.EQ := n - | Ord.GT := node l y (go r); - in unbalancedSet o (go t); - -length {A} : UnbalancedSet A -> Nat - | (unbalancedSet _ t) := Tree.length t; - -to-list {A} : UnbalancedSet A -> List A - | (unbalancedSet _ t) := Tree.to-list t; +type UnbalancedSet (A : Type) := + mkUnbalancedSet { + order : Ord A; + tree : BinaryTree A + }; + +empty {A} {{order : Ord A}} : UnbalancedSet A := mkUnbalancedSet order leaf; + +isMember {A} (elem : A) (set : UnbalancedSet A) : Bool := + case set of + mkUnbalancedSet@{tree} := + let + go : BinaryTree A -> Bool + | leaf := false + | node@{element; left; right} := + case Ord.cmp elem element of + | Ord.LessThan := go left + | Ord.GreaterThan := go right + | Ord.Equal := true; + in go tree; + +insert {A} (elem : A) (set : UnbalancedSet A) : UnbalancedSet A := + case set of + mkUnbalancedSet@{order; tree} := + let + go : BinaryTree A -> BinaryTree A + | leaf := node leaf elem leaf + | tree@(node l y r) := + case Ord.cmp elem y of + | Ord.LessThan := node (go l) y r + | Ord.Equal := tree + | Ord.GreaterThan := node l y (go r); + in mkUnbalancedSet order (go tree); + +length {A} (set : UnbalancedSet A) : Nat := Tree.length (UnbalancedSet.tree set); + +toList {A} (set : UnbalancedSet A) : List A := Tree.toList (UnbalancedSet.tree set); instance -set-ordering {A} {{Ord A}} : Ord (UnbalancedSet A) := - mkOrd λ {s1 s2 := Ord.cmp (to-list s1) (to-list s2)}; +unbalancedSetOrdI {A} {{Ord A}} : Ord (UnbalancedSet A) := + mkOrd@{ + cmp (s1 s2 : UnbalancedSet A) : Ordering := Ord.cmp (toList s1) (toList s2) + }; diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix index e3952ffe..5602f05a 100644 --- a/Stdlib/Data/Unit.juvix +++ b/Stdlib/Data/Unit.juvix @@ -3,6 +3,7 @@ module Stdlib.Data.Unit; import Stdlib.Data.Unit.Base open public; import Stdlib.Data.Bool.Base open; +import Stdlib.Data.String.Base open; import Stdlib.Trait.Eq open; import Stdlib.Trait.Ord open; @@ -10,20 +11,31 @@ import Stdlib.Trait.Show open; import Stdlib.Trait.Foldable open; instance -eqUnitI : Eq Unit := mkEq λ {unit unit := true}; +eqUnitI : Eq Unit := + mkEq@{ + eq (_ _ : Unit) : Bool := true + }; instance -ordUnitI : Ord Unit := mkOrd λ {unit unit := EQ}; +ordUnitI : Ord Unit := + mkOrd@{ + cmp (_ _ : Unit) : Ordering := Equal + }; instance -showUnitI : Show Unit := mkShow λ {unit := "unit"}; +showUnitI : Show Unit := + mkShow@{ + show (_ : Unit) : String := "unit" + }; {-# specialize: true, inline: case #-} instance foldableUnitI : Foldable Unit Unit := mkFoldable@{ {-# inline: true #-} - rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit; + rfor {Acc : Type} (fun : Acc -> Unit -> Acc) (initialValue : Acc) (_ : Unit) : Acc := + fun initialValue unit; {-# inline: true #-} - for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit + for {Acc : Type} (fun : Acc -> Unit -> Acc) (initialValue : Acc) (_ : Unit) : Acc := + fun initialValue unit }; diff --git a/Stdlib/Debug/Fail.juvix b/Stdlib/Debug/Fail.juvix index 9eaf4d60..45a106e6 100644 --- a/Stdlib/Debug/Fail.juvix +++ b/Stdlib/Debug/Fail.juvix @@ -2,6 +2,6 @@ module Stdlib.Debug.Fail; import Stdlib.Data.String.Base open; ---- Primitive that exits the program with an error message. +--- Exit the program with an error message. builtin fail -axiom failwith : {A : Type} → String → A; +axiom failwith : {A : Type} -> (message : String) -> A; diff --git a/Stdlib/Debug/Trace.juvix b/Stdlib/Debug/Trace.juvix index 5495df18..b26d0c01 100644 --- a/Stdlib/Debug/Trace.juvix +++ b/Stdlib/Debug/Trace.juvix @@ -2,4 +2,4 @@ module Stdlib.Debug.Trace; --- Primitive that prints the given element and returns it. builtin trace -axiom trace : {A : Type} → A → A; +axiom trace : {A : Type} -> A -> A; diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix index 5c7455d0..5a7d778b 100644 --- a/Stdlib/Extra/Gcd.juvix +++ b/Stdlib/Extra/Gcd.juvix @@ -6,11 +6,16 @@ import Stdlib.Trait.Eq open; import Stdlib.Trait.Ord open; import Stdlib.Data.Bool open; ---- Computes the greatest common divisor. +--- Computes the greatest common divisor of `a` and `b`. gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} {{DivMod A}} (a b : A) : A := let -- Internal helper for computing the greatest common divisor. The first element -- should be smaller than the second. terminating - gcd' (a b : A) : A := ite (a == 0) b (gcd' (mod b a) a); - in ite (a > b) (gcd' b a) (gcd' a b); + gcd' (a b : A) : A := + if + | a == 0 := b + | else := gcd' (mod b a) a; + in if + | a > b := gcd' b a + | else := gcd' a b; diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix index c1b9e53e..2cdf6874 100644 --- a/Stdlib/Function.juvix +++ b/Stdlib/Function.juvix @@ -6,51 +6,52 @@ import Stdlib.Data.Pair.Base open; syntax operator << composition; ---- Function composition, passing results from the second function to the first. +--- Function composition, passing results from the second function `g` to the first function `f`. {-# inline: 2 #-} -<< {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x); +<< {A B C} (f : B -> C) (g : A -> B) (x : A) : C := f (g x); syntax operator >> lcomposition; ---- Function composition, passing results from the first function to the second. +--- Function composition, passing results from the first function `f` to the second function `g`. {-# inline: 2 #-} ->> {A B C} (f : A → B) (g : B → C) (x : A) : C := g (f x); +>> {A B C} (f : A -> B) (g : B -> C) (x : A) : C := g (f x); ---- Always returns the first argument. +--- Always returns the first argument `a`. {-# inline: 1 #-} const {A B} (a : A) (_ : B) : A := a; --- The identity function. id {A} (a : A) : A := a; ---- Swaps the order of the arguments of the given function. +--- Swaps the order of the arguments of the given function `f`. {-# inline: 1 #-} -flip {A B C} (f : A → B → C) (b : B) (a : A) : C := f a b; +flip {A B C} (f : A -> B -> C) (b : B) (a : A) : C := f a b; syntax operator <| rapp; --- Application operator with right associativity. Usually used as a syntactical --- facility. -<| {A B} (f : A → B) (x : A) : B := f x; +<| {A B} (f : A -> B) (x : A) : B := f x; syntax operator |> lapp; --- Application operator with left associativity. Usually used as a syntactical --- facility. -|> {A B} (x : A) (f : A → B) : B := f x; +|> {A B} (x : A) (f : A -> B) : B := f x; --- Applies a function n times. -iterate {A} : Nat -> (A -> A) -> A -> A +iterate {A} : (n : Nat) -> (fun : A -> A) -> (elem : A) -> A | zero _ a := a | (suc n) f a := iterate n f (f a); syntax operator on lapp; +--- `(f on g) a b` is equivalent to `f (g a) (g b)`. {-# inline: 2 #-} -on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C := f (g a) (g b); +on {A B C} (f : B -> B -> C) (g : A -> B) (a b : A) : C := f (g a) (g b); syntax operator >-> seq; builtin seq ->-> : {A B : Type} → A → B → B +>-> : {A B : Type} -> A -> B -> B | x y := y; diff --git a/Stdlib/System/IO/Base.juvix b/Stdlib/System/IO/Base.juvix index 67722245..1277b331 100644 --- a/Stdlib/System/IO/Base.juvix +++ b/Stdlib/System/IO/Base.juvix @@ -7,4 +7,4 @@ axiom IO : Type; syntax operator >>> seq; builtin IO-sequence -axiom >>> : IO → IO → IO; +axiom >>> : IO -> IO -> IO; diff --git a/Stdlib/System/IO/Bool.juvix b/Stdlib/System/IO/Bool.juvix index 23e53233..8fdecece 100644 --- a/Stdlib/System/IO/Bool.juvix +++ b/Stdlib/System/IO/Bool.juvix @@ -5,6 +5,6 @@ import Stdlib.Data.Bool open; import Stdlib.System.IO.String open; builtin bool-print -axiom printBool : Bool → IO; +axiom printBool : Bool -> IO; printBoolLn (b : Bool) : IO := printBool b >>> printString "\n"; diff --git a/Stdlib/System/IO/Int.juvix b/Stdlib/System/IO/Int.juvix index abe531e8..66f9214a 100644 --- a/Stdlib/System/IO/Int.juvix +++ b/Stdlib/System/IO/Int.juvix @@ -5,6 +5,6 @@ import Stdlib.Data.Int open using {Int}; import Stdlib.System.IO.String open; builtin int-print -axiom printInt : Int → IO; +axiom printInt : Int -> IO; printIntLn (i : Int) : IO := printInt i >>> printString "\n"; diff --git a/Stdlib/System/IO/Nat.juvix b/Stdlib/System/IO/Nat.juvix index 8f787ae6..d21359b8 100644 --- a/Stdlib/System/IO/Nat.juvix +++ b/Stdlib/System/IO/Nat.juvix @@ -5,6 +5,6 @@ import Stdlib.Data.Nat open; import Stdlib.System.IO.String open; builtin nat-print -axiom printNat : Nat → IO; +axiom printNat : Nat -> IO; printNatLn (n : Nat) : IO := printNat n >>> printString "\n"; diff --git a/Stdlib/System/IO/String.juvix b/Stdlib/System/IO/String.juvix index e79c8668..4685d322 100644 --- a/Stdlib/System/IO/String.juvix +++ b/Stdlib/System/IO/String.juvix @@ -4,9 +4,9 @@ import Stdlib.System.IO.Base open; import Stdlib.Data.String open; builtin string-print -axiom printString : String → IO; +axiom printString : String -> IO; builtin IO-readline -axiom readLn : (String → IO) → IO; +axiom readLn : (String -> IO) -> IO; printStringLn (s : String) : IO := printString s >>> printString "\n"; diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix index d556da7c..d6e6c596 100644 --- a/Stdlib/Trait/Applicative.juvix +++ b/Stdlib/Trait/Applicative.juvix @@ -11,22 +11,22 @@ import Stdlib.Trait.Foldable.Polymorphic open; import Stdlib.Data.Unit.Base open; trait -type Applicative (f : Type -> Type) := +type Applicative (F : Type -> Type) := mkApplicative { - {{functor}} : Functor f; - pure : {A : Type} -> A -> f A; - ap : {A B : Type} -> f (A -> B) -> f A -> f B + {{functor}} : Functor F; + pure : {A : Type} -> A -> F A; + ap : {A B : Type} -> F (A -> B) -> F A -> F B }; open Applicative public; --- Sequences computations. --- Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance. -applicativeSeq {f : Type -> Type} {{Applicative f}} {A B : Type} (fa : f A) (fb : f B) : f B := +applicativeSeq {F : Type -> Type} {{Applicative F}} {A B : Type} (fa : F A) (fb : F B) : F B := ap (map λ {_ b := b} fa) fb; --- lifts a binary function to ;Applicative; -liftA2 {f : Type -> Type} {{Applicative f}} {A B C} (fun : A -> B -> C) : f A -> f B -> f C := +liftA2 {F : Type -> Type} {{Applicative F}} {A B C} (fun : A -> B -> C) : F A -> F B -> F C := map fun >> ap; syntax iterator mapA_ {init := 0; range := 1}; @@ -40,10 +40,10 @@ mapA_ (l : t A) : f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc}; -replicateA {f : Type -> Type} {A} {{Applicative f}} : Nat -> f A -> f (List A) +replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A) | zero _ := pure [] | (suc n) x := liftA2 (::) x (replicateA n x); -when {f : Type -> Type} {{Applicative f}} : Bool -> f Unit -> f Unit +when {F : Type -> Type} {{Applicative F}} : Bool -> F Unit -> F Unit | false _ := pure unit | true a := a; diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix index 9ccb3c4d..787809e1 100644 --- a/Stdlib/Trait/Eq.juvix +++ b/Stdlib/Trait/Eq.juvix @@ -13,6 +13,6 @@ syntax operator /= comparison; {-# inline: always, isabelle-operator: {name: "=", prec: 50, assoc: none} #-} == {A} {{Eq A}} : A -> A -> Bool := Eq.eq; ---- Tests for inequality. +--- Test for inequality. {-# inline: always, isabelle-operator: {name: "\\", prec: 50, assoc: none} #-} /= {A} {{Eq A}} (x y : A) : Bool := not (x == y); diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix index 319e62cc..e546414f 100644 --- a/Stdlib/Trait/Foldable/Monomorphic.juvix +++ b/Stdlib/Trait/Foldable/Monomorphic.juvix @@ -6,13 +6,13 @@ import Stdlib.Trait.Foldable.Polymorphic as Poly; --- A trait for combining elements into a single result, processing one element at a time. {-# specialize: true #-} trait -type Foldable (container elem : Type) := +type Foldable (Container Elem : Type) := mkFoldable { syntax iterator for {init := 1; range := 1}; - for : {B : Type} -> (B -> elem -> B) -> B -> container -> B; + for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B; syntax iterator rfor {init := 1; range := 1}; - rfor : {B : Type} -> (B -> elem -> B) -> B → container → B + rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B }; open Foldable public; @@ -21,7 +21,7 @@ open Foldable public; --- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance. {-# inline: case #-} fromPolymorphicFoldable - {f : Type -> Type} {{foldable : Poly.Foldable f}} {elem} : Foldable (f elem) elem := + {F : Type -> Type} {{foldable : Poly.Foldable F}} {Elem} : Foldable (F Elem) Elem := mkFoldable@{ for := Poly.for; rfor := Poly.rfor @@ -29,19 +29,21 @@ fromPolymorphicFoldable {-# inline: true #-} foldl - {container elem} - {{Foldable container elem}} - {B : Type} - (g : B -> elem -> B) - (ini : B) - (ls : container) - : B := for (acc := ini) (x in ls) {g acc x}; + {Container Elem} + {{Foldable Container Elem}} + {Acc : Type} + (fun : Acc -> Elem -> Acc) + (initialValue : Acc) + (container : Container) + : Acc := for (acc := initialValue) (x in container) {fun acc x}; --- Combine the elements of the type using the provided function starting with the element in the right-most position. {-# inline: 2 #-} foldr - {container elem : Type} - {{Foldable container elem}} - {B : Type} - (g : elem -> B -> B) - : B -> container -> B := foldl (flip g); + {Container Elem : Type} + {{Foldable Container Elem}} + {Acc : Type} + (fun : Elem -> Acc -> Acc) + (initialValue : Acc) + (container : Container) + : Acc := foldl (flip fun) initialValue container; diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix index 624cb6cb..45d813e1 100644 --- a/Stdlib/Trait/Foldable/Polymorphic.juvix +++ b/Stdlib/Trait/Foldable/Polymorphic.juvix @@ -4,23 +4,35 @@ import Stdlib.Function open; --- A trait for combining elements into a single result, processing one element at a time. trait -type Foldable (f : Type -> Type) := +type Foldable (F : Type -> Type) := mkFoldable { syntax iterator for {init := 1; range := 1}; - for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B; + for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B; syntax iterator rfor {init := 1; range := 1}; - rfor : {A B : Type} -> (B → A → B) -> B → f A → B + rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B }; open Foldable public; --- Combine the elements of the type using the provided function starting with the element in the left-most position. {-# inline: true #-} -foldl {f : Type -> Type} {{Foldable f}} {A B : Type} (g : B -> A -> B) (ini : B) (ls : f A) : B := - for (acc := ini) (x in ls) {g acc x}; +foldl + {F : Type -> Type} + {{Foldable F}} + {Elem Acc : Type} + (fun : Acc -> Elem -> Acc) + (initialValue : Acc) + (container : F Elem) + : Acc := for (acc := initialValue) (x in container) {fun acc x}; --- Combine the elements of the type using the provided function starting with the element in the right-most position. {-# inline: true #-} -foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) (ini : B) (ls : f A) : B := - rfor (acc := ini) (x in ls) {g x acc}; +foldr + {F : Type -> Type} + {{Foldable F}} + {Elem Acc : Type} + (fun : Elem -> Acc -> Acc) + (initialValue : Acc) + (container : F Elem) + : Acc := rfor (acc := initialValue) (x in container) {fun x acc}; diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix index c5c188e2..8a4343ad 100644 --- a/Stdlib/Trait/Functor/Monomorphic.juvix +++ b/Stdlib/Trait/Functor/Monomorphic.juvix @@ -6,26 +6,35 @@ import Stdlib.Trait.Functor.Polymorphic as Poly; {-# specialize: true #-} trait -type Functor (container elem : Type) := +type Functor (Container Elem : Type) := mkFunctor { syntax iterator map {init := 0; range := 1}; {-# specialize: [1] #-} - map : (elem -> elem) -> container -> container + map : (Elem -> Elem) -> Container -> Container }; open Functor public; {-# inline: case #-} -fromPolymorphicFunctor {f : Type -> Type} {{Poly.Functor f}} {elem} : Functor (f elem) elem := +fromPolymorphicFunctor {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem := mkFunctor@{ map := Poly.map }; syntax operator <$> lapp; {-# inline: true #-} -<$> {container elem} {{Functor container elem}} : (elem -> elem) -> container -> container := map; +<$> + {Container Elem} + {{Functor Container Elem}} + (fun : Elem -> Elem) + (container : Container) + : Container := map fun container; syntax operator $> lapp; {-# inline: true #-} -$> {container elem : Type} {{Functor container elem}} (fa : container) (b : elem) : container := - λ {_ := b} <$> fa; +$> + {Container Elem : Type} + {{Functor Container Elem}} + (container : Container) + (element : Elem) + : Container := \ {_ := element} <$> container; diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix index 37b12c02..6fd60520 100644 --- a/Stdlib/Trait/Functor/Polymorphic.juvix +++ b/Stdlib/Trait/Functor/Polymorphic.juvix @@ -5,22 +5,22 @@ import Stdlib.Data.Unit open; {-# specialize: true #-} trait -type Functor (f : Type -> Type) := +type Functor (F : Type -> Type) := mkFunctor { syntax iterator map {init := 0; range := 1}; {-# specialize: [1] #-} - map : {A B : Type} -> (A -> B) -> f A -> f B + map : {A B : Type} -> (A -> B) -> F A -> F B }; open Functor public; syntax operator <$> lapp; {-# inline: true #-} -<$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f B := map; +<$> {F : Type -> Type} {{Functor F}} {A B} (fun : A -> B) (fa : F A) : F B := map fun fa; syntax operator $> lapp; {-# inline: true #-} -$> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B := λ {_ := b} <$> fa; +$> {F : Type → Type} {A B : Type} {{Functor F}} (fa : F A) (b : B) : F B := λ {_ := b} <$> fa; {-# inline: true #-} -void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := fa $> unit; +void {F : Type → Type} {A : Type} {{Functor F}} (fa : F A) : F Unit := fa $> unit; diff --git a/Stdlib/Trait/Monad.juvix b/Stdlib/Trait/Monad.juvix index 8197b4b4..e59ee45d 100644 --- a/Stdlib/Trait/Monad.juvix +++ b/Stdlib/Trait/Monad.juvix @@ -4,17 +4,17 @@ import Stdlib.Data.Fixity open; import Stdlib.Trait.Applicative open; trait -type Monad (m : Type -> Type) := +type Monad (M : Type -> Type) := mkMonad { - {{applicative}} : Applicative m; + {{applicative}} : Applicative M; builtin monad-bind - bind : {A B : Type} -> m A -> (A -> m B) -> m B + bind : {A B : Type} -> M A -> (A -> M B) -> M B }; open Monad public; syntax operator >>= seq; ->>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g; +>>= {A B} {F : Type -> Type} {{Monad F}} (x : F A) (g : A -> F B) : F B := bind x g; syntax operator >=> seq; ->=> {A B C} {f : Type -> Type} {{Monad f}} (h : A -> f B) (g : B -> f C) (a : A) : f C := h a >>= g; +>=> {A B C} {F : Type -> Type} {{Monad F}} (h : A -> F B) (g : B -> F C) (a : A) : F C := h a >>= g; diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix index 8573c4ba..9d3e2a24 100644 --- a/Stdlib/Trait/Ord.juvix +++ b/Stdlib/Trait/Ord.juvix @@ -5,29 +5,33 @@ import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Eq open; type Ordering := - | LT : Ordering - | EQ : Ordering - | GT : Ordering; + | LessThan + | Equal + | GreaterThan; -isLT : Ordering → Bool - | LT := true - | _ := false; +isLessThan (ordering : Ordering) : Bool := + case ordering of + | LessThan := true + | _ := false; -isEQ : Ordering → Bool - | EQ := true - | _ := false; +isEqual (ordering : Ordering) : Bool := + case ordering of + | Equal := true + | _ := false; -isGT : Ordering → Bool - | GT := true - | _ := false; +isGreaterThan (ordering : Ordering) : Bool := + case ordering of + | GreaterThan := true + | _ := false; instance orderingEqI : Eq Ordering := mkEq@{ - eq (x : Ordering) : Ordering -> Bool - | LT := isLT x - | EQ := isEQ x - | GT := isGT x + eq (ordering1 ordering2 : Ordering) : Bool := + case ordering2 of + | LessThan := isLessThan ordering1 + | Equal := isEqual ordering1 + | GreaterThan := isGreaterThan ordering1 }; --- A trait for defining a total order @@ -40,9 +44,9 @@ syntax operator <= comparison; {-# inline: always, isabelle-operator: {name: "\\", prec: 50, assoc: none} #-} <= {A} {{Ord A}} (x y : A) : Bool := case Ord.cmp x y of - | EQ := true - | LT := true - | GT := false; + | Equal := true + | LessThan := true + | GreaterThan := false; syntax operator < comparison; @@ -50,9 +54,9 @@ syntax operator < comparison; {-# inline: always, isabelle-operator: {name: "<", prec: 50, assoc: none} #-} < {A} {{Ord A}} (x y : A) : Bool := case Ord.cmp x y of - | EQ := false - | LT := true - | GT := false; + | Equal := false + | LessThan := true + | GreaterThan := false; syntax operator > comparison; @@ -68,8 +72,14 @@ syntax operator >= comparison; --- Returns the smaller element. {-# inline: always #-} -min {A} {{Ord A}} (x y : A) : A := ite (x < y) x y; +min {A} {{Ord A}} (x y : A) : A := + if + | x < y := x + | else := y; --- Returns the larger element. {-# inline: always #-} -max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y; +max {A} {{Ord A}} (x y : A) : A := + if + | x > y := x + | else := y; diff --git a/Stdlib/Trait/Ord/Eq.juvix b/Stdlib/Trait/Ord/Eq.juvix index c4e90751..9e690469 100644 --- a/Stdlib/Trait/Ord/Eq.juvix +++ b/Stdlib/Trait/Ord/Eq.juvix @@ -12,7 +12,7 @@ syntax operator == comparison; {-# isabelle-operator: {name: "=", prec: 50, assoc: none} #-} == {A} {{Ord A}} (x y : A) : Bool := case Ord.cmp x y of - | EQ := true + | Equal := true | _ := false; syntax operator /= comparison; diff --git a/test/Package.juvix b/test/Package.juvix index 8b63758a..ca94b3e0 100644 --- a/test/Package.juvix +++ b/test/Package.juvix @@ -7,7 +7,7 @@ package : Package := name := "stdlib-test"; dependencies := [ path "../" - ; github "anoma" "juvix-quickcheck" "b398d3cd58f0a7fb9be24d57fc5b3d82f31de555" - ; github "anoma" "juvix-test" "3103c41e055eb9018a851fd3688cd608cad8f55d" + ; github "anoma" "juvix-quickcheck" "4242b864714f98947753544ea1b2cb435f6473d3" + ; github "anoma" "juvix-test" "85811914324b082549cb1f500323884442fc793c" ] }; diff --git a/test/Test.juvix b/test/Test.juvix index 49f8281c..f52e4311 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -17,118 +17,102 @@ import Test.Map open using {suite as mapSuite}; import Test.Queue open using {suite as queueSuite}; import Test.UnbalancedSet open using {suite as unbalancedSetSuite}; -prop-reverseDoesNotChangeLength : List Int -> Bool - | xs := length (reverse xs) == length xs; - -prop-reverseReverseIsIdentity : List Int -> Bool - | xs := eqListInt xs (reverse (reverse xs)); - -prop-tailLengthOneLess : List Int -> Bool - | xs := null xs || ofNat (length (tail xs)) == intSubNat (length xs) 1; - -prop-splitAtRecombine : Nat -> List Int -> Bool - | n xs := case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs); - -prop-splitAtLength : Nat -> List Int -> Bool - | n xs := - case splitAt n (xs ++ replicate (sub n (length xs)) (ofNat 0)) of - lhs, rhs := length lhs == n && length rhs == sub (length xs) n; --- Make sure the list has length at least n - -prop-mergeSumLengths : List Int -> List Int -> Bool - | xs ys := length xs + length ys == length (merge xs ys); - -prop-partition : List Int -> (Int -> Bool) -> Bool - | xs p := - case partition p xs of - lhs, rhs := all p lhs && not (any p rhs) && eqListInt (sortInt xs) (sortInt (lhs ++ rhs)); - -prop-distributive : Int -> Int -> (Int -> Int) -> Bool - | a b f := f (a + b) == f a + f b; - -prop-add-sub : Int -> Int -> Bool - | a b := a == a + b - b; - -prop-add-sub-bad : Int -> Int -> Bool - | a b := a == ofNat 2; - -prop-gcd-bad : Int -> Int -> Bool - | a b := gcd a b > ofNat 1; - -prop-equal-compare-to-eq : Nat -> Bool - | a := Ord.isEQ (Ord.cmp a a); - -prop-sort : (List Int -> List Int) -> List Int -> Bool - | sort xs := - let - sorted : List Int := sort xs; - isSorted : List Int -> Bool - | nil := true - | (_ :: nil) := true - | (x :: y :: xs) := x <= y && isSorted (y :: xs); - in length sorted == length xs && eqListInt sorted (sort sorted) && isSorted sorted; - -prop-zip : List Int -> List Int -> Bool - | xs ys := - let - zs : List (Pair Int Int) := zip xs ys; - expectedLen : Nat := min (length xs) (length ys); - in length zs == expectedLen - && eqListInt (take expectedLen xs) (map fst zs) - && eqListInt (take expectedLen ys) (map snd zs); - -prop-zipWith : (Int -> Int -> Int) -> List Int -> List Int -> Bool - | f xs ys := - let - zs : List Int := zipWith f xs ys; - zsFlip : List Int := zipWith (flip f) ys xs; - expectedLen : Nat := min (length xs) (length ys); - in length zs == expectedLen - && eqListInt zs zsFlip - && eqListInt (map λ {x := f x x} xs) (zipWith f xs xs); - -prop-snoc : List Int -> Int -> Bool - | xs x := - let - snoc-x : List Int := snoc xs x; - in eqListInt snoc-x (reverse (x :: reverse xs)); - -prop-drop : Nat -> List Int -> Bool - | n xs := - let - drop-n : List Int := drop n xs; - in length drop-n <= length xs && eqListInt (drop n (drop n xs)) (drop (2 * n) xs); +propReverseDoesNotChangeLength (xs : List Int) : Bool := length (reverse xs) == length xs; + +propReverseReverseIsIdentity (xs : List Int) : Bool := eqListInt xs (reverse (reverse xs)); + +propTailLengthOneLess (xs : List Int) : Bool := + null xs || ofNat (length (tail xs)) == intSubNat (length xs) 1; + +propSplitAtRecombine (n : Nat) (xs : List Int) : Bool := + case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs); + +propSplitAtLength (n : Nat) (xs : List Int) : Bool := + case splitAt n (xs ++ replicate (sub n (length xs)) (ofNat 0)) of + lhs, rhs := length lhs == n && length rhs == sub (length xs) n; +-- Make sure the list has length at least n (TODO: make sure where?) + +propMergeSumLengths (xs ys : List Int) : Bool := length xs + length ys == length (merge xs ys); + +propPartition (xs : List Int) (predicate : Int -> Bool) : Bool := + case partition predicate xs of + lhs, rhs := + all predicate lhs && not (any predicate rhs) && eqListInt (sortInt xs) (sortInt (lhs ++ rhs)); + +propDistributive (a b : Int) (f : Int -> Int) : Bool := f (a + b) == f a + f b; + +propAddSub (a b : Int) : Bool := a == a + b - b; + +propAddSubBad (a b : Int) : Bool := a == ofNat 2; + +propGcdBad (a b : Int) : Bool := gcd a b > ofNat 1; + +propEqualCompareToEq (a : Nat) : Bool := Ord.isEqual (Ord.cmp a a); + +propSort (sort : List Int -> List Int) (xs : List Int) : Bool := + let + sorted : List Int := sort xs; + isSorted : List Int -> Bool + | nil := true + | (_ :: nil) := true + | (x :: y :: xs) := x <= y && isSorted (y :: xs); + in length sorted == length xs && eqListInt sorted (sort sorted) && isSorted sorted; + +propZip (xs ys : List Int) : Bool := + let + zs : List (Pair Int Int) := zip xs ys; + expectedLen : Nat := min (length xs) (length ys); + in length zs == expectedLen + && eqListInt (take expectedLen xs) (map fst zs) + && eqListInt (take expectedLen ys) (map snd zs); + +propZipWith (f : Int -> Int -> Int) (xs ys : List Int) : Bool := + let + zs : List Int := zipWith f xs ys; + zsFlip : List Int := zipWith (flip f) ys xs; + expectedLen : Nat := min (length xs) (length ys); + in length zs == expectedLen + && eqListInt zs zsFlip + && eqListInt (map λ {x := f x x} xs) (zipWith f xs xs); + +propSnoc (xs : List Int) (x : Int) : Bool := + let + snoc-x : List Int := snoc xs x; + in eqListInt snoc-x (reverse (x :: reverse xs)); + +propDrop (n : Nat) (xs : List Int) : Bool := + let + drop-n : List Int := drop n xs; + in length drop-n <= length xs && eqListInt (drop n (drop n xs)) (drop (2 * n) xs); -- Assumption: The input list represents a rectangular matrix -prop-transposeMatrixId : List (List Int) -> Bool - | xs := Eq.eq xs (transpose (transpose xs)); +propTransposeMatrixId (xs : List (List Int)) : Bool := Eq.eq xs (transpose (transpose xs)); -- Assumption: The input list represents a rectangular matrix -prop-transposeMatrixDimensions : List (List Int) -> Bool - | xs := - let - txs : List (List Int) := transpose xs; - checkTxsRowXsCol : Bool := - case xs of - | x :: _ := length txs == length x - | _ := null txs; - checkXsRowTxsCol : Bool := - case txs of - | tx :: _ := length xs == length tx - | _ := null xs; - in checkTxsRowXsCol && checkXsRowTxsCol; - -prop-foundElementSatisfiesPredicate (p : Int -> Bool) (xs : List Int) : Bool := +propTransposeMatrixDimensions (xs : List (List Int)) : Bool := + let + txs : List (List Int) := transpose xs; + checkTxsRowXsCol : Bool := + case xs of + | x :: _ := length txs == length x + | _ := null txs; + checkXsRowTxsCol : Bool := + case txs of + | tx :: _ := length xs == length tx + | _ := null xs; + in checkTxsRowXsCol && checkXsRowTxsCol; + +propFoundElementSatisfiesPredicate (p : Int -> Bool) (xs : List Int) : Bool := case find p xs of | just x := p x | nothing := true; -prop-nonExistenceImpliesPredicateFalseForAll (p : Int -> Bool) (xs : List Int) : Bool := +propNonExistenceImpliesPredicateFalseForAll (p : Int -> Bool) (xs : List Int) : Bool := case find p xs of | just _ := true | nothing := all (x in xs) not (p x); -prop-findConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool := +propFindConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool := let ys×zs := splitAt n xs; ys := fst ys×zs; @@ -136,14 +120,14 @@ prop-findConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Boo in case find p xs of | just x := if - | elem (==) x ys := find p ys == just x - | elem (==) x zs := find p zs == just x + | isMember x ys := find p ys == just x + | isMember x zs := find p zs == just x | else := false | nothing := true; -prop-findWithEmptyList (p : Int -> Bool) : Bool := find p [] == nothing; +propFindWithEmptyList (p : Int -> Bool) : Bool := find p [] == nothing; -prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool := +propFindWithAlwaysTrueIsJust (xs : List Int) : Bool := if | null xs := true | else := @@ -151,140 +135,148 @@ prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool := | just _ := true | nothing := false; -prop-findWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing; +propFindWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing; -prop-resultErrorApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := +propResultErrorApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := handleResult f g (error x) == f x; -prop-resultOkApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := +propResultOkApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := handleResult f g (ok x) == g x; -prop-resultIsError : Result Int Bool -> Bool - | x@(error _) := isError x - | x@(ok _) := not (isError x); +propResultIsError (result : Result Int Bool) : Bool := + case result of + | error _ := isError result + | ok _ := not (isError result); -prop-resultIsOk : Result Int Bool -> Bool - | x@(error _) := not (isOk x) - | x@(ok _) := isOk x; +propResultIsOk (result : Result Int Bool) : Bool := + case result of + | error _ := not (isOk result) + | ok _ := isOk result; -prop-resultFromErrorDefault (defaultError : Int) : Result Int Bool -> Bool - | e@(error x) := fromError defaultError e == x - | e@(ok _) := fromError defaultError e == defaultError; +propResultFromErrorDefault (defaultError : Int) (result : Result Int Bool) : Bool := + case result of + | error x := fromError defaultError result == x + | ok _ := fromError defaultError result == defaultError; -prop-resultFromOkDefault (defaultOk : Bool) : Result Int Bool -> Bool - | e@(error _) := fromOk defaultOk e == defaultOk - | e@(ok x) := fromOk defaultOk e == x; +propResultFromOkDefault (defaultOk : Bool) (result : Result Int Bool) : Bool := + case result of + | error _ := fromOk defaultOk result == defaultOk + | ok x := fromOk defaultOk result == x; -prop-resultToMaybe : Result Int Bool -> Bool - | e@(error _) := resultToMaybe e == nothing - | e@(ok x) := resultToMaybe e == just x; +propResultToMaybe (result : Result Int Bool) : Bool := + case result of + | error _ := resultToMaybe result == nothing + | ok x := resultToMaybe result == just x; -prop-maybeToResult (def : Int) : Maybe Bool -> Bool - | m@(just x) := maybeToResult def m == ok x - | m@nothing := maybeToResult def m == error def; +propMaybeToResult (def : Int) (maybe : Maybe Bool) : Bool := + case maybe of + | just x := maybeToResult def maybe == ok x + | nothing := maybeToResult def maybe == error def; -prop-resultMapError (f : Int -> Int) : Result Int Int -> Bool - | e@(error x) := mapError f e == error (f x) - | e@(ok _) := mapError f e == e; +propResultMapError (f : Int -> Int) (result : Result Int Int) : Bool := + case result of + | error x := mapError f result == error (f x) + | ok _ := mapError f result == result; -prop-resultMapOk (f : Int -> Int) : Result Int Int -> Bool - | e@(error _) := mapOk f e == e - | e@(ok x) := mapOk f e == ok (f x); +propResultMapOk (f : Int -> Int) (result : Result Int Int) : Bool := + case result of + | error _ := mapOk f result == result + | ok x := mapOk f result == ok (f x); -sortTest : String -> (List Int -> List Int) -> QC.Test - | sortName sort := QC.mkTest ("sort properties: " ++str sortName) (prop-sort sort); +sortTest (sortName : String) (sort : List Int -> List Int) : QC.Test := + QC.mkTest ("sort properties: " ++str sortName) (propSort sort); -dropTest : QC.Test := QC.mkTest "drop properties" prop-drop; +dropTest : QC.Test := QC.mkTest "drop properties" propDrop; -snocTest : QC.Test := QC.mkTest "snoc properties" prop-snoc; +snocTest : QC.Test := QC.mkTest "snoc properties" propSnoc; -zipTest : QC.Test := QC.mkTest "zip properties" prop-zip; +zipTest : QC.Test := QC.mkTest "zip properties" propZip; -zipWithTest : QC.Test := QC.mkTest "zipWith properties" prop-zipWith; +zipWithTest : QC.Test := QC.mkTest "zipWith properties" propZipWith; -equalCompareToEqTest : QC.Test := QC.mkTest "equal Nats compare to EQ" prop-equal-compare-to-eq; +equalCompareToEqTest : QC.Test := QC.mkTest "equal Nats compare to EQ" propEqualCompareToEq; -gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" prop-gcd-bad; +gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" propGcdBad; partitionTest : QC.Test := - QC.mkTest "partition: recombination of the output equals the input" prop-partition; + QC.mkTest "partition: recombination of the output equals the input" propPartition; -testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" prop-distributive; +testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" propDistributive; -reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength; +reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" propReverseDoesNotChangeLength; reverseReverseIdTest : QC.Test := - QC.mkTest "reverse of reverse is identity" prop-reverseReverseIsIdentity; + QC.mkTest "reverse of reverse is identity" propReverseReverseIsIdentity; splitAtRecombineTest : QC.Test := - QC.mkTest "splitAt: recombination of the output is equal to the input list" prop-splitAtRecombine; + QC.mkTest "splitAt: recombination of the output is equal to the input list" propSplitAtRecombine; 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; + propSplitAtLength; mergeSumLengthsTest : QC.Test := QC.mkTest "merge: sum of the lengths of input lists is equal to the length of output list" - prop-mergeSumLengths; + propMergeSumLengths; tailLengthOneLessTest : QC.Test := - QC.mkTest "tail: length of output is one less than input unless empty" prop-tailLengthOneLess; + QC.mkTest "tail: length of output is one less than input unless empty" propTailLengthOneLess; transposeMatrixIdTest : QC.Test := QC.mkTest {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}} "transpose: recrangular matrix has property transpose . transpose = id" - prop-transposeMatrixId; + propTransposeMatrixId; transposeMatrixDimentionsTest : QC.Test := QC.mkTest {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}} "transpose: transpose swaps dimensions" - prop-transposeMatrixDimensions; + propTransposeMatrixDimensions; findFoundElementSatisfiesPredicate : QC.Test := - QC.mkTest "find: found element satisfies predicate" prop-foundElementSatisfiesPredicate; + QC.mkTest "find: found element satisfies predicate" propFoundElementSatisfiesPredicate; findNonExistenceImpliesPredicateFalseForAll : QC.Test := QC.mkTest "find: non existence implies predicate false for all" - prop-nonExistenceImpliesPredicateFalseForAll; + propNonExistenceImpliesPredicateFalseForAll; findConsistentWithSplitAt : QC.Test := - QC.mkTest "find: consistent with splitAt" prop-findConsistentWithSplitAt; + QC.mkTest "find: consistent with splitAt" propFindConsistentWithSplitAt; findOnEmptyListIsNothing : QC.Test := - QC.mkTest "find: called with empty list is nothing" prop-findWithEmptyList; + QC.mkTest "find: called with empty list is nothing" propFindWithEmptyList; findWithAlwaysTrueIsJust : QC.Test := - QC.mkTest "find: always true predicate returns just" prop-findWithAlwaysTrueIsJust; + QC.mkTest "find: always true predicate returns just" propFindWithAlwaysTrueIsJust; findWithAlwaysFalseIsNothing : QC.Test := - QC.mkTest "find: always false predicate returns nothing" prop-findWithAlwaysFalseIsNothing; + QC.mkTest "find: always false predicate returns nothing" propFindWithAlwaysFalseIsNothing; resultResultErrorApplication : QC.Test := - QC.mkTest "result: result error application" prop-resultErrorApplication; + QC.mkTest "result: result error application" propResultErrorApplication; resultResultOkApplication : QC.Test := - QC.mkTest "result: result ok application" prop-resultOkApplication; + QC.mkTest "result: result ok application" propResultOkApplication; -resultIsError : QC.Test := QC.mkTest "result: isError detects error" prop-resultIsError; +resultIsError : QC.Test := QC.mkTest "result: isError detects error" propResultIsError; -resultIsOk : QC.Test := QC.mkTest "result: isOk detects ok" prop-resultIsOk; +resultIsOk : QC.Test := QC.mkTest "result: isOk detects ok" propResultIsOk; -resultFromError : QC.Test := QC.mkTest "result: fromError uses default" prop-resultFromErrorDefault; +resultFromError : QC.Test := QC.mkTest "result: fromError uses default" propResultFromErrorDefault; -resultFromOk : QC.Test := QC.mkTest "result: fromOk uses default" prop-resultFromOkDefault; +resultFromOk : QC.Test := QC.mkTest "result: fromOk uses default" propResultFromOkDefault; -resultResultToMaybe : QC.Test := QC.mkTest "result: resultToMaybe" prop-resultToMaybe; +resultResultToMaybe : QC.Test := QC.mkTest "result: resultToMaybe" propResultToMaybe; -resultMaybeToResult : QC.Test := QC.mkTest "result: maybeToResult" prop-maybeToResult; +resultMaybeToResult : QC.Test := QC.mkTest "result: maybeToResult" propMaybeToResult; -resultMapError : QC.Test := QC.mkTest "result: mapError" prop-resultMapError; +resultMapError : QC.Test := QC.mkTest "result: mapError" propResultMapError; -resultMapOk : QC.Test := QC.mkTest "result: mapOk" prop-resultMapOk; +resultMapOk : QC.Test := QC.mkTest "result: mapOk" propResultMapOk; main : IO := readLn diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix index 37c924b9..d70ab6a7 100644 --- a/test/Test/AVL.juvix +++ b/test/Test/AVL.juvix @@ -3,7 +3,7 @@ module Test.AVL; import Test.JuvixUnit open; import Stdlib.Prelude open; -import Stdlib.Data.Set.AVL open; +import Stdlib.Data.Set.AVL as AVL open; type Box := mkBox {b : Nat}; @@ -11,16 +11,17 @@ instance BoxOrdI : Ord Box := mkOrd (Ord.cmp on Box.b); --- Test for size and balance. -mkTests {A} : TestDescr A -> List Test - | mkTestDescr@{testTitle; testLen; testSet} := - let - mkTitle : String -> String - | m := testTitle ++str " " ++str m; - sizeMsg : String := "sizes do not match"; - balanceMsg : String := "not balanced"; - in [ testCase (mkTitle "size") (assertEqual sizeMsg (size testSet) testLen) - ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced testSet)) - ]; +mkTests {A} (descr : TestDescr A) : List Test := + case descr of + mkTestDescr@{testTitle; testLen; testSet} := + let + mkTitle : String -> String + | m := testTitle ++str " " ++str m; + sizeMsg : String := "sizes do not match"; + balanceMsg : String := "not balanced"; + in [ testCase (mkTitle "size") (assertEqual sizeMsg (size testSet) testLen) + ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced testSet)) + ]; type TestDescr (A : Type) := mkTestDescr { @@ -29,22 +30,22 @@ type TestDescr (A : Type) := testSet : AVLTree A }; -s1-tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9]; +s1Tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9]; -s2-tree : AVLTree Nat := fromList [1; 3; 0; 4; 4; 8; 2]; +s2Tree : AVLTree Nat := fromList [1; 3; 0; 4; 4; 8; 2]; -s1 : TestDescr Nat := mkTestDescr "s1" 5 s1-tree; +s1 : TestDescr Nat := mkTestDescr "s1" 5 s1Tree; -s2 : TestDescr Nat := mkTestDescr "s2" 6 s2-tree; +s2 : TestDescr Nat := mkTestDescr "s2" 6 s2Tree; -s2-delete : TestDescr Nat := +s2Delete : TestDescr Nat := mkTestDescr@{ testTitle := TestDescr.testTitle s2 ++str "-delete"; testLen := sub (TestDescr.testLen s2) 2; testSet := deleteMany [1; 8] (TestDescr.testSet s2) }; -s2-delete-with : TestDescr Box := +s2DeleteWith : TestDescr Box := mkTestDescr@{ testTitle := TestDescr.testTitle s2 ++str "-delete-with"; testLen := sub (TestDescr.testLen s2) 2; @@ -66,31 +67,26 @@ s4 : TestDescr Nat := }; tests : List Test := - [ testCase "s1-member" (assertTrue "member? 3 s1" (member? 3 s1-tree)) + [ testCase "s1-member" (assertTrue "member? 3 s1" (AVL.isMember 3 s1Tree)) ; testCase "s1-s2-intersection" - (assertEqual - "intersection s1-tree s2-tree" - (intersection s1-tree s2-tree) - (fromList [1; 2; 3; 8])) + (assertEqual "intersection s1Tree s2Tree" (intersection s1Tree s2Tree) (fromList [1; 2; 3; 8])) ; testCase "s1-s2-difference" - (assertEqual "difference s1-tree s2-tree" (difference s1-tree s2-tree) (fromList [9])) + (assertEqual "difference s1Tree s2Tree" (difference s1Tree s2Tree) (fromList [9])) ; testCase "s1-s2-union" - (assertEqual "union s1-tree s2-tree" (union s1-tree s2-tree) (fromList [0; 1; 2; 3; 4; 8; 9])) + (assertEqual "union s1Tree s2Tree" (union s1Tree s2Tree) (fromList [0; 1; 2; 3; 4; 8; 9])) ; testCase "for ascending iteration" <| assertEqual "for iterates in ascending order" [1; 2; 3; 4] - <| for (acc := []) (k in fromList [3; 2; 4; 1]) - snoc acc k + <| for (acc := []) (k in fromList [3; 2; 4; 1]) {snoc acc k} ; testCase "rfor ascending iteration" <| assertEqual "rfor iterates in descending order" [4; 3; 2; 1] - <| rfor (acc := []) (k in fromList [3; 2; 4; 1]) - snoc acc k + <| rfor (acc := []) (k in fromList [3; 2; 4; 1]) {snoc acc k} ] - ++ concatMap mkTests [s1; s2; s3; s4; s2-delete]; + ++ concatMap mkTests [s1; s2; s3; s4; s2Delete]; suite : TestSuite := testSuite "AVL Set" tests; main : IO := - printStringLn (pretty s1-tree) >>> printStringLn (prettyDebug s1-tree) >>> runTestSuite suite; + printStringLn (pretty s1Tree) >>> printStringLn (prettyDebug s1Tree) >>> runTestSuite suite; diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix index 6d14a639..10c5b0a3 100644 --- a/test/Test/Arb.juvix +++ b/test/Test/Arb.juvix @@ -6,21 +6,22 @@ import Test.QuickCheck.Arbitrary open; import Test.QuickCheck.Gen open; import Data.Random open; -arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A) - | (mkArbitrary g) := - mkArbitrary - (mkGen - \ {rand := - let - randList : StdGen -> Nat -> List A - | _ zero := nil - | r (suc n) := - let - rSplit : Pair StdGen StdGen := stdSplit r; - r1 : StdGen := fst rSplit; - r2 : StdGen := snd rSplit; - in Gen.run g r1 :: randList r2 n; - in randList rand size}); +arbitrarySizedList {A} (size : Nat) (arbitraryA : Arbitrary A) : Arbitrary (List A) := + case arbitraryA of + mkArbitrary g := + mkArbitrary + (mkGen + \ {rand := + let + randList : StdGen -> Nat -> List A + | _ zero := nil + | r (suc n) := + let + rSplit : Pair StdGen StdGen := stdSplit r; + r1 : StdGen := fst rSplit; + 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)) := diff --git a/test/Test/Map.juvix b/test/Test/Map.juvix index ce4e134c..1cf9c622 100644 --- a/test/Test/Map.juvix +++ b/test/Test/Map.juvix @@ -14,8 +14,8 @@ tests : List Test := let m : Map Nat String := Map.insert 2 "two" (Map.insert 1 "one" Map.empty); m2 : Map Nat Nat := Map.insert 3 4 (Map.insert 1 2 Map.empty); - assertEqListPair : List (Pair Nat Nat) -> List (Pair Nat Nat) -> Assertion - | actual expected := assertEqual "lists are not equal" (quickSort actual) expected; + assertEqListPair (actual : List (Pair Nat Nat)) (expected : List (Pair Nat Nat)) : Assertion := + assertEqual "lists are not equal" (quickSort actual) expected; in [ testCase "Map.lookup missing key" (assertNothing (const "found a key expected to be missing") (Map.lookup 10 m)) diff --git a/test/Test/Queue.juvix b/test/Test/Queue.juvix index c85de1e0..dee7767b 100644 --- a/test/Test/Queue.juvix +++ b/test/Test/Queue.juvix @@ -20,8 +20,8 @@ q4 : Queue Nat := push 4 q3; tests : List Test := let - checkWithList : Queue Nat -> List Nat -> Assertion - | q q' := assertEqual "Queue should be equal" q (fromList q'); + checkWithList (q : Queue Nat) (q' : List Nat) : Assertion := + assertEqual "Queue should be equal" q (fromList q'); in [ testCase "Queue.empty should be empty" (checkWithList q []) ; testCase "Queue.push should add an element" (checkWithList q1 [1]) ; testCase "Queue.push first element should be first pushed" (checkWithList q2 [1; 2]) diff --git a/test/Test/UnbalancedSet.juvix b/test/Test/UnbalancedSet.juvix index 53c62cfe..3a54bb03 100644 --- a/test/Test/UnbalancedSet.juvix +++ b/test/Test/UnbalancedSet.juvix @@ -17,13 +17,13 @@ tests : List Test := (assertEqual "unexpected size" (Set.length s) 3) ; testCase "Set.to-list computes the expected members" - (assertEqual "unexpected memebrs" (quickSort (Set.to-list s)) [1; 2; 3]) + (assertEqual "unexpected memebrs" (quickSort (Set.toList s)) [1; 2; 3]) ; testCase "Set.member? computes true for expected member" - (assertTrue "expected member is not present" (Set.member? 1 s)) + (assertTrue "expected member is not present" (Set.isMember 1 s)) ; testCase "Set.member? computes false for unexpected member" - (assertFalse "unexpected member is present" (Set.member? 0 s)) + (assertFalse "unexpected member is present" (Set.isMember 0 s)) ; testCase "setInSet has length 1" (assertEqual "unexpected size" (Set.length setInSet) 1) ]; diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml index b565a8e3..b8049268 100644 --- a/test/juvix.lock.yaml +++ b/test/juvix.lock.yaml @@ -2,27 +2,27 @@ # Do not edit this file manually. version: 2 -checksum: 05003064be8ff630775c22735af69a82ddd4ac04fdd3ad6aa0c3f01867777225 +checksum: fbbd33d3d068b3369d271021b23b0407838642655173d086f1c81ead9bb338c8 dependencies: - path: ../ dependencies: [] - git: name: anoma_juvix-quickcheck - ref: b398d3cd58f0a7fb9be24d57fc5b3d82f31de555 + ref: 4242b864714f98947753544ea1b2cb435f6473d3 url: https://github.com/anoma/juvix-quickcheck dependencies: - git: name: anoma_juvix-stdlib - ref: af72f25057217619a03b7a5114000d02d0abed31 + ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6 url: https://github.com/anoma/juvix-stdlib dependencies: [] - git: name: anoma_juvix-test - ref: 3103c41e055eb9018a851fd3688cd608cad8f55d + ref: 85811914324b082549cb1f500323884442fc793c url: https://github.com/anoma/juvix-test dependencies: - git: name: anoma_juvix-stdlib - ref: 615a02c8107076ca9661c5234d41792be91a5104 + ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6 url: https://github.com/anoma/juvix-stdlib dependencies: []