Mercurial > cpdt > repo
comparison src/DataStruct.v @ 569:0ce9829efa3b
Back to working in Coq 8.4
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Jan 2019 15:28:23 -0500 |
parents | 81d63d9c1cc5 |
children | a913f19955e2 |
comparison
equal
deleted
inserted
replaced
568:81d63d9c1cc5 | 569:0ce9829efa3b |
---|---|
241 (* end thide *) | 241 (* end thide *) |
242 End hlist. | 242 End hlist. |
243 | 243 |
244 (* begin thide *) | 244 (* begin thide *) |
245 Arguments HNil [A B]. | 245 Arguments HNil [A B]. |
246 Arguments HCons [A B x ls]. | 246 Arguments HCons [A B x ls] _ _. |
247 | 247 |
248 Arguments HFirst [A elm ls]. | 248 Arguments HFirst [A elm ls]. |
249 Arguments HNext [A elm x ls]. | 249 Arguments HNext [A elm x ls] _. |
250 (* end thide *) | 250 (* end thide *) |
251 | 251 |
252 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *) | 252 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *) |
253 | 253 |
254 Definition someTypes : list Set := nat :: bool :: nil. | 254 Definition someTypes : list Set := nat :: bool :: nil. |
479 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *) | 479 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *) |
480 (* end thide *) | 480 (* end thide *) |
481 | 481 |
482 End fhlist. | 482 End fhlist. |
483 | 483 |
484 Arguments fhget [A B elm ls]. | 484 Arguments fhget [A B elm ls] _ _. |
485 | 485 |
486 (** 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. *) | 486 (** 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. *) |
487 | 487 |
488 | 488 |
489 (** * Data Structures as Index Functions *) | 489 (** * Data Structures as Index Functions *) |
590 | 590 |
591 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [ffin n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *) | 591 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [ffin n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *) |
592 | 592 |
593 End tree. | 593 End tree. |
594 | 594 |
595 Arguments Node [A n]. | 595 Arguments Node [A n] _. |
596 | 596 |
597 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *) | 597 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *) |
598 | 598 |
599 Section rifoldr. | 599 Section rifoldr. |
600 Variables A B : Set. | 600 Variables A B : Set. |
606 | O => fun _ => i | 606 | O => fun _ => i |
607 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx))) | 607 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx))) |
608 end. | 608 end. |
609 End rifoldr. | 609 End rifoldr. |
610 | 610 |
611 Arguments rifoldr [A B] f i [n]. | 611 Arguments rifoldr [A B] f i [n] _. |
612 | 612 |
613 Fixpoint sum (t : tree nat) : nat := | 613 Fixpoint sum (t : tree nat) : nat := |
614 match t with | 614 match t with |
615 | Leaf n => n | 615 | Leaf n => n |
616 | Node _ f => rifoldr plus O (fun idx => sum (f idx)) | 616 | Node _ f => rifoldr plus O (fun idx => sum (f idx)) |
706 (fun idx => tests (Some idx)) | 706 (fun idx => tests (Some idx)) |
707 (fun idx => bodies (Some idx)) | 707 (fun idx => bodies (Some idx)) |
708 end. | 708 end. |
709 End cond. | 709 End cond. |
710 | 710 |
711 Arguments cond [A] default [n]. | 711 Arguments cond [A] default [n] _ _. |
712 (* end thide *) | 712 (* end thide *) |
713 | 713 |
714 (** Now the expression interpreter is straightforward to write. *) | 714 (** Now the expression interpreter is straightforward to write. *) |
715 | 715 |
716 (* begin thide *) | 716 (* begin thide *) |
795 end (bodies None) | 795 end (bodies None) |
796 end | 796 end |
797 end. | 797 end. |
798 End cfoldCond. | 798 End cfoldCond. |
799 | 799 |
800 Arguments cfoldCond [t] default [n]. | 800 Arguments cfoldCond [t] default [n] _ _. |
801 (* end thide *) | 801 (* end thide *) |
802 | 802 |
803 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *) | 803 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *) |
804 | 804 |
805 (* begin thide *) | 805 (* begin thide *) |