1.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Aug 20 13:39:41 2012 +0200
1.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Aug 20 13:58:06 2012 +0200
1.3 @@ -141,7 +141,6 @@
1.4 %
1.5 \begin{isamarkuptext}%
1.6 structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
1.7 -\ \ val\ id\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
1.8 \ \ val\ fold\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\isanewline
1.9 \ \ val\ rev\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline
1.10 \ \ datatype\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ of\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline
1.11 @@ -150,10 +149,8 @@
1.12 \ \ val\ enqueue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline
1.13 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
1.14 \isanewline
1.15 -fun\ id\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fn\ xa\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ xa{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.16 -\isanewline
1.17 -fun\ fold\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id\isanewline
1.18 -\ \ {\isaliteral{7C}{\isacharbar}}\ fold\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fold\ f\ xs\ o\ f\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.19 +fun\ fold\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ s\ {\isaliteral{3D}{\isacharequal}}\ fold\ f\ xs\ {\isaliteral{28}{\isacharparenleft}}f\ x\ s{\isaliteral{29}{\isacharparenright}}\isanewline
1.20 +\ \ {\isaliteral{7C}{\isacharbar}}\ fold\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ s\ {\isaliteral{3D}{\isacharequal}}\ s{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.21 \isanewline
1.22 fun\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ fold\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ b\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ b{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
1.23 \isanewline
2.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex Mon Aug 20 13:39:41 2012 +0200
2.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Mon Aug 20 13:58:06 2012 +0200
2.3 @@ -349,7 +349,6 @@
2.4 %
2.5 \begin{isamarkuptext}%
2.6 structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
2.7 -\ \ val\ id\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
2.8 \ \ val\ fold\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\isanewline
2.9 \ \ val\ rev\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline
2.10 \ \ val\ null\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline
2.11 @@ -361,10 +360,8 @@
2.12 \ \ val\ queue{\isaliteral{5F}{\isacharunderscore}}case\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\isanewline
2.13 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
2.14 \isanewline
2.15 -fun\ id\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fn\ xa\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ xa{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline
2.16 -\isanewline
2.17 -fun\ fold\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id\isanewline
2.18 -\ \ {\isaliteral{7C}{\isacharbar}}\ fold\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fold\ f\ xs\ o\ f\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline
2.19 +fun\ fold\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ s\ {\isaliteral{3D}{\isacharequal}}\ fold\ f\ xs\ {\isaliteral{28}{\isacharparenleft}}f\ x\ s{\isaliteral{29}{\isacharparenright}}\isanewline
2.20 +\ \ {\isaliteral{7C}{\isacharbar}}\ fold\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ s\ {\isaliteral{3D}{\isacharequal}}\ s{\isaliteral{3B}{\isacharsemicolon}}\isanewline
2.21 \isanewline
2.22 fun\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ fold\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ b\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ b{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
2.23 \isanewline
3.1 --- a/doc-src/Codegen/Thy/examples/example.ML Mon Aug 20 13:39:41 2012 +0200
3.2 +++ b/doc-src/Codegen/Thy/examples/example.ML Mon Aug 20 13:58:06 2012 +0200
3.3 @@ -1,5 +1,4 @@
3.4 structure Example : sig
3.5 - val id : 'a -> 'a
3.6 val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
3.7 val rev : 'a list -> 'a list
3.8 datatype 'a queue = AQueue of 'a list * 'a list
3.9 @@ -8,10 +7,8 @@
3.10 val enqueue : 'a -> 'a queue -> 'a queue
3.11 end = struct
3.12
3.13 -fun id x = (fn xa => xa) x;
3.14 -
3.15 -fun fold f [] = id
3.16 - | fold f (x :: xs) = fold f xs o f x;
3.17 +fun fold f (x :: xs) s = fold f xs (f x s)
3.18 + | fold f [] s = s;
3.19
3.20 fun rev xs = fold (fn a => fn b => a :: b) xs [];
3.21