Certified Programming with Dependent Types: src/MoreDep.v comparison

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

-:6833a1b778c0
+:559ec7328410
 End ilist.
 (** * A Tagless Interpreter *)
-(** 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. *)
+(** 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. *)
 Inductive type : Set :=
 | Nat : type
 | Bool : type
 | Prod : type -> type -> type.
 match c with
 | Red => rtree n
 | Black => { c' : color & rbtree c' n }
 end.
-(** 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.
+(** 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.
 Here is the definition of [ins].  Again, we do not want to dwell on the functional details. *)
 Fixpoint ins c n (t : rbtree c n) : insResult c n :=
 match t with
 | Red => fun ins_b => balance2 ins_b y a
 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
 end (ins b)
 end.
-(** 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.
+(** 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.
 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. *)
 Definition insertResult c n :=
 match c with
 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
 regexp (fun s => P1 s \/ P2 s)
 | Star : forall P (r : regexp P),
 regexp (star P).
-(** 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. *)
+(** 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. *)
 (* begin hide *)
 Open Scope specif_scope.
 Lemma length_emp : length "" <= 0.

Mercurial > cpdt > repo

comparison src/MoreDep.v @ 296:559ec7328410