StackMachine
Table of Contents
Initial Setup
Evaluate these two blocks
Set org-confirm-babel-evaluate to a lambda expression that takes the language and body of a code block and returns nil if lang is "coq", otherwise t.
(setq-local org-confirm-babel-evaluate (lambda (lang body) (not (string= lang "coq")))) (setq org-src-preserve-indentation t)
Add LoadPath "../src" as Cpdt. Require Import Bool Arith List Cpdt.CpdtTactics. Set Implicit Arguments.
(* Set Asymmetric Patterns. *)
Tangle and publish.
(progn ;; Load project config. (load-file "../cpdt.el") ;; Tangle this file. (org-babel-tangle-publish nil (buffer-file-name) "../docs/code/") ;; Publish the "cpdt-site" project. (org-publish-project "cpdt-site") "We did it!")
Snippets
(Const 42)
(Binop Plus (Const 2) (Const 2))
(Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))
Definitions
binop datatype
Inductive binop : Set := Plus | Times.
binop is defined binop_rect is defined binop_ind is defined binop_rec is defined
Arithmetic expression
Inductive exp : Set := | Const : nat -> exp | Binop : binop -> exp -> exp -> exp.
exp is defined exp_rect is defined exp_ind is defined exp_rec is defined
The Meaning of a Binary Operator (binop)
Definition binopDenote (b : binop) : nat -> nat -> nat := match b with | Plus => plus | Times => mult end.
binopDenote is defined
The Meaning of an expression
Fixpoint expDenote (e : exp) : nat := match e with | Const n => n | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) end.
expDenote is defined expDenote is recursively defined (decreasing on 1st argument)
Test Evaluations
Eval simpl in expDenote (Const 42).
= 42
: nat
Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)).
= 4
: nat
Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
= 28
: nat
Target Language
Inductive instr : Set := | iConst : nat -> instr | iBinop : binop -> instr.
instr is defined instr_rect is defined instr_ind is defined instr_rec is defined
Definition prog := list instr.
prog is defined
Definition stack := list nat.
stack is defined
Definition instrDenote (i : instr) (s : stack) : option stack := match i with | iConst n => Some (n :: s) | iBinop b => match s with | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s') | _ => None end end.
instrDenote is defined
Fixpoint progDenote (p : prog) (s : stack) : option stack := match p with | nil => Some s | i :: p' => match instrDenote i s with | None => None | Some s' => progDenote p' s' end end.
progDenote is defined progDenote is recursively defined (decreasing on 1st argument)
Translation
Fixpoint compile (e : exp) : prog := match e with | Const n => iConst n :: nil | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil end.
compile is defined compile is recursively defined (decreasing on 1st argument)
Test Evaluations
Eval simpl in compile (Const 42).
= iConst 42 :: nil
: prog
Eval simpl in compile (Binop Plus (Const 2) (Const 2)).
= iConst 2 :: iConst 2 :: iBinop Plus :: nil
: prog
Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
= iConst 7 :: iConst 2 :: iConst 2 :: iBinop Plus :: iBinop Times :: nil
: prog
Eval simpl in progDenote (compile (Const 42)) nil.
= Some (42 :: nil)
: option stack
Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil.
= Some (4 :: nil)
: option stack
Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) nil.
= Some (28 :: nil)
: option stack
Translation Correctness
Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
1 subgoal ============================ forall e : exp, progDenote (compile e) nil = Some (expDenote e :: nil)
Abort.
Lemma compile_correct' : forall e p s, progDenote (compile e ++ p) s = progDenote p (expDenote e :: s).
1 subgoal ============================ forall (e : exp) (p : list instr) (s : stack), progDenote (compile e ++ p) s = progDenote p (expDenote e :: s)
induction e.
2 subgoals n : nat ============================ forall (p : list instr) (s : stack), progDenote (compile (Const n) ++ p) s = progDenote p (expDenote (Const n) :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
intros.
2 subgoals n : nat p : list instr s : stack ============================ progDenote (compile (Const n) ++ p) s = progDenote p (expDenote (Const n) :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
unfold compile.
2 subgoals n : nat p : list instr s : stack ============================ progDenote ((iConst n :: nil) ++ p) s = progDenote p (expDenote (Const n) :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
unfold expDenote.
2 subgoals n : nat p : list instr s : stack ============================ progDenote ((iConst n :: nil) ++ p) s = progDenote p (n :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
unfold progDenote at 1.
2 subgoals n : nat p : list instr s : stack ============================ (fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack := match p0 with | nil => Some s0 | i :: p' => match instrDenote i s0 with | Some s' => progDenote p' s' | None => None end end) ((iConst n :: nil) ++ p) s = progDenote p (n :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
simpl.
2 subgoals n : nat p : list instr s : stack ============================ (fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack := match p0 with | nil => Some s0 | i :: p' => match instrDenote i s0 with | Some s' => progDenote p' s' | None => None end end) p (n :: s) = progDenote p (n :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
fold progDenote.
2 subgoals n : nat p : list instr s : stack ============================ progDenote p (n :: s) = progDenote p (n :: s) subgoal 2 is: forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
reflexivity.
1 subgoal b : binop e1, e2 : exp IHe1 : forall (p : list instr) (s : stack), progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) IHe2 : forall (p : list instr) (s : stack), progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) ============================ forall (p : list instr) (s : stack), progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
intros. unfold compile. fold compile. unfold expDenote. fold expDenote.
1 subgoal b : binop e1, e2 : exp IHe1 : forall (p : list instr) (s : stack), progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) IHe2 : forall (p : list instr) (s : stack), progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) p : list instr s : stack ============================ progDenote (compile (Binop b e1 e2) ++ p) s = progDenote p (expDenote (Binop b e1 e2) :: s)
Check app_assoc_reverse.
app_assoc_reverse
: forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
SearchRewrite ((_ ++ _) ++ _).
app_assoc: forall (A : Type) (l m n : list A), l ++ m ++ n = (l ++ m) ++ n app_assoc_reverse: forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
rewrite app_assoc_reverse.
1 subgoal b : binop e1, e2 : exp IHe1 : forall (p : list instr) (s : stack), progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) IHe2 : forall (p : list instr) (s : stack), progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) p : list instr s : stack ============================ progDenote (compile e2 ++ (compile e1 ++ iBinop b :: nil) ++ p) s = progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
rewrite IHe2.
1 subgoal b : binop e1, e2 : exp IHe1 : forall (p : list instr) (s : stack), progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) IHe2 : forall (p : list instr) (s : stack), progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) p : list instr s : stack ============================ progDenote ((compile e1 ++ iBinop b :: nil) ++ p) (expDenote e2 :: s) = progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
rewrite app_assoc_reverse. rewrite IHe1.
1 subgoal b : binop e1, e2 : exp IHe1 : forall (p : list instr) (s : stack), progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) IHe2 : forall (p : list instr) (s : stack), progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) p : list instr s : stack ============================ progDenote (compile e1 ++ (iBinop b :: nil) ++ p) (expDenote e2 :: s) = progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
unfold progDenote at 1. simpl. fold progDenote. reflexivity.
1 subgoal b : binop e1, e2 : exp IHe1 : forall (p : list instr) (s : stack), progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s) IHe2 : forall (p : list instr) (s : stack), progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s) p : list instr s : stack ============================ (fix progDenote (p0 : prog) (s0 : stack) {struct p0} : option stack := match p0 with | nil => Some s0 | i :: p' => match instrDenote i s0 with | Some s' => progDenote p' s' | None => None end end) ((iBinop b :: nil) ++ p) (expDenote e1 :: expDenote e2 :: s) = progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
Abort.
Lemma compile_correct' : forall e s p, progDenote (compile e ++ p) s = progDenote p (expDenote e :: s). induction e; crush. Qed.
compile_correct' is defined