Mercurial > cpdt > repo
comparison src/DataStruct.v @ 130:464db50b210a
Clarify intent to use hlist
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 22 Oct 2008 09:43:37 -0400 |
| parents | fd52e2a7ffc3 |
| children | cbf2f74a5130 |
comparison
equal
deleted
inserted
replaced
| 129:fd52e2a7ffc3 | 130:464db50b210a |
|---|---|
| 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 [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. | 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 index function.#</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 index function.#</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, using one of the encodings of heterogeneous lists to represent the different branches of a [case] expression. (There are other ways to represent the same thing, but the point of this exercise is to practice using those heterogeneous list types.) The object language is defined informally by this grammar: |
| 837 | 837 |
| 838 [[ | 838 [[ |
| 839 t ::= bool | t + t | 839 t ::= bool | t + t |
| 840 p ::= x | b | inl p | inr p | 840 p ::= x | b | inl p | inr p |
| 841 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e | 841 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e |