comparison src/DataStruct.v @ 128:99be59b9e20d

s/itree/htree
author Adam Chlipala <adamc@hcoop.net>
date Mon, 20 Oct 2008 17:02:04 -0400
parents d176595cf46e
children fd52e2a7ffc3
comparison
equal deleted inserted replaced
127:0bfc75502498 128:99be59b9e20d
827 827
828 (** 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]. 828 (** 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].
829 829
830 %\begin{enumerate}%#<ol># 830 %\begin{enumerate}%#<ol>#
831 831
832 %\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 [itree] indexed by trees. The structure of an [itree] 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 [itree] by path. Define a function [itmap2] for "mapping over two trees in parallel." That is, [itmap2] takes in two [itree]s with the same index tree, and it forms a new [itree] with the same index by applying a binary function pointwise. 832 %\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.
833 833
834 Repeat this process so that you implement each definition for each of the three definition styles covered in this chapter: inductive, recursive, and reflexive.#</li># 834 Repeat this process so that you implement each definition for each of the three definition styles covered in this chapter: inductive, recursive, and reflexive.#</li>#
835 835
836 %\item%#<li># Write a dependently-typed interpreter for a simple programming language with ML-style pattern-matching. The language is defined informally by this grammar: 836 %\item%#<li># Write a dependently-typed interpreter for a simple programming language with ML-style pattern-matching. The language is defined informally by this grammar:
837 837