module Stdlib.Data.Pair.Base;

import Stdlib.Data.Fixity open;

syntax operator , pair;

--- Inductive pair. I.e. a tuple with two components.
builtin pair
type Pair (A B : Type) := , : A → B → Pair A B;

--- Converts a function f of two arguments to a function with a product argument.
uncurry {A B C} (fun : A -> B -> C) (pair : Pair A B) : C :=
  case pair of a, b := fun a b;

--- Converts a function f with a product argument to a function of two arguments.
curry {A B C} (fun : Pair A B -> C) (a : A) (b : B) : C := fun (a, b);

--- Projects the first component of a tuple.
fst {A B} (pair : Pair A B) : A := case pair of a, _ := a;

--- Projects the second component of a tuple.
snd {A B} (pair : Pair A B) : B := case pair of _, b := b;

--- Swaps the components of a tuple.
swap {A B} (pair : Pair A B) : Pair B A := case pair of a, b := b, a;

--- Applies a function f to the first component.
first {A B A'} (fun : A -> A') (pair : Pair A B) : Pair A' B :=
  case pair of a, b := fun a, b;

--- Applies a function f to the second component.
second {A B B'} (fun : B -> B') (pair : Pair A B) : Pair A B' :=
  case pair of a, b := a, fun b;

--- Applies a function f to both components.
both {A B} (fun : A -> B) (pair : Pair A A) : Pair B B :=
  case pair of a, b := fun a, fun b;