src/Doc/Codegen/Foundations.thy

 theory Foundations
 imports Introduction
 begin
 
-section {* Code generation foundations \label{sec:foundations} *}
-
-subsection {* Code generator architecture \label{sec:architecture} *}
-
-text {*
+section \<open>Code generation foundations \label{sec:foundations}\<close>
+
+subsection \<open>Code generator architecture \label{sec:architecture}\<close>
+
+text \<open>
   The code generator is actually a framework consisting of different
   components which can be customised individually.
 
   Conceptually all components operate on Isabelle's logic framework
   @{theory Pure}.  Practically, the object logic @{theory HOL}

   \end{itemize}
 
   \noindent From these steps, only the last two are carried out
   outside the logic; by keeping this layer as thin as possible, the
   amount of code to trust is kept to a minimum.
-*}
-
-
-subsection {* The pre- and postprocessor \label{sec:preproc} *}
-
-text {*
+\<close>
+
+
+subsection \<open>The pre- and postprocessor \label{sec:preproc}\<close>
+
+text \<open>
   Before selected function theorems are turned into abstract code, a
   chain of definitional transformation steps is carried out:
   \emph{preprocessing}.  The preprocessor consists of two
   components: a \emph{simpset} and \emph{function transformers}.
 

   expressions suitable for logical reasoning and expressions 
   suitable for execution.  As example, take list membership; logically
   is is just expressed as @{term "x \<in> set xs"}.  But for execution
   the intermediate set is not desirable.  Hence the following
   specification:
-*}
+\<close>
 
 definition %quote member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
 where
   [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
 
-text {*
+text \<open>
   \noindent The \emph{@{attribute code_abbrev} attribute} declares
   its theorem a rewrite rule for the postprocessor and the symmetric
   of its theorem as rewrite rule for the preprocessor.  Together,
   this has the effect that expressions @{thm (rhs) member_def [no_vars]}
   are replaced by @{thm (lhs) member_def [no_vars]} in generated code, but

   \noindent The current setup of the pre- and postprocessor may be inspected
   using the @{command_def print_codeproc} command.  @{command_def
   code_thms} (see \secref{sec:equations}) provides a convenient
   mechanism to inspect the impact of a preprocessor setup on code
   equations.
-*}
-
-
-subsection {* Understanding code equations \label{sec:equations} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Understanding code equations \label{sec:equations}\<close>
+
+text \<open>
   As told in \secref{sec:principle}, the notion of code equations is
   vital to code generation.  Indeed most problems which occur in
   practice can be resolved by an inspection of the underlying code
   equations.
 
   It is possible to exchange the default code equations for constants
   by explicitly proving alternative ones:
-*}
+\<close>
 
 lemma %quote [code]:
   "dequeue (AQueue xs []) =
      (if xs = [] then (None, AQueue [] [])
        else dequeue (AQueue [] (rev xs)))"
   "dequeue (AQueue xs (y # ys)) =
      (Some y, AQueue xs ys)"
   by (cases xs, simp_all) (cases "rev xs", simp_all)
 
-text {*
+text \<open>
   \noindent The annotation @{text "[code]"} is an @{text attribute}
   which states that the given theorems should be considered as code
   equations for a @{text fun} statement -- the corresponding constant
   is determined syntactically.  The resulting code:
-*}
-
-text %quotetypewriter {*
+\<close>
+
+text %quotetypewriter \<open>
   @{code_stmts dequeue (consts) dequeue (Haskell)}
-*}
-
-text {*
+\<close>
+
+text \<open>
   \noindent You may note that the equality test @{term "xs = []"} has
   been replaced by the predicate @{term "List.null xs"}.  This is due
   to the default setup of the \qn{preprocessor}.
 
   This possibility to select arbitrary code equations is the key

   print_codesetup} command.
 
   The code equations after preprocessing are already are blueprint of
   the generated program and can be inspected using the @{command
   code_thms} command:
-*}
+\<close>
 
 code_thms %quote dequeue
 
