comparison src/DataStruct.v @ 455:df0a45de158a

Proofreading pass through Chapter 9
author Adam Chlipala <adam@chlipala.net>
date Mon, 27 Aug 2012 17:51:15 -0400
parents 97c60ffdb998
children b1fead9f68f2
comparison
equal deleted inserted replaced
454:49bd155dfc52 455:df0a45de158a
281 (* end thide *) 281 (* end thide *)
282 282
283 283
284 (** ** A Lambda Calculus Interpreter *) 284 (** ** A Lambda Calculus Interpreter *)
285 285
286 (** Heterogeneous lists are very useful in implementing %\index{interpreters}%interpreters for functional programming languages. Using the types and operations we have already defined, it is trivial to write an interpreter for simply typed lambda calculus%\index{lambda calculus}%. Our interpreter can alternatively be thought of as a denotational semantics. 286 (** Heterogeneous lists are very useful in implementing %\index{interpreters}%interpreters for functional programming languages. Using the types and operations we have already defined, it is trivial to write an interpreter for simply typed lambda calculus%\index{lambda calculus}%. Our interpreter can alternatively be thought of as a denotational semantics (but worry not if you are not familiar with such terminology from semantics).
287 287
288 We start with an algebraic datatype for types. *) 288 We start with an algebraic datatype for types. *)
289 289
290 Inductive type : Set := 290 Inductive type : Set :=
291 | Unit : type 291 | Unit : type
432 match ls with 432 match ls with
433 | nil => Empty_set 433 | nil => Empty_set
434 | x :: ls' => (x = elm) + fmember ls' 434 | x :: ls' => (x = elm) + fmember ls'
435 end%type. 435 end%type.
436 436
437 (** The definition of [fmember] follows the definition of [ffin]. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that with a sum type whose left branch is the appropriate equality proposition. Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type]. 437 (** The definition of [fmember] follows the definition of [ffin]. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that idea with a sum type whose left branch is the appropriate equality proposition. Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
438 438
439 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s. 439 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
440 [[ 440 [[
441 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm := 441 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
442 match ls with 442 match ls with
479 (* end thide *) 479 (* end thide *)
480 480
481 End fhlist. 481 End fhlist.
482 482
483 Implicit Arguments fhget [A B elm ls]. 483 Implicit Arguments fhget [A B elm ls].
484
485 (** How does one choose between the two data structure encoding strategies we have presented so far? Before answering that question in this chapter's final section, we introduce one further approach. *)
484 486
485 487
486 (** * Data Structures as Index Functions *) 488 (** * Data Structures as Index Functions *)
487 489
488 (** %\index{index function}%Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor. *) 490 (** %\index{index function}%Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor. *)
788 Implicit Arguments cfoldCond [t n]. 790 Implicit Arguments cfoldCond [t n].
789 (* end thide *) 791 (* end thide *)
790 792
791 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *) 793 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
792 794
795 (* begin thide *)
793 Fixpoint cfold t (e : exp' t) : exp' t := 796 Fixpoint cfold t (e : exp' t) : exp' t :=
794 match e with 797 match e with
795 | NConst n => NConst n 798 | NConst n => NConst n
796 | Plus e1 e2 => 799 | Plus e1 e2 =>
797 let e1' := cfold e1 in 800 let e1' := cfold e1 in
808 | _, _ => Eq e1' e2' 811 | _, _ => Eq e1' e2'
809 end 812 end
810 813
811 | BConst b => BConst b 814 | BConst b => BConst b
812 | Cond _ _ tests bodies default => 815 | Cond _ _ tests bodies default =>
813 (* begin thide *)
814 cfoldCond 816 cfoldCond
815 (cfold default) 817 (cfold default)
816 (fun idx => cfold (tests idx)) 818 (fun idx => cfold (tests idx))
817 (fun idx => cfold (bodies idx)) 819 (fun idx => cfold (bodies idx))
818 (* end thide *) 820 end.
819 end. 821 (* end thide *)
820 822
821 (* begin thide *) 823 (* begin thide *)
822 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. This lemma formalizes that property. The proof is a standard mostly automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *) 824 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. The following lemma formalizes that property. The proof is a standard mostly automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *)
823 825
824 Lemma cfoldCond_correct : forall t (default : exp' t) 826 Lemma cfoldCond_correct : forall t (default : exp' t)
825 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t), 827 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
826 exp'Denote (cfoldCond default tests bodies) 828 exp'Denote (cfoldCond default tests bodies)
827 = exp'Denote (Cond n tests bodies default). 829 = exp'Denote (Cond n tests bodies default).