Mercurial > cpdt > repo

comparison src/StackMachine.v @ 12:bcf375310f5f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Squash book into main directory
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 13:30:05 -0400
parents book/src/StackMachine.v@f913d32a49e4
children ea400f692b07
comparison
equal deleted inserted replaced
6:b22369f7f0fe 12:bcf375310f5f
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 (** ** Source language *)
20
21 Inductive binop : Set := Plus | Times.
22
23 Inductive exp : Set :=
24 | Const : nat -> exp
25 | Binop : binop -> exp -> exp -> exp.
26
27 Definition binopDenote (b : binop) : nat -> nat -> nat :=
28 match b with
29 | Plus => plus
30 | Times => mult
31 end.
32
33 Fixpoint expDenote (e : exp) : nat :=
34 match e with
35 | Const n => n
36 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
37 end.
38
39
40 (** ** Target language *)
41
42 Inductive instr : Set :=
43 | IConst : nat -> instr
44 | IBinop : binop -> instr.
45
46 Definition prog := list instr.
47 Definition stack := list nat.
48
49 Definition instrDenote (i : instr) (s : stack) : option stack :=
50 match i with
51 | IConst n => Some (n :: s)
52 | IBinop b =>
53 match s with
54 | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
55 | _ => None
56 end
57 end.
58
59 Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack :=
60 match p with
61 | nil => Some s
62 | i :: p' =>
63 match instrDenote i s with
64 | None => None
65 | Some s' => progDenote p' s'
66 end
67 end.
68
69
70 (** ** Translation *)
71
72 Fixpoint compile (e : exp) : prog :=
73 match e with
74 | Const n => IConst n :: nil
75 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil
76 end.
77
78
79 (** ** Translation correctness *)
80
81 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
82 progDenote p (expDenote e :: s).
83 induction e.
84
85 intros.
86 unfold compile.
87 unfold expDenote.
88 simpl.
89 reflexivity.
90
91 intros.
92 unfold compile.
93 fold compile.
94 unfold expDenote.
95 fold expDenote.
96 rewrite app_ass.
97 rewrite IHe2.
98 rewrite app_ass.
99 rewrite IHe1.
100 simpl.
101 reflexivity.
102 Abort.
103
104 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s =
105 progDenote p (expDenote e :: s).
106 induction e; crush.
107 Qed.
108
109 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
110 intro.
111 rewrite (app_nil_end (compile e)).
112 rewrite compileCorrect'.
113 reflexivity.
114 Qed.