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

module X5 where

----------------------------------------------------------------------
-- Exercise 5 : Generic induction and the container view            --
----------------------------------------------------------------------

-- LIBRARY

data Zero : Set where

magic : {X : Set} -> Zero -> X
magic ()

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 _:+:_ (S T : Set) : Set where
  inl : S -> S :+: T
  inr : T -> S :+: T

case : {S T X : Set} -> (S -> X) -> (T -> X) -> S :+: T -> X
case sf tf (inl s) = sf s
case sf tf (inr t) = tf 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*_

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

infixr 30 _D+_

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

NAT : Description
NAT = D1 D+ DPlace

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

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

_!_ : 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 ] 

nil : {X : Set} -> Data (LIST X)
nil = [ left  , void  ] 

cons : {X : Set} -> X -> Data (LIST X) -> Data (LIST X)
cons x xs = [ right , x  , xs ] 

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 d = d 

[_<|_] : (S : Set)(P : S -> Set) -> Set -> Set
[ S <| P ] X = Sigma S \ s -> P s -> X

Shape : Description -> Set
Shape D = D ! One

Positions : (D : Description) -> Shape D -> Set
Positions (DSigma S D) (s , d) = Positions (D s) d 
Positions DPlace       d = One 
Positions (S D* T)     (s , t) = Positions S s :+: Positions T t 
Positions D1           d = Zero 

-- EXERCISES

{- (5.1) Define the constructors for TREE in this style -}

leaf : Data TREE
leaf = {! !}

node : Data TREE -> Data TREE -> Data TREE
node s t = {! !}

{- (5.2) Check that the following induction principle holds. -}

indTREE : (P : Data TREE -> Set) ->
          P leaf ->
          ((s t : Data TREE) -> P s -> P t -> P (node s t)) ->
          (x : Data TREE) -> P x
indTREE P pl pn t = {! !}

{- (5.3) Define Everywhere and everywhere for (D ! X) in the same
   style as Exercise 4. -}

Everywhere : (D : Description){X : Set} -> (X -> Set) -> D ! X -> Set
Everywhere D P dx = {! !}

everywhere : (D : Description){X : Set}(P : X -> Set) ->
             ((x : X) -> P x) ->
             (xs : D ! X) -> Everywhere D P xs

everywhere D P p dx = {! !}

{- (5.4*) Implement the induction principle.
   Hint: it's a bit like fold; it's worth producing a version which the
   termination checker doesn't like, then transforming it. -}

induction : (D : Description)(P : Data D -> Set) ->
            ((dt : D ! Data D) -> Everywhere D P dt -> P [ dt ]) ->
            (t : Data D) -> P t
induction D P p t = {! !}

{- (5.5) Show how to build a D ! X from the corresponding element
   of [ Shape D <| Positions D ] X -}

build : (D : Description){X : Set} -> [ Shape D <| Positions D ] X -> D ! X
build D sf = {! !}

{- (5.6) Given s : Shape D, show how to build a (D ! Positions D s)
   where each place holds its own position. -}

layout : (D : Description){X : Set}(d1 : Shape D) -> D ! Positions D d1
layout D d1 = {! !}

{- (5.7*) Construct the "view" which shows how each element of D ! X is
   given by some (build D (s , f)) -}

data Container (D : Description)(X : Set) : D ! X -> Set where
  _<?|_ : (s : Shape D)(f : Positions D s -> X) ->
            Container D X (build D (s , f))

container : (D : Description)(X : Set)(dx : D ! X) -> Container D X dx
container D X d = {! !}