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