Mercurial > cpdt > repo
comparison src/MoreDep.v @ 296:559ec7328410
Spelling errors found preparing JFR paper
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 09 Dec 2010 14:39:49 -0500 |
parents | 1b6c81e51799 |
children | b441010125d4 |
comparison
equal
deleted
inserted
replaced
295:6833a1b778c0 | 296:559ec7328410 |
---|---|
162 End ilist. | 162 End ilist. |
163 | 163 |
164 | 164 |
165 (** * A Tagless Interpreter *) | 165 (** * A Tagless Interpreter *) |
166 | 166 |
167 (** A favorite example for motivating the power of functional programming is implementation of a simple expression language interpreter. In ML and Haskell, such interpreters are often implemented using an algebraic datatype of values, where at many points it is checked that a value was built with the right constructor of the value type. With dependent types, we can implement a %\textit{%#<i>#tagless#</i>#%}% interpreter that both removes this source of runtime ineffiency and gives us more confidence that our implementation is correct. *) | 167 (** A favorite example for motivating the power of functional programming is implementation of a simple expression language interpreter. In ML and Haskell, such interpreters are often implemented using an algebraic datatype of values, where at many points it is checked that a value was built with the right constructor of the value type. With dependent types, we can implement a %\textit{%#<i>#tagless#</i>#%}% interpreter that both removes this source of runtime inefficiency and gives us more confidence that our implementation is correct. *) |
168 | 168 |
169 Inductive type : Set := | 169 Inductive type : Set := |
170 | Nat : type | 170 | Nat : type |
171 | Bool : type | 171 | Bool : type |
172 | Prod : type -> type -> type. | 172 | Prod : type -> type -> type. |
582 match c with | 582 match c with |
583 | Red => rtree n | 583 | Red => rtree n |
584 | Black => { c' : color & rbtree c' n } | 584 | Black => { c' : color & rbtree c' n } |
585 end. | 585 end. |
586 | 586 |
587 (** That is, inserting into a tree with root color [c] and black depth [n], the variety of tree we get out depends on [c]. If we started with a red root, then we get back a possibly-invalid tree of depth [n]. If we started with a black root, we get back a valid tree of depth [n] with a root node of an arbitary color. | 587 (** That is, inserting into a tree with root color [c] and black depth [n], the variety of tree we get out depends on [c]. If we started with a red root, then we get back a possibly-invalid tree of depth [n]. If we started with a black root, we get back a valid tree of depth [n] with a root node of an arbitrary color. |
588 | 588 |
589 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *) | 589 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *) |
590 | 590 |
591 Fixpoint ins c n (t : rbtree c n) : insResult c n := | 591 Fixpoint ins c n (t : rbtree c n) : insResult c n := |
592 match t with | 592 match t with |
607 | Red => fun ins_b => balance2 ins_b y a | 607 | Red => fun ins_b => balance2 ins_b y a |
608 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >} | 608 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >} |
609 end (ins b) | 609 end (ins b) |
610 end. | 610 end. |
611 | 611 |
612 (** The one new trick is a variation of the convoy pattern. In each of the last two pattern matches, we want to take advantage of the typing connection between the trees [a] and [b]. We might naively apply the convoy pattern directly on [a] in the first [match] and on [b] in the second. This satisifies the type checker per se, but it does not satisfy the termination checker. Inside each [match], we would be calling [ins] recursively on a locally-bound variable. The termination checker is not smart enough to trace the dataflow into that variable, so the checker does not know that this recursive argument is smaller than the original argument. We make this fact clearer by applying the convoy pattern on %\textit{%#<i>#the result of a recursive call#</i>#%}%, rather than just on that call's argument. | 612 (** The one new trick is a variation of the convoy pattern. In each of the last two pattern matches, we want to take advantage of the typing connection between the trees [a] and [b]. We might naively apply the convoy pattern directly on [a] in the first [match] and on [b] in the second. This satisfies the type checker per se, but it does not satisfy the termination checker. Inside each [match], we would be calling [ins] recursively on a locally-bound variable. The termination checker is not smart enough to trace the dataflow into that variable, so the checker does not know that this recursive argument is smaller than the original argument. We make this fact clearer by applying the convoy pattern on %\textit{%#<i>#the result of a recursive call#</i>#%}%, rather than just on that call's argument. |
613 | 613 |
614 Finally, we are in the home stretch of our effort to define [insert]. We just need a few more definitions of non-recursive functions. First, we need to give the final characterization of [insert]'s return type. Inserting into a red-rooted tree gives a black-rooted tree where black depth has increased, and inserting into a black-rooted tree gives a tree where black depth has stayed the same and where the root is an arbitrary color. *) | 614 Finally, we are in the home stretch of our effort to define [insert]. We just need a few more definitions of non-recursive functions. First, we need to give the final characterization of [insert]'s return type. Inserting into a red-rooted tree gives a black-rooted tree where black depth has increased, and inserting into a black-rooted tree gives a tree where black depth has stayed the same and where the root is an arbitrary color. *) |
615 | 615 |
616 Definition insertResult c n := | 616 Definition insertResult c n := |
617 match c with | 617 match c with |
795 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2), | 795 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2), |
796 regexp (fun s => P1 s \/ P2 s) | 796 regexp (fun s => P1 s \/ P2 s) |
797 | Star : forall P (r : regexp P), | 797 | Star : forall P (r : regexp P), |
798 regexp (star P). | 798 regexp (star P). |
799 | 799 |
800 (** Many theorems about strings are useful for implementing a certified regexp matcher, and few of them are in the [Strings] library. The book source includes statements, proofs, and hint commands for a handful of such omittted theorems. Since they are orthogonal to our use of dependent types, we hide them in the rendered versions of this book. *) | 800 (** Many theorems about strings are useful for implementing a certified regexp matcher, and few of them are in the [Strings] library. The book source includes statements, proofs, and hint commands for a handful of such omitted theorems. Since they are orthogonal to our use of dependent types, we hide them in the rendered versions of this book. *) |
801 | 801 |
802 (* begin hide *) | 802 (* begin hide *) |
803 Open Scope specif_scope. | 803 Open Scope specif_scope. |
804 | 804 |
805 Lemma length_emp : length "" <= 0. | 805 Lemma length_emp : length "" <= 0. |