1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/IsaMakefile	Tue Oct 10 12:08:12 2006 +0200
     1.3 @@ -0,0 +1,33 @@
     1.4 +
     1.5 +## targets
     1.6 +
     1.7 +default: Thy
     1.8 +images: 
     1.9 +test: Thy
    1.10 +
    1.11 +all: images test
    1.12 +
    1.13 +
    1.14 +## global settings
    1.15 +
    1.16 +SRC = $(ISABELLE_HOME)/src
    1.17 +OUT = $(ISABELLE_OUTPUT)
    1.18 +LOG = $(OUT)/log
    1.19 +
    1.20 +USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    1.21 +
    1.22 +
    1.23 +## Thy
    1.24 +
    1.25 +THY = $(LOG)/HOL-Thy.gz
    1.26 +
    1.27 +Thy: $(THY)
    1.28 +
    1.29 +$(THY): Thy/ROOT.ML Thy/Codegen.thy
    1.30 +	@$(USEDIR) HOL Thy
    1.31 +
    1.32 +
    1.33 +## clean
    1.34 +
    1.35 +clean:
    1.36 +	@rm -f $(THY)

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Makefile	Tue Oct 10 12:08:12 2006 +0200
     2.3 @@ -0,0 +1,43 @@
     2.4 +#
     2.5 +# $Id$
     2.6 +#
     2.7 +
     2.8 +## targets
     2.9 +
    2.10 +default: dvi
    2.11 +
    2.12 +
    2.13 +## dependencies
    2.14 +
    2.15 +include ../../Makefile.in
    2.16 +
    2.17 +isabelle_isar.eps:
    2.18 +	test -r isabelle_isar.eps || ln -s ../../gfx/isabelle_isar.eps .
    2.19 +
    2.20 +isabelle_isar.pdf:
    2.21 +	test -r isabelle_isar.pdf || ln -s ../../gfx/isabelle_isar.pdf .
    2.22 +
    2.23 +NAME = codegen
    2.24 +
    2.25 +FILES = $(NAME).tex Thy/document/Codegen.tex \
    2.26 +  style.sty ../../iman.sty ../../extra.sty ../../isar.sty \
    2.27 +  ../../manual.bib ../../proof.sty
    2.28 +
    2.29 +dvi: $(NAME).dvi
    2.30 +
    2.31 +$(NAME).dvi: $(FILES) isabelle_isar.eps
    2.32 +	$(LATEX) $(NAME)
    2.33 +	$(BIBTEX) $(NAME)
    2.34 +	$(LATEX) $(NAME)
    2.35 +	$(LATEX) $(NAME)
    2.36 +
    2.37 +pdf: $(NAME).pdf
    2.38 +
    2.39 +$(NAME).pdf: $(FILES) isabelle_isar.pdf
    2.40 +	$(PDFLATEX) $(NAME)
    2.41 +	$(BIBTEX) $(NAME)
    2.42 +	$(PDFLATEX) $(NAME)
    2.43 +	$(PDFLATEX) $(NAME)
    2.44 +	$(FIXBOOKMARKS) $(NAME).out
    2.45 +	$(PDFLATEX) $(NAME)
    2.46 +	$(PDFLATEX) $(NAME)

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Oct 10 12:08:12 2006 +0200
     3.3 @@ -0,0 +1,47 @@
     3.4 +
     3.5 +(* $Id$ *)
     3.6 +
     3.7 +theory Codegen
     3.8 +imports Main
     3.9 +begin
    3.10 +
    3.11 +chapter {* Code generation from Isabelle theories *}
    3.12 +
    3.13 +section {* Introduction *}
    3.14 +
    3.15 +text {*
    3.16 +  \cite{isa-tutorial}
    3.17 +*} (* add graphics here *)
    3.18 +
    3.19 +section {* Basics *}
    3.20 +
    3.21 +subsection {* Invoking the code generator *}
    3.22 +
    3.23 +subsection {* Theorem selection *}
    3.24 +
    3.25 +(* print_codethms, code func, default setup code nofunc *)
    3.26 +
    3.27 +subsection {* Type classes *}
    3.28 +
    3.29 +subsection {* Preprocessing *}
    3.30 +
    3.31 +(* preprocessing, print_codethms () *)
    3.32 +
    3.33 +subsection {* Incremental code generation *}
    3.34 +
    3.35 +(* print_codethms (\<dots>) *)
    3.36 +
    3.37 +
    3.38 +section {* Customizing serialization  *}
    3.39 +
    3.40 +section {* Recipes and advanced topics *}
    3.41 +
    3.42 +(* understanding the type game, reflexive equations, code inline code_constsubst, code_abstype*)
    3.43 +
    3.44 +section {* ML interfaces *}
    3.45 +
    3.46 +subsection {* codegen\_data.ML *}
    3.47 +
    3.48 +subsection {* Implementing code generator applications *}
    3.49 +
    3.50 +end

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML	Tue Oct 10 12:08:12 2006 +0200
     4.3 @@ -0,0 +1,4 @@
     4.4 +
     4.5 +(* $Id$ *)
     4.6 +
     4.7 +use_thy "Codegen";

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Tue Oct 10 12:08:12 2006 +0200
     5.3 @@ -0,0 +1,77 @@
     5.4 +
     5.5 +%% $Id$
     5.6 +
     5.7 +\documentclass[12pt,a4paper,fleqn]{report}
     5.8 +\usepackage{latexsym,graphicx}
     5.9 +\usepackage[refpage]{nomencl}
    5.10 +\usepackage{../../iman,../../extra,../../isar,../../proof}
    5.11 +\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
    5.12 +\usepackage{style}
    5.13 +\usepackage{Thy/document/pdfsetup}
    5.14 +
    5.15 +\newcommand{\cmd}[1]{\isacommand{#1}}
    5.16 +
    5.17 +\newcommand{\isasymINFIX}{\cmd{infix}}
    5.18 +\newcommand{\isasymLOCALE}{\cmd{locale}}
    5.19 +\newcommand{\isasymINCLUDES}{\cmd{includes}}
    5.20 +\newcommand{\isasymDATATYPE}{\cmd{datatype}}
    5.21 +\newcommand{\isasymAXCLASS}{\cmd{axclass}}
    5.22 +\newcommand{\isasymFIXES}{\cmd{fixes}}
    5.23 +\newcommand{\isasymASSUMES}{\cmd{assumes}}
    5.24 +\newcommand{\isasymDEFINES}{\cmd{defines}}
    5.25 +\newcommand{\isasymNOTES}{\cmd{notes}}
    5.26 +\newcommand{\isasymSHOWS}{\cmd{shows}}
    5.27 +\newcommand{\isasymCLASS}{\cmd{class}}
    5.28 +\newcommand{\isasymINSTANCE}{\cmd{instance}}
    5.29 +\newcommand{\isasymLEMMA}{\cmd{lemma}}
    5.30 +\newcommand{\isasymPROOF}{\cmd{proof}}
    5.31 +\newcommand{\isasymQED}{\cmd{qed}}
    5.32 +\newcommand{\isasymFIX}{\cmd{fix}}
    5.33 +\newcommand{\isasymASSUME}{\cmd{assume}}
    5.34 +\newcommand{\isasymSHOW}{\cmd{show}}
    5.35 +\newcommand{\isasymNOTE}{\cmd{note}}
    5.36 +\newcommand{\isasymIN}{\cmd{in}}
    5.37 +
    5.38 +\newcommand{\qt}[1]{``#1''}
    5.39 +\newcommand{\qtt}[1]{"{}{#1}"{}}
    5.40 +\newcommand{\qn}[1]{\emph{#1}}
    5.41 +\newcommand{\strong}[1]{{\bfseries #1}}
    5.42 +\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
    5.43 +
    5.44 +\hyphenation{Isabelle}
    5.45 +\hyphenation{Isar}
    5.46 +
    5.47 +\isadroptag{theory}
    5.48 +\title{\includegraphics[scale=0.5]{isabelle_isar}
    5.49 +  \\[4ex] Code generation from Isabelle theories}
    5.50 +\author{\emph{Florian Haftmann}}
    5.51 +
    5.52 +
    5.53 +\begin{document}
    5.54 +
    5.55 +\maketitle
    5.56 +
    5.57 +\begin{abstract}
    5.58 +  \fixme
    5.59 +\end{abstract}
    5.60 +
    5.61 +\thispagestyle{empty}\clearpage
    5.62 +
    5.63 +\pagenumbering{roman}
    5.64 +\clearfirst
    5.65 +
    5.66 +\input{Thy/document/Codegen.tex}
    5.67 +
    5.68 +\begingroup
    5.69 +%\tocentry{\bibname}
    5.70 +\bibliographystyle{plain} \small\raggedright\frenchspacing
    5.71 +\bibliography{../../manual}
    5.72 +\endgroup
    5.73 +
    5.74 +\end{document}
    5.75 +
    5.76 +
    5.77 +%%% Local Variables: 
    5.78 +%%% mode: latex
    5.79 +%%% TeX-master: t
    5.80 +%%% End: 

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/style.sty	Tue Oct 10 12:08:12 2006 +0200
     6.3 @@ -0,0 +1,64 @@
     6.4 +
     6.5 +%% $Id$
     6.6 +
     6.7 +%% toc
     6.8 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     6.9 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
    6.10 +
    6.11 +%% references
    6.12 +\newcommand{\secref}[1]{\S\ref{#1}}
    6.13 +\newcommand{\chref}[1]{chapter~\ref{#1}}
    6.14 +\newcommand{\figref}[1]{figure~\ref{#1}}
    6.15 +
    6.16 +%% glossary
    6.17 +\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
    6.18 +\newcommand{\seeglossary}[1]{\emph{#1}}
    6.19 +\newcommand{\glossaryname}{Glossary}
    6.20 +\renewcommand{\nomname}{\glossaryname}
    6.21 +\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
    6.22 +
    6.23 +%% index
    6.24 +\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
    6.25 +\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    6.26 +\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    6.27 +\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    6.28 +
    6.29 +%% math
    6.30 +\newcommand{\text}[1]{\mbox{#1}}
    6.31 +\newcommand{\isasymvartheta}{\isamath{\theta}}
    6.32 +\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    6.33 +
    6.34 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    6.35 +
    6.36 +\pagestyle{headings}
    6.37 +\sloppy
    6.38 +\binperiod
    6.39 +\underscoreon
    6.40 +
    6.41 +\renewcommand{\isadigit}[1]{\isamath{#1}}
    6.42 +
    6.43 +\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    6.44 +
    6.45 +\isafoldtag{FIXME}
    6.46 +\isakeeptag{mlref}
    6.47 +\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
    6.48 +\renewcommand{\endisatagmlref}{\endgroup}
    6.49 +
    6.50 +\newcommand{\isasymGUESS}{\isakeyword{guess}}
    6.51 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    6.52 +\newcommand{\isasymTHEORY}{\isakeyword{theory}}
    6.53 +\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
    6.54 +\newcommand{\isasymUSES}{\isakeyword{uses}}
    6.55 +\newcommand{\isasymBEGIN}{\isakeyword{begin}}
    6.56 +\newcommand{\isasymEND}{\isakeyword{end}}
    6.57 +\newcommand{\isasymCONSTS}{\isakeyword{consts}}
    6.58 +\newcommand{\isasymDEFS}{\isakeyword{defs}}
    6.59 +\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    6.60 +\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    6.61 +
    6.62 +\isabellestyle{it}
    6.63 +
    6.64 +%%% Local Variables: 
    6.65 +%%% mode: latex
    6.66 +%%% TeX-master: "implementation"
    6.67 +%%% End: