From 2bc3b8be3c712fef8667157d1148b4dcd14c3802 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Tue, 7 Nov 2023 17:45:36 +0100 Subject: [PATCH] Literal casts (#87) * Adapts to https://github.com/anoma/juvix/pull/2457 --------- Co-authored-by: Paul Cadman --- Stdlib/Data/Int/Ord.juvix | 3 ++- Stdlib/Data/List/Base.juvix | 4 ++-- Stdlib/Data/Range.juvix | 4 ++-- Stdlib/Data/String.juvix | 1 - Stdlib/Data/String/Base.juvix | 3 +-- Stdlib/Extra/Gcd.juvix | 3 +-- Stdlib/System/IO/Base.juvix | 1 - Stdlib/Trait/Integral.juvix | 1 + Stdlib/Trait/Natural.juvix | 1 + test/Test.juvix | 22 +++++++++++++++++----- 10 files changed, 27 insertions(+), 16 deletions(-) diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix index 1f8d0724..2ae3252b 100644 --- a/Stdlib/Data/Int/Ord.juvix +++ b/Stdlib/Data/Int/Ord.juvix @@ -6,6 +6,7 @@ import Stdlib.Data.Int.Base open; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering}; +import Stdlib.Data.Nat.Base as Nat; import Stdlib.Data.Nat.Ord as Nat; syntax operator == comparison; @@ -32,7 +33,7 @@ syntax operator < comparison; --- Returns ;true; iff the first element is less than the second. builtin int-lt -< (m n : Int) : Bool := m + 1 <= n; +< (m n : Int) : Bool := m + ofNat (Nat.suc Nat.zero) <= n; syntax operator > comparison; diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index b8403f8f..d6a8b120 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -68,7 +68,7 @@ filter {A} (f : A → Bool) : List A → List A --- 𝒪(𝓃). Returns the length of the ;List;. length {A} (l : List A) : Nat := - for (acc := 0) (_ in l) {acc + 1}; + for (acc := zero) (_ in l) {suc acc}; --- 𝒪(𝓃). Returns the given ;List; in reverse order. reverse {A} (l : List A) : List A := @@ -197,7 +197,7 @@ mergeSort {A} {{Ord A}} (l : List A) : List A := | (suc zero) xs := xs | len xs := let - len' : Nat := div len 2; + len' : Nat := div len (suc (suc zero)); splitXs : List A × List A := splitAt len' xs; left : List A := fst splitXs; right : List A := snd splitXs; diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix index 44a13cc9..a4379b14 100644 --- a/Stdlib/Data/Range.juvix +++ b/Stdlib/Data/Range.juvix @@ -5,6 +5,7 @@ import Stdlib.Data.Fixity open; import Stdlib.Data.Bool.Base open; import Stdlib.Trait.Natural open; import Stdlib.Trait.Ord open; +import Stdlib.Data.Nat open; --- A range of naturals type Range N := @@ -31,8 +32,7 @@ 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 (fromNat 1); +to {N} {{Natural N}} (l h : N) : Range N := mkRange l h 1; syntax operator step step; diff --git a/Stdlib/Data/String.juvix b/Stdlib/Data/String.juvix index a7848f6e..745610d5 100644 --- a/Stdlib/Data/String.juvix +++ b/Stdlib/Data/String.juvix @@ -15,4 +15,3 @@ showStringI : Show String := let go (s : String) : String := "\"" ++str s ++str "\""; in mkShow go; - diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix index 4e470104..447c2337 100644 --- a/Stdlib/Data/String/Base.juvix +++ b/Stdlib/Data/String/Base.juvix @@ -1,9 +1,8 @@ module Stdlib.Data.String.Base; -import Stdlib.Data.Fixity open; - import Stdlib.Data.List.Base open; import Stdlib.Function open; +import Stdlib.Data.Fixity open; --- Primitive representation of a sequence of characters. builtin string diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix index 1cecd8d2..a1e3b6a7 100644 --- a/Stdlib/Extra/Gcd.juvix +++ b/Stdlib/Extra/Gcd.juvix @@ -11,6 +11,5 @@ gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} (a b : A) : A := -- Internal helper for computing the greatest common divisor. The first element -- should be smaller than the second. terminating - gcd' (a b : A) : A := - if (a == fromNat 0) b (gcd' (mod b a) a); + gcd' (a b : A) : A := if (a == 0) b (gcd' (mod b a) a); in if (a > b) (gcd' b a) (gcd' a b); diff --git a/Stdlib/System/IO/Base.juvix b/Stdlib/System/IO/Base.juvix index f9f8ebcb..bb04458e 100644 --- a/Stdlib/System/IO/Base.juvix +++ b/Stdlib/System/IO/Base.juvix @@ -8,4 +8,3 @@ axiom IO : Type; syntax operator >> seq; builtin IO-sequence axiom >> : IO → IO → IO; - diff --git a/Stdlib/Trait/Integral.juvix b/Stdlib/Trait/Integral.juvix index 88d65ca1..634f51c5 100644 --- a/Stdlib/Trait/Integral.juvix +++ b/Stdlib/Trait/Integral.juvix @@ -10,6 +10,7 @@ type Integral A := naturalI : Natural A; syntax operator - additive; - : A -> A -> A; + builtin from-int fromInt : Int -> A }; diff --git a/Stdlib/Trait/Natural.juvix b/Stdlib/Trait/Natural.juvix index 28c64e41..9b88cb83 100644 --- a/Stdlib/Trait/Natural.juvix +++ b/Stdlib/Trait/Natural.juvix @@ -12,6 +12,7 @@ type Natural A := * : A -> A -> A; div : A -> A -> A; mod : A -> A -> A; + builtin from-nat fromNat : Nat -> A }; diff --git a/test/Test.juvix b/test/Test.juvix index 57b8946b..deb7b632 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -212,8 +212,20 @@ main : IO := QC.runTestsIO 100 (stringToNat seed) - [partitionTest; reverseLengthTest; reverseReverseIdTest; splitAtRecombineTest; splitAtLengthTest; mergeSumLengthsTest; tailLengthOneLessTest; equalCompareToEqTest; zipTest; zipWithTest; snocTest; dropTest; sortTest - "mergeSort" - mergeSort; sortTest - "quickSort" - quickSort; transposeMatrixIdTest; transposeMatrixDimentionsTest]}; + [ partitionTest + ; reverseLengthTest + ; reverseReverseIdTest + ; splitAtRecombineTest + ; splitAtLengthTest + ; mergeSumLengthsTest + ; tailLengthOneLessTest + ; equalCompareToEqTest + ; zipTest + ; zipWithTest + ; snocTest + ; dropTest + ; sortTest "mergeSort" mergeSort + ; sortTest "quickSort" quickSort + ; transposeMatrixIdTest + ; transposeMatrixDimentionsTest + ]};