Literal casts (#87)

* Adapts to anoma/juvix#2457 --------- Co-authored-by: Paul Cadman <[email protected]>
anoma · Nov 7, 2023 · 2bc3b8b · 2bc3b8b
1 parent aa3809f
commit 2bc3b8b
Show file tree

Hide file tree

Showing 10 changed files with 27 additions and 16 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
+        ]};
Original file line number	Diff line number	Diff line change
Expand Up		@@ -15,4 +15,3 @@ showStringI : Show String :=
		let
		go (s : String) : String := "\"" ++str s ++str "\"";
		in mkShow go;
Original file line number	Diff line number	Diff line change
Expand Up		@@ -8,4 +8,3 @@ axiom IO : Type;
		syntax operator >> seq;
		builtin IO-sequence
		axiom >> : IO → IO → IO;