Mercurial > cpdt > repo
comparison book/StackMachine.v @ 2:b3f7de74d38f
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. |