Mercurial > cpdt > repo
comparison src/Interps.v @ 223:2a34c4dc6a10
Port Interps
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 16 Nov 2009 12:18:55 -0500 |
parents | cbf2f74a5130 |
children | 05250878e4ca |
comparison
equal
deleted
inserted
replaced
222:13620dfd5f97 | 223:2a34c4dc6a10 |
---|---|
1 (* Copyright (c) 2008, Adam Chlipala | 1 (* Copyright (c) 2008-2009, Adam Chlipala |
2 * | 2 * |
3 * This work is licensed under a | 3 * This work is licensed under a |
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
5 * Unported License. | 5 * Unported License. |
6 * The license text is available at: | 6 * The license text is available at: |
83 match t with | 83 match t with |
84 | Nat => nat | 84 | Nat => nat |
85 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 85 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
86 end. | 86 end. |
87 | 87 |
88 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | 88 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := |
89 match e in (exp _ t) return (typeDenote t) with | 89 match e with |
90 | Var _ v => v | 90 | Var _ v => v |
91 | 91 |
92 | Const n => n | 92 | Const n => n |
93 | Plus e1 e2 => expDenote e1 + expDenote e2 | 93 | Plus e1 e2 => expDenote e1 + expDenote e2 |
94 | 94 |
111 | 111 |
112 (* begin thide *) | 112 (* begin thide *) |
113 Section cfold. | 113 Section cfold. |
114 Variable var : type -> Type. | 114 Variable var : type -> Type. |
115 | 115 |
116 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := | 116 Fixpoint cfold t (e : exp var t) : exp var t := |
117 match e in exp _ t return exp _ t with | 117 match e with |
118 | Var _ v => #v | 118 | Var _ v => #v |
119 | 119 |
120 | Const n => ^n | 120 | Const n => ^n |
121 | Plus e1 e2 => | 121 | Plus e1 e2 => |
122 let e1' := cfold e1 in | 122 let e1' := cfold e1 in |
258 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 258 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
259 | t1 ** t2 => typeDenote t1 * typeDenote t2 | 259 | t1 ** t2 => typeDenote t1 * typeDenote t2 |
260 | t1 ++ t2 => typeDenote t1 + typeDenote t2 | 260 | t1 ++ t2 => typeDenote t1 + typeDenote t2 |
261 end%type. | 261 end%type. |
262 | 262 |
263 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | 263 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := |
264 match e in (exp _ t) return (typeDenote t) with | 264 match e with |
265 | Var _ v => v | 265 | Var _ v => v |
266 | 266 |
267 | Const n => n | 267 | Const n => n |
268 | Plus e1 e2 => expDenote e1 + expDenote e2 | 268 | Plus e1 e2 => expDenote e1 + expDenote e2 |
269 | 269 |
310 match t return pairOutType t with | 310 match t return pairOutType t with |
311 | _ ** _ => None | 311 | _ ** _ => None |
312 | _ => tt | 312 | _ => tt |
313 end. | 313 end. |
314 | 314 |
315 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) := | 315 Definition pairOut t1 t2 (e : exp var (t1 ** t2)) |
316 : option (exp var t1 * exp var t2) := | |
316 match e in exp _ t return pairOutType t with | 317 match e in exp _ t return pairOutType t with |
317 | Pair _ _ e1 e2 => Some (e1, e2) | 318 | Pair _ _ e1 e2 => Some (e1, e2) |
318 | _ => pairOutDefault _ | 319 | _ => pairOutDefault _ |
319 end. | 320 end. |
320 | 321 |
321 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := | 322 Fixpoint cfold t (e : exp var t) : exp var t := |
322 match e in exp _ t return exp _ t with | 323 match e with |
323 | Var _ v => #v | 324 | Var _ v => #v |
324 | 325 |
325 | Const n => ^n | 326 | Const n => ^n |
326 | Plus e1 e2 => | 327 | Plus e1 e2 => |
327 let e1' := cfold e1 in | 328 let e1' := cfold e1 in |