Mercurial > cpdt > repo

comparison src/DataStruct.v @ 107:924d77a177e8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hlist and hget
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 12:35:48 -0400
parents 1d2746eae1a6
children 7abf5535baab
comparison
equal deleted inserted replaced
106:1d2746eae1a6 107:924d77a177e8
113 end. 113 end.
114 End ilist. 114 End ilist.
115 115
116 Implicit Arguments Nil [A]. 116 Implicit Arguments Nil [A].
117 117
118 (** Our [get] function is quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *)
119
118 Section ilist_map. 120 Section ilist_map.
119 Variables A B : Set. 121 Variables A B : Set.
120 Variable f : A -> B. 122 Variable f : A -> B.
121 123
122 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n := 124 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
123 match ls in ilist _ n return ilist B n with 125 match ls in ilist _ n return ilist B n with
124 | Nil => Nil 126 | Nil => Nil
125 | Cons _ x ls' => Cons (f x) (imap ls') 127 | Cons _ x ls' => Cons (f x) (imap ls')
126 end. 128 end.
127 129
128 Theorem get_imap : forall n (ls : ilist A n) (idx : index n), 130 (** It is easy to prove that [get] "distributes over" [imap] calls. The only tricky bit is remembering to use the [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
131
132 Theorem get_imap : forall n (idx : index n) (ls : ilist A n),
129 get (imap ls) idx = f (get ls idx). 133 get (imap ls) idx = f (get ls idx).
130 induction ls; crush; 134 induction ls; dep_destruct idx; crush.
131 match goal with
132 | [ |- context[match ?IDX with First _ => _ | Next _ _ => _ end] ] =>
133 dep_destruct IDX; crush
134 end.
135 Qed. 135 Qed.
136 End ilist_map. 136 End ilist_map.
137
138
139 (** * Heterogeneous Lists *)
140
141 (** Programmers who move to statically-typed functional languages from "scripting languages" often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a "type-level" list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and it we can do it much more cleanly and directly in Coq. *)
142
143 Section hlist.
144 Variable A : Type.
145 Variable B : A -> Type.
146
147 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
148
149 Inductive hlist : list A -> Type :=
150 | MNil : hlist nil
151 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
152
153 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to. *)
154
155 Variable elm : A.
156
157 Inductive member : list A -> Type :=
158 | MFirst : forall ls, member (elm :: ls)
159 | MNext : forall x ls, member ls -> member (x :: ls).
160
161 (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable. In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too. The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
162
163 We can use [member] to adapt our definition of [get] to [hlists]. The same basic [match] tricks apply. In the [MCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match]. We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
164
165 Fixpoint hget ls (mls : hlist ls) {struct mls} : member ls -> B elm :=
166 match mls in hlist ls return member ls -> B elm with
167 | MNil => fun mem =>
168 match mem in member ls' return (match ls' with
169 | nil => B elm
170 | _ :: _ => unit
171 end) with
172 | MFirst _ => tt
173 | MNext _ _ _ => tt
174 end
175 | MCons _ _ x mls' => fun mem =>
176 match mem in member ls' return (match ls' with
177 | nil => Empty_set
178 | x' :: ls'' =>
179 B x' -> (member ls'' -> B elm) -> B elm
180 end) with
181 | MFirst _ => fun x _ => x
182 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
183 end x (hget mls')
184 end.
185 End hlist.