# HG changeset patch
# User haftmann
# Date 1238068869 -3600
# Node ID ab05be086c4a68a82c28f9567eaf41dba396659a
# Parent  4cf38ea4fad2416168c1a5a15f28db569bfb137c
step towards proper pictures in dvi

diff -r 4cf38ea4fad2 -r ab05be086c4a doc-src/Codegen/Makefile
--- a/doc-src/Codegen/Makefile	Mon Mar 23 08:16:24 2009 +0100
+++ b/doc-src/Codegen/Makefile	Thu Mar 26 13:01:09 2009 +0100
@@ -17,7 +17,7 @@
 
 dvi: $(NAME).dvi
 
-$(NAME).dvi: $(FILES) isabelle_isar.eps codegen_process.ps
+$(NAME).dvi: $(FILES) isabelle_isar.eps Thy/pictures/architecture.eps Thy/pictures/adaption.eps
 	$(LATEX) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -25,7 +25,7 @@
 
 pdf: $(NAME).pdf
 
-$(NAME).pdf: $(FILES) isabelle_isar.pdf codegen_process.pdf
+$(NAME).pdf: $(FILES) isabelle_isar.pdf Thy/pictures/architecture.pdf Thy/pictures/adaption.pdf
 	$(PDFLATEX) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
@@ -33,3 +33,12 @@
 	$(FIXBOOKMARKS) $(NAME).out
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
+
+Thy/pictures/%.dvi: Thy/pictures/%.tex
+	latex -output-directory=$(dir $@) $<
+
+Thy/pictures/%.eps: Thy/pictures/%.dvi
+	dvips -E -o $@ $<
+
+Thy/pictures/%.pdf: Thy/pictures/%.eps
+	epstopdf --outfile=$@ $<
diff -r 4cf38ea4fad2 -r ab05be086c4a doc-src/Codegen/Thy/ROOT.ML
--- a/doc-src/Codegen/Thy/ROOT.ML	Mon Mar 23 08:16:24 2009 +0100
+++ b/doc-src/Codegen/Thy/ROOT.ML	Thu Mar 26 13:01:09 2009 +0100
@@ -1,5 +1,3 @@
-
-(* $Id$ *)
 
 no_document use_thy "Setup";
 no_document use_thys ["Efficient_Nat"];
