Mercurial > cpdt > repo

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