Mercurial > cpdt > repo

comparison src/MoreDep.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents 22f111d5cda2
children c4b1c0de7af9
comparison
equal deleted inserted replaced
203:71ade09024ac 204:cbf2f74a5130
245 245
246 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages, but is similar to what goes on with Haskell type classes. 246 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages, but is similar to what goes on with Haskell type classes.
247 247
248 With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. *) 248 With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. *)
249 249
250 Fixpoint cfold t (e : exp t) {struct e} : exp t := 250 Fixpoint cfold t (e : exp t) : exp t :=
251 match e in (exp t) return (exp t) with 251 match e with
252 | NConst n => NConst n 252 | NConst n => NConst n
253 | Plus e1 e2 => 253 | Plus e1 e2 =>
254 let e1' := cfold e1 in 254 let e1' := cfold e1 in
255 let e2' := cfold e2 in 255 let e2' := cfold e2 in
256 match e1', e2' with 256 match e1', e2' return _ with
257 | NConst n1, NConst n2 => NConst (n1 + n2) 257 | NConst n1, NConst n2 => NConst (n1 + n2)
258 | _, _ => Plus e1' e2' 258 | _, _ => Plus e1' e2'
259 end 259 end
260 | Eq e1 e2 => 260 | Eq e1 e2 =>
261 let e1' := cfold e1 in 261 let e1' := cfold e1 in
262 let e2' := cfold e2 in 262 let e2' := cfold e2 in
263 match e1', e2' with 263 match e1', e2' return _ with
264 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) 264 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
265 | _, _ => Eq e1' e2' 265 | _, _ => Eq e1' e2'
266 end 266 end
267 267
268 | BConst b => BConst b 268 | BConst b => BConst b
269 | And e1 e2 => 269 | And e1 e2 =>
270 let e1' := cfold e1 in 270 let e1' := cfold e1 in
271 let e2' := cfold e2 in 271 let e2' := cfold e2 in
272 match e1', e2' with 272 match e1', e2' return _ with
273 | BConst b1, BConst b2 => BConst (b1 && b2) 273 | BConst b1, BConst b2 => BConst (b1 && b2)
274 | _, _ => And e1' e2' 274 | _, _ => And e1' e2'
275 end 275 end
276 | If _ e e1 e2 => 276 | If _ e e1 e2 =>
277 let e' := cfold e in 277 let e' := cfold e in
1026 Defined. 1026 Defined.
1027 1027
1028 (** Finally, we have [dec_star]. It has a straightforward implementation. We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star]. The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *) 1028 (** Finally, we have [dec_star]. It has a straightforward implementation. We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star]. The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
1029 1029
1030 Definition dec_star : {star P s} + { ~star P s}. 1030 Definition dec_star : {star P s} + { ~star P s}.
1031 refine (match s with 1031 refine (match s return _ with
1032 | "" => Reduce (dec_star' (n := length s) 0 _) 1032 | "" => Reduce (dec_star' (n := length s) 0 _)
1033 | _ => Reduce (dec_star' (n := length s) 0 _) 1033 | _ => Reduce (dec_star' (n := length s) 0 _)
1034 end); crush. 1034 end); crush.
1035 Defined. 1035 Defined.
1036 End dec_star. 1036 End dec_star.