Mercurial > cpdt > repo

comparison src/Generic.v @ 504:04177dd1b133

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Chapter 11
author Adam Chlipala <adam@chlipala.net>
date Sat, 09 Feb 2013 10:45:21 -0500
parents 31258618ef73
children ed829eaa91b2
comparison
equal deleted inserted replaced
503:929c12a95b87 504:04177dd1b133
85 (** Finally, the evidence for type [T] is a %\index{Gallina terms!hlist}%heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *) 85 (** Finally, the evidence for type [T] is a %\index{Gallina terms!hlist}%heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *)
86 86
87 End denote. 87 End denote.
88 (* end thide *) 88 (* end thide *)
89 89
90 (** Some example pieces of evidence should help clarify the convention. First, we define some helpful notations, providing different ways of writing constructor denotations. There is really just one notation, but we need several versions of it to cover different choices of which variables will be used in the body of a definition. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *) 90 (** Some example pieces of evidence should help clarify the convention. First, we define a helpful notation for constructor denotations. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *)
91 91
92 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
93 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
94 Notation "[ ! , r ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ _)).
95 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)). 92 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)).
96 93
97 (* begin thide *) 94 (* begin thide *)
98 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := 95 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
99 HNil. 96 HNil.
100 Definition unit_den : datatypeDenote unit unit_dt := 97 Definition unit_den : datatypeDenote unit unit_dt :=
101 [!, ! ~> tt] ::: HNil. 98 [_, _ ~> tt] ::: HNil.
102 Definition bool_den : datatypeDenote bool bool_dt := 99 Definition bool_den : datatypeDenote bool bool_dt :=
103 [!, ! ~> true] ::: [!, ! ~> false] ::: HNil. 100 [_, _ ~> true] ::: [_, _ ~> false] ::: HNil.
104 Definition nat_den : datatypeDenote nat nat_dt := 101 Definition nat_den : datatypeDenote nat nat_dt :=
105 [!, ! ~> O] ::: [!, r ~> S (hd r)] ::: HNil. 102 [_, _ ~> O] ::: [_, r ~> S (hd r)] ::: HNil.
106 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := 103 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
107 [!, ! ~> nil] ::: [x, r ~> x :: hd r] ::: HNil. 104 [_, _ ~> nil] ::: [x, r ~> x :: hd r] ::: HNil.
108 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := 105 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
109 [v, ! ~> Leaf v] ::: [!, r ~> Node (hd r) (hd (tl r))] ::: HNil. 106 [v, _ ~> Leaf v] ::: [_, r ~> Node (hd r) (hd (tl r))] ::: HNil.
110 (* end thide *) 107 (* end thide *)
111 108
112 (** Recall that the [hd] and [tl] calls above operate on richly typed lists, where type indices tell us the lengths of lists, guaranteeing the safety of operations like [hd]. The type annotation attached to each definition provides enough information for Coq to infer list lengths at appropriate points. *) 109 (** Recall that the [hd] and [tl] calls above operate on richly typed lists, where type indices tell us the lengths of lists, guaranteeing the safety of operations like [hd]. The type annotation attached to each definition provides enough information for Coq to infer list lengths at appropriate points. *)
113 110
114 111