module Encoded.Pair

import Control.Function.FunExt
import Encoded.Bool
import Encoded.Union
import Term.Semantics
import Term.Syntax

-- Type ------------------------------------------------------------------------

export
(*) : Ty -> Ty -> Ty
ty1 * ty2 = B ~> (ty1 <+> ty2)

-- Universal Properties --------------------------------------------------------

export
pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
pair = Abs $ Abs $ Abs $
  let t = Var (There $ There Here) in
  let u = Var (There Here) in
  let b = Var Here in
  App if' [<b, App inL [<t], App inR [<u]]

export
fst : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty1) ctx
fst = Abs $ App (prL . Var Here) [<True]

export
snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
snd = Abs $ App (prR . Var Here) [<False]

-- Utilities -------------------------------------------------------------------

export
bimap :
  {ty1, ty1', ty2, ty2' : Ty} ->
  Term ((ty1 ~> ty1') ~> (ty2 ~> ty2') ~> ty1 * ty2 ~> ty1' * ty2') ctx
bimap = Abs $ Abs $ Abs $ Abs $
  let f = Var (There $ There $ There Here) in
  let g = Var (There $ There Here) in
  let x = Var (There $ Here) in
  let b = Var Here in
  App if'
    [<b
    , App (inL . f . prL . x) [<True]
    , App (inR . g . prR . x) [<False]
    ]

export
mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
mapSnd = Abs $ Abs $
  let f = Var (There Here) in
  let x = Var Here in
  App pair [<App fst [<x], App (f . snd) [<x]]

export
uncurry : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty2 ~> ty) ~> ty1 * ty2 ~> ty) ctx
uncurry = Abs $ Abs $
  let f = Var $ There Here in
  let p = Var Here in
  App f [<App fst [<p], App snd [<p]]

-- Semantics -------------------------------------------------------------------

-- Conversion to Idris

export
toPair : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> (TypeOf ty1, TypeOf ty2)
toPair f = (prL (f True), prR (f False))

export
fromPair : {ty1, ty2 : Ty} -> (TypeOf ty1, TypeOf ty2) -> TypeOf (ty1 * ty2)
fromPair (x, y) b = if' b (inL x) (inR y)

export
toFromId :
  FunExt =>
  {ty1, ty2 : Ty} ->
  (p : (TypeOf ty1, TypeOf ty2)) ->
  toPair {ty1, ty2} (fromPair {ty1, ty2} p) = p
toFromId (x, y) = cong2 (,) (retractL {ty1, ty2} x) (retractR {ty1, ty2} y)

-- Redefinition in Idris

namespace Sem
  public export
  pair : {ty1, ty2 : Ty} -> TypeOf ty1 -> TypeOf ty2 -> TypeOf (ty1 * ty2)
  pair x y b = if' b (inL x) (inR y)

  public export
  fst : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> TypeOf ty1
  fst f = prL (f True)

  public export
  snd : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> TypeOf ty2
  snd f = prR (f False)

-- Proofs

export
pairHomo :
  FunExt =>
  {ty1, ty2 : Ty} ->
  (0 x : TypeOf ty1) ->
  (0 y : TypeOf ty2) ->
  toPair {ty1, ty2} (pair {ty1, ty2} x y) = (x, y)
pairHomo x y = irrelevantEq $ toFromId (x, y)

export
fstHomo :
  FunExt =>
  {ty1, ty2 : Ty} ->
  (0 p : (TypeOf ty1, TypeOf ty2)) ->
  fst {ty1, ty2} (fromPair {ty1, ty2} p) = fst p
fstHomo (x, y) = cong fst (pairHomo x y)

export
sndHomo :
  FunExt =>
  {ty1, ty2 : Ty} ->
  (0 p : (TypeOf ty1, TypeOf ty2)) ->
  snd {ty1, ty2} (fromPair {ty1, ty2} p) = snd p
sndHomo (x, y) = cong snd (pairHomo x y)