Mercurial > cpdt > repo

comparison src/Interps.v @ 171:b00b6a9b6b58

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PSLC
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 13:59:51 -0500
parents f8353e2a21d6
children 653c03f6061e
comparison
equal deleted inserted replaced
170:f8353e2a21d6 171:b00b6a9b6b58
59 Implicit Arguments Abs [var t1 t2]. 59 Implicit Arguments Abs [var t1 t2].
60 60
61 Notation "# v" := (Var v) (at level 70). 61 Notation "# v" := (Var v) (at level 70).
62 62
63 Notation "^ n" := (Const n) (at level 70). 63 Notation "^ n" := (Const n) (at level 70).
64 Infix "++" := Plus. 64 Infix "+^" := Plus (left associativity, at level 79).
65 65
66 Infix "@" := App (left associativity, at level 77). 66 Infix "@" := App (left associativity, at level 77).
67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). 67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). 68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
69 69
97 | Plus e1 e2 => 97 | Plus e1 e2 =>
98 let e1' := cfold e1 in 98 let e1' := cfold e1 in
99 let e2' := cfold e2 in 99 let e2' := cfold e2 in
100 match e1', e2' with 100 match e1', e2' with
101 | Const n1, Const n2 => ^(n1 + n2) 101 | Const n1, Const n2 => ^(n1 + n2)
102 | _, _ => e1' ++ e2' 102 | _, _ => e1' +^ e2'
103 end 103 end
104 104
105 | App _ _ e1 e2 => cfold e1 @ cfold e2 105 | App _ _ e1 e2 => cfold e1 @ cfold e2
106 | Abs _ _ e' => Abs (fun x => cfold (e' x)) 106 | Abs _ _ e' => Abs (fun x => cfold (e' x))
107 end. 107 end.
120 Theorem Cfold_correct : forall t (E : Exp t), 120 Theorem Cfold_correct : forall t (E : Exp t),
121 ExpDenote (Cfold E) = ExpDenote E. 121 ExpDenote (Cfold E) = ExpDenote E.
122 unfold ExpDenote, Cfold; intros; apply cfold_correct. 122 unfold ExpDenote, Cfold; intros; apply cfold_correct.
123 Qed. 123 Qed.
124 End STLC. 124 End STLC.
125
126
127 (** * Adding Products and Sums *)
128
129 Module PSLC.
130 Inductive type : Type :=
131 | Nat : type
132 | Arrow : type -> type -> type
133 | Prod : type -> type -> type
134 | Sum : type -> type -> type.
135
136 Infix "-->" := Arrow (right associativity, at level 62).
137 Infix "**" := Prod (right associativity, at level 61).
138 Infix "++" := Sum (right associativity, at level 60).
139
140 Section vars.
141 Variable var : type -> Type.
142
143 Inductive exp : type -> Type :=
144 | Var : forall t,
145 var t
146 -> exp t
147
148 | Const : nat -> exp Nat
149 | Plus : exp Nat -> exp Nat -> exp Nat
150
151 | App : forall t1 t2,
152 exp (t1 --> t2)
153 -> exp t1
154 -> exp t2
155 | Abs : forall t1 t2,
156 (var t1 -> exp t2)
157 -> exp (t1 --> t2)
158
159 | Pair : forall t1 t2,
160 exp t1
161 -> exp t2
162 -> exp (t1 ** t2)
163 | Fst : forall t1 t2,
164 exp (t1 ** t2)
165 -> exp t1
166 | Snd : forall t1 t2,
167 exp (t1 ** t2)
168 -> exp t2
169
170 | Inl : forall t1 t2,
171 exp t1
172 -> exp (t1 ++ t2)
173 | Inr : forall t1 t2,
174 exp t2
175 -> exp (t1 ++ t2)
176 | SumCase : forall t1 t2 t,
177 exp (t1 ++ t2)
178 -> (var t1 -> exp t)
179 -> (var t2 -> exp t)
180 -> exp t.
181 End vars.
182
183 Definition Exp t := forall var, exp var t.
184
185 Implicit Arguments Var [var t].
186 Implicit Arguments Const [var].
187 Implicit Arguments Abs [var t1 t2].
188 Implicit Arguments Inl [var t1 t2].
189 Implicit Arguments Inr [var t1 t2].
190
191 Notation "# v" := (Var v) (at level 70).
192
193 Notation "^ n" := (Const n) (at level 70).
194 Infix "+^" := Plus (left associativity, at level 79).
195
196 Infix "@" := App (left associativity, at level 77).
197 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
198 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
199
200 Notation "[ e1 , e2 ]" := (Pair e1 e2).
201 Notation "#1 e" := (Fst e) (at level 75).
202 Notation "#2 e" := (Snd e) (at level 75).
203
204 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
205 (at level 79).
206
207 Fixpoint typeDenote (t : type) : Set :=
208 match t with
209 | Nat => nat
210 | t1 --> t2 => typeDenote t1 -> typeDenote t2
211 | t1 ** t2 => typeDenote t1 * typeDenote t2
212 | t1 ++ t2 => typeDenote t1 + typeDenote t2
213 end%type.
214
215 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
216 match e in (exp _ t) return (typeDenote t) with
217 | Var _ v => v
218
219 | Const n => n
220 | Plus e1 e2 => expDenote e1 + expDenote e2
221
222 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
223 | Abs _ _ e' => fun x => expDenote (e' x)
224
225 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
226 | Fst _ _ e' => fst (expDenote e')
227 | Snd _ _ e' => snd (expDenote e')
228
229 | Inl _ _ e' => inl _ (expDenote e')
230 | Inr _ _ e' => inr _ (expDenote e')
231 | SumCase _ _ _ e' e1 e2 =>
232 match expDenote e' with
233 | inl v => expDenote (e1 v)
234 | inr v => expDenote (e2 v)
235 end
236 end.
237
238 Definition ExpDenote t (e : Exp t) := expDenote (e _).
239
240 Section cfold.
241 Variable var : type -> Type.
242
243 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
244 match e in exp _ t return exp _ t with
245 | Var _ v => #v
246
247 | Const n => ^n
248 | Plus e1 e2 =>
249 let e1' := cfold e1 in
250 let e2' := cfold e2 in
251 match e1', e2' with
252 | Const n1, Const n2 => ^(n1 + n2)
253 | _, _ => e1' +^ e2'
254 end
255
256 | App _ _ e1 e2 => cfold e1 @ cfold e2
257 | Abs _ _ e' => Abs (fun x => cfold (e' x))
258
259 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
260 | Fst _ _ e' => #1 (cfold e')
261 | Snd _ _ e' => #2 (cfold e')
262
263 | Inl _ _ e' => Inl (cfold e')
264 | Inr _ _ e' => Inr (cfold e')
265 | SumCase _ _ _ e' e1 e2 =>
266 case cfold e' of
267 x => cfold (e1 x)
268 | y => cfold (e2 y)
269 end.
270 End cfold.
271
272 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
273
274 Lemma cfold_correct : forall t (e : exp _ t),
275 expDenote (cfold e) = expDenote e.
276 induction e; crush; try (ext_eq; crush);
277 repeat (match goal with
278 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
279 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
280 end; crush).
281 Qed.
282
283 Theorem Cfold_correct : forall t (E : Exp t),
284 ExpDenote (Cfold E) = ExpDenote E.
285 unfold ExpDenote, Cfold; intros; apply cfold_correct.
286 Qed.
287 End PSLC.