Mercurial > cpdt > repo
comparison src/DataStruct.v @ 475:1fd4109f7b31
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 22 Oct 2012 14:23:52 -0400 |
| parents | 218361342cd2 |
| children | f02b698aadb1 |
comparison
equal
deleted
inserted
replaced
| 474:d9e1fb184672 | 475:1fd4109f7b31 |
|---|---|
| 309 match t with | 309 match t with |
| 310 | Unit => unit | 310 | Unit => unit |
| 311 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 | 311 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 |
| 312 end. | 312 end. |
| 313 | 313 |
| 314 (** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *) | 314 (** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply an [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *) |
| 315 | 315 |
| 316 (* EX: Define an interpreter for [exp]s. *) | 316 (* EX: Define an interpreter for [exp]s. *) |
| 317 | 317 |
| 318 (* begin thide *) | 318 (* begin thide *) |
| 319 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t := | 319 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t := |