Mercurial > cpdt > repo

annotate 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
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@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.