path: root/src/Soat/Data/Product.idr

module Soat.Data.Product

import Data.List.Elem
import Data.Morphism.Indexed
import Data.Setoid.Indexed

%default total

infix 10 ^
infix 5 ++

-- Definitions

public export
data (^) : (0 _ : a -> Type) -> List a -> Type where
  Nil  : x ^ []
  (::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is)

public export
ary : List Type -> Type -> Type
ary []        y = y
ary (x :: xs) y = x -> ary xs y

-- Conversions

public export
uncurry : map x is `ary` a -> x ^ is -> a
uncurry f []        = f
uncurry f (x :: xs) = uncurry (f x) xs

-- Destructors

public export
head : x ^ (i :: is) -> x i
head (x :: xs) = x

public export
tail : x ^ (i :: is) -> x ^ is
tail (x :: xs) = xs

public export
consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs
consHeadTail (x :: xs) = Refl

public export
index : x ^ is -> Elem i is -> x i
index xs Here         = head xs
index xs (There elem) = index (tail xs) elem

-- Constructors

public export
tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is
tabulate {is = []}        f = []
tabulate {is = (i :: is)} f = f Here :: tabulate (f . There)

public export
indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is)
  -> index (tabulate f) elem = f elem
indexTabulate f Here         = Refl
indexTabulate f (There elem) = indexTabulate (f . There) elem

-- Operations

public export
map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
map f []        = []
map f (x :: xs) = f _ x :: map f xs

public export
indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is)
  -> index (map f xs) elem = f i (index xs elem)
indexMap (x :: xs) Here         = Refl
indexMap (x :: xs) (There elem) = indexMap xs elem

public export
mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs
mapId []        = Refl
mapId (x :: xs) = cong ((::) x) $ mapId xs

public export
mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is)
  -> map (\i => f i . g i) xs = map f (map g xs)
mapComp []        = Refl
mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs

public export
(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
(++) []        ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

public export
wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is
wrap f []        = []
wrap f (x :: xs) = x :: wrap f xs

public export
mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
  -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs)
mapWrap g []        = Refl
mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs

public export
unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is
unwrap f {is = []}        []        = []
unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs

public export
mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is)
  -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs)
mapUnwrap g {is = []}        []        = Refl
mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs

public export
unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs
unwrapWrap u []        = Refl
unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs

public export
wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs
wrapUnwrap {is = []}        []        = Refl
wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs

-- Relations

namespace Pointwise
  public export
  data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
    Nil  : Pointwise rel [] []
    (::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)}
      -> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys)

  -- Destructors

  public export
  index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem)
  index (r :: rs) Here         = r
  index (r :: rs) (There elem) = index rs elem

  -- Operators

  public export
  map : forall b . {0 r, s : (i : a) -> Rel (b i)}
    -> ((i : a) -> {x, y : b i} -> r i x y -> s i x y)
    -> {is : List a} -> {xs, ys : b ^ is} -> Pointwise r {is} xs ys -> Pointwise s {is} xs ys
  map f []        = []
  map f (r :: rs) = f _ r :: map f rs

  -- Relational Properties

  public export
  pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
  pwEqImpliesEqual []        = Refl
  pwEqImpliesEqual (r :: rs) = trans
    (sym $ consHeadTail _)
    (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))

  public export
  equalImpliesPwEq : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys
  equalImpliesPwEq {xs = []}        {ys = []}        eq = []
  equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} eq =
    cong head eq :: equalImpliesPwEq (cong tail eq)

  -- FIXME: work out how to expose interfaces

  public export
  pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
    -> ((i : a) -> Reflexive (x i) (rel i))
    -> {is : List a} -> {xs : x ^ is} -> Pointwise rel xs xs
  pwRefl f {xs = []}        = []
  pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f


  public export
  pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
    -> ((i : a) -> Reflexive (x i) (rel i))
    -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys
  pwReflexive refl Refl = pwRefl refl

  public export
  pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
    -> ((i : a) -> Symmetric (x i) (rel i))
    -> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs
  pwSym f []        = []
  pwSym f (r :: rs) = symmetric r :: pwSym f rs

  public export
  pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
    -> ((i : a) -> Transitive (x i) (rel i))
    -> {is : List a} -> {xs, ys, zs : x ^ is}
    -> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs
  pwTrans f []        []        = []
  pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss

  public export
  pwEquivalence : IEquivalence x rel -> {is : _} -> Setoid.Equivalence (x ^ is) (Pointwise rel)
  pwEquivalence eq = MkEquivalence
    (MkReflexive $ pwRefl (\i => (eq i).refl))
    (MkSymmetric $ pwSym (\i => (eq i).sym))
    (MkTransitive $ pwTrans (\i => (eq i).trans))

  public export
  pwSetoid : ISetoid a -> List a -> Setoid
  pwSetoid x is = MkSetoid (x.U ^ is) _ (pwEquivalence x.equivalence)

  -- Introductors and Eliminators

  public export
  mapIntro'' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
    -> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v))
    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
  mapIntro'' cong []        = []
  mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs

  public export
  mapIntro' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
    -> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v))
    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
  mapIntro' cong = mapIntro'' (\t, _, _ => cong t)

  public export
  mapIntro : (f : IFunction x y) -> {is : _} -> {xs, ys : x.U ^ is}
    -> Pointwise x.relation xs ys -> Pointwise y.relation (map f.func xs) (map f.func ys)
  mapIntro f = mapIntro' f.cong

  public export
  wrapIntro : forall f . {0 rel : IRel x} -> {0 xs, ys : (x . f) ^ is}
    -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys)
  wrapIntro []        = []
  wrapIntro (r :: rs) = r :: wrapIntro rs

  public export
  unwrapIntro : {0 f : a -> b} -> {0 rel : IRel x} -> {is : List a} -> {0 xs, ys : x ^ map f is}
    -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
  unwrapIntro {is = []}        []        = []
  unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs