Mercurial > cpdt > repo

comparison src/StackMachine.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents 123f466faedc
children f7ac1e0c0d60
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
309 p : list instr 309 p : list instr
310 ============================ 310 ============================
311 progDenote ((IConst n :: nil) ++ p) s = 311 progDenote ((IConst n :: nil) ++ p) s =
312 progDenote p (expDenote (Const n) :: s) 312 progDenote p (expDenote (Const n) :: s)
313 313
314 ]] *) 314 ]]
315 *)
315 316
316 unfold expDenote. 317 unfold expDenote.
318
317 (** [[ 319 (** [[
318 n : nat 320 n : nat
319 s : stack 321 s : stack
320 p : list instr 322 p : list instr
321 ============================ 323 ============================
527 529
528 Check app_nil_end. 530 Check app_nil_end.
529 (** [[ 531 (** [[
530 app_nil_end 532 app_nil_end
531 : forall (A : Type) (l : list A), l = l ++ nil 533 : forall (A : Type) (l : list A), l = l ++ nil
532 ]] *) 534 ]]
535 *)
533 536
534 rewrite (app_nil_end (compile e)). 537 rewrite (app_nil_end (compile e)).
535 538
536 (** This time, we explicitly specify the value of the variable [l] from the theorem statement, since multiple expressions of list type appear in the conclusion. [rewrite] might choose the wrong place to rewrite if we did not specify which we want. 539 (** This time, we explicitly specify the value of the variable [l] from the theorem statement, since multiple expressions of list type appear in the conclusion. [rewrite] might choose the wrong place to rewrite if we did not specify which we want.
537 540
825 tconcat (tcompile arg2 e2 ts) 828 tconcat (tcompile arg2 e2 ts)
826 (tconcat (tcompile arg1 e1 (arg2 :: ts)) 829 (tconcat (tcompile arg1 e1 (arg2 :: ts))
827 (TCons (TIBinop ts b) (TNil (res :: ts)))) 830 (TCons (TIBinop ts b) (TNil (res :: ts))))
828 end 831 end
829 : forall t : type, texp t -> forall ts : tstack, tprog ts (t :: ts) 832 : forall t : type, texp t -> forall ts : tstack, tprog ts (t :: ts)
830 ]] *) 833 ]]
834 *)
831 835
832 836
833 (** We can check that the compiler generates programs that behave appropriately on our sample programs from above: *) 837 (** We can check that the compiler generates programs that behave appropriately on our sample programs from above: *)
834 838
835 Eval simpl in tprogDenote (tcompile (TNConst 42) nil) tt. 839 Eval simpl in tprogDenote (tcompile (TNConst 42) nil) tt.