diff -r 4cf38ea4fad2 -r ab05be086c4a doc-src/Codegen/Thy/pictures/adaption.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex	Thu Mar 26 13:01:09 2009 +0100
@@ -0,0 +1,46 @@
+
+\documentclass[12pt]{article}
+\usepackage{pgf}
+\usepackage{pgflibraryshapes}
+\usepackage{tikz}
+
+\begin{document}
+
+\begin{tikzpicture}[scale = 0.5]
+  \tikzstyle water=[color = blue, thick]
+  \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
+  \tikzstyle process=[color = green, semithick, ->]
+  \tikzstyle adaption=[color = red, semithick, ->]
+  \tikzstyle target=[color = black]
+  \foreach \x in {0, ..., 24}
+    \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
+      + (0.25, -0.25) cos + (0.25, 0.25);
+  \draw[style=ice] (1, 0) --
+    (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
+  \draw[style=ice] (9, 0) --
+    (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
+  \draw[style=ice] (15, -6) --
+    (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
+  \draw[style=process]
+    (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
+  \draw[style=process]
+    (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
+  \node (adaption) at (11, -2) [style=adaption] {adaption};
+  \node at (19, 3) [rotate=90] {generated};
+  \node at (19.5, -5) {language};
+  \node at (19.5, -3) {library};
+  \node (includes) at (19.5, -1) {includes};
+  \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
+  \draw[style=process]
+    (includes) -- (serialisation);
+  \draw[style=process]
+    (reserved) -- (serialisation);
+  \draw[style=adaption]
+    (adaption) -- (serialisation);
+  \draw[style=adaption]
+    (adaption) -- (includes);
+  \draw[style=adaption]
+    (adaption) -- (reserved);
+\end{tikzpicture}
+
+\end{document}
diff -r 4cf38ea4fad2 -r ab05be086c4a doc-src/Codegen/Thy/pictures/architecture.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex	Thu Mar 26 13:01:09 2009 +0100
@@ -0,0 +1,33 @@
+
+\documentclass[12pt]{article}
+\usepackage{pgf}
+\usepackage{pgflibraryshapes}
+\usepackage{tikz}
+
+\begin{document}
+
+\begin{tikzpicture}[x = 4.2cm, y = 1cm]
+  \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
+  \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
+  \tikzstyle process_arrow=[->, semithick, color = green];
+  \node (HOL) at (0, 4) [style=entity] {Isabelle/HOL theory};
+  \node (eqn) at (2, 2) [style=entity] {code equations};
+  \node (iml) at (2, 0) [style=entity] {intermediate language};
+  \node (seri) at (1, 0) [style=process] {serialisation};
+  \node (SML) at (0, 3) [style=entity] {SML};
+  \node (OCaml) at (0, 2) [style=entity] {OCaml};
+  \node (further) at (0, 1) [style=entity] {\ldots};
+  \node (Haskell) at (0, 0) [style=entity] {Haskell};
+  \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
+    node [style=process, near start] {selection}
+    node [style=process, near end] {preprocessing}
+    (eqn);
+  \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
+  \draw [style=process_arrow] (iml) -- (seri);
+  \draw [style=process_arrow] (seri) -- (SML);
+  \draw [style=process_arrow] (seri) -- (OCaml);
+  \draw [style=process_arrow, dashed] (seri) -- (further);
+  \draw [style=process_arrow] (seri) -- (Haskell);
+\end{tikzpicture}
+
+\end{document}
diff -r 4cf38ea4fad2 -r ab05be086c4a doc-src/Codegen/codegen_process.pdf
Binary file doc-src/Codegen/codegen_process.pdf has changed
diff -r 4cf38ea4fad2 -r ab05be086c4a doc-src/Codegen/codegen_process.ps
--- a/doc-src/Codegen/codegen_process.ps	Mon Mar 23 08:16:24 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,586 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005)
-%%For: (haftmann) Florian Haftmann
-%%Title: _anonymous_0
-%%Pages: (atend)
-%%BoundingBox: 35 35 451 291
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
-  dup 306 /AE
-  dup 301 /Aacute
-  dup 302 /Acircumflex
-  dup 304 /Adieresis
-  dup 300 /Agrave
-  dup 305 /Aring
-  dup 303 /Atilde
-  dup 307 /Ccedilla
-  dup 311 /Eacute
-  dup 312 /Ecircumflex
-  dup 313 /Edieresis
-  dup 310 /Egrave
-  dup 315 /Iacute
-  dup 316 /Icircumflex
-  dup 317 /Idieresis
-  dup 314 /Igrave
-  dup 334 /Udieresis
-  dup 335 /Yacute
-  dup 376 /thorn
-  dup 337 /germandbls
-  dup 341 /aacute
-  dup 342 /acircumflex
-  dup 344 /adieresis
-  dup 346 /ae
-  dup 340 /agrave
-  dup 345 /aring
-  dup 347 /ccedilla
-  dup 351 /eacute
-  dup 352 /ecircumflex
-  dup 353 /edieresis
-  dup 350 /egrave
-  dup 355 /iacute
-  dup 356 /icircumflex
-  dup 357 /idieresis
-  dup 354 /igrave
-  dup 360 /dcroat
-  dup 361 /ntilde
-  dup 363 /oacute
-  dup 364 /ocircumflex
-  dup 366 /odieresis
-  dup 362 /ograve
-  dup 365 /otilde
-  dup 370 /oslash
-  dup 372 /uacute
-  dup 373 /ucircumflex
-  dup 374 /udieresis
-  dup 371 /ugrave
-  dup 375 /yacute
-  dup 377 /ydieresis  
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
-        dup dup findfont dup length dict begin
-        { 1 index /FID ne { def }{ pop pop } ifelse
-        } forall
-        /Encoding EncodingVector def
-        currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
-	dup 1 exch div /InvScaleFactor exch def
-	dup scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color 
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage {	% i j npages
-	/npages exch def
-	/j exch def
-	/i exch def
-	/str 10 string def
-	npages 1 gt {
-		gsave
-			coordfont setfont
-			0 0 moveto
-			(\() show i str cvs show (,) show j str cvs show (\)) show
-		grestore
-	} if
-} bind def
-
-/set_font {
-	findfont exch
-	scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext {			% width adj text
-	/text exch def
-	/adj exch def
-	/width exch def
-	gsave
-		width 0 gt {
-			text stringwidth pop adj mul 0 rmoveto
-		} if
-		[] 0 setdash
-		text show
-	grestore
-} def
-
-/boxprim {				% xcorner ycorner xsize ysize
-		4 2 roll
-		moveto
-		2 copy
-		exch 0 rlineto
-		0 exch rlineto
-		pop neg 0 rlineto
-		closepath
-} bind def
-
-/ellipse_path {
-	/ry exch def
-	/rx exch def
-	/y exch def
-	/x exch def
-	matrix currentmatrix
-	newpath
-	x y translate
-	rx ry scale
-	0 0 1 0 360 arc
-	setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
-	[	% layer color sequence - darkest to lightest
-		[0 0 0]
-		[.2 .8 .8]
-		[.4 .8 .8]
-		[.6 .8 .8]
-		[.8 .8 .8]
-	]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
-	layercolorseq curlayer 1 sub layerlen mod get
-	aload pop sethsbcolor
-	/nodecolor {nopcolor} def
-	/edgecolor {nopcolor} def
-	/graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
-	/myupper exch def
-	/mylower exch def
-	curlayer mylower lt
-	curlayer myupper gt
-	or
-	{invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
-    userdict (<<) cvn ([) cvn load put
-    userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-%%Page: 1 1
-%%PageBoundingBox: 36 36 451 291
-%%PageOrientation: Portrait
-gsave
-35 35 416 256 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0 0 translate 0 rotate
-[ /CropBox [36 36 451 291] /PAGES pdfmark
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-%	theory
-gsave 10 dict begin
-newpath 93 254 moveto
-1 254 lineto
-1 214 lineto
-93 214 lineto
-closepath
-stroke
-gsave 10 dict begin
-8 237 moveto
-(Isabelle/HOL)
-[4.56 5.52 6.24 6.96 6.24 3.84 3.84 6.24 3.84 10.08 10.08 8.64]
-xshow
-16 221 moveto
-(Isar theory)
-[4.56 5.52 6.24 4.56 3.6 4.08 6.96 6.24 6.96 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	selection
-gsave 10 dict begin
-183 234 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-158 229 moveto
-(selection)
-[5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	theory -> selection
-newpath 94 234 moveto
-107 234 121 234 135 234 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 135 238 moveto
-145 234 lineto
-135 231 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 135 238 moveto
-145 234 lineto
-135 231 lineto
-closepath
-stroke
-end grestore
-
-%	sml
-gsave 10 dict begin
-newpath 74 144 moveto
-20 144 lineto
-20 108 lineto
-74 108 lineto
-closepath
-stroke
-gsave 10 dict begin
-32 121 moveto
-(SML)
-[7.68 12.48 8.64]
-xshow
-end grestore
-end grestore
-
-%	other
-gsave 10 dict begin
-gsave 10 dict begin
-41 67 moveto
-(...)
-[3.6 3.6 3.6]
-xshow
-end grestore
-end grestore
-
-%	haskell
-gsave 10 dict begin
-newpath 77 36 moveto
-17 36 lineto
-17 0 lineto
-77 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-25 13 moveto
-(Haskell)
-[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-%	preprocessing
-gsave 10 dict begin
-183 180 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-143 175 moveto
-(preprocessing)
-[6.96 4.56 6.24 6.96 4.56 6.96 6.24 6.24 5.52 5.52 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	selection -> preprocessing
-newpath 183 216 moveto
-183 213 183 211 183 208 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 187 208 moveto
-183 198 lineto
-180 208 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 187 208 moveto
-183 198 lineto
-180 208 lineto
-closepath
-stroke
-end grestore
-
-%	def_eqn
-gsave 10 dict begin
-newpath 403 198 moveto
-283 198 lineto
-283 162 lineto
-403 162 lineto
-closepath
-stroke
-gsave 10 dict begin
-291 175 moveto
-(defining equations)
-[6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	preprocessing -> def_eqn
-newpath 236 180 moveto
-248 180 260 180 273 180 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 273 184 moveto
-283 180 lineto
-273 177 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 273 184 moveto
-283 180 lineto
-273 177 lineto
-closepath
-stroke
-end grestore
-
-%	serialization
-gsave 10 dict begin
-183 72 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-148 67 moveto
-(serialization)
-[5.52 6.24 4.8 3.84 6.24 3.84 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	serialization -> sml
-newpath 150 85 moveto
-129 93 104 103 83 111 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 82 108 moveto
-74 115 lineto
-85 114 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 82 108 moveto
-74 115 lineto
-85 114 lineto
-closepath
-stroke
-end grestore
-
-%	serialization -> other
-gsave 10 dict begin
-dotted
-newpath 135 72 moveto
-119 72 100 72 84 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 84 69 moveto
-74 72 lineto
-84 76 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 84 69 moveto
-74 72 lineto
-84 76 lineto
-closepath
-stroke
-end grestore
-end grestore
-
-%	serialization -> haskell
-newpath 150 59 moveto
-131 51 107 42 86 34 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 88 31 moveto
-77 30 lineto
-85 37 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 88 31 moveto
-77 30 lineto
-85 37 lineto
-closepath
-stroke
-end grestore
-
-%	translation
-gsave 10 dict begin
-343 126 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-313 121 moveto
-(translation)
-[3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	def_eqn -> translation
-newpath 343 162 moveto
-343 159 343 157 343 154 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 347 154 moveto
-343 144 lineto
-340 154 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 347 154 moveto
-343 144 lineto
-340 154 lineto
-closepath
-stroke
-end grestore
-
-%	iml
-gsave 10 dict begin
-newpath 413 90 moveto
-273 90 lineto
-273 54 lineto
-413 54 lineto
-closepath
-stroke
-gsave 10 dict begin
-280 67 moveto
-(intermediate language)
-[3.84 6.96 3.84 6.24 4.8 10.8 6.24 6.96 3.84 6.24 3.84 6.24 3.6 3.84 6.24 6.96 6.96 6.96 6.24 6.72 6.24]
-xshow
-end grestore
-end grestore
-
-%	translation -> iml
-newpath 343 108 moveto
-343 105 343 103 343 100 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 347 100 moveto
-343 90 lineto
-340 100 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 347 100 moveto
-343 90 lineto
-340 100 lineto
-closepath
-stroke
-end grestore
-
-%	iml -> serialization
-newpath 272 72 moveto
-262 72 251 72 241 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 241 69 moveto
-231 72 lineto
-241 76 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 241 69 moveto
-231 72 lineto
-241 76 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF