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