Mercurial > cpdt > repo

comparison book/src/StackMachine.v @ 10:d8363f2a3bef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Target language and translation
author Adam Chlipala <adamc@hcoop.net>
date Mon, 01 Sep 2008 11:30:27 -0400
parents c2e8e9c20643
children e5501b9c965d
comparison
equal deleted inserted replaced
9:c2e8e9c20643 10:d8363f2a3bef
90 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *) 90 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *)
91 91
92 92
93 (** ** Target language *) 93 (** ** Target language *)
94 94
95 (** We will compile our source programs onto a simple stack machine, whose syntax is: *)
96
95 Inductive instr : Set := 97 Inductive instr : Set :=
96 | IConst : nat -> instr 98 | IConst : nat -> instr
97 | IBinop : binop -> instr. 99 | IBinop : binop -> instr.
98 100
99 Definition prog := list instr. 101 Definition prog := list instr.
100 Definition stack := list nat. 102 Definition stack := list nat.
103
104 (** An instruction either pushes a constant onto the stack or pops two arguments, applies a binary operator to them, and pushes the result onto the stack. A program is a list of instructions, and a stack is a list of natural numbers.
105
106 We can give instructions meanings as functions from stacks to optional stacks, where running an instruction results in [None] in case of a stack underflow and results in [Some s'] when the result of execution is the new stack [s']. [::] is the "list cons" operator from the Coq standard library. *)
101 107
102 Definition instrDenote (i : instr) (s : stack) : option stack := 108 Definition instrDenote (i : instr) (s : stack) : option stack :=
103 match i with 109 match i with
104 | IConst n => Some (n :: s) 110 | IConst n => Some (n :: s)
105 | IBinop b => 111 | IBinop b =>
107 | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s') 113 | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
108 | _ => None 114 | _ => None
109 end 115 end
110 end. 116 end.
111 117
118 (** With [instrDenote] defined, it is easy to define a function [progDenote], which iterates application of [instrDenote] through a whole program. *)
119
112 Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack := 120 Fixpoint progDenote (p : prog) (s : stack) {struct p} : option stack :=
113 match p with 121 match p with
114 | nil => Some s 122 | nil => Some s
115 | i :: p' => 123 | i :: p' =>
116 match instrDenote i s with 124 match instrDenote i s with
117 | None => None 125 | None => None
118 | Some s' => progDenote p' s' 126 | Some s' => progDenote p' s'
119 end 127 end
120 end. 128 end.
121 129
130 (** There is one interesting difference compared to our previous example of a [Fixpoint]. This recursive function takes two arguments, [p] and [s]. It is critical for the soundness of Coq that every program terminate, so a shallow syntactic termination check is imposed on every recursive function definition. One of the function parameters must be designated to decrease monotonically across recursive calls. That is, every recursive call must use a version of that argument that has been pulled out of the current argument by some number of [match] expressions. [expDenote] has only one argument, so we did not need to specify which of its arguments decreases. For [progDenote], we resolve the ambiguity by writing [{struct p}] to indicate that argument [p] decreases structurally. *)
131
122 132
123 (** ** Translation *) 133 (** ** Translation *)
134
135 (** Our compiler itself is now unsurprising. [++] is the list concatenation operator from the Coq standard library. *)
124 136
125 Fixpoint compile (e : exp) : prog := 137 Fixpoint compile (e : exp) : prog :=
126 match e with 138 match e with
127 | Const n => IConst n :: nil 139 | Const n => IConst n :: nil
128 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil 140 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil