Mercurial > cpdt > repo
comparison src/DataStruct.v @ 216:d1464997078d
Switch DepList to inductive, not recursive, types
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 11 Nov 2009 14:28:47 -0500 |
| parents | f8bcd33bdd91 |
| children | 6601384e7e14 |
comparison
equal
deleted
inserted
replaced
| 215:f8bcd33bdd91 | 216:d1464997078d |
|---|---|
| 839 | 839 |
| 840 (** * Exercises *) | 840 (** * Exercises *) |
| 841 | 841 |
| 842 (** remove printing * *) | 842 (** remove printing * *) |
| 843 | 843 |
| 844 (** Some of the type family definitions from this chapter are duplicated in the [DepList] module of the book source. Only the recursive versions of length-indexed and heterogeneous lists are included, and they are renamed without the [f] prefixes, e.g., [ilist] in place of [filist]. | 844 (** Some of the type family definitions and associated functions from this chapter are duplicated in the [DepList] module of the book source. Some of their names have been changed to be more sensible in a general context. |
| 845 | 845 |
| 846 %\begin{enumerate}%#<ol># | 846 %\begin{enumerate}%#<ol># |
| 847 | 847 |
| 848 %\item%#<li># Define a tree analogue of [hlist]. That is, define a parameterized type of binary trees with data at their leaves, and define a type family [htree] indexed by trees. The structure of an [htree] mirrors its index tree, with the type of each data element (which only occur at leaves) determined by applying a type function to the corresponding element of the index tree. Define a type standing for all possible paths from the root of a tree to leaves and use it to implement a function [tget] for extracting an element of an [htree] by path. Define a function [htmap2] for "mapping over two trees in parallel." That is, [htmap2] takes in two [htree]s with the same index tree, and it forms a new [htree] with the same index by applying a binary function pointwise. | 848 %\item%#<li># Define a tree analogue of [hlist]. That is, define a parameterized type of binary trees with data at their leaves, and define a type family [htree] indexed by trees. The structure of an [htree] mirrors its index tree, with the type of each data element (which only occur at leaves) determined by applying a type function to the corresponding element of the index tree. Define a type standing for all possible paths from the root of a tree to leaves and use it to implement a function [tget] for extracting an element of an [htree] by path. Define a function [htmap2] for "mapping over two trees in parallel." That is, [htmap2] takes in two [htree]s with the same index tree, and it forms a new [htree] with the same index by applying a binary function pointwise. |
| 849 | 849 |