Mercurial > cpdt > repo
diff src/DataStruct.v @ 457:b1fead9f68f2
Proofreading pass through Chapter 11
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 28 Aug 2012 15:53:21 -0400 |
parents | df0a45de158a |
children | 218361342cd2 |
line wrap: on
line diff
--- a/src/DataStruct.v Tue Aug 28 11:48:06 2012 -0400 +++ b/src/DataStruct.v Tue Aug 28 15:53:21 2012 -0400 @@ -197,8 +197,8 @@ (* begin thide *) Inductive hlist : list A -> Type := - | MNil : hlist nil - | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). + | HNil : hlist nil + | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). (** 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.%\index{Gallina terms!member}% *) @@ -214,11 +214,11 @@ (** 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. - We can use [member] to adapt our definition of [get] to [hlist]s. 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. *) + We can use [member] to adapt our definition of [get] to [hlist]s. The same basic [match] tricks apply. In the [HCons] 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. *) Fixpoint hget ls (mls : hlist ls) : member ls -> B elm := match mls with - | MNil => fun mem => + | HNil => fun mem => match mem in member ls' return (match ls' with | nil => B elm | _ :: _ => unit @@ -226,7 +226,7 @@ | MFirst _ => tt | MNext _ _ _ => tt end - | MCons _ _ x mls' => fun mem => + | HCons _ _ x mls' => fun mem => match mem in member ls' return (match ls' with | nil => Empty_set | x' :: ls'' => @@ -241,8 +241,8 @@ End hlist. (* begin thide *) -Implicit Arguments MNil [A B]. -Implicit Arguments MCons [A B x ls]. +Implicit Arguments HNil [A B]. +Implicit Arguments HCons [A B x ls]. Implicit Arguments MFirst [A elm ls]. Implicit Arguments MNext [A elm x ls]. @@ -255,7 +255,7 @@ (* begin thide *) Example someValues : hlist (fun T : Set => T) someTypes := - MCons 5 (MCons true MNil). + HCons 5 (HCons true HNil). Eval simpl in hget someValues MFirst. (** %\vspace{-.15in}% [[ @@ -274,7 +274,7 @@ (** We can also build indexed lists of pairs in this way. *) Example somePairs : hlist (fun T : Set => T * T)%type someTypes := - MCons (1, 2) (MCons (true, false) MNil). + HCons (1, 2) (HCons (true, false) HNil). (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *) @@ -311,7 +311,7 @@ | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 end. -(** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [MCons] to extend the environment in the [Abs] case. *) +(** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *) (* EX: Define an interpreter for [exp]s. *) @@ -322,19 +322,19 @@ | Var _ _ mem => fun s => hget s mem | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s) - | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s) + | Abs _ _ _ e' => fun s => fun x => expDenote e' (HCons x s) end. (** Like for previous examples, our interpreter is easy to run with [simpl]. *) -Eval simpl in expDenote Const MNil. +Eval simpl in expDenote Const HNil. (** %\vspace{-.15in}% [[ = tt : typeDenote Unit ]] *) -Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil. +Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) HNil. (** %\vspace{-.15in}% [[ = fun x : unit => x : typeDenote (Arrow Unit Unit) @@ -342,21 +342,21 @@ *) Eval simpl in expDenote (Abs (dom := Unit) - (Abs (dom := Unit) (Var (MNext MFirst)))) MNil. + (Abs (dom := Unit) (Var (MNext MFirst)))) HNil. (** %\vspace{-.15in}% [[ = fun x _ : unit => x : typeDenote (Arrow Unit (Arrow Unit Unit)) ]] *) -Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil. +Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) HNil. (** %\vspace{-.15in}% [[ = fun _ x0 : unit => x0 : typeDenote (Arrow Unit (Arrow Unit Unit)) ]] *) -Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil. +Eval simpl in expDenote (App (Abs (Var MFirst)) Const) HNil. (** %\vspace{-.15in}% [[ = tt : typeDenote Unit