Mercurial > cpdt > repo

comparison src/Interps.v @ 223:2a34c4dc6a10

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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