Mercurial > cpdt > repo

comparison src/StackMachine.v @ 439:393b8ed99c2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of improvements to vertical spacing, up through end of InductiveTypes
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 Jul 2012 13:21:36 -0400
parents 686cf945dd02
children 89c67796754e
comparison
equal deleted inserted replaced
438:f1f779c6a232 439:393b8ed99c2f
211 211
212 induction e. 212 induction e.
213 213
214 (** We declare that this proof will proceed by induction on the structure of the expression [e]. This swaps out our initial subgoal for two new subgoals, one for each case of the inductive proof: 214 (** We declare that this proof will proceed by induction on the structure of the expression [e]. This swaps out our initial subgoal for two new subgoals, one for each case of the inductive proof:
215 215
216 %\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt># 216 [[
217 217 2 subgoals
218 [[ 218
219 n : nat 219 n : nat
220 ============================ 220 ============================
221 forall (s : stack) (p : list instr), 221 forall (s : stack) (p : list instr),
222 progDenote (compile (Const n) ++ p) s = 222 progDenote (compile (Const n) ++ p) s =
223 progDenote p (expDenote (Const n) :: s) 223 progDenote p (expDenote (Const n) :: s)
224 ]] 224
225 %\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt># 225 subgoal 2 is
226 [[ 226
227 forall (s : stack) (p : list instr), 227 forall (s : stack) (p : list instr),
228 progDenote (compile (Binop b e1 e2) ++ p) s = 228 progDenote (compile (Binop b e1 e2) ++ p) s =
229 progDenote p (expDenote (Binop b e1 e2) :: s) 229 progDenote p (expDenote (Binop b e1 e2) :: s)
230 230
231 ]] 231 ]]
386 ]] 386 ]]
387 387
388 What we need is the associative law of list concatenation, which is available as a theorem [app_assoc_reverse] in the standard library.%\index{Vernacular commands!Check}% *) 388 What we need is the associative law of list concatenation, which is available as a theorem [app_assoc_reverse] in the standard library.%\index{Vernacular commands!Check}% *)
389 389
390 Check app_assoc. 390 Check app_assoc.
391 391 (** %\vspace{-.15in}%[[
392 (** [[
393 app_assoc_reverse 392 app_assoc_reverse
394 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n 393 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
395 394
396 ]] 395 ]]
397 396
398 If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) 397 If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *)
399 398
400 SearchRewrite ((_ ++ _) ++ _). 399 SearchRewrite ((_ ++ _) ++ _).
401 (** [[ 400 (** %\vspace{-.15in}%[[
402 app_assoc_reverse: 401 app_assoc_reverse:
403 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n 402 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
404 ]] 403 ]]
405 %\vspace{-.25in}% 404 %\vspace{-.25in}%
406 [[ 405 [[
410 409
411 We use [app_assoc_reverse] to perform a rewrite: %\index{tactics!rewrite}% *) 410 We use [app_assoc_reverse] to perform a rewrite: %\index{tactics!rewrite}% *)
412 411
413 rewrite app_assoc_reverse. 412 rewrite app_assoc_reverse.
414 413
415 (** changing the conclusion to: 414 (** %\noindent{}%changing the conclusion to:
416 415
417 [[ 416 [[
418 progDenote (compile e2 ++ (compile e1 ++ iBinop b :: nil) ++ p) s = 417 progDenote (compile e2 ++ (compile e1 ++ iBinop b :: nil) ++ p) s =
419 progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) 418 progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
420 419
723 (** One interesting feature of the definition is the underscores appearing to the right of [=>] arrows. Haskell and ML programmers are quite familiar with compilers that infer type parameters to polymorphic values. In Coq, it is possible to go even further and ask the system to infer arbitrary terms, by writing underscores in place of specific values. You may have noticed that we have been calling functions without specifying all of their arguments. For instance, the recursive calls here to [tcompile] omit the [t] argument. Coq's _implicit argument_ mechanism automatically inserts underscores for arguments that it will probably be able to infer. Inference of such values is far from complete, though; generally, it only works in cases similar to those encountered with polymorphic type instantiation in Haskell and ML. 722 (** One interesting feature of the definition is the underscores appearing to the right of [=>] arrows. Haskell and ML programmers are quite familiar with compilers that infer type parameters to polymorphic values. In Coq, it is possible to go even further and ask the system to infer arbitrary terms, by writing underscores in place of specific values. You may have noticed that we have been calling functions without specifying all of their arguments. For instance, the recursive calls here to [tcompile] omit the [t] argument. Coq's _implicit argument_ mechanism automatically inserts underscores for arguments that it will probably be able to infer. Inference of such values is far from complete, though; generally, it only works in cases similar to those encountered with polymorphic type instantiation in Haskell and ML.
724 723
725 The underscores here are being filled in with stack types. That is, the Coq type inferencer is, in a sense, inferring something about the flow of control in the translated programs. We can take a look at exactly which values are filled in: *) 724 The underscores here are being filled in with stack types. That is, the Coq type inferencer is, in a sense, inferring something about the flow of control in the translated programs. We can take a look at exactly which values are filled in: *)
726 725
727 Print tcompile. 726 Print tcompile.
728 (** [[ 727 (** %\vspace{-.15in}%[[
729 tcompile = 728 tcompile =
730 fix tcompile (t : type) (e : texp t) (ts : tstack) {struct e} : 729 fix tcompile (t : type) (e : texp t) (ts : tstack) {struct e} :
731 tprog ts (t :: ts) := 730 tprog ts (t :: ts) :=
732 match e in (texp t0) return (tprog ts (t0 :: ts)) with 731 match e in (texp t0) return (tprog ts (t0 :: ts)) with
733 | TNConst n => TCons (TiNConst ts n) (TNil (Nat :: ts)) 732 | TNConst n => TCons (TiNConst ts n) (TNil (Nat :: ts))