# HG changeset patch
# User haftmann
# Date 1160474892 -7200
# Node ID 9b9910b82645100cbd7525656e9d09c7092e67a7
# Parent  bc827aa5015efb5ea4e7fb3082d0e9ea10589a2f
initial draft

diff -r bc827aa5015e -r 9b9910b82645 doc-src/IsarAdvanced/Codegen/IsaMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/IsaMakefile	Tue Oct 10 12:08:12 2006 +0200
@@ -0,0 +1,33 @@
+
+## targets
+
+default: Thy
+images: 
+test: Thy
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+
+
+## Thy
+
+THY = $(LOG)/HOL-Thy.gz
+
+Thy: $(THY)
+
+$(THY): Thy/ROOT.ML Thy/Codegen.thy
+	@$(USEDIR) HOL Thy
+
+
+## clean
+
+clean:
+	@rm -f $(THY)
diff -r bc827aa5015e -r 9b9910b82645 doc-src/IsarAdvanced/Codegen/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Makefile	Tue Oct 10 12:08:12 2006 +0200
@@ -0,0 +1,43 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+
+## dependencies
+
+include ../../Makefile.in
+
+isabelle_isar.eps:
+	test -r isabelle_isar.eps || ln -s ../../gfx/isabelle_isar.eps .
+
+isabelle_isar.pdf:
+	test -r isabelle_isar.pdf || ln -s ../../gfx/isabelle_isar.pdf .
+
+NAME = codegen
+
+FILES = $(NAME).tex Thy/document/Codegen.tex \
+  style.sty ../../iman.sty ../../extra.sty ../../isar.sty \
+  ../../manual.bib ../../proof.sty
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES) isabelle_isar.eps
+	$(LATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_isar.pdf
+	$(PDFLATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
diff -r bc827aa5015e -r 9b9910b82645 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Oct 10 12:08:12 2006 +0200
@@ -0,0 +1,47 @@
+
+(* $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
diff -r bc827aa5015e -r 9b9910b82645 doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML	Tue Oct 10 12:08:12 2006 +0200
@@ -0,0 +1,4 @@
+
+(* $Id$ *)
+
+use_thy "Codegen";
diff -r bc827aa5015e -r 9b9910b82645 doc-src/IsarAdvanced/Codegen/codegen.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Tue Oct 10 12:08:12 2006 +0200
@@ -0,0 +1,77 @@
+
+%% $Id$
+
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{latexsym,graphicx}
+\usepackage[refpage]{nomencl}
+\usepackage{../../iman,../../extra,../../isar,../../proof}
+\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
+\usepackage{style}
+\usepackage{Thy/document/pdfsetup}
+
+\newcommand{\cmd}[1]{\isacommand{#1}}
+
+\newcommand{\isasymINFIX}{\cmd{infix}}
+\newcommand{\isasymLOCALE}{\cmd{locale}}
+\newcommand{\isasymINCLUDES}{\cmd{includes}}
+\newcommand{\isasymDATATYPE}{\cmd{datatype}}
+\newcommand{\isasymAXCLASS}{\cmd{axclass}}
+\newcommand{\isasymFIXES}{\cmd{fixes}}
+\newcommand{\isasymASSUMES}{\cmd{assumes}}
+\newcommand{\isasymDEFINES}{\cmd{defines}}
+\newcommand{\isasymNOTES}{\cmd{notes}}
+\newcommand{\isasymSHOWS}{\cmd{shows}}
+\newcommand{\isasymCLASS}{\cmd{class}}
+\newcommand{\isasymINSTANCE}{\cmd{instance}}
+\newcommand{\isasymLEMMA}{\cmd{lemma}}
+\newcommand{\isasymPROOF}{\cmd{proof}}
+\newcommand{\isasymQED}{\cmd{qed}}
+\newcommand{\isasymFIX}{\cmd{fix}}
+\newcommand{\isasymASSUME}{\cmd{assume}}
+\newcommand{\isasymSHOW}{\cmd{show}}
+\newcommand{\isasymNOTE}{\cmd{note}}
+\newcommand{\isasymIN}{\cmd{in}}
+
+\newcommand{\qt}[1]{``#1''}
+\newcommand{\qtt}[1]{"{}{#1}"{}}
+\newcommand{\qn}[1]{\emph{#1}}
+\newcommand{\strong}[1]{{\bfseries #1}}
+\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+
+\isadroptag{theory}
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+  \\[4ex] Code generation from Isabelle theories}
+\author{\emph{Florian Haftmann}}
+
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+  \fixme
+\end{abstract}
+
+\thispagestyle{empty}\clearpage
+
+\pagenumbering{roman}
+\clearfirst
+
+\input{Thy/document/Codegen.tex}
+
+\begingroup
+%\tocentry{\bibname}
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{../../manual}
+\endgroup
+
+\end{document}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r bc827aa5015e -r 9b9910b82645 doc-src/IsarAdvanced/Codegen/style.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/style.sty	Tue Oct 10 12:08:12 2006 +0200
@@ -0,0 +1,64 @@
+
+%% $Id$
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\chref}[1]{chapter~\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% glossary
+\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
+\newcommand{\seeglossary}[1]{\emph{#1}}
+\newcommand{\glossaryname}{Glossary}
+\renewcommand{\nomname}{\glossaryname}
+\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
+
+%% index
+\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
+\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
+\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
+\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
+
+%% math
+\newcommand{\text}[1]{\mbox{#1}}
+\newcommand{\isasymvartheta}{\isamath{\theta}}
+\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\pagestyle{headings}
+\sloppy
+\binperiod
+\underscoreon
+
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+
+\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
+
+\isafoldtag{FIXME}
+\isakeeptag{mlref}
+\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
+\renewcommand{\endisatagmlref}{\endgroup}
+
+\newcommand{\isasymGUESS}{\isakeyword{guess}}
+\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
+\newcommand{\isasymTHEORY}{\isakeyword{theory}}
+\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
+\newcommand{\isasymUSES}{\isakeyword{uses}}
+\newcommand{\isasymBEGIN}{\isakeyword{begin}}
+\newcommand{\isasymEND}{\isakeyword{end}}
+\newcommand{\isasymCONSTS}{\isakeyword{consts}}
+\newcommand{\isasymDEFS}{\isakeyword{defs}}
+\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
+\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
+
+\isabellestyle{it}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End: