--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Mon Nov 06 16:28:30 2006 +0100
@@ -0,0 +1,14 @@
+structure ROOT =
+struct
+
+structure Codegen =
+struct
+
+val arbitrary_option : 'a option = NONE;
+
+fun dummy_option [] = arbitrary_option
+ | dummy_option (x :: xs) = SOME x;
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML Mon Nov 06 16:28:30 2006 +0100
@@ -9,24 +9,23 @@
end; (*struct HOL*)
-structure IntDef =
+structure Nat =
struct
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Succ_nat n) = true
+fun less_nat Zero_nat (Suc n) = true
| less_nat n Zero_nat = false
- | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
+ | less_nat (Suc m) (Suc n) = less_nat m n;
fun less_eq_nat m n = HOL.nota (less_nat n m);
-end; (*struct IntDef*)
+end; (*struct Nat*)
structure Codegen =
struct
-fun in_interval (k, l) n =
- IntDef.less_eq_nat k n andalso IntDef.less_eq_nat n l;
+fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Mon Nov 06 16:28:30 2006 +0100
@@ -1,28 +1,28 @@
structure ROOT =
struct
-structure IntDef =
+structure Nat =
struct
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
-end; (*struct IntDef*)
+end; (*struct Nat*)
structure Codegen =
struct
type 'a null = {null_ : 'a};
-fun Null (A_:'a null) = #null_ A_;
+fun null (A_:'a null) = #null_ A_;
fun head (A_1_:'a_1 null) (y :: xs) = y
- | head (A_1_:'a_1 null) [] = Null A_1_;
+ | head (A_1_:'a_1 null) [] = null A_1_;
val null_option : 'b option = NONE;
fun null_optiona () = {null_ = null_option} : ('b option) null
-val dummy : IntDef.nat option =
- head (null_optiona ()) [SOME (IntDef.Succ_nat IntDef.Zero_nat), NONE];
+val dummy : Nat.nat option =
+ head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Mon Nov 06 16:28:30 2006 +0100
@@ -5,14 +5,14 @@
struct
type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun Eq (A_:'a eq) = #eq_ A_;
+fun eq (A_:'a eq) = #eq_ A_;
end; (*struct Code_Generator*)
structure HOL =
struct
-fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.Eq A_ a b;
+fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.eq A_ a b;
end; (*struct HOL*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Mon Nov 06 16:28:30 2006 +0100
@@ -0,0 +1,22 @@
+structure ROOT =
+struct
+
+structure Nat =
+struct
+
+datatype nat = Zero_nat | Suc of nat;
+
+end; (*struct Nat*)
+
+structure Codegen =
+struct
+
+val dummy_set : Nat.nat -> Nat.nat list = Nat.Suc :: [];
+
+val foobar_set : Nat.nat list =
+ Nat.Zero_nat ::
+ (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Mon Nov 06 16:28:30 2006 +0100
@@ -1,24 +1,24 @@
structure ROOT =
struct
-structure IntDef =
+structure Nat =
struct
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
-fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
+fun plus_nat (Suc m) n = plus_nat m (Suc n)
| plus_nat Zero_nat y = y;
-fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
| times_nat Zero_nat n = Zero_nat;
-end; (*struct IntDef*)
+end; (*struct Nat*)
structure Codegen =
struct
-fun fac (IntDef.Succ_nat n) = IntDef.times_nat (IntDef.Succ_nat n) (fac n)
- | fac IntDef.Zero_nat = IntDef.Succ_nat IntDef.Zero_nat;
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
+ | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Mon Nov 06 16:28:30 2006 +0100
@@ -1,25 +1,25 @@
structure ROOT =
struct
-structure IntDef =
+structure Nat =
struct
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
-fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
+fun plus_nat (Suc m) n = plus_nat m (Suc n)
| plus_nat Zero_nat y = y;
-fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
| times_nat Zero_nat n = Zero_nat;
-end; (*struct IntDef*)
+end; (*struct Nat*)
structure Codegen =
struct
fun fac n =
- (case n of IntDef.Zero_nat => IntDef.Succ_nat IntDef.Zero_nat
- | IntDef.Succ_nat ma => IntDef.times_nat n (fac ma));
+ (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
+ | Nat.Suc ma => Nat.times_nat n (fac ma));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Mon Nov 06 16:28:30 2006 +0100
@@ -5,7 +5,7 @@
struct
type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun Eq (A_:'a eq) = #eq_ A_;
+fun eq (A_:'a eq) = #eq_ A_;
end; (*struct Code_Generator*)
@@ -13,38 +13,37 @@
struct
fun eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
- (x2, y2) = Code_Generator.Eq A_ x1 x2 andalso Code_Generator.Eq B_ y1 y2;
+ (x2, y2) = Code_Generator.eq A_ x1 x2 andalso Code_Generator.eq B_ y1 y2;
end; (*struct Product_Type*)
structure Orderings =
struct
-type 'a ord =
- {Code_Generator__eq : 'a Code_Generator.eq, less_eq_ : 'a -> 'a -> bool,
- less_ : 'a -> 'a -> bool};
-fun Less_eq (A_:'a ord) = #less_eq_ A_;
-fun Less (A_:'a ord) = #less_ A_;
+type 'a ord = {less_eq_ : 'a -> 'a -> bool, less_ : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #less_eq_ A_;
+fun less (A_:'a ord) = #less_ A_;
end; (*struct Orderings*)
structure Codegen =
struct
-fun less_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 =
+fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
+ (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
let
val (x1a, y1a) = p1;
val (x2a, y2a) = p2;
in
- Orderings.Less B_ x1a x2a orelse
- Code_Generator.Eq (#Code_Generator__eq B_) x1a x2a andalso
- Orderings.Less C_ y1a y2a
+ Orderings.less (#2 B_) x1a x2a orelse
+ Code_Generator.eq (#1 B_) x1a x2a andalso
+ Orderings.less (#2 C_) y1a y2a
end;
-fun less_eq_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 =
- less_prod B_ C_ p1 p2 orelse
- Product_Type.eq_prod (#Code_Generator__eq B_) (#Code_Generator__eq C_)
- p1 p2;
+fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
+ (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
+ less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
+ Product_Type.eq_prod (#1 B_) (#1 C_) p1 p2;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Mon Nov 06 16:28:30 2006 +0100
@@ -1,31 +1,31 @@
structure ROOT =
struct
-structure IntDef =
+structure Nat =
struct
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Succ_nat n) = true
+fun less_nat Zero_nat (Suc n) = true
| less_nat n Zero_nat = false
- | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
+ | less_nat (Suc m) (Suc n) = less_nat m n;
-fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
| minus_nat Zero_nat n = Zero_nat
| minus_nat y Zero_nat = y;
-end; (*struct IntDef*)
+end; (*struct Nat*)
structure Codegen =
struct
fun pick ((k, v) :: xs) n =
- (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k))
+ (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
| pick (x :: xs) n =
let
val (ka, va) = x;
in
- (if IntDef.less_nat n ka then va else pick xs (IntDef.minus_nat n ka))
+ (if Nat.less_nat n ka then va else pick xs (Nat.minus_nat n ka))
end;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Mon Nov 06 16:28:30 2006 +0100
@@ -1,26 +1,26 @@
structure ROOT =
struct
-structure IntDef =
+structure Nat =
struct
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Succ_nat n) = true
+fun less_nat Zero_nat (Suc n) = true
| less_nat n Zero_nat = false
- | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
+ | less_nat (Suc m) (Suc n) = less_nat m n;
-fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
| minus_nat Zero_nat n = Zero_nat
| minus_nat y Zero_nat = y;
-end; (*struct IntDef*)
+end; (*struct Nat*)
structure Codegen =
struct
fun pick ((k, v) :: xs) n =
- (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k));
+ (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Nov 06 16:28:30 2006 +0100
@@ -40,6 +40,8 @@
\newcommand{\isasymCODERESERVED}{\cmd{code\_reserved}}
\newcommand{\isasymCODEMODULENAME}{\cmd{code\_modulename}}
\newcommand{\isasymCODEMODULEPROLOG}{\cmd{code\_moduleprolog}}
+\newcommand{\isasymCODEAXIOMS}{\cmd{code\_axioms}}
+\newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}}
\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
\newcommand{\isasymFUN}{\cmd{fun}}
\newcommand{\isasymFUNCTION}{\cmd{function}}
--- a/doc-src/IsarAdvanced/Codegen/codegen_process.eps Mon Nov 06 16:28:29 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,582 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005)
-%%For: (haftmann) Florian Haftmann
-%%Title: _anonymous_0
-%%Pages: (atend)
-%%BoundingBox: 35 35 241 577
-%%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 241 577
-%%PageOrientation: Portrait
-gsave
-35 35 206 542 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0 0 translate 0 rotate
-[ /CropBox [36 36 241 577] /PAGES pdfmark
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-% theory
-gsave 10 dict begin
-newpath 126 540 moveto
-72 540 lineto
-72 504 lineto
-126 504 lineto
-closepath
-stroke
-gsave 10 dict begin
-80 517 moveto
-(theory)
-[4.08 6.96 6.24 6.96 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-% selection
-gsave 10 dict begin
-99 450 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-74 445 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 99 504 moveto
-99 496 99 487 99 478 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 478 moveto
-99 468 lineto
-96 478 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 478 moveto
-99 468 lineto
-96 478 lineto
-closepath
-stroke
-end grestore
-
-% preprocessing
-gsave 10 dict begin
-99 378 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-59 373 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 99 432 moveto
-99 424 99 415 99 406 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 406 moveto
-99 396 lineto
-96 406 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 406 moveto
-99 396 lineto
-96 406 lineto
-closepath
-stroke
-end grestore
-
-% code_thm
-gsave 10 dict begin
-newpath 148 324 moveto
-50 324 lineto
-50 288 lineto
-148 288 lineto
-closepath
-stroke
-gsave 10 dict begin
-58 301 moveto
-(code theorems)
-[6.24 6.96 6.96 6.24 3.6 4.08 6.96 6.24 6.96 4.56 6.24 10.8 5.52]
-xshow
-end grestore
-end grestore
-
-% preprocessing -> code_thm
-newpath 99 360 moveto
-99 352 99 343 99 334 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 334 moveto
-99 324 lineto
-96 334 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 334 moveto
-99 324 lineto
-96 334 lineto
-closepath
-stroke
-end grestore
-
-% extraction
-gsave 10 dict begin
-99 234 41 18 ellipse_path
-stroke
-gsave 10 dict begin
-71 229 moveto
-(extraction)
-[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% code_thm -> extraction
-newpath 99 288 moveto
-99 280 99 271 99 262 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 262 moveto
-99 252 lineto
-96 262 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 262 moveto
-99 252 lineto
-96 262 lineto
-closepath
-stroke
-end grestore
-
-% iml
-gsave 10 dict begin
-newpath 169 180 moveto
-29 180 lineto
-29 144 lineto
-169 144 lineto
-closepath
-stroke
-gsave 10 dict begin
-36 157 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
-
-% extraction -> iml
-newpath 99 216 moveto
-99 208 99 199 99 190 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 190 moveto
-99 180 lineto
-96 190 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 190 moveto
-99 180 lineto
-96 190 lineto
-closepath
-stroke
-end grestore
-
-% serialization
-gsave 10 dict begin
-99 90 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-64 85 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
-
-% iml -> serialization
-newpath 99 144 moveto
-99 136 99 127 99 118 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 118 moveto
-99 108 lineto
-96 118 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 118 moveto
-99 108 lineto
-96 118 lineto
-closepath
-stroke
-end grestore
-
-% sml
-gsave 10 dict begin
-newpath 54 36 moveto
-0 36 lineto
-0 0 lineto
-54 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-12 13 moveto
-(SML)
-[7.68 12.48 8.64]
-xshow
-end grestore
-end grestore
-
-% serialization -> sml
-newpath 82 73 moveto
-73 64 62 53 52 43 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 55 41 moveto
-45 36 lineto
-50 46 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 55 41 moveto
-45 36 lineto
-50 46 lineto
-closepath
-stroke
-end grestore
-
-% other
-gsave 10 dict begin
-gsave 10 dict begin
-93 13 moveto
-(...)
-[3.6 3.6 3.6]
-xshow
-end grestore
-end grestore
-
-% serialization -> other
-gsave 10 dict begin
-dotted
-newpath 99 72 moveto
-99 64 99 55 99 46 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 46 moveto
-99 36 lineto
-96 46 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 46 moveto
-99 36 lineto
-96 46 lineto
-closepath
-stroke
-end grestore
-end grestore
-
-% haskell
-gsave 10 dict begin
-newpath 204 36 moveto
-144 36 lineto
-144 0 lineto
-204 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-152 13 moveto
-(Haskell)
-[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-% serialization -> haskell
-newpath 117 73 moveto
-127 64 138 53 148 43 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 150 46 moveto
-155 36 lineto
-145 41 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 150 46 moveto
-155 36 lineto
-145 41 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF
Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed