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