From 50aa5838bce1a361a5e0302967debf0671f2daaa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Thu, 28 Sep 2023 18:39:09 +0200 Subject: [PATCH] Add `none` fixity (#84) --- Stdlib/Data/Fixity.juvix | 2 ++ Stdlib/Data/List/Base.juvix | 10 ++++++---- test/Test.juvix | 27 +++++++++++++++------------ 3 files changed, 23 insertions(+), 16 deletions(-) diff --git a/Stdlib/Data/Fixity.juvix b/Stdlib/Data/Fixity.juvix index b4e5465f..df8fe107 100644 --- a/Stdlib/Data/Fixity.juvix +++ b/Stdlib/Data/Fixity.juvix @@ -1,5 +1,7 @@ module Stdlib.Data.Fixity; +syntax fixity none := none; + syntax fixity rapp := binary {assoc := right}; syntax fixity lapp := binary {assoc := left; same := rapp}; syntax fixity seq := binary {assoc := left; above := [lapp]}; diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 47acb4f2..59a1af10 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -114,8 +114,9 @@ merge {A} {{Ord A}} : List A → List A → List A partition {A} (f : A → Bool) : List A → List A × List A | nil := nil, nil | (x :: xs) := - case partition f xs of {l1, l2 := - if (f x) (x :: l1, l2) (l1, x :: l2)}; + case partition f xs of { + l1, l2 := if (f x) (x :: l1, l2) (l1, x :: l2) + }; syntax operator ++ cons; @@ -209,8 +210,9 @@ quickSort {A} {{Ord A}} : List A → List A := | nil := nil | xs@(_ :: nil) := xs | (x :: xs) := - case partition (isGT ∘ Ord.cmp x) xs of {l1, l2 := - go l1 ++ x :: go l2}; + case partition (isGT ∘ Ord.cmp x) xs of { + l1, l2 := go l1 ++ x :: go l2 + }; in go; --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;. diff --git a/test/Test.juvix b/test/Test.juvix index 587611f3..985f59d1 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -28,17 +28,18 @@ prop-tailLengthOneLess : List Int -> Bool prop-splitAtRecombine : Nat -> List Int -> Bool | n xs := - case splitAt n xs of {lhs, rhs := - eqListInt xs (lhs ++ rhs)}; + 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 Nat.== n - && length rhs Nat.== sub (length xs) n}; + case + splitAt n (xs ++ replicate (sub n (length xs)) (ofNat 0)) + of { + lhs, rhs := + length lhs Nat.== n && length rhs Nat.== sub (length xs) n + }; -- Make sure the list has length at least n prop-mergeSumLengths : List Int -> List Int -> Bool @@ -47,10 +48,12 @@ prop-mergeSumLengths : List Int -> List Int -> Bool 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))}; + 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;