GLTC1.agda

open import Data.Nat hiding (_⊔_ ; _⊓_)
open import Data.Bool
open import Data.Empty
open import Data.List renaming (_∷_ to _::_) hiding (drop)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any hiding (map)
open import Data.List.Relation.Unary.All renaming (lookup to Alookup) hiding (map)
open import Data.Maybe hiding (map)
open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Data.Unit

open import Function

open import Level
open import Level.Literals

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

module GTLC1 where

  -- type and term syntax for gradually typed lambda calculus

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


  -- type compatibility relation

  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 ~ ??

  -- decidable equality for types

  ≡-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))) 

  -- properties of type compatibility relation

  ~-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₁


  -- type compatibility is decidable

  ~-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)))

  -- term 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 Blame : Set where
    blame : ∀ {t t'} -> t ~ t' -> Blame

  data Cast : Bool -> Ctx -> Ty -> Set where
    var : forall {t G b} -> t ∈ G -> Cast b G t
    tt  : forall {G} -> Cast false G bool
    ff  : forall {G} -> Cast false G bool
    lam : forall {G t t' b} -> Cast b (t :: G) t' -> Cast b G (t => t')
    app : forall {G t1 t2 b b'} -> Cast b G (t1 => t2) ->
          Cast b' G t1 -> Cast (b ∨ b') G t2
    cast  : forall {G t t' b} -> Cast b G t -> t ~ t' -> Cast b G t'
    -- can only appear at run-time
    blame : ∀ {G t} → Blame -> Cast true G t 

  -- cast insertion algorithm

  mkApp : forall {G t1 t2 t3} -> Cast false G (t1 => t2) ->
                                 Cast false G t3 -> t3 ~ t1 ->
                                 Cast false 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-insert : forall {G t} -> Term G t -> Cast false 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

  -- some boring lemmas about disjunction

  true-∨-elim : ∀ {b b' : Bool} -> true ≡ b ∨ b' -> b ≡ true ⊎ b' ≡ true
  true-∨-elim {false} {b'} eq = inj₂ (sym eq)
  true-∨-elim {true} {b'} eq = inj₁ refl

  false-∨-elim : ∀ {b b' : Bool} -> false ≡ b ∨ b' → b ≡ false × b' ≡ false
  false-∨-elim {false} {b'} eq rewrite eq = refl , refl

  true-∨-elim-l : ∀ b -> true ≡ b ∨ true
  true-∨-elim-l false = refl
  true-∨-elim-l true  = refl

  -- normal forms

  mutual
    data Nf (G : Ctx) : Ty → Bool -> Set where
      lam : ∀ {t t' b} → Nf (t' :: G) t b -> Nf G (t' => t) b
      ne? : ∀ {t b} → Ne G t b → Nf G t b
      con : Bool -> Nf G bool false
      dyn : ∀ {t b} → Nf G t b -> Nf G ?? b
      blame : ∀ {t} -> Blame -> Nf G t true

    data Ne (G : Ctx) : Ty -> Bool -> Set where
      var : ∀ {t} → t ∈ G → Ne G t false
      app : ∀ {t t' b1 b2 b} → Ne G (t' => t) b1 -> Nf G t' b2 ->
                               b ≡ b1 ∨ b2 -> Ne G t b

  mutual
    causeNf : ∀ {G t} -> Nf G t true -> Blame
    causeNf (lam n) = causeNf n
    causeNf (ne? x) = causeNe x
    causeNf (dyn n) = causeNf n
    causeNf (blame x) = x

    causeNe : ∀ {G t} -> Ne G t true -> Blame
    causeNe (app {b1 = b1}{b2 = b2} n n' eq) with true-∨-elim {b1}{b2} eq
    ...| inj₁ eql rewrite eql = causeNe n
    ...| inj₂ eqr rewrite eqr = causeNf n'
    
  -- order preserving embeddings

  data OPE : Ctx -> Ctx -> Set where
    ●    : OPE [] []
    drop : ∀ {G G' t} -> OPE G G' -> OPE (t :: G) G'
    keep : ∀ {G G' t} -> OPE G G' -> OPE (t :: G) (t :: G')

  -- composition of embeddings

  _●e_ : ∀ {G G' G''} -> OPE G' G'' -> OPE G G' -> OPE G G''
  s ●e ● = s
  s ●e drop s' = drop (s ●e s')
  drop s ●e keep s' = drop (s ●e s')
  keep s ●e keep s' = keep (s ●e s')

  -- action of embeddings on variables

  embedVar : ∀ {G G' t} → OPE G G' → t ∈ G' → t ∈ G
  embedVar (drop e) v = there (embedVar e v)
  embedVar (keep e) (here refl) = here refl
  embedVar (keep e) (there v) = there (embedVar e v)

  -- embedding on cast terms

  embedCast : ∀ {G G' t b} → OPE G G' → Cast b G' t → Cast b G t
  embedCast s (var v) = var (embedVar s v)
  embedCast s tt = tt
  embedCast s ff = ff
  embedCast s (lam e) = lam (embedCast (keep s) e)
  embedCast s (app e e') = app (embedCast s e) (embedCast s e')
  embedCast s (cast e eq) = cast (embedCast s e) eq
  embedCast s (blame eq) = blame eq

  -- identity embedding

  embedId : ∀ {G} → OPE G G
  embedId {[]} = ●
  embedId {x :: G} = keep embedId

  -- removing the last entry on a context

  wk : ∀ {G t} -> OPE (t :: G) G
  wk = drop embedId
 
  -- substitutions

  data Sub (G : Ctx) : Ctx -> Set where
    ● : Sub G []
    _,_ : ∀ {G' t b} → Sub G G' → Cast b G t → Sub G (t :: G')

  -- embeddings on substitutions

  embedSub : ∀ {G G' G''} -> Sub G'' G' -> OPE G G'' -> Sub G G'
  embedSub ● ope = ●
  embedSub (s , t) ope = (embedSub s ope) , embedCast ope t

  -- drop operation for substitutions

  dropSub : ∀ {G G' t} -> Sub G G' -> Sub (t :: G) G'
  dropSub s = embedSub s wk

  keepSub : ∀ {G G' t} → Sub G G' -> Sub (t :: G) (t :: G')
  keepSub s = dropSub s , var {b = false} (here refl)

  -- converting embeddings in substitutions

  embed2Sub : ∀ {G G'} -> OPE G G' -> Sub G G'
  embed2Sub ● = ●
  embed2Sub (drop op) = dropSub (embed2Sub op)
  embed2Sub (keep op) = keepSub (embed2Sub op)

  -- applying a substitution to a variable
  
  applyVar : ∀ {G G' t} → Sub G G' → t ∈ G' -> ∃ (λ b -> Cast b G t)
  applyVar (s , e) (here refl) = _ , e
  applyVar (s , e) (there v) = applyVar s v

  -- applying a substitution to a term

  applyTerm : ∀ {G G' t b} → Sub G G' -> Cast b G' t -> ∃ (λ b' -> Cast b' G t)
  applyTerm s (var v) = applyVar s v
  applyTerm s tt = false , tt
  applyTerm s ff = false , ff
  applyTerm s (lam t) with applyTerm (keepSub s) t
  ...| b , t' = b , lam t'
  applyTerm s (app t t') with applyTerm s t | applyTerm s t'
  ...| b , q | b' , q' =  b ∨ b' , app q q'
  applyTerm s (cast t eq) with applyTerm s t
  ...| b , t' = b , cast t' eq
  applyTerm s (blame eq) = true , blame eq
  
  -- identity substitution

  idSub : ∀ {G} -> Sub G G
  idSub {[]} = ●
  idSub {t :: G} = keepSub (idSub {G})

  -- action of embeddings on normal forms

  mutual
    embedNf : ∀ {G G' t b} -> OPE G G' -> Nf G' t b -> Nf G t b
    embedNf op (lam nt) = lam (embedNf (keep op) nt)
    embedNf op (ne? ne) = ne? (embedNe op ne)
    embedNf op (con c) = con c
    embedNf op (dyn nt) = dyn (embedNf op nt)
    embedNf op (blame eq) = blame eq

    embedNe : ∀ {G G' t b} → OPE G G' -> Ne G' t b -> Ne G t b
    embedNe op (var v) = var (embedVar op v)
    embedNe {b = false} op (app {b1 = b1}{b2 = b2}{b = .false} ne nt eq) with false-∨-elim {b1} {b2} eq
    ...| (eql , eqr) rewrite eql | eqr = app (embedNe op ne) (embedNf op nt) refl
    embedNe {b = true} op (app {b1 = b1}{b2 = b2}{b = .true} ne nt eq) with true-∨-elim {b1}{b2} eq
    ...| inj₁ eql rewrite eql = app (embedNe op ne) (embedNf op nt) refl
    ...| inj₂ eqr rewrite eqr = app (embedNe op ne) (embedNf op nt) (true-∨-elim-l b1)

-- injecting normal forms back into cast terms

  mutual
    injectNf : ∀ {G t b} -> Nf G t b -> Cast b G t
    injectNf (lam nt) = lam (injectNf nt)
    injectNf (ne? ne) = injectNe ne
    injectNf (con false) = ff
    injectNf (con true) = tt
    injectNf (dyn nt) = cast (injectNf nt) CUnR
    injectNf (blame eq) = blame eq

    injectNe : ∀ {G t b} -> Ne G t b -> Cast b G t
    injectNe (var v) = var v
    injectNe {b = false} (app {b1 = b1}{b2 = b2} ne nt eq) with false-∨-elim {b1}{b2} eq
    ...| eql , eqr rewrite eql | eqr = app (injectNe ne) (injectNf nt)
    injectNe {b = true} (app {b1 = b1}{b2 = b2} ne nt eq) with true-∨-elim {b1}{b2} eq
    ...| inj₁ eql rewrite eql = app (injectNe ne) (injectNf nt)
    ...| inj₂ eqr rewrite eqr = subst (λ b -> Cast b _ _) (sym eq) (app (injectNe ne) (injectNf nt))

  -- semantic objects for types

  SemTy : Bool -> Ty -> Ctx -> Set
  SemTy true _ _ = Blame
  SemTy false ?? G = Nf G ?? false 
  SemTy false bool G = Nf G bool false
  SemTy false (t => t') G = ∀ {G'} -> OPE G' G -> SemTy false t G' ->
                                                  ∃ (λ b → SemTy b t' G')

  -- semantic objects for contexts

  data SemCon : Ctx -> Ctx -> Set where
    ●   : ∀ {G} -> SemCon [] G
    _,_ : ∀ {G G' t b} -> SemCon G' G -> SemTy b t G -> SemCon (t :: G') G

  SemVar : ∀ {G t} -> t ∈ G -> ∀ {G'} -> SemCon G G' -> ∃ (λ b -> SemTy b t G')
  SemVar (here refl) (env , val) = _ , val
  SemVar (there v) (env , _) = SemVar v env

  -- embeddings on semantic types and contexts

  EmbedSemTy : ∀ {b G G' t} -> OPE G G' -> SemTy b t G' -> SemTy b t G
  EmbedSemTy {b = true} ope st = st
  EmbedSemTy {b = false}{t = ??} ope st = embedNf ope st
  EmbedSemTy {b = false}{t = bool} ope st = embedNf ope st
  EmbedSemTy {b = false}{t = t => t'} ope st = λ ope' st' -> st (ope ●e ope') st'

  EmbedSemCon : ∀ {G G' G''} -> OPE G' G'' -> SemCon G G'' -> SemCon G G'
  EmbedSemCon ope ● = ●
  EmbedSemCon ope (env , t) = EmbedSemCon ope env , EmbedSemTy ope t

  -- semantic objects for cast calculus

  UpCast : ∀ {G t} → ¬ (t ≡ ??) -> SemTy false t G -> Nf G ?? false
  UpCast {t = ??} neq v = ⊥-elim (neq refl)
  UpCast {t = bool} neq v = dyn v
  UpCast {t = t => t'} neq v = {!!}

  SemTerm : ∀ {G t b} -> Cast b G t -> ∀ {G'} -> SemCon G G' ->
                                                 ∃ (λ b' -> SemTy b' t G')
  SemTerm (var v) env = SemVar v env
  SemTerm tt env = false , con true
  SemTerm ff env = false , con false
  SemTerm (lam e) env = false , λ ope st ->  SemTerm e (EmbedSemCon ope env , st)
  SemTerm (app e e') env with SemTerm e env | SemTerm e' env
  ... | false , f | false , a = f embedId a
  ... | false , f | true , a = true , a
  ... | true , bl | b' , a = true , bl
  SemTerm (cast {t = t} {t' = t'} e eq) env with SemTerm e env | ≡-Ty t t' | ≡-Ty t' ??
  ... | false , v | yes p  | q rewrite p = false , v 
  ... | false , v | no  p  | yes q rewrite q = false , UpCast p v
  ... | false , v | no  p  | no  q  = true , blame eq 
  ... | true , v  | _      | q = true , v
  SemTerm (blame eq) _ = true , eq

  mutual 
    quo : ∀ {t G} -> SemTy false t G -> ∃ (λ b -> Nf G t b)
    quo {??} st = _ , st
    quo {bool} st = _ , st
    quo {t => t'} st with st wk (unquo (var (here refl)))
    quo {t => t'} st | false , p with quo p
    quo {t => t'} st | false , p | false , q = false , lam q
    quo {t => t'} st | false , p | true , q = true , blame (causeNf q)
    quo {t => t'} st | true , p = true , blame p

    unquo' : ∀ {G' G t t'} -> Ne G (t => t') false -> OPE G' G -> SemTy false t  G' -> ∃ (λ b -> SemTy b t' G')
    unquo' ne op st with quo st | embedNe op ne 
    ...| b' , st' | ne' = b' , unquo (app ne' st' refl)

    unquo : ∀ {b t G} -> Ne G t b -> SemTy b t G
    unquo {true} ne = causeNe ne
    unquo {false}{??} ne = ne? ne
    unquo {false}{bool} ne = ne? ne
    unquo {false}{t => t'} ne
      = unquo' ne

  -- building the initial context. We assume that no term is a blame.

  unquoCon : ∀ {G} -> SemCon G G
  unquoCon {[]} = ●
  unquoCon {t :: G}
    = EmbedSemCon wk unquoCon , unquo {b = false}(var {G = t :: G}(here refl))

  -- normalization

  nf : ∀ {G t} → Term G t → ∃ (λ b -> Nf G t b)
  nf e with SemTerm (cast-insert e) unquoCon
  ... | false , e' = quo e' 
  ... | true , e' = true , blame e'