GTLC.agda

open import Data.Bool
open import Data.Nat
open import Data.List renaming (_∷_ to _::_)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All renaming (lookup to Alookup)
open import Data.Maybe
open import Data.Product
open import Data.Unit

open import Function

open import Relation.Unary hiding (_∈_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module GTLC where

  data Ty : Set where
    ??   : Ty
    bool : Ty
    _=>_ : Ty -> Ty -> Ty


  data _~_ : Ty -> Ty -> Set where
    CRefl : forall {t} -> t ~ t
    CFun  : forall {t1 t2 t1' t2'} ->
            t1 ~ t1' ->
            t2 ~ t2' ->
            (t1 => t2) ~ (t1' => t2')
    CUnL  : forall {t} -> ?? ~ t
    CUnR  : forall {t} -> t ~ ??

  ≡-inv : forall {t1 t2 t1' t2'} -> (t1 => t2) ≡ (t1' => t2') -> t1 ≡ t1' × t2 ≡ t2'
  ≡-inv refl = refl , refl

  ≡-Ty : forall (t t' : Ty) -> Dec (t ≡ t')
  ≡-Ty ?? ?? = yes refl
  ≡-Ty ?? bool = no (λ ())
  ≡-Ty ?? (t' => t'') = no (λ ())
  ≡-Ty bool ?? = no (λ ())
  ≡-Ty bool bool = yes refl
  ≡-Ty bool (t' => t'') = no (λ ())
  ≡-Ty (t => t₁) ?? = no (λ ())
  ≡-Ty (t => t₁) bool = no (λ ())
  ≡-Ty (t => t₁) (t' => t'') with ≡-Ty t t' | ≡-Ty t₁ t''
  ≡-Ty (t => t₁) (t' => t'') | yes p | yes p₁ rewrite p | p₁ = yes refl
  ≡-Ty (t => t₁) (t' => t'') | yes p | no ¬p = no (λ eq → ¬p (proj₂ (≡-inv eq)))
  ≡-Ty (t => t₁) (t' => t'') | no ¬p | q = no (λ eq → ¬p (proj₁ (≡-inv eq))) 

  -- proposition 1

  ~-refl : forall {t} -> t ~ t
  ~-refl = CRefl

  ~-sym : forall {t t'} -> t ~ t' -> t' ~ t
  ~-sym CRefl = CRefl
  ~-sym (CFun p p') = CFun (~-sym p) (~-sym p')
  ~-sym CUnL = CUnR
  ~-sym CUnR = CUnL


  ~-inv : forall {t1 t2 t1' t2'} -> (t1 => t2) ~ (t1' => t2') -> t1 ~ t1' × t2 ~ t2'
  ~-inv CRefl = CRefl , CRefl
  ~-inv (CFun p p₁) = p , p₁


  ~-Dec : forall (t t' : Ty) -> Dec (t ~ t')
  ~-Dec ?? ?? = yes CRefl
  ~-Dec ?? bool = yes CUnL
  ~-Dec ?? (t' => t'') = yes CUnL
  ~-Dec bool ?? = yes CUnR
  ~-Dec bool bool = yes CRefl
  ~-Dec bool (t' => t'') = no (λ ())
  ~-Dec (t1 => t2) ?? = yes CUnR
  ~-Dec (t1 => t2) bool = no (λ ())
  ~-Dec (t1 => t2) (t' => t'') with ~-Dec t1 t' | ~-Dec t2 t''
  ~-Dec (t1 => t2) (t' => t'') | yes p | yes p₁ = yes (CFun p p₁)
  ~-Dec (t1 => t2) (t' => t'') | yes p | no ¬p = no (λ np → ¬p (proj₂ (~-inv np)))
  ~-Dec (t1 => t2) (t' => t'') | no ¬p | yes p = no (λ np → ¬p (proj₁ (~-inv np)))
  ~-Dec (t1 => t2) (t' => t'') | no ¬p | no ¬p₁ = no (λ np → ¬p (proj₁ (~-inv np)))

  -- typed syntax
  
  Ctx : Set
  Ctx = List Ty

  data Term : Ctx -> Ty -> Set where
    var : forall {t G} -> t ∈ G -> Term G t
    tt  : forall {G} -> Term G bool
    ff  : forall {G} -> Term G bool
    lam : forall {G t t'} -> Term (t :: G) t' -> Term G (t => t')
    app1 : forall {G t2} -> Term G ?? -> Term G t2 -> Term G ??
    app2 : forall {G t t' t2} -> Term G (t => t') -> Term G t2 -> t2 ~ t -> Term G t'


  data Cast : Ctx -> Ty -> Set where
    var : forall {t G} -> t ∈ G -> Cast G t
    tt  : forall {G} -> Cast G bool
    ff  : forall {G} -> Cast G bool
    lam : forall {G t t'} -> Cast (t :: G) t' -> Cast G (t => t')
    app : forall {G t1 t2} -> Cast G (t1 => t2) -> Cast G t1 -> Cast G t2
    cast : forall {G t t'} -> Cast G t -> t ~ t' -> Cast G t'

  mkApp : forall {G t1 t2 t3} -> Cast G (t1 => t2) -> Cast G t3 -> t3 ~ t1 -> Cast G t2
  mkApp {t1 = t1}{t3 = t3} l r eq with ≡-Ty t3 t1
  mkApp {t1 = t1} {t3 = t3} l r eq | yes p rewrite p = app l r
  mkApp {t1 = t1} {t3 = t3} l r eq | no ¬p = app l (cast r eq)

  -- cast insertion algorithm

  cast-insert : forall {G t} -> Term G t -> Cast G t
  cast-insert (var x) = var x
  cast-insert tt = tt
  cast-insert ff = tt
  cast-insert (lam t) = lam (cast-insert t)
  cast-insert (app1 l r) with cast-insert l | cast-insert r
  ...| l1 | r1 = app (cast l1 CUnL) r1
  cast-insert (app2 l r eq) with cast-insert l | cast-insert r
  ...| l1 | r1 = mkApp l1 r1 eq


  res : Ty -> Set 
  res ?? = Σ Bool (const (⊤ × Ty))
  res bool = Σ Bool (const Bool)
  res (t => t₁) = Σ Bool (const (res t -> res t₁))

  Env : Ctx -> Set
  Env G = All res G

  res-cast : ∀ {t t'} → t ~ t' -> res t -> res t'
  res-cast CRefl p = p
  res-cast (CFun {t2' = t2'} eq eq') p = false , (λ x → res-cast CUnL (false , tt , t2'))
  res-cast {t' = ??} CUnL p = p
  res-cast {t' = bool} CUnL p = false , proj₁ p
  res-cast {t' = t' => t''} CUnL p = false , (λ x → res-cast CUnL p)
  res-cast {t = ??} CUnR p = p
  res-cast {t = bool} CUnR p = false , tt , ??
  res-cast {t = t => t₁} CUnR p = false , tt , t₁

  eval-cast : ∀ {G t} → Cast G t -> Env G → res t
  eval-cast (var x) E = Alookup E x
  eval-cast tt E = true , true
  eval-cast ff E = true , false
  eval-cast (lam e) E = true , λ v → eval-cast e (v ∷ E)
  eval-cast (app e e') E with eval-cast e E | eval-cast e' E
  ...| b , p | p' = p p'
  eval-cast (cast e eq) E with eval-cast e E
  ...| p = res-cast eq p

  eval : ∀ {G t} → Term G t → Env G → res t
  eval e E = eval-cast (cast-insert e) E