Mercurial > cpdt > repo

comparison book/src/StackMachine.v @ 4:f913d32a49e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Intro
author Adam Chlipala <adamc@hcoop.net>
date Fri, 29 Aug 2008 16:41:49 -0400
parents 9fea5674367c
children c2e8e9c20643
comparison
equal deleted inserted replaced
3:9fea5674367c 4:f913d32a49e4
14 (* end hide *) 14 (* end hide *)
15 15
16 16
17 (** * Arithmetic expressions over natural numbers *) 17 (** * Arithmetic expressions over natural numbers *)
18 18
19 (* begin hide *)
20 Module Nat.
21 (* end hide *)
22 (** ** Source language *) 19 (** ** Source language *)
23 20
24 Inductive binop : Set := Plus | Times. 21 Inductive binop : Set := Plus | Times.
25 22
26 Inductive exp : Set := 23 Inductive exp : Set :=
27 | Const : nat -> exp 24 | Const : nat -> exp
28 | Binop : binop -> exp -> exp -> exp. 25 | Binop : binop -> exp -> exp -> exp.
29 26
30 Definition binopDenote (b : binop) : nat -> nat -> nat := 27 Definition binopDenote (b : binop) : nat -> nat -> nat :=
31 match b with 28 match b with
32 | Plus => plus 29 | Plus => plus
33 | Times => mult 30 | Times => mult
34 end. 31 end.
35 32
36 Fixpoint expDenote (e : exp) : nat := 33 Fixpoint expDenote (e : exp) : nat :=
37 match e with 34 match e with
38 | Const n => n 35 | Const n => n
39 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) 36 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
40 end. 37 end.
41 38
42 39
43 (** ** Target language *) 40 (** ** Target language *)
44 41
45 Inductive instr : Set := 42 Inductive instr : Set :=
46 | IConst : nat -> instr 43 | IConst : nat -> instr
47 | IBinop : binop -> instr. 44 | IBinop : binop -> instr.
48 45
49 Definition prog := list instr. 46 Definition prog := list instr.
50 Definition stack := list nat. 47 Definition stack := list nat.
51 48
52 Definition instrDenote (i : instr) (s : stack) : option stack := 49 Definition instrDenote (i : instr) (s : stack) : option stack :=
53 match i with 50 match i with
54 | IConst n => Some (n :: s) 51 | IConst n => Some (n :: s)
55 | IBinop b => 52 | IBinop b =>
56 match s with 53 match s with
57 | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s') 54 | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
58 | _ => None 55 | _ => None
59 end 56 end
60 end. 57 end.
61 58
62 Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack := 59 Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack :=
63 match p with 60 match p with
64 | nil => Some s 61 | nil => Some s
65 | i :: p' => 62 | i :: p' =>
66 match instrDenote i s with 63 match instrDenote i s with
67 | None => None 64 | None => None
68 | Some s' => progDenote p' s' 65 | Some s' => progDenote p' s'
69 end 66 end
70 end. 67 end.
71 68
72 69
73 (** ** Translation *) 70 (** ** Translation *)
74 71
75 Fixpoint compile (e : exp) : prog := 72 Fixpoint compile (e : exp) : prog :=
76 match e with 73 match e with
77 | Const n => IConst n :: nil 74 | Const n => IConst n :: nil
78 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil 75 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil
79 end. 76 end.
80 77
81 78
82 (** ** Translation correctness *) 79 (** ** Translation correctness *)
83 80
84 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s = 81 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
85 progDenote p (expDenote e :: s). 82 progDenote p (expDenote e :: s).
86 induction e. 83 induction e.
87 84
88 intros. 85 intros.
89 unfold compile. 86 unfold compile.
90 unfold expDenote. 87 unfold expDenote.
91 simpl. 88 simpl.
92 reflexivity. 89 reflexivity.
93 90
94 intros. 91 intros.
95 unfold compile. 92 unfold compile.
96 fold compile. 93 fold compile.
97 unfold expDenote. 94 unfold expDenote.
98 fold expDenote. 95 fold expDenote.
99 rewrite app_ass. 96 rewrite app_ass.
100 rewrite IHe2. 97 rewrite IHe2.
101 rewrite app_ass. 98 rewrite app_ass.
102 rewrite IHe1. 99 rewrite IHe1.
103 simpl. 100 simpl.
104 reflexivity. 101 reflexivity.
105 Abort. 102 Abort.
106 103
107 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s = 104 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
108 progDenote p (expDenote e :: s). 105 progDenote p (expDenote e :: s).
109 induction e; crush. 106 induction e; crush.
110 Qed. 107 Qed.
111 108
112 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). 109 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
113 intro. 110 intro.
114 rewrite (app_nil_end (compile e)). 111 rewrite (app_nil_end (compile e)).
115 rewrite compileCorrect'. 112 rewrite compileCorrect'.
116 reflexivity. 113 reflexivity.
117 Qed. 114 Qed.
118
119 (* begin hide *)
120 End Nat.
121 (* end hide *)