doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy

initial draft

(* $Id$ *)

theory Codegen
imports Main
begin

chapter {* Code generation from Isabelle theories *}

section {* Introduction *}

text {*
  \cite{isa-tutorial}
*} (* add graphics here *)

section {* Basics *}

subsection {* Invoking the code generator *}

subsection {* Theorem selection *}

(* print_codethms, code func, default setup code nofunc *)

subsection {* Type classes *}

subsection {* Preprocessing *}

(* preprocessing, print_codethms () *)

subsection {* Incremental code generation *}

(* print_codethms (\<dots>) *)


section {* Customizing serialization  *}

section {* Recipes and advanced topics *}

(* understanding the type game, reflexive equations, code inline code_constsubst, code_abstype*)

section {* ML interfaces *}

subsection {* codegen\_data.ML *}

subsection {* Implementing code generator applications *}

end