1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105

use crate::{
  nat_trans::*,
  row::*,
  type_app::*,
};

pub trait Sum
{
}

pub enum Bottom {}

pub enum Union<X, Tail>
{
  Inl(X),
  Inr(Tail),
}

pub use Union::{
  Inl,
  Inr,
};

impl Sum for Bottom {}

impl<X, Tail> Sum for Union<X, Tail> where Tail : Sum {}

impl RowCon for Bottom {}
impl<X, Tail> RowCon for Union<X, Tail> {}

impl<'a, F : 'a> RowApp<'a, F> for Bottom
where
  F : TypeCon,
{
  type Applied = Bottom;
}

impl<'a, X : 'a, Tail : 'a, F : 'a> RowApp<'a, F> for Union<X, Tail>
where
  F : TypeCon,
{
  type Applied = Union<App<'a, F, X>, AppRow<'a, Tail, F>>;
}

impl RowAppGeneric for Bottom
{
  fn with_row_app<'a, F : 'a, R : 'a>(
    cont : impl RowAppGenericCont<'a, Self, F, R>
  ) -> R
  where
    Self : 'a,
    F : TypeAppGeneric,
  {
    cont.on_row_app()
  }
}

impl<X, Tail> RowAppGeneric for Union<X, Tail>
where
  Tail : RowAppGeneric,
{
  fn with_row_app<'a, F : 'a, R : 'a>(
    cont : impl RowAppGenericCont<'a, Self, F, R>
  ) -> R
  where
    Self : 'a,
    F : TypeAppGeneric,
  {
    cont.on_row_app()
  }
}

impl LiftRow for Bottom
{
  fn lift<'a, F : 'a, G : 'a>(
    _ : impl NaturalTransformation<F, G>,
    row : AppRow<'a, Self, F>,
  ) -> AppRow<'a, Self, G>
  where
    F : TypeAppGeneric,
    G : TypeAppGeneric,
  {
    match *row.get_applied() {}
  }
}

impl<X, Tail> LiftRow for Union<X, Tail>
where
  Tail : LiftRow,
{
  fn lift<'a, F : 'a, G : 'a>(
    trans : impl NaturalTransformation<F, G> + Clone,
    row : AppRow<'a, Self, F>,
  ) -> AppRow<'a, Self, G>
  where
    Self : 'a,
    F : TypeAppGeneric,
    G : TypeAppGeneric,
  {
    match *row.get_applied() {
      Inl(fx) => wrap_row(Inl(trans.lift(fx))),
      Inr(tail) => wrap_row(Inr(Tail::lift(trans, tail))),
    }
  }
}