-- Code from Section 12.5

module Normalise where
import PhantomTypes

import System.IO.Unsafe
import Data.IORef

infixr |->

data Type t =              RBase  (Base   :=: t)
            | forall a b . TypFun ((a->b) :=: t) (Type a) (Type b)

(|->) :: Type a -> Type b -> Type (a->b)
(|->) = TypFun refl

b :: Type Base
b = RBase refl

data Term t = forall a b . App (b      :=: t) (Term (a->b)) (Term a)
            | forall a b . Fun ((a->b) :=: t) (Term a -> Term b)

newtype Term' phi a = Term { unTerm :: phi (Term a) }
term :: forall a b . (a :=: b) -> (Term a :=: Term b)
term p = Proof (unTerm . apply p . Term)

newtype Base = In { out :: Term Base }

reify :: forall t . Type t -> (t -> Term t)
reify (RBase p) v = from (term p) (out (to p v))
reify (TypFun p ra rb) v = Fun p (\x -> reify rb (to p v (reflect ra x)))

reflect :: forall t . Type t -> (Term t -> t)
reflect (RBase p) e = from p (In (to (term p) e))
reflect (TypFun p ra rb) e 
 = from p $ \x -> reflect rb (App refl (to (term p) e) (reify ra x))

s = \x y z -> (x z) (y z)
k = \x y -> x
i = \x -> x

e = (s ((s (k s)) ((s (k k)) i)) ((s ((s (k s)) ((s (k k)) i))) (k i)))
et = (b |-> b) |-> (b |-> b)