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 VType : Set :=
  VUnit : VType
| VTimes : forall (A A' : VType), VType
| VU : forall (B : CType), VType
with
CType : Set :=
| CTo : forall (A : VType) (B : CType), CType
| CF  : forall (A : VType), CType.

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

Definition CCtx := StCtx CType.

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
.