adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * adamc@2: * This work is licensed under a adamc@2: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@2: * Unported License. adamc@2: * The license text is available at: adamc@2: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@2: *) adamc@2: adamc@3: (* begin hide *) adamc@2: Require Import List. adamc@2: adamc@2: Require Import Tactics. adamc@3: (* end hide *) adamc@2: adamc@2: adamc@2: (** * Arithmetic expressions over natural numbers *) adamc@2: adamc@3: (* begin hide *) adamc@2: Module Nat. adamc@3: (* end hide *) adamc@2: (** ** Source language *) adamc@2: adamc@2: Inductive binop : Set := Plus | Times. adamc@2: adamc@2: Inductive exp : Set := adamc@2: | Const : nat -> exp adamc@2: | Binop : binop -> exp -> exp -> exp. adamc@2: adamc@2: Definition binopDenote (b : binop) : nat -> nat -> nat := adamc@2: match b with adamc@2: | Plus => plus adamc@2: | Times => mult adamc@2: end. adamc@2: adamc@2: Fixpoint expDenote (e : exp) : nat := adamc@2: match e with adamc@2: | Const n => n adamc@2: | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) adamc@2: end. adamc@2: adamc@2: adamc@2: (** ** Target language *) adamc@2: adamc@2: Inductive instr : Set := adamc@2: | IConst : nat -> instr adamc@2: | IBinop : binop -> instr. adamc@2: adamc@2: Definition prog := list instr. adamc@2: Definition stack := list nat. adamc@2: adamc@2: Definition instrDenote (i : instr) (s : stack) : option stack := adamc@2: match i with adamc@2: | IConst n => Some (n :: s) adamc@2: | IBinop b => adamc@2: match s with adamc@2: | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s') adamc@2: | _ => None adamc@2: end adamc@2: end. adamc@2: adamc@2: Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack := adamc@2: match p with adamc@2: | nil => Some s adamc@2: | i :: p' => adamc@2: match instrDenote i s with adamc@2: | None => None adamc@2: | Some s' => progDenote p' s' adamc@2: end adamc@2: end. adamc@2: adamc@2: adamc@2: (** ** Translation *) adamc@2: adamc@2: Fixpoint compile (e : exp) : prog := adamc@2: match e with adamc@2: | Const n => IConst n :: nil adamc@2: | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil adamc@2: end. adamc@2: adamc@2: adamc@2: (** ** Translation correctness *) adamc@2: adamc@2: Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s = adamc@2: progDenote p (expDenote e :: s). adamc@2: induction e. adamc@2: adamc@2: intros. adamc@2: unfold compile. adamc@2: unfold expDenote. adamc@2: simpl. adamc@2: reflexivity. adamc@2: adamc@2: intros. adamc@2: unfold compile. adamc@2: fold compile. adamc@2: unfold expDenote. adamc@2: fold expDenote. adamc@2: rewrite app_ass. adamc@2: rewrite IHe2. adamc@2: rewrite app_ass. adamc@2: rewrite IHe1. adamc@2: simpl. adamc@2: reflexivity. adamc@2: Abort. adamc@2: adamc@2: Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s = adamc@2: progDenote p (expDenote e :: s). adamc@2: induction e; crush. adamc@2: Qed. adamc@2: adamc@2: Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). adamc@2: intro. adamc@2: rewrite (app_nil_end (compile e)). adamc@2: rewrite compileCorrect'. adamc@2: reflexivity. adamc@2: Qed. adamc@2: adamc@3: (* begin hide *) adamc@2: End Nat. adamc@3: (* end hide *)