Rename the Product type to Pair (#102)

* Closes #101

Stdlib/Data/List/Base.juvix

@@ -7,7 +7,7 @@ import Stdlib.Function open;
 import Stdlib.Data.Nat.Base open;
 import Stdlib.Data.Maybe.Base open;
 import Stdlib.Trait.Ord open;
-import Stdlib.Data.Product.Base open;
+import Stdlib.Data.Pair.Base open;
 
 --- 𝒪(𝓃). Returns ;true; if the given
 --- object is in the ;List;.
@@ -82,7 +82,7 @@ drop {A} : Nat → List A → List A
 
 --- 𝒪(𝓃). 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 → List A × List A
+splitAt {A} : Nat → List A → Pair (List A) (List A)
   | _ nil := nil, nil
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
@@ -101,7 +101,8 @@ merge {A} {{Ord A}} : List A → List A → List A
 
 --- 𝒪(𝓃). 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 → List A × List A
+partition
+  {A} (f : A → Bool) : List A → Pair (List A) (List A)
   | nil := nil, nil
   | (x :: xs) :=
     case partition f xs of
@@ -171,7 +172,7 @@ zipWith
   | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
 
 --- 𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists.
-zip {A B} : List A -> List B -> List (A × B)
+zip {A B} : List A -> List B -> List (Pair A B)
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := (x, y) :: zip xs ys;
@@ -187,7 +188,7 @@ mergeSort {A} {{Ord A}} (l : List A) : List A :=
       | len xs :=
         let
           len' : Nat := div len (suc (suc zero));
-          splitXs : List A × List A := splitAt len' xs;
+          splitXs : Pair (List A) (List A) := splitAt len' xs;
           left : List A := fst splitXs;
           right : List A := snd splitXs;
         in merge (go len' left) (go (sub len len') right);

Stdlib/Data/Product.juvix → Stdlib/Data/Pair.juvix

@@ -1,6 +1,6 @@
-module Stdlib.Data.Product;
+module Stdlib.Data.Pair;
 
-import Stdlib.Data.Product.Base open public;
+import Stdlib.Data.Pair.Base open public;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
 
@@ -9,12 +9,12 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 instance
-eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (A × B)
+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};
 
 instance
-ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (A × B)
+ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
   | {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=
     mkOrd
       λ {(a1, b1) (a2, b2) :=
@@ -25,7 +25,7 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (A × B)
 
 instance
 showProductI
-  {A B} : {{Show A}} -> {{Show B}} -> Show (A × B)
+  {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
   | {{mkShow show-a}} {{mkShow show-b}} :=
     mkShow
       λ {(a, b) :=

Stdlib/Data/Product/Base.juvix → Stdlib/Data/Pair/Base.juvix

@@ -1,41 +1,40 @@
-module Stdlib.Data.Product.Base;
+module Stdlib.Data.Pair.Base;
 
 import Stdlib.Data.Fixity open;
 
-syntax operator × functor;
 syntax operator , pair;
 
 --- Inductive pair. I.e. a tuple with two components.
-type × (A B : Type) := , : A → B → A × B;
+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) : A × B -> C
+uncurry {A B C} (f : A -> B -> C) : Pair A B -> C
   | (a, b) := f a b;
 
 --- Converts a function with a product argument to a function of two arguments.
-curry {A B C} (f : A × B -> C) (a : A) (b : B) : C :=
+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} : A × B → A
+fst {A B} : Pair A B → A
   | (a, _) := a;
 
 --- Projects the second component of a tuple.
-snd {A B} : A × B → B
+snd {A B} : Pair A B → B
   | (_, b) := b;
 
 --- Swaps the components of a tuple.
-swap {A B} : A × B → B × A
+swap {A B} : Pair A B → Pair B A
   | (a, b) := b, a;
 
 --- Applies a function to the first component.
-first {A B A'} (f : A → A') : A × B → A' × B
+first {A B A'} (f : A → A') : Pair A B → Pair A' B
   | (a, b) := f a, b;
 
 --- Applies a function to the second component.
-second {A B B'} (f : B → B') : A × B → A × B'
+second {A B B'} (f : B → B') : Pair A B → Pair A B'
   | (a, b) := a, f b;
 
 --- Applies a function to both components.
-both {A B} (f : A → B) : A × A → B × B
+both {A B} (f : A → B) : Pair A A → Pair B B
   | (a, b) := f a, f b;

Stdlib/Function.juvix

@@ -2,7 +2,7 @@ module Stdlib.Function;
 
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Nat.Base open;
-import Stdlib.Data.Product.Base open;
+import Stdlib.Data.Pair.Base open;
 
 syntax operator ∘ composition;
 

Stdlib/Prelude.juvix

@@ -10,7 +10,7 @@ import Stdlib.Data.Maybe open public;
 import Stdlib.Data.Nat open public;
 import Stdlib.Data.Int open public;
 import Stdlib.Data.Field open public;
-import Stdlib.Data.Product open public;
+import Stdlib.Data.Pair open public;
 import Stdlib.Data.String open public;
 import Stdlib.Function open public;
 import Stdlib.System.IO open public;

test/Package.juvix

@@ -9,5 +9,5 @@ package : Package :=
                      ; github
                        "anoma"
                        "juvix-quickcheck"
-                       "d9696bb0c038e12df4a7b736a4030b6940011404"
+                       "b6ca4d4bd80d62b95e2d7e28e881c5b547643564"
                      ]};

test/Test.juvix

@@ -76,7 +76,7 @@ prop-sort : (List Int -> List Int) -> List Int -> Bool
 prop-zip : List Int -> List Int -> Bool
   | xs ys :=
     let
-      zs : List (Int × Int) := zip xs ys;
+      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)

test/Test/Arb.juvix

@@ -17,7 +17,7 @@ arbitrarySizedList
               | _ zero := nil
               | r (suc n) :=
                 let
-                  rSplit : StdGen × StdGen := stdSplit r;
+                  rSplit : Pair StdGen StdGen := stdSplit r;
                   r1 : StdGen := fst rSplit;
                   r2 : StdGen := snd rSplit;
                 in Gen.run g r1 :: randList r2 n;
@@ -30,7 +30,7 @@ arbitraryMatrix
     (mkGen
       \ {rand :=
         let
-          randSplit : StdGen × StdGen := stdSplit rand;
+          randSplit : Pair StdGen StdGen := stdSplit rand;
           rand1 : StdGen := fst randSplit;
           rand2 : StdGen := snd randSplit;
           cols : Nat := fst (randNat rand1 1 10);

test/juvix.lock.yaml

@@ -1,18 +1,18 @@
-# This file was autogenerated by Juvix version 0.6.1.
+# This file was autogenerated by Juvix version 0.6.2.
 # Do not edit this file manually.
 
 version: 2
-checksum: 5db5ab8aab6fa95f39544dd18cb95ae8a80d88ae261add7801926ac96f7955e6
+checksum: c311ba35a484fb649358719f7720cf706aa8b13d8066bb0fe600ef0d7bc4ca2c
 dependencies:
 - path: ../
   dependencies: []
 - git:
     name: anoma_juvix-quickcheck
-    ref: d9696bb0c038e12df4a7b736a4030b6940011404
+    ref: b6ca4d4bd80d62b95e2d7e28e881c5b547643564
     url: https://github.com/anoma/juvix-quickcheck
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: 27f54ef11c3b21cea18c6b00c54b1d4f3b0cb9f8
+      ref: 3f2c29880e749c7dd222011527a077b5f5050a95
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []