Mercurial > cpdt > repo
comparison src/MoreDep.v @ 417:539ed97750bb
Update for Coq trunk version intended for final 8.4 release
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 17 Jul 2012 16:37:58 -0400 |
| parents | ded318830bb0 |
| children | 6ed5ee4845e4 |
comparison
equal
deleted
inserted
replaced
| 416:ded318830bb0 | 417:539ed97750bb |
|---|---|
| 278 end. | 278 end. |
| 279 (* end thide *) | 279 (* end thide *) |
| 280 | 280 |
| 281 (** 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%\index{Hindley-Milner}%, but is similar to what goes on with Haskell type classes%\index{type classes}%. | 281 (** 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%\index{Hindley-Milner}%, but is similar to what goes on with Haskell type classes%\index{type classes}%. |
| 282 | 282 |
| 283 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. In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference off by writing [return _]. *) | 283 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. In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference with explicit [return] clauses. *) |
| 284 | 284 |
| 285 Fixpoint cfold t (e : exp t) : exp t := | 285 Fixpoint cfold t (e : exp t) : exp t := |
| 286 match e with | 286 match e with |
| 287 | NConst n => NConst n | 287 | NConst n => NConst n |
| 288 | Plus e1 e2 => | 288 | Plus e1 e2 => |
| 289 let e1' := cfold e1 in | 289 let e1' := cfold e1 in |
| 290 let e2' := cfold e2 in | 290 let e2' := cfold e2 in |
| 291 match e1', e2' return _ with | 291 match e1', e2' return exp Nat with |
| 292 | NConst n1, NConst n2 => NConst (n1 + n2) | 292 | NConst n1, NConst n2 => NConst (n1 + n2) |
| 293 | _, _ => Plus e1' e2' | 293 | _, _ => Plus e1' e2' |
| 294 end | 294 end |
| 295 | Eq e1 e2 => | 295 | Eq e1 e2 => |
| 296 let e1' := cfold e1 in | 296 let e1' := cfold e1 in |
| 297 let e2' := cfold e2 in | 297 let e2' := cfold e2 in |
| 298 match e1', e2' return _ with | 298 match e1', e2' return exp Bool with |
| 299 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) | 299 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) |
| 300 | _, _ => Eq e1' e2' | 300 | _, _ => Eq e1' e2' |
| 301 end | 301 end |
| 302 | 302 |
| 303 | BConst b => BConst b | 303 | BConst b => BConst b |
| 304 | And e1 e2 => | 304 | And e1 e2 => |
| 305 let e1' := cfold e1 in | 305 let e1' := cfold e1 in |
| 306 let e2' := cfold e2 in | 306 let e2' := cfold e2 in |
| 307 match e1', e2' return _ with | 307 match e1', e2' return exp Bool with |
| 308 | BConst b1, BConst b2 => BConst (b1 && b2) | 308 | BConst b1, BConst b2 => BConst (b1 && b2) |
| 309 | _, _ => And e1' e2' | 309 | _, _ => And e1' e2' |
| 310 end | 310 end |
| 311 | If _ e e1 e2 => | 311 | If _ e e1 e2 => |
| 312 let e' := cfold e in | 312 let e' := cfold e in |