{-# OPTIONS --no-positivity-check
  #-}

module L5 where

----------------------------------------------------------------------
-- Lecture 5 : A grammar of datatypes
----------------------------------------------------------------------

data Zero : Set where

data One : Set where
  void : One

data Two : Set where
  left  : Two
  right : Two

data Sigma (S : Set)(T : S -> Set) : Set where
  _,_ : (s : S)(t : T s) -> Sigma S T

infixr 40 _,_

_*_ : Set -> Set -> Set
S * T = Sigma S \ s -> T

data Description : Set1 where  -- that's a set of sets!
  DSigma : (S : Set) -> (S -> Description) -> Description
  DPlace : Description
  _D*_   : Description -> Description -> Description
  D1     : Description

infixr 40 _D*_

{-
NAT : Description
NAT = DSigma Two Args where
  Args : Two -> Description
  Args left  = D1
  Args right = DPlace

TREE : Description
TREE = DSigma Two Args where
  Args : Two -> Description
  Args left  = D1
  Args right = DPlace D* DPlace

LIST : Set -> Description
LIST X =  DSigma Two Args where
  Args : Two -> Description
  Args left  = D1
  Args right = DSigma X \ _ -> DPlace
-}

_D+_ : Description -> Description -> Description
S D+ T = DSigma Two Args where
  Args : Two -> Description
  Args left  = S
  Args right = T

infixr 30 _D+_

NAT : Description
NAT = D1 D+ DPlace

TREE : Description
TREE = D1 D+ DPlace D* DPlace

LIST : Set -> Description
LIST X = D1 D+ DSigma X \ _ -> DPlace

D0 : Description
D0 = DSigma Zero Args where
  Args : Zero -> Description
  Args ()

_!_ : Description -> Set -> Set
DSigma S D ! X = Sigma S \ s -> D s ! X
DPlace     ! X = X
(S D* T)   ! X = (S ! X) * (T ! X)
D1         ! X = One

data Data (D : Description) : Set where
  [_] : D ! Data D -> Data D

zero : Data NAT
zero = [ left , void  ] 

suc : Data NAT -> Data NAT
suc n = [ right , n ]

map : (D : Description){A B : Set} -> (A -> B) -> D ! A -> D ! B
map (DSigma S D) f (s , d) = s , map (D s) f d
map DPlace       f a       = f a
map (S D* T)     f (s , t) = map S f s , map T f t
map D1           f void    = void

{-
fold : {D : Description}{T : Set} -> (D ! T -> T) -> Data D -> T
fold {D} f [ d ] = f (map D (fold D f) d)
-}

mapFold : (R D : Description){T : Set} -> (R ! T -> T) -> D ! Data R -> D ! T
mapFold R (DSigma S D) f (s , d) = s , mapFold R (D s) f d
mapFold R DPlace       f [ r ]   = f (mapFold R R f r)
mapFold R (S D* T)     f (s , t) = mapFold R S f s , mapFold R T f t
mapFold R D1           f void    = void

fold : {R : Description}{T : Set} -> (R ! T -> T) -> Data R -> T
fold {R} f [ r ] = f (mapFold R R f r)

length : {X : Set} -> Data (LIST X) -> Data NAT
length {X} = fold f where
  f : LIST X ! Data NAT -> Data NAT
  f (left , void)   = zero
  f (right , x , n) = suc n

-------------------------------------------