module Nobby2 where

-- a variation on http://personal.cis.strath.ac.uk/~conor/fooling/Nobby2.agda
open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Nat hiding (_+_; _*_; _>_) renaming (_≟_ to _==_; ℕ to Nat; suc to su; zero to ze)
open import Data.Nat.Properties

data Ty : Set where
  iota : Ty
  _>_ : (S T : Ty) -> Ty

data Cx : Set where
  E : Cx
  _,_ : (G : Cx) -> (S : Ty) -> Cx

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

mutual
  data Nm (G : Cx) : Ty -> Set where
    ! : Ne G iota -> Nm G iota
    lam : ∀ {S T} -> Nm (G , S) T -> Nm G (S > T)

  data Ne (G : Cx) : Ty -> Set where
    var : ∀ {T} -> Var G T -> Ne G T
    _$_ : ∀ {S T} -> Ne G (S > T) -> Nm G S -> Ne G T

_⇒_ : Cx -> Cx -> Set
G ⇒ D = ∀ T -> Var G T -> Var D T

id⇒ : ∀ {G} -> G ⇒ G
id⇒ T x = x

su⇒ : ∀ {G S} -> G ⇒ (G , S)
su⇒ = \ T x -> su x

cons⇒ : ∀ {G D S} -> G ⇒ D -> (G , S) ⇒ (D , S)
cons⇒ r T ze = ze
cons⇒ r T (su v) = su (r _ v) 

mutual
  wkNe : ∀ {G D T} -> G ⇒ D -> Ne G T -> Ne D T
  wkNe r (var x) = var (r _ x)
  wkNe r (e $ x) = wkNe r e $ wkNm r x

  wkNm : ∀ {G D T} -> G ⇒ D -> Nm G T -> Nm D T
  wkNm ρ (! x) = ! (wkNe ρ x)
  wkNm ρ (lam e) = lam (wkNm (cons⇒ ρ) e)
  
mutual
  _[_] : Cx -> Ty -> Set
  G [ T ] = G [ T ]act

  _[_]act : Cx -> Ty -> Set
  G [ iota  ]act = Ne G iota
  G [ S > T ]act = ∀ D -> G ⇒ D -> D [ S ] -> D [ T ]

_$$_ : forall {G S T} -> G [ S > T ] -> G [ S ] -> G [ T ]
_$$_ f x = f _ id⇒ x

wk[] : ∀ {G D T} -> G ⇒ D -> G [ T ] -> D [ T ]
wk[] {G} {D} {iota}  r e = wkNe r e
wk[] {G} {D} {_ > _} r e = λ _ r₁ s → e _ (λ _ v → r₁ _ (r _ v)) s

data All (P : Ty -> Set) : Cx -> Set where
  E : All P E
  _,_ : ∀ {G S} -> All P G -> P S -> All P (G , S)

mapAll : ∀ {P Q G} -> (∀ T -> P T -> Q T) -> All P G -> All Q G
mapAll f E = E
mapAll f (g , s) = mapAll f g , f _ s

Env : Cx -> Cx -> Set
Env D G = All (_[_] D) G 

wkEnv : ∀ {D0 D G} -> D0 ⇒ D -> Env D0 G -> Env D G
wkEnv r g = mapAll (\ _ -> wk[] r) g

mutual
  quo : ∀ {G} (T : Ty) -> G [ T ] -> Nm G T
  quo iota    e = ! e 
  quo (S > T) f = lam (quo T (wk[] su⇒ f $$ (exp S (var ze))))

  exp : ∀ {G} (T : Ty) -> Ne G T -> G [ T ]
  exp iota    e = e
  exp (S > T) e = λ _ ρ s → exp T (wkNe ρ e $ quo S s)

injv : ∀ {G T} -> Var G T -> G [ T ]
injv v = exp _ (var v)

get : forall {G D T} -> Var G T -> Env D G -> D [ T ]
get ze     (g , s) = s
get (su x) (g , t) = get x g

mutual
  evNm : forall {G D T} -> Nm G T -> Env D G -> D [ T ]
  evNm (! x) g = evNe x g
  evNm (lam e) g = λ _ ρ s → evNm e (wkEnv ρ g , s)

  evNe : forall {G D T} -> Ne G T -> Env D G -> D [ T ]
  evNe (var x) g = get x g
  evNe (e $ x) g = evNe e g $$ evNm x g

idEnv : ∀ {D} -> Env D D
idEnv {E} = E
idEnv {D , S} = wkEnv su⇒ idEnv , injv ze

sub : forall {G D T} -> Nm G T -> All (Nm D) G -> Nm D T
sub n g = quo _ (evNm n (mapAll (λ T x → evNm x idEnv) g))