Mercurial > cpdt > repo
comparison src/StackMachine.v @ 273:a636eda02176
Typo pointed out by Ben Moseley
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 15 May 2010 06:42:05 -0400 |
| parents | 191a66cd7cb5 |
| children | a57e75752c80 |
comparison
equal
deleted
inserted
replaced
| 272:19fbda8a8117 | 273:a636eda02176 |
|---|---|
| 616 | TLt => lt | 616 | TLt => lt |
| 617 end. | 617 end. |
| 618 | 618 |
| 619 (** This function has just a few differences from the denotation functions we saw earlier. First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote]. Second, we need to perform a genuine %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks. In each branch of the [match], we need to use branch-specific information about the indices to [tbinop]. General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match]. | 619 (** This function has just a few differences from the denotation functions we saw earlier. First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote]. Second, we need to perform a genuine %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks. In each branch of the [match], we need to use branch-specific information about the indices to [tbinop]. General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match]. |
| 620 | 620 |
| 621 The [in] annotation restates the type of the term being case-analyzed. Though we use the same names for the indices as we use in the type of the original argument binder, these are actually fresh variables, and they are %\textit{%#<i>#binding occurrences#</i>#%}%. Their scope is the [return] clause. That is, [arg1], [arg2], and [arg3] are new bound variables bound only within the return clause [typeDenote arg1 -> typeDenote arg2 -> typeDenote res]. By being explicit about the functional relationship between the type indices and the match result, we regain decidable type inference. | 621 The [in] annotation restates the type of the term being case-analyzed. Though we use the same names for the indices as we use in the type of the original argument binder, these are actually fresh variables, and they are %\textit{%#<i>#binding occurrences#</i>#%}%. Their scope is the [return] clause. That is, [arg1], [arg2], and [res] are new bound variables bound only within the return clause [typeDenote arg1 -> typeDenote arg2 -> typeDenote res]. By being explicit about the functional relationship between the type indices and the match result, we regain decidable type inference. |
| 622 | 622 |
| 623 In fact, recent Coq versions use some heuristics that can save us the trouble of writing [match] annotations, and those heuristics get the job done in this case. We can get away with writing just: *) | 623 In fact, recent Coq versions use some heuristics that can save us the trouble of writing [match] annotations, and those heuristics get the job done in this case. We can get away with writing just: *) |
| 624 | 624 |
| 625 (* begin hide *) | 625 (* begin hide *) |
| 626 Reset tbinopDenote. | 626 Reset tbinopDenote. |