-- By indexing the program and WHNF types on a universe one can handle
-- several types at the same time

module Universe where

open import Coinduction
open import Data.Product
open import Data.Stream

infixr 5 _∷_
infixr 4 _,_

data U : Set₁ where
  lift    : Set  U
  stream  : U  U
  product : U  U  U

El : U  Set
El (lift A)      = A
El (stream a)    = Stream (El a)
El (product a b) = El a × El b

data ElP : U  Set₁ where
  interleave :  {a}  ElP (stream a)  ElP (stream a)  ElP (stream a)
  fst        :  {a b}  ElP (product a b)  ElP a
  snd        :  {a b}  ElP (product a b)  ElP b

data ElW : U  Set₁ where
  _∷_  :  {a}  ElW a  ElP (stream a)  ElW (stream a)
  _,_  :  {a b}  ElW a  ElW b  ElW (product a b)
  ⌈_⌉  :  {A}  A  ElW (lift A)

interleaveW :  {a}  ElW (stream a)  ElP (stream a)  ElW (stream a)
interleaveW (x  xs) ys = x  interleave ys xs

fstW :  {a b}  ElW (product a b)  ElW a
fstW (x , y) = x

sndW :  {a b}  ElW (product a b)  ElW b
sndW (x , y) = y

whnf :  {a}  ElP a  ElW a
whnf (interleave xs ys) = interleaveW (whnf xs) ys
whnf (fst p)            = fstW (whnf p)
whnf (snd p)            = sndW (whnf p)


  ⟦_⟧W :  {a}  ElW a  El a
   x  xs ⟧W =  x ⟧W    xs ⟧P
   x , y  ⟧W = ( x ⟧W ,  y ⟧W)
    x   ⟧W = x

  ⟦_⟧P :  {a}  ElP a  El a
   p ⟧P =  whnf p ⟧W