Mercurial > cpdt > repo

comparison book/StackMachine.v @ 2:b3f7de74d38f

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