Newer
Older
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
CType : Set :=
| CTo : forall (A : VType) (B : CType), CType
| CF : forall (A : VType), CType.
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
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.
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
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
.