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