Quelle  CodeGen.thy

(*<*)
theory CodeGen imports Main begin
(*>*)

section‹Case Study: Compiling Expressions›

text‹\label{sec:ExprCompiler}
 index{compiling expressions example|(}%
  task is to develop a compiler from a generic type of expressions (built
  variables, constants and binary operations) to a stack machine. This
  type of expressions is a generalization of the boolean expressions in
 S\ref{sec:boolex}. This time we do not commit ourselves to a particular
  of variables or values but make them type parameters. Neither is there
  fixed set of binary operations: instead the expression contains the
  function itself.
 ›

type_synonym 'v binop = "'v ==> 'v ==> 'v"
datatype (dead 'a, 'v) expr = Cex 'v
                      | Vex 'a
                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr"

text‹\noindent
  three constructors represent constants, variables and the application of
  binary operation to two subexpressions.

  value of an expression with respect to an environment that maps variables to
  is easily defined:
 ›

primrec "value" :: "('a,'v)expr ==> ('a ==> 'v) ==> 'v" where
"value (Cex v) env = v" |
"value (Vex a) env = env a" |
"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"

text‹
  stack machine has three instructions: load a constant value onto the
 , load the contents of an address onto the stack, and apply a
  operation to the two topmost elements of the stack, replacing them by
  result. As for ‹expr›, addresses and values are type parameters:
 ›

datatype (dead 'a, 'v) instr = Const 'v
                       | Load 'a
                       | Apply "'v binop"

text‹
  execution of the stack machine is modelled by a function
 ‹exec› that takes a list of instructions, a store (modelled as a
  from addresses to values, just like the environment for
  expressions), and a stack (modelled as a list) of values,
  returns the stack at the end of the execution --- the store remains
 :
 ›

primrec exec :: "('a,'v)instr list ==> ('a==>'v) ==> 'v list ==> 'v list"
where
"exec [] s vs = vs" |
"exec (i#is) s vs = (case i of
    Const v ==> exec is s (v#vs)
  | Load a ==> exec is s ((s a)#vs)
  | Apply f ==> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"

text‹\noindent
  that term‹hd› and term‹tl›
  the first element and the remainder of a list.
  all functions are total, \cdx{hd} is defined even for the empty
 , although we do not know what the result is. Thus our model of the
  always terminates properly, although the definition above does not
  us much about the result in situations where term‹Apply› was executed
  fewer than two elements on the stack.

  compiler is a function from expressions to a list of instructions. Its
  is obvious:
 ›

primrec compile :: "('a,'v)expr ==> ('a,'v)instr list" where
"compile (Cex v) = [Const v]" |
"compile (Vex a) = [Load a]" |
"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"

text‹
  we have to prove the correctness of the compiler, i.e.\ that the
  of a compiled expression results in the value of the expression:
 ›
theorem "exec (compile e) s [] = [value e s]"
(*<*)oops(*>*)
text‹\noindent
  theorem needs to be generalized:
 ›

theorem "∀vs. exec (compile e) s vs = (value e s) # vs"

txt‹\noindent
  will be proved by induction on term‹e› followed by simplification.
 , we must prove a lemma about executing the concatenation of two
  sequences:
 ›
(*<*)oops(*>*)
lemma exec_app[simp]:
  "∀vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" 

txt‹\noindent
  requires induction on term‹xs› and ordinary simplification for the
  cases. In the induction step, simplification leaves us with a formula
  contains two ‹case›-expressions over instructions. Thus we add
  case splitting, which finishes the proof:
 ›
apply(induct_tac xs, simp, simp split: instr.split)
(*<*)done(*>*)
text‹\noindent
  that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
  modified in the same way as ‹simp›. Thus the proof can be
  as
 ›
(*<*)
declare exec_app[simp del]
lemma [simp]: "∀vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" 
(*>*)
apply(induct_tac xs, simp_all split: instr.split)
(*<*)done(*>*)
text‹\noindent
  this is more compact, it is less clear for the reader of the proof.

  could now go back and prove prop‹exec (compile e) s [] = [value e s]›
  by simplification with the generalized version we just proved.
 , this is unnecessary because the generalized version fully subsumes
  instance.%
 index{compiling expressions example|)}
 ›
(*<*)
theorem "∀vs. exec (compile e) s vs = (value e s) # vs"
by(induct_tac e, auto)
end
(*>*)