start on agda, coq encodings of gcbpv, use dimension indices!

code/gcbpv.agda

+module gcbpv where
+
+open import Data.Empty
+open import Data.Unit
+open import Relation.Binary.PropositionalEquality
+
+data Stoup : Set where
+  None : Stoup
+  One  : Stoup
+
+⟦_⟧st : Stoup -> Set
+⟦ None ⟧st = ⊥
+⟦ One ⟧st = ⊤
+
+record StCtx (X : Set) : Set where
+  constructor ctx
+  field
+    S : Stoup
+    ty : ⟦ S ⟧st -> X
+
+cdot : forall (X : Set) -> StCtx X
+cdot X = record { S = None ; ty = ⊥-elim }
+
+hstoup : forall (Y : Set) -> Y -> StCtx Y
+hstoup Y B = record { S = One ; ty = \ x → B }
+
+data Dimension : Set where
+  Top : Dimension
+  Bot : Dimension
+
+DCtx : Set
+DCtx = StCtx ⊤
+
+onevar : StCtx ⊤
+onevar = hstoup ⊤ tt
+
+infix 90 _⟨_⟩v
+infix 90 _⟨_⟩c
+
+data VType : DCtx -> Set
+_⟨_⟩v : VType onevar -> Dimension -> VType (cdot _)
+data CType : DCtx -> Set
+_⟨_⟩c : CType onevar -> Dimension -> CType (cdot _)
+
+data VType where
+  VUnit  : forall I -> VType I
+  _×_    : forall {I} -> VType I -> VType I -> VType I
+  U      : forall {I} -> CType I -> VType I
+  vtrans : forall (Atop : VType onevar) (Abot : VType onevar) ->
+           Atop ⟨ Bot ⟩v ≡ Abot ⟨ Top ⟩v ->
+           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 Atop Abot p ⟨ Top ⟩v = Atop ⟨ Top ⟩v
+vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩v
+
+data CType where
+  _⇀_ : forall {I} -> VType I -> CType I -> CType I
+  F   : forall {I} -> VType I -> CType I
+
+(A ⇀ B) ⟨ i ⟩c = (A ⟨ i ⟩v) ⇀ (B ⟨ i ⟩c)
+F A ⟨ i ⟩c = F (A ⟨ i ⟩v)
+
+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)
+

code/gcbpv.v

+Close Scope nat_scope.
+Open Scope type_scope.
+
+Inductive Stoup := None | One.
+Definition StoupSem (S : Stoup) :=
+  match S with
+    | None => Empty_set
+    | One  => unit
+  end.
+
+Record StCtx X := mkStCtx {
+                      S  : Stoup;
+                      ty : StoupSem S -> X
+                    }.
+
+Definition cdot X : StCtx X := mkStCtx _ None (fun x => match x with end).
+Definition hstoup Y (B : Y) : StCtx Y := mkStCtx _ One (fun x => match x with tt => B end).
+
+Inductive Dimension := Top | Bot.
+Definition DCtx := StCtx Dimension.
+
+Inductive VType : DCtx -> Set :=
+  VUnit : forall I, VType I
+| VTimes : forall {I} (A A' : VType I), VType I
+| VU : forall {I} (B : CType I), VType I
+with
+CType : DCtx -> Set :=
+| CTo : forall {I} (A : VType I) (B : CType I), CType I
+| CF  : forall {I} (A : VType I), CType I.
+
+Inductive Vlt : VType -> VType -> Set :=
+  vrefl : forall A, Vlt A A
+| vtrans : forall A1 A2 A3, Vlt A1 A2 -> Vlt A2 A3 -> Vlt A1 A3
+| vtimesmon : forall A1 A1' A2 A2',
+                Vlt A1 A2 ->
+                Vlt A1' A2' ->
+                Vlt (VTimes A1 A1') (VTimes A2 A2')
+| vumon : forall B1 B2,
+            Clt B1 B2 ->
+            Vlt (VU B1) (VU B2)
+with
+Clt : CType -> CType -> Set :=
+  crefl : forall B, Clt B B
+| ctrans : forall B1 B2 B3, Clt B1 B2 -> Clt B2 B3 -> Clt B1 B3
+| ctimesmon : forall A1 A2 B1 B2,
+                Vlt A1 A2 ->
+                Clt B1 B2 ->
+                Clt (CTo A1 B1) (CTo A2 B2)
+| cfmon : forall A1 A2,
+            Vlt A1 A2 ->
+            Clt (CF A1) (CF A2)
+.
+
+Definition Vars := Set.
+(* Definition VCtx (U : Vars) := U -> VType. *)
+Record VCtx := mkVCtx {
+                    U : Vars;
+                    vty : U -> VType
+                 }.
+
+
+Definition ext (G : VCtx) (A : VType) : VCtx :=
+  mkVCtx (U G + unit)
+         (fun x =>
+            match x with
+              | inl x => vty G x
+              | inr tt => A            
+            end).
+
+Inductive Value : VCtx -> VType -> Type :=
+| var : forall G (x : U G), Value G (vty G x)
+| vunit : forall G, Value G VUnit
+| vpair : forall {G} A A' (v : Value G A) (v' : Value G A'), Value G (VTimes A A')
+| vdestr : forall {G} A A' Am
+                  (v : Value G (VTimes A A'))
+                  (vk  : Value (ext G A) Am)
+                  (vk' : Value (ext G A') Am),
+                  Value G Am
+| vthunk : forall {G} B
+                  (M : Term G cdot B),
+             Value G (VU B)
+with
+Term : VCtx -> CCtx -> CType -> Type :=
+| hole   : forall G B, Term G (hstoup B) B
+| lambda : forall {G Dt B} A
+                  (M : Term (ext G A) Dt B),
+             Term G Dt (CTo A B)
+| app    : forall {G Dt A B} 
+                  (M : Term G Dt (CTo A B))
+                  (v : Value G A),
+             Term G Dt B
+| force : forall {G B}
+                 (v : Value G (VU B)),
+            Term G cdot B
+| ret : forall {G A}
+               (v : Value G A),
+          Term G cdot (CF A)
+| lett : forall {G Dt A B}
+                (M : Term G Dt (CF A))
+                (N : Term (ext G A) cdot B),
+           Term G Dt B
+.
+
+
+
+
+asdf
+  . 
\ No newline at end of file