Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
open import Data.List
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to mapSum)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality
Con : Set Set
Con = List
data Var {A : Set} (t : A) : Con A Set where
here : : Con A} Var t (t ∷ Γ)
there : {t′} {Γ : Con A} (v : Var t Γ) Var t (t′ ∷ Γ)
data _⊆_ {A : Set} : Con A -> Con A -> Set where
stop : [] ⊆ []
skip : {Γ Δ a} -> Γ ⊆ Δ -> Γ ⊆ (a ∷ Δ)
keep : {Γ Δ a} -> Γ ⊆ Δ -> (a ∷ Γ) ⊆ (a ∷ Δ)
⊆-refl : {A} {Γ : Con A} Γ ⊆ Γ
⊆-refl {Γ = []} = stop
⊆-refl {Γ = x ∷ Γ} = keep ⊆-refl
⊆-trans : {A} {Γ₁ Γ₂ Γ₃ : Con A} Γ₁ ⊆ Γ₂ Γ₂ ⊆ Γ₃ Γ₁ ⊆ Γ₃
⊆-trans σ₁ stop = σ₁
⊆-trans σ₁ (skip σ₂) = skip (⊆-trans σ₁ σ₂)
⊆-trans (skip σ₁) (keep σ₂) = skip (⊆-trans σ₁ σ₂)
⊆-trans (keep σ₁) (keep σ₂) = keep (⊆-trans σ₁ σ₂)
⊆-trans-idʳ : {A} {Γ Γ′ : Con A} : Γ ⊆ Γ′) ⊆-trans σ ⊆-refl ≡ σ
⊆-trans-idʳ stop = refl
⊆-trans-idʳ (skip σ) = cong skip (⊆-trans-idʳ σ)
⊆-trans-idʳ (keep σ) = cong keep (⊆-trans-idʳ σ)
⊆-trans-idˡ : {A} {Γ Γ′ : Con A} : Γ ⊆ Γ′) ⊆-trans ⊆-refl σ ≡ σ
⊆-trans-idˡ stop = refl
⊆-trans-idˡ (skip σ) = cong skip (⊆-trans-idˡ σ)
⊆-trans-idˡ (keep σ) = cong keep (⊆-trans-idˡ σ)
top : {A a} {Γ : Con A} -> Γ ⊆ (a ∷ Γ)
top = skip ⊆-refl
renᵛ : {A a} {Γ Δ : Con A} -> Γ ⊆ Δ -> Var a Γ Var a Δ
renᵛ stop ()
renᵛ (skip σ) v = there (renᵛ σ v)
renᵛ (keep σ) here = here
renᵛ (keep σ) (there v) = there (renᵛ σ v)
renᵛ-compose : {A a} {Γ₁ Γ₂ Γ₃ : Con A} (σ₁ : Γ₁ ⊆ Γ₂) (σ₂ : Γ₂ ⊆ Γ₃)
renᵛ {a = a} σ₂ ∘ renᵛ σ₁ ≗ renᵛ (⊆-trans σ₁ σ₂)
renᵛ-compose () stop here
renᵛ-compose () stop (there v)
renᵛ-compose σ₁ (skip σ₂) v = cong there (renᵛ-compose σ₁ σ₂ v)
renᵛ-compose (skip σ₁) (keep σ₂) v = cong there (renᵛ-compose σ₁ σ₂ v)
renᵛ-compose (keep σ₁) (keep σ₂) here = refl
renᵛ-compose (keep σ₁) (keep σ₂) (there v) = cong there (renᵛ-compose σ₁ σ₂ v)
data Env {A} (_⊢_ : Con A A Set) (Δ : Con A) : Con A Set where
[] : Env _⊢_ Δ []
_∷_ : {Γ t} (Δ ⊢ t) Env _⊢_ Δ Γ Env _⊢_ Δ (t ∷ Γ)
lookup : {A _⊢_ a} {Γ Δ : Con A} Env _⊢_ Δ Γ Var a Γ Δ ⊢ a
lookup (x ∷ ρ) here = x
lookup (x ∷ ρ) (there v) = lookup ρ v
data Kind : Set where
: Kind
KCon : Set
KCon = Con Kind
mutual
Ty : KCon Set
Ty Γ = Γ ⊢ₖ ⋆
data _⊢ₖ_: KCon) : Kind Set where
TyVar : {κ} : Var κ Γ) Γ ⊢ₖ κ
_⟶_ : (t₁ t₂ : Ty Γ) Ty Γ
Forall : {κ′} : Kind) (t : (κ ∷ Γ) ⊢ₖ κ′) Γ ⊢ₖ κ′
renᵗʸ : {Γ Γ′ κ} Γ ⊆ Γ′ Γ ⊢ₖ κ Γ′ ⊢ₖ κ
renᵗʸ σ (TyVar α) = TyVar (renᵛ σ α)
renᵗʸ σ (t₁ ⟶ t₂) = renᵗʸ σ t₁ ⟶ renᵗʸ σ t₂
renᵗʸ σ (Forall κ t) = Forall κ (renᵗʸ (keep σ) t)
renᵗʸ-compose : {Γ₁ Γ₂ Γ₃ κ} (σ₁ : Γ₁ ⊆ Γ₂) (σ₂ : Γ₂ ⊆ Γ₃) renᵗʸ {κ = κ} σ₂ ∘ renᵗʸ σ₁ ≗ renᵗʸ (⊆-trans σ₁ σ₂)
renᵗʸ-compose σ₁ σ₂ (TyVar α) = cong TyVar (renᵛ-compose σ₁ σ₂ α)
renᵗʸ-compose σ₁ σ₂ (t₁ ⟶ t₂) = cong₂ _⟶_ (renᵗʸ-compose σ₁ σ₂ t₁) (renᵗʸ-compose σ₁ σ₂ t₂)
renᵗʸ-compose σ₁ σ₂ (Forall κ t) = cong (Forall κ) (renᵗʸ-compose (keep σ₁) (keep σ₂) t)
wkᵗʸ : {κ₀ Γ κ} (Γ ⊢ₖ κ) (κ₀ ∷ Γ) ⊢ₖ κ
wkᵗʸ = renᵗʸ top
KEnv : KCon KCon Set
KEnv = Env _⊢ₖ_
renᵗʸᴱ : {Γ Δ Ω : KCon} Γ ⊆ Ω KEnv Γ Δ KEnv Ω Δ
renᵗʸᴱ σ [] = []
renᵗʸᴱ σ (t ∷ ρ) = (renᵗʸ σ t) ∷ (renᵗʸᴱ σ ρ)
keepᵗʸᴱ : {Γ Δ κ} KEnv Γ Δ KEnv (κ ∷ Γ) (κ ∷ Δ)
keepᵗʸᴱ ρ = TyVar here ∷ renᵗʸᴱ top ρ
reflᵗʸᴱ : : KCon} KEnv Γ Γ
reflᵗʸᴱ {[]} = []
reflᵗʸᴱ {_ ∷ _} = keepᵗʸᴱ reflᵗʸᴱ
subᵗʸ : {Γ Γ′ κ} KEnv Γ′ Γ Γ ⊢ₖ κ Γ′ ⊢ₖ κ
subᵗʸ ρ (TyVar α) = lookup ρ α
subᵗʸ ρ (t₁ ⟶ t₂) = subᵗʸ ρ t₁ ⟶ subᵗʸ ρ t₂
subᵗʸ ρ (Forall κ t) = Forall κ (subᵗʸ (keepᵗʸᴱ ρ) t)
_[_]ᵗʸ : {Γ κ κ′}
(κ′ ∷ Γ) ⊢ₖ κ
Γ ⊢ₖ κ′
Γ ⊢ₖ κ
t [ t′ ]ᵗʸ = subᵗʸ (t′ ∷ reflᵗʸᴱ) t
TyCon :: KCon) Set
TyCon Γ = Con (Ty Γ)
⊆-wk : {Γ κ} {Σ Σ′ : TyCon Γ} Σ ⊆ Σ′ (map (wkᵗʸ {κ}) Σ) ⊆ (map wkᵗʸ Σ′)
⊆-wk stop = stop
⊆-wk (skip σ) = skip (⊆-wk σ)
⊆-wk (keep σ) = keep (⊆-wk σ)
data _,_⊢ₜ_: KCon) (Σ : TyCon Γ) : Ty Γ Set where
var : {t} Var t Σ Γ , Σ ⊢ₜ t
lam : t {t′} (e : Γ , (t ∷ Σ) ⊢ₜ t′) Γ , Σ ⊢ₜ (t ⟶ t′)
_‿_ : {t₁ t₂} (e₁ : Γ , Σ ⊢ₜ (t₁ ⟶ t₂)) (e₂ : Γ , Σ ⊢ₜ t₁) Γ , Σ ⊢ₜ t₂
Lam : : Kind) {t} (e : (κ ∷ Γ) , map wkᵗʸ Σ ⊢ₜ t) Γ , Σ ⊢ₜ Forall κ t
_&_ : {κ t₀} (e : Γ , Σ ⊢ₜ (Forall κ t₀)) (t : Γ ⊢ₖ κ) Γ , Σ ⊢ₜ (t₀ [ t ]ᵗʸ)
renᵗⱽₜ : {Γ Γ′ t} {Σ : TyCon Γ}
: Γ ⊆ Γ′)
Var t Σ
Var (renᵗʸ σ t) (map (renᵗʸ σ) Σ)
renᵗⱽₜ σ here = here
renᵗⱽₜ σ (there v) = there (renᵗⱽₜ σ v)
open import Data.List.Properties
wk-renᵛ : {Γ Γ′ κ Σ} {t : Ty (κ ∷ Γ)} (σ : Γ ⊆ Γ′)
Var t (map (wkᵗʸ {κ}) Σ)
Var (renᵗʸ (keep σ) t) (map (wkᵗʸ ∘ renᵗʸ σ) Σ)
wk-renᵛ {Σ = []} σ ()
wk-renᵛ {κ = κ} {t ∷ Σ} σ here rewrite
renᵗʸ-compose (skip {a = κ} ⊆-refl) (keep σ) t | ⊆-trans-idˡ σ |
map-cong (renᵗʸ-compose σ (top {a = κ})) (t ∷ Σ) | ⊆-trans-idʳ σ
= here
wk-renᵛ {κ = κ} {t ∷ Σ} σ (there v) = there (wk-renᵛ σ v)
renᵗ : {Γ Σ Σ′ t}
: Σ ⊆ Σ′)
Γ , Σ ⊢ₜ t
Γ , Σ′ ⊢ₜ t
renᵗ σ (var v) = var (renᵛ σ v)
renᵗ σ (lam t e) = lam t (renᵗ (keep σ) e)
renᵗ σ (e₁ ‿ e₂) = renᵗ σ e₁ ‿ renᵗ σ e₂
renᵗ σ (Lam κ e) = Lam κ (renᵗ (⊆-wk σ) e)
renᵗ σ (e & t) = renᵗ σ e & t
TyEnv : {Γ} TyCon Γ TyCon Γ Set
TyEnv {Γ} = Env (λ Σ t Γ , Σ ⊢ₜ t)
renᵗᴱ : {Γ} {Σ Σ′ Ω : TyCon Γ} Σ ⊆ Ω TyEnv Σ Σ′ TyEnv Ω Σ′
renᵗᴱ σ [] = []
renᵗᴱ σ (e ∷ ρ) = (renᵗ σ e) ∷ (renᵗᴱ σ ρ)
keepᵗᴱ : {Γ} {Σ Σ′ : TyCon Γ} {t} TyEnv Σ Σ′ TyEnv (t ∷ Σ) (t ∷ Σ′)
keepᵗᴱ ρ = var here ∷ renᵗᴱ top ρ
reflᵗᴱ : {Γ} {Σ : TyCon Γ} TyEnv Σ Σ
reflᵗᴱ {Σ = []} = []
reflᵗᴱ {Σ = _ ∷ _} = keepᵗᴱ reflᵗᴱ
wkᵗₜ : {Γ κ} {Σ : TyCon Γ} {t} Γ , Σ ⊢ₜ t (κ ∷ Γ) , map wkᵗʸ Σ ⊢ₜ wkᵗʸ t
wkᵗₜ (var v) = var (renᵗⱽₜ (skip ⊆-refl) v)
wkᵗₜ (lam t e) = lam (wkᵗʸ t) (wkᵗₜ e)
wkᵗₜ (e₁ ‿ e₂) = wkᵗₜ e₁ ‿ wkᵗₜ e₂
wkᵗₜ (Lam κ e) = Lam κ {!!}
wkᵗₜ (e & t) = wkᵗₜ {!e!} & wkᵗʸ t
wkᵗᴱ : {Γ κ} {Σ Σ′ : TyCon Γ} TyEnv Σ Σ′ TyEnv (map (wkᵗʸ {κ}) Σ) (map wkᵗʸ Σ′)
wkᵗᴱ [] = []
wkᵗᴱ (e ∷ ρ) = wkᵗₜ e ∷ wkᵗᴱ ρ
subᵗ : {Γ} {Σ Σ′ t} TyEnv Σ′ Σ Γ , Σ ⊢ₜ t Γ , Σ′ ⊢ₜ t
subᵗ ρ (var v) = lookup ρ v
subᵗ ρ (lam t e) = lam t (subᵗ (keepᵗᴱ ρ) e)
subᵗ ρ (e₁ ‿ e₂) = subᵗ ρ e₁ ‿ subᵗ ρ e₂
subᵗ ρ (Lam κ e) = Lam κ (subᵗ (wkᵗᴱ ρ) e)
subᵗ ρ (e & t) = subᵗ ρ e & t
_[_]ᵗ : {Γ Σ t t′}
Γ , (t′ ∷ Σ) ⊢ₜ t
Γ , Σ ⊢ₜ t′
Γ , Σ ⊢ₜ t
e [ e′ ]ᵗ = subᵗ (e′ ∷ reflᵗᴱ) e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.