# HG changeset patch # User haftmann # Date 1285333898 -7200 # Node ID f75a01ee6c41dc12dc23fda965561de060ad26fc # Parent 066e2d4d0de89757faf2ef0b1401b8fcd9eb6b86 prefer typewrite tag over raw latex environment diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/Adaptation.thy Fri Sep 24 15:11:38 2010 +0200 @@ -175,10 +175,8 @@ code_const %invisible True and False and "op \" and Not (SML and and and) (*>*) -text %quote {* - \begin{typewriter} - @{code_stmts in_interval (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts in_interval (SML)} *} text {* @@ -208,10 +206,8 @@ placeholder for the type constructor's (the constant's) arguments. *} -text %quote {* - \begin{typewriter} - @{code_stmts in_interval (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts in_interval (SML)} *} text {* @@ -225,10 +221,8 @@ code_const %quotett "op \" (SML infixl 1 "andalso") -text %quote {* - \begin{typewriter} - @{code_stmts in_interval (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts in_interval (SML)} *} text {* diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/Foundations.thy --- a/doc-src/Codegen/Thy/Foundations.thy Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/Foundations.thy Fri Sep 24 15:11:38 2010 +0200 @@ -161,10 +161,8 @@ is determined syntactically. The resulting code: *} -text %quote {* - \begin{typewriter} - @{code_stmts dequeue (consts) dequeue (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts dequeue (consts) dequeue (Haskell)} *} text {* @@ -219,10 +217,8 @@ equality check, as can be seen in the corresponding @{text SML} code: *} -text %quote {* - \begin{typewriter} - @{code_stmts collect_duplicates (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts collect_duplicates (SML)} *} text {* @@ -259,10 +255,8 @@ for the pattern @{term "AQueue [] []"}: *} -text %quote {* - \begin{typewriter} - @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)} *} text {* @@ -302,10 +296,8 @@ exception at the appropriate position: *} -text %quote {* - \begin{typewriter} - @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)} *} text {* diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Fri Sep 24 15:11:38 2010 +0200 @@ -112,10 +112,8 @@ After this setup procedure, code generation can continue as usual: *} -text %quote {* - \begin{typewriter} - @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)} *} diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/Introduction.thy Fri Sep 24 15:11:38 2010 +0200 @@ -70,10 +70,8 @@ text {* \noindent resulting in the following code: *} -text %quote {* - \begin{typewriter} - @{code_stmts empty enqueue dequeue (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts empty enqueue dequeue (SML)} *} text {* @@ -95,10 +93,8 @@ \noindent This is the corresponding code: *} -text %quote {* - \begin{typewriter} - @{code_stmts empty enqueue dequeue (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts empty enqueue dequeue (Haskell)} *} text {* @@ -172,10 +168,8 @@ native classes: *} -text %quote {* - \begin{typewriter} - @{code_stmts bexp (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts bexp (Haskell)} *} text {* @@ -184,10 +178,8 @@ @{text SML}: *} -text %quote {* - \begin{typewriter} - @{code_stmts bexp (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts bexp (SML)} *} text {* diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/Refinement.thy --- a/doc-src/Codegen/Thy/Refinement.thy Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/Refinement.thy Fri Sep 24 15:11:38 2010 +0200 @@ -31,10 +31,8 @@ to two recursive calls: *} -text %quote {* - \begin{typewriter} - @{code_stmts fib (consts) fib (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts fib (consts) fib (Haskell)} *} text {* @@ -71,10 +69,8 @@ \noindent The resulting code shows only linear growth of runtime: *} -text %quote {* - \begin{typewriter} - @{code_stmts fib (consts) fib fib_step (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts fib (consts) fib fib_step (Haskell)} *} @@ -161,10 +157,8 @@ \noindent The resulting code looks as expected: *} -text %quote {* - \begin{typewriter} - @{code_stmts empty enqueue dequeue (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts empty enqueue dequeue (SML)} *} text {* @@ -259,10 +253,8 @@ \noindent Then the corresponding code is as follows: *} -text %quote {* - \begin{typewriter} - @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)} *} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *) text {* diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Fri Sep 24 15:11:38 2010 +0200 @@ -228,15 +228,14 @@ % \endisadeliminvisible % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline \ \ datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False\isanewline \ \ val\ conj\ {\isacharcolon}\ boola\ {\isacharminus}{\isachargreater}\ boola\ {\isacharminus}{\isachargreater}\ boola\isanewline @@ -261,18 +260,16 @@ \isanewline fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ conj\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent Though this is correct code, it is a little bit @@ -314,15 +311,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline \ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline \ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline @@ -338,18 +334,16 @@ \isanewline fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ andalso\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent This still is not perfect: the parentheses around the @@ -375,15 +369,14 @@ % \endisadelimquotett % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline \ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline \ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline @@ -399,18 +392,16 @@ \isanewline fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n\ andalso\ less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent The attentive reader may ask how we assert that no diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/document/Foundations.tex --- a/doc-src/Codegen/Thy/document/Foundations.tex Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Fri Sep 24 15:11:38 2010 +0200 @@ -238,29 +238,27 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline +dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline \ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline -\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon} - \end{typewriter}% +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has @@ -269,7 +267,7 @@ This possibility to select arbitrary code equations is the key technique for program and datatype refinement (see - \secref{sec:refinement}. + \secref{sec:refinement}). Due to the preprocessor, there is the distinction of raw code equations (before preprocessing) and code equations (after @@ -340,15 +338,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ type\ {\isacharprime}a\ equal\isanewline \ \ val\ equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline \ \ val\ eq\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline @@ -372,18 +369,16 @@ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}\isanewline \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent Obviously, polymorphic equality is implemented the Haskell @@ -436,30 +431,28 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline +strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline \ \ let\ {\isacharbraceleft}\isanewline \ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ xs{\isacharsemicolon}\isanewline \ \ {\isacharbraceright}\ in\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline -strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon} - \end{typewriter}% +strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent In some cases it is desirable to have this @@ -527,32 +520,30 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline +empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline empty{\isacharunderscore}queue\ {\isacharequal}\ error\ {\isachardoublequote}empty{\isacharunderscore}queue{\isachardoublequote}{\isacharsemicolon}\isanewline \isanewline strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline \ \ {\isacharparenleft}if\ null\ xs\ then\ empty{\isacharunderscore}queue\isanewline -\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon} - \end{typewriter}% +\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent This feature however is rarely needed in practice. Note diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Fri Sep 24 15:11:38 2010 +0200 @@ -207,31 +207,29 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline +funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline funpow\ Zero{\isacharunderscore}nat\ f\ {\isacharequal}\ id{\isacharsemicolon}\isanewline funpow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ f\ {\isacharequal}\ f\ {\isachardot}\ funpow\ n\ f{\isacharsemicolon}\isanewline \isanewline funpows\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharbrackleft}Nat{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline funpows\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isacharsemicolon}\isanewline -funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon} - \end{typewriter}% +funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \isamarkupsubsection{Imperative data structures% } diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Fri Sep 24 15:11:38 2010 +0200 @@ -133,15 +133,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline \ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline \ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline @@ -173,18 +172,16 @@ \isanewline fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a @@ -219,15 +216,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - module\ Example\ where\ {\isacharbraceleft}\isanewline +module\ Example\ where\ {\isacharbraceleft}\isanewline \isanewline data\ Queue\ a\ {\isacharequal}\ AQueue\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline \isanewline @@ -245,18 +241,16 @@ enqueue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a\ {\isacharminus}{\isachargreater}\ Queue\ a\ {\isacharminus}{\isachargreater}\ Queue\ a{\isacharsemicolon}\isanewline enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ ys{\isacharsemicolon}\isanewline \isanewline -{\isacharbraceright}\isanewline - - \end{typewriter}% +{\isacharbraceright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see @@ -388,15 +382,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - module\ Example\ where\ {\isacharbraceleft}\isanewline +module\ Example\ where\ {\isacharbraceleft}\isanewline \isanewline data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline \isanewline @@ -434,18 +427,16 @@ bexp\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -{\isacharbraceright}\isanewline - - \end{typewriter}% +{\isacharbraceright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent This is a convenient place to show how explicit dictionary @@ -454,15 +445,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline \ \ val\ plus{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline \ \ type\ {\isacharprime}a\ semigroup\isanewline @@ -505,18 +495,16 @@ \isanewline fun\ bexp\ n\ {\isacharequal}\ pow\ monoid{\isacharunderscore}nat\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.% diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Fri Sep 24 15:11:38 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Fri Sep 24 15:11:38 2010 +0200 @@ -65,28 +65,26 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline +fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline -fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon} - \end{typewriter}% +fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% \noindent A more efficient implementation would use dynamic @@ -163,15 +161,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline +fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline @@ -179,17 +176,16 @@ \isanewline fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline -fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon} - \end{typewriter}% +fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \isamarkupsubsection{Datatype refinement% } @@ -341,15 +337,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - structure\ Example\ {\isacharcolon}\ sig\isanewline +structure\ Example\ {\isacharcolon}\ sig\isanewline \ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline \ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline \ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline @@ -381,18 +376,16 @@ \isanewline fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline - - \end{typewriter}% +end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% The same techniques can also be applied to types which are not @@ -578,15 +571,14 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % -\isatagquote +\isatagtypewriter % \begin{isamarkuptext}% -\begin{typewriter} - module\ Example\ where\ {\isacharbraceleft}\isanewline +module\ Example\ where\ {\isacharbraceleft}\isanewline \isanewline newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline \isanewline @@ -613,18 +605,16 @@ remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline \isanewline -{\isacharbraceright}\isanewline - - \end{typewriter}% +{\isacharbraceright}\isanewline% \end{isamarkuptext}% \isamarkuptrue% % -\endisatagquote -{\isafoldquote}% +\endisatagtypewriter +{\isafoldtypewriter}% % -\isadelimquote +\isadelimtypewriter % -\endisadelimquote +\endisadelimtypewriter % \begin{isamarkuptext}% Typical data structures implemented by representations involving