annotate src/StackMachine.v @ 12:bcf375310f5f

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
rev   line source
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.