gcbpv.agda

module gcbpv where

open import Data.Empty
open import Data.Unit
open import Data.Sum hiding (map)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin
open import Data.Vec
import Data.Vec
open import Data.Vec.Properties
open ≡-Reasoning

data Stoup : Set where
  None : Stoup
  One  : Stoup

-- | Semantics
-- | ⟦ S ⟧st X =~ ⟦ S ⟧ -> X
⟦_⟧st : Stoup -> Set -> Set
⟦ None ⟧st X = ⊤
⟦ One ⟧st X = X

record StCtx (X : Set) : Set where
  constructor stctx
  field
    S : Stoup
    ty : ⟦ S ⟧st X

cdot : forall (X : Set) -> StCtx X
cdot X = record { S = None ; ty = tt }

hstoup : forall {Y : Set} -> Y -> StCtx Y
hstoup B = record { S = One ; ty = B }

data Dimension : Set where
  GT : Dimension
  LT : Dimension

DCtx : Set
DCtx = StCtx ⊤

onevar : StCtx ⊤
onevar = hstoup tt

infixl 90 _⟨_⟩v
infixl 90 _⟨_⟩vsq
infixl 90 _⟨_⟩c

data VType : DCtx -> Set
_⟨_⟩v : VType onevar -> Dimension -> VType (cdot _)
record VTC : Set
data CType : DCtx -> Set
_⟨_⟩c : CType onevar -> Dimension -> CType (cdot _)

-- | Transitivvity-composable pair of value types
-- | "Value Transitivity Composite"
record VTC where
  inductive
  field
    Agt : VType onevar
    Alt : VType onevar
    eq : Agt ⟨ LT ⟩v ≡ Alt ⟨ GT ⟩v

data VType where
  VUnit  : forall I -> VType I
  _×_    : forall {I} -> VType I -> VType I -> VType I
  U      : forall {I} -> CType I -> VType I
  vtrans : VTC -> VType onevar

VUnit _ ⟨ i ⟩v = VUnit _
(A × A') ⟨ i ⟩v = (A ⟨ i ⟩v) × (A' ⟨ i ⟩v)
U B ⟨ i ⟩v = U (B ⟨ i ⟩c)
vtrans Vsq ⟨ GT ⟩v = VTC.Agt Vsq ⟨ GT ⟩v -- morally this: Vsq ⟨ GT ⟩vsq ⟨ GT ⟩v
vtrans Vsq ⟨ LT ⟩v = VTC.Alt Vsq ⟨ LT ⟩v -- morally this: Vsq ⟨ LT ⟩vsq ⟨ LT ⟩v
-- vtrans Atop Abot p ⟨ GT ⟩v = Atop ⟨ GT ⟩v
-- vtrans Atop Abot p ⟨ LT ⟩v = Abot ⟨ LT ⟩v

data CType where
  _⇀_ : forall {I} -> VType I -> CType I -> CType I
  F   : forall {I} -> VType I -> CType I
  ctrans : forall (Btop : CType onevar) (Bbot : CType onevar) ->
           Btop ⟨ LT ⟩c ≡ Bbot ⟨ GT ⟩c ->
           CType onevar

(A ⇀ B) ⟨ i ⟩c = (A ⟨ i ⟩v) ⇀ (B ⟨ i ⟩c)
F A ⟨ i ⟩c = F (A ⟨ i ⟩v)
ctrans Btop Bbot p ⟨ GT ⟩c = Btop ⟨ GT ⟩c
ctrans Btop Bbot p ⟨ LT ⟩c = Bbot ⟨ LT ⟩c

_⟨_⟩vsq : VTC -> Dimension -> VType onevar
Vsq ⟨ GT ⟩vsq = VTC.Agt Vsq
Vsq ⟨ LT ⟩vsq = VTC.Alt Vsq

