# HG changeset patch
# User haftmann
# Date 1221421835 -7200
# Node ID b52f9205a02d8cc43e1f39fa90e825a481fed3f2
# Parent  44831b5839991e5aae528f560810825cf5fe8daa
New outline for codegen tutorial -- draft

diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/IsaMakefile
--- a/doc-src/IsarAdvanced/Codegen/IsaMakefile	Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/IsaMakefile	Sun Sep 14 21:50:35 2008 +0200
@@ -23,7 +23,7 @@
 
 Thy: $(THY)
 
-$(THY): Thy/ROOT.ML Thy/Codegen.thy ../../antiquote_setup.ML
+$(THY): Thy/ROOT.ML Thy/*.thy ../../antiquote_setup.ML
 	@$(USEDIR) HOL Thy
 
 
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Makefile
--- a/doc-src/IsarAdvanced/Codegen/Makefile	Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Makefile	Sun Sep 14 21:50:35 2008 +0200
@@ -13,7 +13,7 @@
 
 NAME = codegen
 
-FILES = $(NAME).tex Thy/document/Codegen.tex \
+FILES = $(NAME).tex Thy/document/*.tex \
   style.sty ../../iman.sty ../../extra.sty ../../isar.sty \
   ../../isabelle.sty ../../isabellesym.sty ../../pdfsetup.sty \
   ../../manual.bib ../../proof.sty
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,9 @@
+theory Adaption
+imports Setup
+begin
+
+section {* Adaption to target languages *}
+
+subsection {* \ldots *}
+
+end
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/Further.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,17 @@
+theory Further
+imports Setup
+begin
+
+section {* Further topics *}
+
+subsection {* Serializer options *}
+
+subsection {* Evaluation oracle *}
+
+subsection {* Code antiquotation *}
+
+subsection {* Creating new targets *}
+
+text {* extending targets, adding targets *}
+
+end
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,22 @@
+theory Introduction
+imports Setup
+begin
+
+chapter {* Code generation from @{text "Isabelle/HOL"} theories *}
+
+section {* Introduction and Overview *}
+
+text {*
+  This tutorial introduces a generic code generator for the
+  Isabelle system \cite{isa-tutorial}.
+*}
+
+subsection {* Code generation via shallow embedding *}
+
+text {* example *}
+
+subsection {* Code generator architecture *}
+
+text {* foundation, forward references for yet unexplained things  *}
+
+end
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/ML.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,7 @@
+theory "ML"
+imports Setup
+begin
+
+section {* ML system interfaces *}
+
+end
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/Program.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,27 @@
+theory Program
+imports Setup
+begin
+
+section {* Turning Theories into Programs *}
+
+subsection {* The @{text "Isabelle/HOL"} default setup *}
+
+text {* Invoking the code generator *}
+
+subsection {* Selecting code equations *}
+
+text {* inspection by @{text "code_thms"} *}
+
+subsection {* The preprocessor *}
+
+subsection {* Datatypes *}
+
+text {* example: @{text "rat"}, cases *}
+
+subsection {* Equality and wellsortedness *}
+
+subsection {* Partiality *}
+
+text {* @{text "code_abort"}, examples: maps *}
+
+end
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML	Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML	Sun Sep 14 21:50:35 2008 +0200
@@ -2,3 +2,11 @@
 (* $Id$ *)
 
 use_thy "Codegen";
+
+(*no_document use_thy "Setup";
+
+use_thy "Introduction";
+use_thy "Program";
+use_thy "Adaption";
+use_thy "Further";
+use_thy "ML";*)
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/Thy/Setup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Sun Sep 14 21:50:35 2008 +0200
@@ -0,0 +1,8 @@
+theory Setup
+imports Main
+uses "../../../antiquote_setup.ML"
+begin
+
+ML_val {* Code_Target.code_width := 74 *}
+
+end
diff -r 44831b583999 -r b52f9205a02d doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Sun Sep 14 21:50:35 2008 +0200
@@ -80,10 +80,9 @@
 \maketitle
 
 \begin{abstract}
-  This tutorial gives a motivation-driven introduction
-  to a generic code generator framework in Isabelle
-  for generating executable code in functional
-  programming languages from logical specifications.
+  This tutorial gives am introduction to a generic code generator framework in Isabelle
+  for generating executable code in functional programming languages from logical
+  specifications in Isabelle/HOL.
 \end{abstract}
 
 \thispagestyle{empty}\clearpage
@@ -92,6 +91,11 @@
 \clearfirst
 
 \input{Thy/document/Codegen.tex}
+% \input{Thy/document/Introduction.tex}
+% \input{Thy/document/Program.tex}
+% \input{Thy/document/Adaption.tex}
+% \input{Thy/document/Further.tex}
+% \input{Thy/document/ML.tex}
 
 \begingroup
 %\tocentry{\bibname}