[agda] start implementing renaming

code/gcbpv.agda

@@ -148,12 +148,27 @@ _⟪_⟫v : VCtx onevar -> Dimension -> VCtx (cdot _)
 Vars (Γ ⟪ i ⟫v) = Vars Γ
 vty (Γ ⟪ i ⟫v)  = map (\A -> A ⟨ i ⟩v) (vty Γ)
 
--- ctx-app-lem : ∀ Γ i -> Γ ⟪ i ⟫v
-
 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 : ℕ
@@ -201,6 +216,7 @@ 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) ->
@@ -211,6 +227,7 @@ _⟨_⟩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
@@ -245,6 +262,17 @@ data Value where
            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
@@ -283,7 +311,7 @@ data Term where
          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)