equal
deleted
inserted
replaced
26 |
26 |
27 The value of an expression with respect to an environment that maps variables to |
27 The value of an expression with respect to an environment that maps variables to |
28 values is easily defined: |
28 values is easily defined: |
29 *} |
29 *} |
30 |
30 |
31 consts "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v"; |
31 primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where |
32 primrec |
32 "value (Cex v) env = v" | |
33 "value (Cex v) env = v" |
33 "value (Vex a) env = env a" | |
34 "value (Vex a) env = env a" |
34 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)" |
35 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"; |
|
36 |
35 |
37 text{* |
36 text{* |
38 The stack machine has three instructions: load a constant value onto the |
37 The stack machine has three instructions: load a constant value onto the |
39 stack, load the contents of an address onto the stack, and apply a |
38 stack, load the contents of an address onto the stack, and apply a |
40 binary operation to the two topmost elements of the stack, replacing them by |
39 binary operation to the two topmost elements of the stack, replacing them by |
52 evaluating expressions), and a stack (modelled as a list) of values, |
51 evaluating expressions), and a stack (modelled as a list) of values, |
53 and returns the stack at the end of the execution --- the store remains |
52 and returns the stack at the end of the execution --- the store remains |
54 unchanged: |
53 unchanged: |
55 *} |
54 *} |
56 |
55 |
57 consts exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list"; |
56 primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" |
58 primrec |
57 where |
59 "exec [] s vs = vs" |
58 "exec [] s vs = vs" | |
60 "exec (i#is) s vs = (case i of |
59 "exec (i#is) s vs = (case i of |
61 Const v \<Rightarrow> exec is s (v#vs) |
60 Const v \<Rightarrow> exec is s (v#vs) |
62 | Load a \<Rightarrow> exec is s ((s a)#vs) |
61 | Load a \<Rightarrow> exec is s ((s a)#vs) |
63 | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"; |
62 | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))" |
64 |
63 |
65 text{*\noindent |
64 text{*\noindent |
66 Recall that @{term"hd"} and @{term"tl"} |
65 Recall that @{term"hd"} and @{term"tl"} |
67 return the first element and the remainder of a list. |
66 return the first element and the remainder of a list. |
68 Because all functions are total, \cdx{hd} is defined even for the empty |
67 Because all functions are total, \cdx{hd} is defined even for the empty |
73 |
72 |
74 The compiler is a function from expressions to a list of instructions. Its |
73 The compiler is a function from expressions to a list of instructions. Its |
75 definition is obvious: |
74 definition is obvious: |
76 *} |
75 *} |
77 |
76 |
78 consts compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" |
77 primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where |
79 primrec |
78 "compile (Cex v) = [Const v]" | |
80 "compile (Cex v) = [Const v]" |
79 "compile (Vex a) = [Load a]" | |
81 "compile (Vex a) = [Load a]" |
|
82 "compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]" |
80 "compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]" |
83 |
81 |
84 text{* |
82 text{* |
85 Now we have to prove the correctness of the compiler, i.e.\ that the |
83 Now we have to prove the correctness of the compiler, i.e.\ that the |
86 execution of a compiled expression results in the value of the expression: |
84 execution of a compiled expression results in the value of the expression: |