vrefl : VType (cdot _) -> VType onevar
crefl : CType (cdot _) -> CType onevar
vrefl (VUnit _) = VUnit _
vrefl (A × A') = vrefl A × vrefl A'
vrefl (U B) = U (crefl B)

crefl (A ⇀ B) = vrefl A ⇀ crefl B
crefl (F A) = F (vrefl A)

vreflretract : forall A i -> vrefl A ⟨ i ⟩v ≡ A
creflretract : forall B i -> crefl B ⟨ i ⟩c ≡ B

vreflretract (VUnit _) i = refl
vreflretract (A × A₁) i = cong₂ _×_ (vreflretract A i) (vreflretract A₁ i)
vreflretract (U B) i = cong U (creflretract B i)

creflretract (A ⇀ B) i = cong₂ _⇀_ (vreflretract A i) (creflretract B i)
creflretract (F A) i = cong F (vreflretract A i)

-- | For a more traditional presentation of ordering
data VLt (A A' : VType (cdot _)) : Set where
  lt : forall (Aord : VType onevar) -> Aord ⟨ GT ⟩v ≡ A -> Aord ⟨ LT ⟩v ≡ A' -> VLt A A'
data CLt (B B' : CType (cdot _)) : Set where
  lt : forall (Bord : CType onevar) -> Bord ⟨ GT ⟩c ≡ B -> Bord ⟨ LT ⟩c ≡ B' -> CLt B B'

-- | Now the term structure
-- Values correspond to complex values in cbpv
-- Terms correspond to both terms and complex stacks in cbpv
-- Everything is also indexed by a dimension stoup, so that we simultaneously
-- implement the term constructors and their monotonicity, meaning like the
-- types we can implement reflexivity as weakening and only have to add in
-- transitivity, beta and eta

record VCtx (I : DCtx) : Set where
  constructor vctx
  field
    Vars : ℕ
    vty  : Vec (VType I) Vars
open VCtx

vcdot : ∀ I -> VCtx I
vcdot I = vctx zero []

infixl 20 _,,_
_,,_ : forall {I} -> VCtx I -> VType I -> VCtx I
Vars (Γ ,, A) = suc (Vars Γ)
vty  (Γ ,, A) = A ∷ vty Γ

infixl 90 _⟪_⟫v
infixl 90 _⟪_⟫vsq
infixl 90 _⟪_⟫c

_⟪_⟫v : VCtx onevar -> Dimension -> VCtx (cdot _)
Vars (Γ ⟪ i ⟫v) = Vars Γ
vty (Γ ⟪ i ⟫v)  = map (\A -> A ⟨ i ⟩v) (vty Γ)

vctxrefl : VCtx (cdot _) -> VCtx onevar
Vars (vctxrefl Γ) = Vars Γ
vty  (vctxrefl Γ) = map vrefl (vty Γ)

record Var {I} (Γ : VCtx I) (A : VType I) : Set where
  constructor mkVar
  field
    name  : Fin (Vars Γ)
    types : A ≡ lookup name (vty Γ)

-- | Based on Allais-Chapman-McBride-McKenna "Type-and-Scope Safe Programs and Their Proofs"
VModel : Set₁
VModel = forall {I} -> VCtx I -> VType I -> Set

record VEnv {I} (V : VModel) (Γ : VCtx I) (Γ' : VCtx I) : Set
  where constructor pack
        field env-lookup : forall A -> Var Γ' A -> V Γ A
open VEnv
Renaming : forall {I} -> VCtx I -> VCtx I -> Set
Renaming = VEnv Var

record VCtxTC : Set where
  field
    Vars : ℕ
    vty  : Vec VTC Vars
open VCtxTC

_⟪_⟫vsq : VCtxTC -> Dimension -> VCtx onevar
Vars (Γsq ⟪ i ⟫vsq) = Vars Γsq
vty  (Γsq ⟪ i ⟫vsq) = (map (λ Vsq → Vsq ⟨ i ⟩vsq) (vty Γsq))

vctxtrans : VCtxTC -> VCtx onevar
vctxtrans Γsq = vctx (Vars Γsq) (map vtrans (vty Γsq))

vtrans-dapp-lem : ∀ Vsq i ->  vtrans Vsq ⟨ i ⟩v ≡ Vsq ⟨ i ⟩vsq ⟨ i ⟩v
vtrans-dapp-lem Vsq GT = refl
vtrans-dapp-lem Vsq LT = refl

ctxttrans-dapp-lem : ∀ Γsq i -> vctxtrans Γsq ⟪ i ⟫v ≡ Γsq ⟪ i ⟫vsq ⟪ i ⟫v
ctxttrans-dapp-lem Γsq i =
  begin
    vctxtrans Γsq ⟪ i ⟫v
    ≡⟨ cong (vctx (Vars Γsq)) (
      begin
        map (λ A → A ⟨ i ⟩v) (vty (vctxtrans Γsq))
        ≡⟨ sym (map-∘ (\A -> A ⟨ i ⟩v) vtrans (vty Γsq)) ⟩
        map (λ Vsq → vtrans Vsq ⟨ i ⟩v) (vty Γsq)
        ≡⟨ map-cong (λ x → vtrans-dapp-lem x i) (vty Γsq) ⟩
        map (λ Vsq → Vsq ⟨ i ⟩vsq ⟨ i ⟩v) (vty Γsq)
        ≡⟨ map-∘ ((λ A → A ⟨ i ⟩v)) ((λ Vsq → Vsq ⟨ i ⟩vsq)) (vty Γsq) ⟩
        map (λ A → A ⟨ i ⟩v) (map (λ Vsq → Vsq ⟨ i ⟩vsq) (vty Γsq))
      ∎
    )⟩
    Γsq ⟪ i ⟫vsq ⟪ i ⟫v
  ∎

CCtx : DCtx -> Set
CCtx I = StCtx (CType I)

_⟪_⟫c : CCtx onevar -> Dimension -> CCtx (cdot _)
stctx None ty ⟪ i ⟫c = stctx None tt
stctx One ty ⟪ i ⟫c = stctx One (ty ⟨ i ⟩c)

cctxrefl : CCtx (cdot _) -> CCtx onevar
cctxrefl (stctx None ty) = stctx None tt
cctxrefl (stctx One ty) = stctx One (crefl ty)

data Value : forall {I} -> VCtx I -> VType I -> Set
renV : forall {I} {Γ : VCtx I} {Γ'}{A} -> Renaming Γ Γ' -> Value Γ' A -> Value Γ A
_⟨_⟩vv : forall {Γ : VCtx onevar} {A} ->
         Value Γ A ->
         (i : Dimension) ->
         Value (Γ ⟪ i ⟫v) (A ⟨ i ⟩v)
record ValTC : Set
data Term  : forall {I} -> VCtx I -> CCtx I -> CType I -> Set
_⟨_⟩cc : forall {Γ : VCtx onevar}{Δ}{B} ->
         Term Γ Δ B ->
         (i : Dimension) ->
         Term (Γ ⟪ i ⟫v) (Δ ⟪ i ⟫c) (B ⟨ i ⟩c)
renC : forall {I} {Γ : VCtx I}{Δ}{Γ'}{A} -> Renaming Γ Γ' -> Term Γ' Δ A -> Term Γ Δ A

record ValTC where
  inductive
  field
    ΓΓ : VCtxTC
    AA : VTC
    Vgt : Value (ΓΓ ⟪ GT ⟫vsq) (AA ⟨ GT ⟩vsq)
    Vlt : Value (ΓΓ ⟪ LT ⟫vsq) (AA ⟨ LT ⟩vsq)

data Value where
  var : forall {I} (Γ : VCtx I) (x : Fin (Vars Γ)) A -> A ≡ lookup x (vty Γ) -> Value Γ A
  vunit : forall {I} (Γ : VCtx I) -> Value Γ (VUnit _)
  vpair : forall {I}{Γ : VCtx I}{A}{A'} -> Value Γ A -> Value Γ A' -> Value Γ (A × A')
  vdestr : forall {I}{Γ : VCtx I}{A}{A'}{Am} ->
           Value Γ (A × A') ->
           Value (Γ ,, A ,, A') Am ->
           Value Γ Am
  vthunk : forall {I}{Γ : VCtx I}{B} ->
           Term Γ (cdot _) B ->
           Value Γ (U B)
  valtrans : forall
              (sq : ValTC) ->
              Value (vctxtrans (ValTC.ΓΓ sq)) (vtrans (ValTC.AA sq))
  vupcast : forall
              {Γ} Aord ->
              Value Γ (Aord ⟨ LT ⟩v) ->
              Value Γ (Aord ⟨ GT ⟩v)
  vupl : forall
           Aord ->
           Value (vcdot _ ,, vrefl (Aord ⟨ LT ⟩v)) Aord
  vupr : forall
           Aord ->
           Value (vcdot _ ,, Aord) (vrefl (Aord ⟨ GT ⟩v))

renV ρ (var Γ x A p) with env-lookup ρ A (mkVar x p)
... | y = var _ (Var.name y) _ (Var.types y)
renV ρ (vunit Γ) = vunit _
renV ρ (vpair V V') = vpair (renV ρ V) (renV ρ V')
renV ρ (vdestr V V₁) = {!!}
renV ρ (vthunk M) = vthunk (renC ρ M)
renV ρ (valtrans sq) = {!!}
renV ρ (vupcast Aord V) = {!!}
renV ρ (vupl Aord) = {!!}
renV ρ (vupr Aord) = {!!}

var Γ x A p ⟨ i ⟩vv = var (Γ ⟪ i ⟫v) x (A ⟨ i ⟩v)
  (begin
    A ⟨ i ⟩v
    ≡⟨ cong (λ A → A ⟨ i ⟩v) p ⟩
    (lookup x (vty Γ)) ⟨ i ⟩v
    ≡⟨ sym (lookup-map x (\A -> A ⟨ i ⟩v) (vty Γ)) ⟩
    lookup x (vty (Γ ⟪ i ⟫v))
  ∎)
vunit Γ ⟨ i ⟩vv = vunit (Γ ⟪ i ⟫v)
vpair V V' ⟨ i ⟩vv = vpair (V ⟨ i ⟩vv) (V' ⟨ i ⟩vv)
vdestr V Vk ⟨ i ⟩vv = vdestr (V ⟨ i ⟩vv) (Vk ⟨ i ⟩vv)
vthunk M ⟨ i ⟩vv = vthunk (M ⟨ i ⟩cc)
valtrans sq ⟨ GT ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) GT = ValTC.Vgt sq ⟨ GT ⟩vv
valtrans sq ⟨ LT ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) LT = ValTC.Vlt sq ⟨ LT ⟩vv
vupl Aord ⟨ GT ⟩vv = vupcast Aord (var _ zero _ (sym (vreflretract _ _)))
vupl Aord ⟨ LT ⟩vv = var _ zero _ (sym (vreflretract _ _))
vupr Aord ⟨ GT ⟩vv = var _ zero _ (vreflretract _ _)
vupr Aord ⟨ LT ⟩vv rewrite vreflretract (Aord ⟨ GT ⟩v) LT = vupcast Aord (var _ zero _ refl)

data Term where
  hole : forall {I}{Γ : VCtx I}{B} -> Term Γ (hstoup B) B
  lambda : forall {I}{Γ : VCtx I}{Δ}{A}{B} ->
           Term (Γ ,, A) Δ B ->
           Term Γ Δ (A ⇀ B)
  app : forall {I}{Γ : VCtx I}{Δ}{A}{B} ->
           Term Γ Δ (A ⇀ B) ->
           Value Γ A ->
           Term Γ Δ B
  force : forall {I}{Γ : VCtx I}{B} ->
          Value Γ (U B) ->
          Term Γ (cdot _) B
  ret : forall {I}{Γ : VCtx I}{A} ->
        Value Γ A ->
        Term Γ (cdot _) (F A)
  lett : forall {I}{Γ : VCtx I}{Δ}{A}{B} ->
         Term Γ Δ (F A) ->
         Term Γ (cdot _) B ->
         Term Γ Δ B
renC ρ M = {!!}
hole ⟨ i ⟩cc = hole
lambda M ⟨ i ⟩cc = lambda (M ⟨ i ⟩cc)
app M V ⟨ i ⟩cc = app (M ⟨ i ⟩cc) (V ⟨ i ⟩vv)
force V ⟨ i ⟩cc = force (V ⟨ i ⟩vv)
ret V ⟨ i ⟩cc = ret (V ⟨ i ⟩vv)
lett M Mk ⟨ i ⟩cc = lett (M ⟨ i ⟩cc) (Mk ⟨ i ⟩cc)

valrefl : forall {Γ}{A} -> Value Γ A -> Value (vctxrefl Γ) (vrefl A)
termrefl : forall {Γ}{Δ}{B} -> Term Γ Δ B -> Term (vctxrefl Γ) (cctxrefl Δ) (crefl B)

valrefl (var Γ x A p) = var (vctxrefl Γ) x (vrefl A) (
  begin
    vrefl A
    ≡⟨ cong vrefl p ⟩
    vrefl (lookup x (vty Γ))
    ≡⟨ sym (lookup-map x vrefl (vty Γ)) ⟩
    lookup x (vty (vctxrefl Γ))
  ∎)
valrefl (vunit Γ) = vunit _
valrefl (vpair V V') = vpair (valrefl V) (valrefl V')
valrefl (vdestr V Vk) = vdestr (valrefl V) (valrefl Vk)
valrefl (vthunk M) = vthunk (termrefl M)
valrefl (vupcast Aord V) = {!!} -- Need to use substitution here!

termrefl hole = hole
termrefl (lambda M) = lambda (termrefl M)
termrefl (app M V) = app (termrefl M) (valrefl V)
termrefl (force V) = force (valrefl V)
termrefl (ret V) = ret (valrefl V)
termrefl (lett M Mk) = lett (termrefl M) ((termrefl Mk))