doc-src/TutorialI/CodeGen/CodeGen.thy
changeset 9844 8016321c7de1
parent 9792 bbefb6ce5cb2
child 9933 9feb1e0c4cb3
equal deleted inserted replaced
9843:cc8aa63bdad6 9844:8016321c7de1
     1 (*<*)
     1 (*<*)
     2 theory CodeGen = Main:
     2 theory CodeGen = Main:
     3 (*>*)
     3 (*>*)
     4 
     4 
     5 text{*\noindent
     5 section{*Case study: compiling expressions*}
       
     6 
       
     7 text{*\label{sec:ExprCompiler}
     6 The task is to develop a compiler from a generic type of expressions (built
     8 The task is to develop a compiler from a generic type of expressions (built
     7 up from variables, constants and binary operations) to a stack machine.  This
     9 up from variables, constants and binary operations) to a stack machine.  This
     8 generic type of expressions is a generalization of the boolean expressions in
    10 generic type of expressions is a generalization of the boolean expressions in
     9 \S\ref{sec:boolex}.  This time we do not commit ourselves to a particular
    11 \S\ref{sec:boolex}.  This time we do not commit ourselves to a particular
    10 type of variables or values but make them type parameters.  Neither is there
    12 type of variables or values but make them type parameters.  Neither is there