Mercurial > cpdt > repo

annotate book/src/StackMachine.v @ 3:9fea5674367c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pretty LaTeX generation
author Adam Chlipala <adamc@hcoop.net>
date Fri, 29 Aug 2008 14:24:38 -0400
parents book/StackMachine.v@b3f7de74d38f
children f913d32a49e4
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 *
adamc@2 3 * This work is licensed under a
adamc@2 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2 5 * Unported License.
adamc@2 6 * The license text is available at:
adamc@2 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2 8 *)
adamc@2 9
adamc@3 10 (* begin hide *)
adamc@2 11 Require Import List.
adamc@2 12
adamc@2 13 Require Import Tactics.
adamc@3 14 (* end hide *)
adamc@2 15
adamc@2 16
adamc@2 17 (** * Arithmetic expressions over natural numbers *)
adamc@2 18
adamc@3 19 (* begin hide *)
adamc@2 20 Module Nat.
adamc@3 21 (* end hide *)
adamc@2 22 (** ** Source language *)
adamc@2 23
adamc@2 24 Inductive binop : Set := Plus | Times.
adamc@2 25
adamc@2 26 Inductive exp : Set :=
adamc@2 27 | Const : nat -> exp
adamc@2 28 | Binop : binop -> exp -> exp -> exp.
adamc@2 29
adamc@2 30 Definition binopDenote (b : binop) : nat -> nat -> nat :=
adamc@2 31 match b with
adamc@2 32 | Plus => plus
adamc@2 33 | Times => mult
adamc@2 34 end.
adamc@2 35
adamc@2 36 Fixpoint expDenote (e : exp) : nat :=
adamc@2 37 match e with
adamc@2 38 | Const n => n
adamc@2 39 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
adamc@2 40 end.
adamc@2 41
adamc@2 42
adamc@2 43 (** ** Target language *)
adamc@2 44
adamc@2 45 Inductive instr : Set :=
adamc@2 46 | IConst : nat -> instr
adamc@2 47 | IBinop : binop -> instr.
adamc@2 48
adamc@2 49 Definition prog := list instr.
adamc@2 50 Definition stack := list nat.
adamc@2 51
adamc@2 52 Definition instrDenote (i : instr) (s : stack) : option stack :=
adamc@2 53 match i with
adamc@2 54 | IConst n => Some (n :: s)
adamc@2 55 | IBinop b =>
adamc@2 56 match s with
adamc@2 57 | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
adamc@2 58 | _ => None
adamc@2 59 end
adamc@2 60 end.
adamc@2 61
adamc@2 62 Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack :=
adamc@2 63 match p with
adamc@2 64 | nil => Some s
adamc@2 65 | i :: p' =>
adamc@2 66 match instrDenote i s with
adamc@2 67 | None => None
adamc@2 68 | Some s' => progDenote p' s'
adamc@2 69 end
adamc@2 70 end.
adamc@2 71
adamc@2 72
adamc@2 73 (** ** Translation *)
adamc@2 74
adamc@2 75 Fixpoint compile (e : exp) : prog :=
adamc@2 76 match e with
adamc@2 77 | Const n => IConst n :: nil
adamc@2 78 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil
adamc@2 79 end.
adamc@2 80
adamc@2 81
adamc@2 82 (** ** Translation correctness *)
adamc@2 83
adamc@2 84 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
adamc@2 85 progDenote p (expDenote e :: s).
adamc@2 86 induction e.
adamc@2 87
adamc@2 88 intros.
adamc@2 89 unfold compile.
adamc@2 90 unfold expDenote.
adamc@2 91 simpl.
adamc@2 92 reflexivity.
adamc@2 93
adamc@2 94 intros.
adamc@2 95 unfold compile.
adamc@2 96 fold compile.
adamc@2 97 unfold expDenote.
adamc@2 98 fold expDenote.
adamc@2 99 rewrite app_ass.
adamc@2 100 rewrite IHe2.
adamc@2 101 rewrite app_ass.
adamc@2 102 rewrite IHe1.
adamc@2 103 simpl.
adamc@2 104 reflexivity.
adamc@2 105 Abort.
adamc@2 106
adamc@2 107 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
adamc@2 108 progDenote p (expDenote e :: s).
adamc@2 109 induction e; crush.
adamc@2 110 Qed.
adamc@2 111
adamc@2 112 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
adamc@2 113 intro.
adamc@2 114 rewrite (app_nil_end (compile e)).
adamc@2 115 rewrite compileCorrect'.
adamc@2 116 reflexivity.
adamc@2 117 Qed.
adamc@2 118
adamc@3 119 (* begin hide *)
adamc@2 120 End Nat.
adamc@3 121 (* end hide *)