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

module UniverseIndex 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)

mutual

  ⟦_⟧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