-text {*
+text \<open>
   \noindent This prints a table with the code equations for @{const
   dequeue}, including \emph{all} code equations those equations depend
   on recursively.  These dependencies themselves can be visualized using
   the @{command_def code_deps} command.
-*}
-
-
-subsection {* Equality *}
-
-text {*
+\<close>
+
+
+subsection \<open>Equality\<close>
+
+text \<open>
   Implementation of equality deserves some attention.  Here an example
   function involving polymorphic equality:
-*}
+\<close>
 
 primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "collect_duplicates xs ys [] = xs"
 | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
     then if z \<in> set ys
       then collect_duplicates xs ys zs
       else collect_duplicates xs (z#ys) zs
     else collect_duplicates (z#xs) (z#ys) zs)"
 
-text {*
+text \<open>
   \noindent During preprocessing, the membership test is rewritten,
   resulting in @{const List.member}, which itself performs an explicit
   equality check, as can be seen in the corresponding @{text SML} code:
-*}
-
-text %quotetypewriter {*
+\<close>
+
+text %quotetypewriter \<open>
   @{code_stmts collect_duplicates (SML)}
-*}
-
-text {*
+\<close>
+
+text \<open>
   \noindent Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces an
   explicit class @{class equal} with a corresponding operation @{const
   HOL.equal} such that @{thm equal [no_vars]}.  The preprocessing
   framework does the rest by propagating the @{class equal} constraints
   through all dependent code equations.  For datatypes, instances of
   @{class equal} are implicitly derived when possible.  For other types,
   you may instantiate @{text equal} manually like any other type class.
-*}
-
-
-subsection {* Explicit partiality \label{sec:partiality} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Explicit partiality \label{sec:partiality}\<close>
+
+text \<open>
   Partiality usually enters the game by partial patterns, as
   in the following example, again for amortised queues:
-*}
+\<close>
 
 definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   "strict_dequeue q = (case dequeue q
     of (Some x, q') \<Rightarrow> (x, q'))"
 

   "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
   "strict_dequeue (AQueue xs []) =
     (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
   by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
 
-text {*
+text \<open>
   \noindent In the corresponding code, there is no equation
   for the pattern @{term "AQueue [] []"}:
-*}
-
-text %quotetypewriter {*
+\<close>
+
+text %quotetypewriter \<open>
   @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
-*}
-
-text {*
+\<close>
+
+text \<open>
   \noindent In some cases it is desirable to have this
   pseudo-\qt{partiality} more explicitly, e.g.~as follows:
-*}
+\<close>
 
 axiomatization %quote empty_queue :: 'a
 
 definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"

      else strict_dequeue' (AQueue [] (rev xs)))"
   "strict_dequeue' (AQueue xs (y # ys)) =
      (y, AQueue xs ys)"
   by (simp_all add: strict_dequeue'_def split: list.splits)
 
-text {*
+text \<open>
   Observe that on the right hand side of the definition of @{const
   "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
 
   Normally, if constants without any code equations occur in a
   program, the code generator complains (since in most cases this is

   of as function definitions which always fail,
   since there is never a successful pattern match on the left hand
   side.  In order to categorise a constant into that category
   explicitly, use the @{attribute code} attribute with
   @{text abort}:
-*}
+\<close>
 
 declare %quote [[code abort: empty_queue]]
 
-text {*
+text \<open>
   \noindent Then the code generator will just insert an error or
   exception at the appropriate position:
-*}
-
-text %quotetypewriter {*
+\<close>
+
+text %quotetypewriter \<open>
   @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
-*}
-
-text {*
+\<close>
+
+text \<open>
   \noindent This feature however is rarely needed in practice.  Note
   also that the HOL default setup already declares @{const undefined},
   which is most likely to be used in such situations, as
   @{text "code abort"}.
-*}
-
-
-subsection {* If something goes utterly wrong \label{sec:utterly_wrong} *}
-
-text {*
+\<close>
+
+
+subsection \<open>If something goes utterly wrong \label{sec:utterly_wrong}\<close>
+
+text \<open>
   Under certain circumstances, the code generator fails to produce
   code entirely.  To debug these, the following hints may prove
   helpful:
 
   \begin{description}

       generation, whose result in turn can be used to trace the
       problem.  The most prominent case here are mismatches in type
       class signatures (\qt{wellsortedness error}).
 
   \end{description}
-*}
+\<close>
 
 end