{-# OPTIONS --universe-polymorphism #-}

module DepNobby where

open import Level

_o_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f o g = λ x → f (g x)
infixl 50 _o_

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

data Bool : Set where
  tt ff : Bool

bool : forall {a}(P : Bool -> Set a) -> P tt -> P ff -> (b : Bool) -> P b
bool P t f tt = t
bool P t f ff = f

data _+_ (S T : Set) : Set where
  inl : S -> S + T
  inr : T -> S + T


either : forall {a S T}(P : S + T -> Set a)->
           ((s : S) -> P (inl s)) -> ((t : T) -> P (inr t)) ->
           (x : S + T) -> P x
either P f g (inl s) = f s
either P f g (inr t) = g t

data NM : Bool -> Set where
  Pi : Nat -> NM tt -> NM tt -> NM tt
  lam : Nat -> NM tt -> NM tt
  Two ff tt : NM tt
  !_ : NM ff -> NM tt
  var : Nat -> NM ff
  _$_ : NM ff -> NM tt -> NM ff
  Case : NM ff -> NM tt -> NM tt -> NM ff
  case : NM ff -> Nat -> NM tt -> NM tt -> NM tt -> NM ff

infixl 90 _$_

Nm : Set
Nm = NM tt
Ne : Set
Ne = NM ff

_=N=_ : Nat -> Nat -> Bool
ze =N= ze = tt
su m =N= su n = m =N= n
_ =N= _ = ff

infixr 40 _=N=_

_&_ : Bool -> Bool -> Bool
tt & b = b
ff & b = ff

infixr 30 _&_
infixr 40 _=NM=_

_=NM=_ : {b : Bool} -> NM b -> NM b -> Bool
Pi x S T        =NM= Pi y U V        = x =N= y  &  S =NM= U  &  T =NM= V
lam x t         =NM= lam y v         = x =N= y  &  t =NM= v
Two             =NM= Two             = tt
ff              =NM= ff              = tt
tt              =NM= tt              = tt
(! d)           =NM= (! e)           = d =NM= e
var x           =NM= var y           = x =N= y
f $ s           =NM= g $ t           = f =NM= g  &  s =NM= t
Case b S T      =NM= Case c U V      = b =NM= c  &  S =NM= U  &  T =NM= V
case b x P s t  =NM= case c y Q u v  = b =NM= c  &  x =N= y  &  P =NM= Q
                                     & s =NM= u  &  t =NM= v
_               =NM= _               = ff

data Zero : Set where
record One : Set where

mutual
  data Ty : Set where
    Pi  : (S : Ty) -> (El S -> Ty) -> Ty
    Two : Ty
    !_ : (Nat -> Ne) -> Ty
  Can : Ty -> Set
  Can (Pi S T) = (s : El S) -> El (T s)
  Can Two = Bool
  Can (! _) = Zero
  El : Ty -> Set
  El T = (Nat -> Ne) + Can T

injv : ∀ {T} -> Nat -> (Nat -> Ne) + T
injv n = inl (\ _ -> var n)

Quo : Ty -> Nat -> Nm
Quo (Pi S T) n = Pi n (Quo S n) (Quo (T (injv n)) (su n))
Quo Two n = Two
Quo (! E) n = ! E n

mutual
  que : (T : Ty) -> El T -> Nat -> Nm
  que (Pi S T) f n = lam n (que (T (injv n)) (f $$ n) (su n))
  que T (inl e) n = ! (e n)
  que T (inr c) n = quc T c n
  quc : (T : Ty) -> Can T -> Nat -> Nm
  quc (Pi S T) f n = lam n (que (T (injv n)) (f (injv n)) (su n))
  quc Two tt n = tt
  quc Two ff n = ff
  quc (! E) () n
  _$$_ : {S : Ty}{T : (El S) -> Ty} ->
         El (Pi S T) -> (n : Nat) -> El (T (injv n))
  inr f $$ x = f (injv x)
  _$$_ {S} (inl e) x = inl \ n -> (e n $ que S (injv x) n)


record _*_ (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst

open _*_

spl : forall {a S T} -> {P : S * T -> Set a} ->
      ((s : S)(t : T s) -> P (s , t)) ->
      (st : S * T) -> P st
spl p st = p (fst st) (snd st)

mutual 
  data Cx : Set where
    E : Cx
    _,_ : (G : Cx)(S : Env G -> Ty) -> Cx
  Env : Cx -> Set
  Env E = One
  Env (G , S) = Env G * \ g -> El (S g)

data Var : (G : Cx)(T : Env G -> Ty) -> Set where
  ze : forall {G S} -> Var (G , S) (S o fst)
  su : forall {G S T} -> Var G T -> Var (G , S) (T o fst)

get : {G : Cx}{T : Env G -> Ty} -> Var G T ->
         (g : Env G) -> El (T g)
get ze gs = snd gs
get (su x) gs = get x (fst gs)

mutual
  data TY : (G : Cx)(T : Env G -> Ty) -> Set where
    Pi : forall {G S T} ->
           TY G S -> TY (G , S) T ->
           TY G \ g -> Pi (S g) \ s -> T (g , s)
    Two : forall {G} ->
            TY G \ _ -> Two
    Case : forall {G T F} ->
             (b : TM G (\ _ -> Two)) -> TY G T -> TY G F ->
             TY G \ g -> either (\ _ -> Ty)
               (\ e -> ! \ n -> Case (e n) (Quo (T g) n) (Quo (F g) n))
               (bool _ (T g) (F g))
               (eval b g)
  data TM : (G : Cx)(T : Env G -> Ty) -> Set where
    var : forall {G T} ->
           Var G T ->
           TM G T
    lam : forall {G S T} ->
           TM (G , S) (spl T) ->
           TM G \ g -> Pi (S g) \ s -> T g s
    _$_ : forall {G S}{T : (g : Env G) -> El (S g) -> Ty} ->
           TM G (\ g -> Pi (S g) \ s -> T g s) -> (s : TM G S) ->
           TM G \ g -> T g (eval s g)
    tt ff : forall {G} ->
              TM G \ _ -> Two
    case : forall {G}{T} ->
             (b : TM G \ _ -> Two) ->
             TY (G , \ _ -> Two) T ->
             TM G (\ g -> T (g , (inr tt))) ->
             TM G (\ g -> T (g , (inr ff))) ->
             TM G \ g -> T (g , (eval b g))
  eval : forall {G T} -> TM G T -> (g : Env G) -> El (T g)
  eval {G}{T} (var x) g = get x g
  eval (lam t) g = inr (\ s -> eval t (g , s))
  eval (f $ s) g with eval f g
  ... | inl e = inl (\ n -> e n $ que _ (eval s g) n)
  ... | inr f' = f' ((eval s g))
  eval tt g = inr tt
  eval ff g = inr ff
  eval (case {T = T} b _ t f) g with eval b g
  ... | inl e = inl \ n ->
     case (e n) n (Quo (T (g , injv n)) (su n))
      (que (T (g , (inr tt))) (eval t g) n)
      (que (T (g , (inr ff))) (eval f g) n)
  ... | inr tt = eval t g
  ... | inr ff = eval f g

norm : (G : Cx)(g : Env G){T : Env G -> Ty} -> TM G T -> Nat -> Nm
norm G g t n = que _ (eval t g) n

ty : forall {G}{T} -> TY G T -> (g : Env G) -> Ty
ty {G}{T} _ g = T g

NOT : forall {G} -> TM G \ g -> Pi Two \ _ -> Two
NOT = lam (case (var ze) Two ff tt)

FOOTY : forall {G} -> TY (G , \ _ -> Two) _
FOOTY = Case (var ze) Two (Pi Two Two)

FOOTM : forall {G} -> TM G (ty (Pi Two FOOTY))
FOOTM = lam (case (var ze) FOOTY ff NOT)

HIOID : forall {G} -> TM G (ty (Pi (Pi Two Two) (Pi Two Two)))
HIOID = lam (var ze)