# HG changeset patch # User haftmann # Date 1283439720 -7200 # Node ID 928c5a5bdc93848464195efd6e0fe417da503f4b # Parent c51e80de9b7e9d9f3f59aa83f34881b92055c70e# Parent 352bcd845998990531b2aa73af30b8a7a5d16676 merged diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Classes/Thy/document/Classes.tex --- a/doc-src/Classes/Thy/document/Classes.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Classes/Thy/document/Classes.tex Thu Sep 02 17:02:00 2010 +0200 @@ -1134,26 +1134,27 @@ \noindent% \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\ \hspace*{0pt}\\ -\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\ -\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\ +\hspace*{0pt}nat{\char95}aux ::~Integer -> Example.Nat -> Example.Nat;\\ +\hspace*{0pt}nat{\char95}aux i n =\\ +\hspace*{0pt} ~(if i <= 0 then n else Example.nat{\char95}aux (i - 1) (Example.Suc n));\\ \hspace*{0pt}\\ -\hspace*{0pt}nat ::~Integer -> Nat;\\ -\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\ +\hspace*{0pt}nat ::~Integer -> Example.Nat;\\ +\hspace*{0pt}nat i = Example.nat{\char95}aux i Example.Zero{\char95}nat;\\ \hspace*{0pt}\\ \hspace*{0pt}class Semigroup a where {\char123}\\ \hspace*{0pt} ~mult ::~a -> a -> a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\ +\hspace*{0pt}class (Example.Semigroup a) => Monoidl a where {\char123}\\ \hspace*{0pt} ~neutral ::~a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\ +\hspace*{0pt}class (Example.Monoidl a) => Monoid a where {\char123}\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\ +\hspace*{0pt}class (Example.Monoid a) => Group a where {\char123}\\ \hspace*{0pt} ~inverse ::~a -> a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ @@ -1166,32 +1167,32 @@ \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ \hspace*{0pt}inverse{\char95}int i = negate i;\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Semigroup Integer where {\char123}\\ -\hspace*{0pt} ~mult = mult{\char95}int;\\ +\hspace*{0pt}instance Example.Semigroup Integer where {\char123}\\ +\hspace*{0pt} ~mult = Example.mult{\char95}int;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Monoidl Integer where {\char123}\\ -\hspace*{0pt} ~neutral = neutral{\char95}int;\\ +\hspace*{0pt}instance Example.Monoidl Integer where {\char123}\\ +\hspace*{0pt} ~neutral = Example.neutral{\char95}int;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Monoid Integer where {\char123}\\ +\hspace*{0pt}instance Example.Monoid Integer where {\char123}\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Group Integer where {\char123}\\ -\hspace*{0pt} ~inverse = inverse{\char95}int;\\ +\hspace*{0pt}instance Example.Group Integer where {\char123}\\ +\hspace*{0pt} ~inverse = Example.inverse{\char95}int;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\ -\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\ -\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\ +\hspace*{0pt}pow{\char95}nat ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\ +\hspace*{0pt}pow{\char95}nat Example.Zero{\char95}nat x = Example.neutral;\\ +\hspace*{0pt}pow{\char95}nat (Example.Suc n) x = Example.mult x (Example.pow{\char95}nat n x);\\ \hspace*{0pt}\\ -\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\ +\hspace*{0pt}pow{\char95}int ::~forall a.~(Example.Group a) => Integer -> a -> a;\\ \hspace*{0pt}pow{\char95}int k x =\\ -\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\ -\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\ +\hspace*{0pt} ~(if 0 <= k then Example.pow{\char95}nat (Example.nat k) x\\ +\hspace*{0pt} ~~~else Example.inverse (Example.pow{\char95}nat (Example.nat (negate k)) x));\\ \hspace*{0pt}\\ \hspace*{0pt}example ::~Integer;\\ -\hspace*{0pt}example = pow{\char95}int 10 (-2);\\ +\hspace*{0pt}example = Example.pow{\char95}int 10 (-2);\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% \end{isamarkuptext}% @@ -1232,15 +1233,15 @@ \hspace*{0pt} ~type 'a group\\ \hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\ \hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\ +\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\ +\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\ \hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\ +\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ \hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\ -\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ -\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\ \hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\ \hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\ +\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\ \hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\ -\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\ -\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\ \hspace*{0pt} ~val example :~IntInf.int\\ \hspace*{0pt}end = struct\\ \hspace*{0pt}\\ @@ -1266,23 +1267,6 @@ \hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\ \hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ -\hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val monoidl{\char95}int =\\ -\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ -\hspace*{0pt} ~IntInf.int monoidl;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ -\hspace*{0pt} ~IntInf.int group;\\ -\hspace*{0pt}\\ \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ @@ -1292,6 +1276,23 @@ \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ \hspace*{0pt}\\ +\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ +\hspace*{0pt}\\ +\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ +\hspace*{0pt}\\ +\hspace*{0pt}val monoidl{\char95}int =\\ +\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ +\hspace*{0pt} ~IntInf.int monoidl;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ +\hspace*{0pt} ~IntInf.int group;\\ +\hspace*{0pt}\\ \hspace*{0pt}val example :~IntInf.int =\\ \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ \hspace*{0pt}\\ @@ -1335,9 +1336,6 @@ \noindent% \hspace*{0pt}object Example {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}import /*implicits*/ Example.semigroup{\char95}int,~Example.monoidl{\char95}int,\\ -\hspace*{0pt} ~Example.monoid{\char95}int,~Example.group{\char95}int\\ -\hspace*{0pt}\\ \hspace*{0pt}abstract sealed class nat\\ \hspace*{0pt}final case object Zero{\char95}nat extends nat\\ \hspace*{0pt}final case class Suc(a:~nat) extends nat\\ @@ -1348,23 +1346,23 @@ \hspace*{0pt}def nat(i:~BigInt):~nat = nat{\char95}aux(i,~Zero{\char95}nat)\\ \hspace*{0pt}\\ \hspace*{0pt}trait semigroup[A] {\char123}\\ -\hspace*{0pt} ~val `Example+mult`:~(A,~A) => A\\ +\hspace*{0pt} ~val `Example.mult`:~(A,~A) => A\\ \hspace*{0pt}{\char125}\\ \hspace*{0pt}def mult[A](a:~A,~b:~A)(implicit A:~semigroup[A]):~A =\\ -\hspace*{0pt} ~A.`Example+mult`(a,~b)\\ +\hspace*{0pt} ~A.`Example.mult`(a,~b)\\ \hspace*{0pt}\\ \hspace*{0pt}trait monoidl[A] extends semigroup[A] {\char123}\\ -\hspace*{0pt} ~val `Example+neutral`:~A\\ +\hspace*{0pt} ~val `Example.neutral`:~A\\ \hspace*{0pt}{\char125}\\ -\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example+neutral`\\ +\hspace*{0pt}def neutral[A](implicit A:~monoidl[A]):~A = A.`Example.neutral`\\ \hspace*{0pt}\\ \hspace*{0pt}trait monoid[A] extends monoidl[A] {\char123}\\ \hspace*{0pt}{\char125}\\ \hspace*{0pt}\\ \hspace*{0pt}trait group[A] extends monoid[A] {\char123}\\ -\hspace*{0pt} ~val `Example+inverse`:~A => A\\ +\hspace*{0pt} ~val `Example.inverse`:~A => A\\ \hspace*{0pt}{\char125}\\ -\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example+inverse`(a)\\ +\hspace*{0pt}def inverse[A](a:~A)(implicit A:~group[A]):~A = A.`Example.inverse`(a)\\ \hspace*{0pt}\\ \hspace*{0pt}def pow{\char95}nat[A:~monoid](xa0:~nat,~x:~A):~A = (xa0,~x) match {\char123}\\ \hspace*{0pt} ~case (Zero{\char95}nat,~x) => neutral[A]\\ @@ -1378,27 +1376,27 @@ \hspace*{0pt}def mult{\char95}int(i:~BigInt,~j:~BigInt):~BigInt = i + j\\ \hspace*{0pt}\\ \hspace*{0pt}implicit def semigroup{\char95}int:~semigroup[BigInt] = new semigroup[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ +\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ \hspace*{0pt}{\char125}\\ \hspace*{0pt}\\ \hspace*{0pt}def neutral{\char95}int:~BigInt = BigInt(0)\\ \hspace*{0pt}\\ \hspace*{0pt}implicit def monoidl{\char95}int:~monoidl[BigInt] = new monoidl[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\ -\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ +\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ +\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ \hspace*{0pt}{\char125}\\ \hspace*{0pt}\\ \hspace*{0pt}implicit def monoid{\char95}int:~monoid[BigInt] = new monoid[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\ -\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ +\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ +\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ \hspace*{0pt}{\char125}\\ \hspace*{0pt}\\ \hspace*{0pt}def inverse{\char95}int(i:~BigInt):~BigInt = (- i)\\ \hspace*{0pt}\\ \hspace*{0pt}implicit def group{\char95}int:~group[BigInt] = new group[BigInt] {\char123}\\ -\hspace*{0pt} ~val `Example+inverse` = (a:~BigInt) => inverse{\char95}int(a)\\ -\hspace*{0pt} ~val `Example+neutral` = neutral{\char95}int\\ -\hspace*{0pt} ~val `Example+mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ +\hspace*{0pt} ~val `Example.inverse` = (a:~BigInt) => inverse{\char95}int(a)\\ +\hspace*{0pt} ~val `Example.neutral` = neutral{\char95}int\\ +\hspace*{0pt} ~val `Example.mult` = (a:~BigInt,~b:~BigInt) => mult{\char95}int(a,~b)\\ \hspace*{0pt}{\char125}\\ \hspace*{0pt}\\ \hspace*{0pt}def example:~BigInt = pow{\char95}int[BigInt](BigInt(10),~BigInt(- 2))\\ diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/Adaptation.thy Thu Sep 02 17:02:00 2010 +0200 @@ -272,12 +272,12 @@ text {* For convenience, the default @{text HOL} setup for @{text Haskell} - maps the @{class eq} class to its counterpart in @{text Haskell}, - giving custom serialisations for the class @{class eq} (by command - @{command_def code_class}) and its operation @{const HOL.eq} + maps the @{class equal} class to its counterpart in @{text Haskell}, + giving custom serialisations for the class @{class equal} (by command + @{command_def code_class}) and its operation @{const HOL.equal} *} -code_class %quotett eq +code_class %quotett equal (Haskell "Eq") code_const %quotett "op =" @@ -285,19 +285,19 @@ text {* \noindent A problem now occurs whenever a type which is an instance - of @{class eq} in @{text HOL} is mapped on a @{text + of @{class equal} in @{text HOL} is mapped on a @{text Haskell}-built-in type which is also an instance of @{text Haskell} @{text Eq}: *} typedecl %quote bar -instantiation %quote bar :: eq +instantiation %quote bar :: equal begin -definition %quote "eq_class.eq (x\bar) y \ x = y" +definition %quote "HOL.equal (x\bar) y \ x = y" -instance %quote by default (simp add: eq_bar_def) +instance %quote by default (simp add: equal_bar_def) end %quote (*<*) @@ -310,7 +310,7 @@ suppress this additional instance, use @{command_def "code_instance"}: *} -code_instance %quotett bar :: eq +code_instance %quotett bar :: equal (Haskell -) diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/Evaluation.thy --- a/doc-src/Codegen/Thy/Evaluation.thy Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/Evaluation.thy Thu Sep 02 17:02:00 2010 +0200 @@ -96,7 +96,7 @@ allows to use pattern matching on constructors stemming from compiled @{text "datatypes"}. - For a less simplistic example, theory @{theory Ferrack} is + For a less simplistic example, theory @{text Ferrack} is a good reference. *} diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Thu Sep 02 17:02:00 2010 +0200 @@ -122,7 +122,7 @@ specific application, you should consider \emph{Imperative Functional Programming with Isabelle/HOL} \cite{bulwahn-et-al:2008:imperative}; the framework described there - is available in session @{theory Imperative_HOL}. + is available in session @{text Imperative_HOL}. *} diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/Inductive_Predicate.thy --- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Thu Sep 02 17:02:00 2010 +0200 @@ -220,8 +220,8 @@ "values"} and the number of elements. *} -values %quote [mode: i \ o \ bool] 20 "{n. tranclp succ 10 n}" -values %quote [mode: o \ i \ bool] 10 "{n. tranclp succ n 10}" +values %quote [mode: i \ o \ bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\1*) +values %quote [mode: o \ i \ bool] 1 "{n. tranclp succ n 10}" subsection {* Embedding into functional code within Isabelle/HOL *} diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Thu Sep 02 17:02:00 2010 +0200 @@ -1,15 +1,12 @@ theory Setup -imports Complex_Main More_List RBT Dlist Mapping +imports + Complex_Main + More_List RBT Dlist Mapping uses "../../antiquote_setup.ML" "../../more_antiquote.ML" begin -ML {* no_document use_thys - ["Efficient_Nat", "Code_Char_chr", "Product_ord", - "~~/src/HOL/Imperative_HOL/Imperative_HOL", - "~~/src/HOL/Decision_Procs/Ferrack"] *} - setup {* let val typ = Simple_Syntax.read_typ; diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu Sep 02 17:02:00 2010 +0200 @@ -499,9 +499,9 @@ % \begin{isamarkuptext}% For convenience, the default \isa{HOL} setup for \isa{Haskell} - maps the \isa{eq} class to its counterpart in \isa{Haskell}, - giving custom serialisations for the class \isa{eq} (by command - \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}% + maps the \isa{equal} class to its counterpart in \isa{Haskell}, + giving custom serialisations for the class \isa{equal} (by command + \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{equal{\isacharunderscore}class{\isachardot}equal}% \end{isamarkuptext}% \isamarkuptrue% % @@ -511,7 +511,7 @@ % \isatagquotett \isacommand{code{\isacharunderscore}class}\isamarkupfalse% -\ eq\isanewline +\ equal\isanewline \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline \isanewline \isacommand{code{\isacharunderscore}const}\isamarkupfalse% @@ -526,7 +526,7 @@ % \begin{isamarkuptext}% \noindent A problem now occurs whenever a type which is an instance - of \isa{eq} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell} + of \isa{equal} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell} \isa{Eq}:% \end{isamarkuptext}% \isamarkuptrue% @@ -540,15 +540,15 @@ \ bar\isanewline \isanewline \isacommand{instantiation}\isamarkupfalse% -\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline +\ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline \isakeyword{begin}\isanewline \isanewline \isacommand{definition}\isamarkupfalse% -\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}HOL{\isachardot}equal\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline \isanewline \isacommand{instance}\isamarkupfalse% \ \isacommand{by}\isamarkupfalse% -\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline +\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ equal{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline \isanewline \isacommand{end}\isamarkupfalse% % @@ -587,7 +587,7 @@ % \isatagquotett \isacommand{code{\isacharunderscore}instance}\isamarkupfalse% -\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline +\ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% \endisatagquotett {\isafoldquotett}% diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Evaluation.tex --- a/doc-src/Codegen/Thy/document/Evaluation.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Thu Sep 02 17:02:00 2010 +0200 @@ -225,7 +225,7 @@ allows to use pattern matching on constructors stemming from compiled \isa{datatypes}. - For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is + For a less simplistic example, theory \isa{Ferrack} is a good reference.% \end{isamarkuptext}% \isamarkuptrue% diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Foundations.tex --- a/doc-src/Codegen/Thy/document/Foundations.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Thu Sep 02 17:02:00 2010 +0200 @@ -247,11 +247,11 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ -\hspace*{0pt}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% +\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\ +\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\ +\hspace*{0pt}dequeue (Example.AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\ +\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % @@ -350,21 +350,21 @@ \isatypewriter% \noindent% \hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~type 'a eq\\ -\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\ +\hspace*{0pt} ~type 'a equal\\ +\hspace*{0pt} ~val equal :~'a equal -> 'a -> 'a -> bool\\ +\hspace*{0pt} ~val eq :~'a equal -> 'a -> 'a -> bool\\ +\hspace*{0pt} ~val member :~'a equal -> 'a list -> 'a -> bool\\ \hspace*{0pt} ~val collect{\char95}duplicates :\\ -\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\ +\hspace*{0pt} ~~~'a equal -> 'a list -> 'a list -> 'a list -> 'a list\\ \hspace*{0pt}end = struct\\ \hspace*{0pt}\\ -\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ -\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\ +\hspace*{0pt}type 'a equal = {\char123}equal :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}val equal = {\char35}equal :~'a equal -> 'a -> 'a -> bool;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\ +\hspace*{0pt}fun eq A{\char95}~a b = equal A{\char95}~a b;\\ \hspace*{0pt}\\ \hspace*{0pt}fun member A{\char95}~[] y = false\\ -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\ +\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eq A{\char95}~x y orelse member A{\char95}~xs y;\\ \hspace*{0pt}\\ \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ @@ -387,11 +387,11 @@ \begin{isamarkuptext}% \noindent Obviously, polymorphic equality is implemented the Haskell way using a type class. How is this achieved? HOL introduces an - explicit class \isa{eq} with a corresponding operation \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. The preprocessing - framework does the rest by propagating the \isa{eq} constraints + explicit class \isa{equal} with a corresponding operation \isa{equal{\isacharunderscore}class{\isachardot}equal} such that \isa{equal{\isacharunderscore}class{\isachardot}equal\ {\isacharequal}\ op\ {\isacharequal}}. The preprocessing + framework does the rest by propagating the \isa{equal} constraints through all dependent code equations. For datatypes, instances of - \isa{eq} are implicitly derived when possible. For other types, - you may instantiate \isa{eq} manually like any other type class.% + \isa{equal} are implicitly derived when possible. For other types, + you may instantiate \isa{equal} manually like any other type class.% \end{isamarkuptext}% \isamarkuptrue% % @@ -444,12 +444,12 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\ \hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% +\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\ +\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);% \end{isamarkuptext}% \isamarkuptrue% % @@ -538,11 +538,11 @@ \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ \hspace*{0pt}\\ -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\ +\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\ +\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));% \end{isamarkuptext}% \isamarkuptrue% % diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Thu Sep 02 17:02:00 2010 +0200 @@ -216,13 +216,13 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\ -\hspace*{0pt}funpow Zero{\char95}nat f = id;\\ -\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\ +\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\ +\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\ +\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\ \hspace*{0pt}\\ -\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\ +\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\ \hspace*{0pt}funpows [] = id;\\ -\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;% +\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;% \end{isamarkuptext}% \isamarkuptrue% % @@ -242,7 +242,7 @@ specific application, you should consider \emph{Imperative Functional Programming with Isabelle/HOL} \cite{bulwahn-et-al:2008:imperative}; the framework described there - is available in session \hyperlink{theory.Imperative-HOL}{\mbox{\isa{Imperative{\isacharunderscore}HOL}}}.% + is available in session \isa{Imperative{\isacharunderscore}HOL}.% \end{isamarkuptext}% \isamarkuptrue% % diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Thu Sep 02 17:02:00 2010 +0200 @@ -422,9 +422,9 @@ % \isatagquote \isacommand{values}\isamarkupfalse% -\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline +\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline \isacommand{values}\isamarkupfalse% -\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}% +\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}% \endisatagquote {\isafoldquote}% % diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Sep 02 17:02:00 2010 +0200 @@ -231,19 +231,19 @@ \hspace*{0pt}\\ \hspace*{0pt}data Queue a = AQueue [a] [a];\\ \hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a.~Queue a;\\ -\hspace*{0pt}empty = AQueue [] [];\\ +\hspace*{0pt}empty ::~forall a.~Example.Queue a;\\ +\hspace*{0pt}empty = Example.AQueue [] [];\\ \hspace*{0pt}\\ -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ -\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\ -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ -\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ +\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\ +\hspace*{0pt}dequeue (Example.AQueue [] []) = (Nothing,~Example.AQueue [] []);\\ +\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\ +\hspace*{0pt}dequeue (Example.AQueue (v :~va) []) =\\ \hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = reverse (v :~va);\\ -\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ +\hspace*{0pt} ~{\char125}~in (Just y,~Example.AQueue [] ys);\\ \hspace*{0pt}\\ -\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ -\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\ +\hspace*{0pt}enqueue ::~forall a.~a -> Example.Queue a -> Example.Queue a;\\ +\hspace*{0pt}enqueue x (Example.AQueue xs ys) = Example.AQueue (x :~xs) ys;\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% \end{isamarkuptext}% @@ -397,41 +397,41 @@ \noindent% \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Example.Nat;\\ \hspace*{0pt}\\ -\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ -\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ -\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}plus{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\ +\hspace*{0pt}plus{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat m (Example.Suc n);\\ +\hspace*{0pt}plus{\char95}nat Example.Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ \hspace*{0pt}class Semigroup a where {\char123}\\ \hspace*{0pt} ~mult ::~a -> a -> a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ +\hspace*{0pt}class (Example.Semigroup a) => Monoid a where {\char123}\\ \hspace*{0pt} ~neutral ::~a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ -\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ -\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ +\hspace*{0pt}pow ::~forall a.~(Example.Monoid a) => Example.Nat -> a -> a;\\ +\hspace*{0pt}pow Example.Zero{\char95}nat a = Example.neutral;\\ +\hspace*{0pt}pow (Example.Suc n) a = Example.mult a (Example.pow n a);\\ \hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ -\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ -\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}mult{\char95}nat ::~Example.Nat -> Example.Nat -> Example.Nat;\\ +\hspace*{0pt}mult{\char95}nat Example.Zero{\char95}nat n = Example.Zero{\char95}nat;\\ +\hspace*{0pt}mult{\char95}nat (Example.Suc m) n = Example.plus{\char95}nat n (Example.mult{\char95}nat m n);\\ \hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}neutral{\char95}nat ::~Example.Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Example.Suc Example.Zero{\char95}nat;\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Semigroup Nat where {\char123}\\ -\hspace*{0pt} ~mult = mult{\char95}nat;\\ +\hspace*{0pt}instance Example.Semigroup Example.Nat where {\char123}\\ +\hspace*{0pt} ~mult = Example.mult{\char95}nat;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}instance Monoid Nat where {\char123}\\ -\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ +\hspace*{0pt}instance Example.Monoid Example.Nat where {\char123}\\ +\hspace*{0pt} ~neutral = Example.neutral{\char95}nat;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}bexp ::~Nat -> Nat;\\ -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}bexp ::~Example.Nat -> Example.Nat;\\ +\hspace*{0pt}bexp n = Example.pow n (Example.Suc (Example.Suc Example.Zero{\char95}nat));\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% \end{isamarkuptext}% @@ -470,8 +470,8 @@ \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ \hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ \hspace*{0pt} ~val neutral{\char95}nat :~nat\\ -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ \hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ \hspace*{0pt} ~val bexp :~nat -> nat\\ \hspace*{0pt}end = struct\\ @@ -494,9 +494,9 @@ \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ \hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ \hspace*{0pt}\\ -\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ \hspace*{0pt}\\ \hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ \hspace*{0pt} ~:~nat monoid;\\ diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Thu Sep 02 17:02:00 2010 +0200 @@ -74,10 +74,11 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}fib ::~Nat -> Nat;\\ -\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\ -\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\ -\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));% +\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\ +\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;\\ +\hspace*{0pt}fib (Example.Suc Example.Zero{\char95}nat) = Example.Suc Example.Zero{\char95}nat;\\ +\hspace*{0pt}fib (Example.Suc (Example.Suc n)) =\\ +\hspace*{0pt} ~Example.plus{\char95}nat (Example.fib n) (Example.fib (Example.Suc n));% \end{isamarkuptext}% \isamarkuptrue% % @@ -172,15 +173,17 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\ -\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\ -\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\ -\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\ -\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\ +\hspace*{0pt}fib{\char95}step ::~Example.Nat -> (Example.Nat,~Example.Nat);\\ +\hspace*{0pt}fib{\char95}step (Example.Suc n) =\\ +\hspace*{0pt} ~let {\char123}\\ +\hspace*{0pt} ~~~(m,~q) = Example.fib{\char95}step n;\\ +\hspace*{0pt} ~{\char125}~in (Example.plus{\char95}nat m q,~m);\\ +\hspace*{0pt}fib{\char95}step Example.Zero{\char95}nat =\\ +\hspace*{0pt} ~(Example.Suc Example.Zero{\char95}nat,~Example.Zero{\char95}nat);\\ \hspace*{0pt}\\ -\hspace*{0pt}fib ::~Nat -> Nat;\\ -\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\ -\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;% +\hspace*{0pt}fib ::~Example.Nat -> Example.Nat;\\ +\hspace*{0pt}fib (Example.Suc n) = fst (Example.fib{\char95}step n);\\ +\hspace*{0pt}fib Example.Zero{\char95}nat = Example.Zero{\char95}nat;% \end{isamarkuptext}% \isamarkuptrue% % @@ -590,28 +593,30 @@ \hspace*{0pt}\\ \hspace*{0pt}newtype Dlist a = Dlist [a];\\ \hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a.~Dlist a;\\ -\hspace*{0pt}empty = Dlist [];\\ +\hspace*{0pt}empty ::~forall a.~Example.Dlist a;\\ +\hspace*{0pt}empty = Example.Dlist [];\\ \hspace*{0pt}\\ \hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\ \hspace*{0pt}member [] y = False;\\ -\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\ +\hspace*{0pt}member (x :~xs) y = x == y || Example.member xs y;\\ \hspace*{0pt}\\ \hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\ -\hspace*{0pt}inserta x xs = (if member xs x then xs else x :~xs);\\ +\hspace*{0pt}inserta x xs = (if Example.member xs x then xs else x :~xs);\\ \hspace*{0pt}\\ -\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\ -\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\ +\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Example.Dlist a -> [a];\\ +\hspace*{0pt}list{\char95}of{\char95}dlist (Example.Dlist x) = x;\\ \hspace*{0pt}\\ -\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ -\hspace*{0pt}insert x dxs = Dlist (inserta x (list{\char95}of{\char95}dlist dxs));\\ +\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\ +\hspace*{0pt}insert x dxs =\\ +\hspace*{0pt} ~Example.Dlist (Example.inserta x (Example.list{\char95}of{\char95}dlist dxs));\\ \hspace*{0pt}\\ \hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\ \hspace*{0pt}remove1 x [] = [];\\ -\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\ +\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~Example.remove1 x xs);\\ \hspace*{0pt}\\ -\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\ -\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\ +\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Example.Dlist a -> Example.Dlist a;\\ +\hspace*{0pt}remove x dxs =\\ +\hspace*{0pt} ~Example.Dlist (Example.remove1 x (Example.list{\char95}of{\char95}dlist dxs));\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% \end{isamarkuptext}% diff -r c51e80de9b7e -r 928c5a5bdc93 doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Thu Sep 02 15:48:32 2010 +0200 +++ b/doc-src/Codegen/Thy/examples/Example.hs Thu Sep 02 17:02:00 2010 +0200 @@ -4,18 +4,18 @@ data Queue a = AQueue [a] [a]; -empty :: forall a. Queue a; -empty = AQueue [] []; +empty :: forall a. Example.Queue a; +empty = Example.AQueue [] []; -dequeue :: forall a. Queue a -> (Maybe a, Queue a); -dequeue (AQueue [] []) = (Nothing, AQueue [] []); -dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys); -dequeue (AQueue (v : va) []) = +dequeue :: forall a. Example.Queue a -> (Maybe a, Example.Queue a); +dequeue (Example.AQueue [] []) = (Nothing, Example.AQueue [] []); +dequeue (Example.AQueue xs (y : ys)) = (Just y, Example.AQueue xs ys); +dequeue (Example.AQueue (v : va) []) = let { (y : ys) = reverse (v : va); - } in (Just y, AQueue [] ys); + } in (Just y, Example.AQueue [] ys); -enqueue :: forall a. a -> Queue a -> Queue a; -enqueue x (AQueue xs ys) = AQueue (x : xs) ys; +enqueue :: forall a. a -> Example.Queue a -> Example.Queue a; +enqueue x (Example.AQueue xs ys) = Example.AQueue (x : xs) ys; } diff -r c51e80de9b7e -r 928c5a5bdc93 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Thu Sep 02 15:48:32 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Thu Sep 02 17:02:00 2010 +0200 @@ -261,13 +261,31 @@ end; in print_stmt end; +fun mk_name_module reserved module_prefix module_alias program = + let + fun mk_alias name = case module_alias name + of SOME name' => name' + | NONE => name + |> Long_Name.explode + |> map (fn name => (the_single o fst) (Name.variants [name] reserved)) + |> Long_Name.implode; + fun mk_prefix name = case module_prefix + of SOME module_prefix => Long_Name.append module_prefix name + | NONE => name; + val tab = + Symtab.empty + |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) + o fst o Code_Namespace.dest_name o fst) + program + in the o Symtab.lookup tab end; + fun haskell_program_of_program labelled_name module_prefix reserved module_alias program = let val reserved = Name.make_context reserved; val mk_name_module = mk_name_module reserved module_prefix module_alias program; fun add_stmt (name, (stmt, deps)) = let - val (module_name, base) = dest_name name; + val (module_name, base) = Code_Namespace.dest_name name; val module_name' = mk_name_module module_name; val mk_name_stmt = yield_singleton Name.variants; fun add_fun upper (nsp_fun, nsp_typ) = @@ -309,14 +327,14 @@ (Graph.get_node program name, Graph.imm_succs program name)) (Graph.strong_conn program |> flat)) Symtab.empty; fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the - o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name + o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Namespace.dest_name) name))) name handle Option => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, hs_program) end; fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms, includes, module_alias, class_syntax, tyco_syntax, const_syntax, program, - names, presentation_names } = + names } = let val reserved = fold (insert (op =) o fst) includes reserved_syms; val (deresolver, hs_program) = haskell_program_of_program labelled_name @@ -347,10 +365,10 @@ content, str "}" ]); - fun serialize_module1 (module_name', (deps, (stmts, _))) = + fun serialize_module (module_name', (deps, (stmts, _))) = let val stmt_names = map fst stmts; - val qualified = null presentation_names; + val qualified = true; val imports = subtract (op =) stmt_names deps |> distinct (op =) |> map_filter (try deresolver) @@ -363,18 +381,10 @@ val import_ps = map print_import_include includes @ map print_import_module imports val content = Pretty.chunks2 ((if null import_ps then [] else [Pretty.chunks import_ps]) @ map_filter - (fn (name, (_, SOME stmt)) => SOME (print_stmt qualified (name, stmt)) + (fn (name, (_, SOME stmt)) => SOME (markup_stmt name (print_stmt qualified (name, stmt))) | (_, (_, NONE)) => NONE) stmts ); in print_module module_name' content end; - fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter - (fn (name, (_, SOME stmt)) => if null presentation_names - orelse member (op =) presentation_names name - then SOME (print_stmt false (name, stmt)) - else NONE - | (_, (_, NONE)) => NONE) stmts); - val serialize_module = - if null presentation_names then serialize_module1 else pair "" o serialize_module2; fun write_module width (SOME destination) (modlname, content) = let val _ = File.check destination; @@ -386,9 +396,9 @@ val _ = File.mkdir_leaf (Path.dir pathname); in File.write pathname ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n" - ^ format false width content) + ^ format [] width content) end - | write_module width NONE (_, content) = writeln (format false width content); + | write_module width NONE (_, content) = writeln (format [] width content); in Code_Target.serialization (fn width => fn destination => K () o map (write_module width destination)) diff -r c51e80de9b7e -r 928c5a5bdc93 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Sep 02 15:48:32 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Sep 02 17:02:00 2010 +0200 @@ -759,10 +759,10 @@ fun modify_class stmts = single (SOME (ML_Class (the_single (map_filter (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))) - fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) = - [modify_fun stmt] + fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) = + if Code_Thingol.is_case stmt' then [] else [modify_fun stmt] | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = - modify_funs stmts + modify_funs (filter_out (Code_Thingol.is_case o snd) stmts) | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = modify_datatypes stmts | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) = @@ -787,25 +787,21 @@ fun serialize_ml target print_module print_stmt with_signatures { labelled_name, reserved_syms, includes, module_alias, class_syntax, tyco_syntax, - const_syntax, program, names, presentation_names } = + const_syntax, program, names } = let val is_cons = Code_Thingol.is_cons program; - val is_presentation = not (null presentation_names); val { deresolver, hierarchical_program = ml_program } = ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program; + val print_stmt = print_stmt labelled_name tyco_syntax const_syntax + (make_vars reserved_syms) is_cons; fun print_node _ (_, Code_Namespace.Dummy) = NONE - | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) = - if is_presentation andalso - (null o filter (member (op =) presentation_names) o stmt_names_of) stmt - then NONE - else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms) - is_cons (deresolver prefix_fragments) stmt) + | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) = + SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt)) | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) = let val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes; - val p = if is_presentation then Pretty.chunks2 body - else print_module name_fragment + val p = print_module name_fragment (if with_signatures then SOME decls else NONE) body; in SOME ([], p) end and print_nodes prefix_fragments nodes = (map_filter @@ -815,8 +811,8 @@ |> (fn (decls, body) => (flat decls, body)) val names' = map (try (deresolver [])) names; val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program)); - fun write width NONE = writeln o format false width - | write width (SOME p) = File.write p o format false width; + fun write width NONE = writeln o format [] width + | write width (SOME p) = File.write p o format [] width; in Code_Target.serialization write (rpair names' ooo format) p end; diff -r c51e80de9b7e -r 928c5a5bdc93 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Thu Sep 02 15:48:32 2010 +0200 +++ b/src/Tools/Code/code_namespace.ML Thu Sep 02 17:02:00 2010 +0200 @@ -6,6 +6,7 @@ signature CODE_NAMESPACE = sig + val dest_name: string -> string * string datatype ('a, 'b) node = Dummy | Stmt of 'a @@ -23,7 +24,13 @@ structure Code_Namespace : CODE_NAMESPACE = struct -(* hierarchical program structure *) +(** splitting names in module and base part **) + +val dest_name = + apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; + + +(** hierarchical program structure **) datatype ('a, 'b) node = Dummy @@ -46,10 +53,10 @@ of SOME name' => Long_Name.explode name' | NONE => map (fn name => fst (yield_singleton Name.variants name reserved)) (Long_Name.explode name); - val module_names = Graph.fold (insert (op =) o fst o Code_Printer.dest_name o fst) program []; + val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program []; val fragments_tab = fold (fn name => Symtab.update (name, alias_fragments name)) module_names Symtab.empty; - val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab); + val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab); (* building empty module hierarchy *) val empty_module = (empty_data, Graph.empty); diff -r c51e80de9b7e -r 928c5a5bdc93 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Thu Sep 02 15:48:32 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Thu Sep 02 17:02:00 2010 +0200 @@ -25,8 +25,8 @@ val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T val indent: int -> Pretty.T -> Pretty.T - val markup_stmt: string -> Pretty.T list -> Pretty.T - val format: bool -> int -> Pretty.T -> string + val markup_stmt: string -> Pretty.T -> Pretty.T + val format: string list -> int -> Pretty.T -> string val first_upper: string -> string val first_lower: string -> string @@ -70,7 +70,6 @@ val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option - type tyco_syntax type simple_const_syntax type complex_const_syntax @@ -93,10 +92,6 @@ val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> fixity -> iterm -> var_ctxt -> Pretty.T * var_ctxt - - val mk_name_module: Name.context -> string option -> (string -> string option) - -> 'a Graph.T -> string -> string - val dest_name: string -> string * string end; structure Code_Printer : CODE_PRINTER = @@ -110,7 +105,7 @@ | eqn_error NONE s = error s; val code_presentationN = "code_presentation"; -val _ = Output.add_mode code_presentationN; +val stmt_nameN = "stmt_name"; val _ = Markup.add_mode code_presentationN YXML.output_markup; @@ -132,21 +127,35 @@ fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; fun indent i = Print_Mode.setmp [] (Pretty.indent i); -val stmt_nameN = "stmt_name"; -fun markup_stmt name = Pretty.markup (code_presentationN, [(stmt_nameN, name)]); -fun filter_presentation selected (XML.Elem ((name, _), xs)) = - implode (map (filter_presentation (selected orelse name = code_presentationN)) xs) - | filter_presentation selected (XML.Text s) = +fun markup_stmt name = Print_Mode.setmp [code_presentationN] + (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); + +fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) = + implode (map (filter_presentation presentation_names + (selected orelse (name = code_presentationN + andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs) + | filter_presentation presentation_names selected (XML.Text s) = if selected then s else ""; -fun format presentation_only width p = - if presentation_only then - Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p - |> YXML.parse_body - |> map (filter_presentation false) - |> implode - |> suffix "\n" - else Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"; +fun maps_string s f [] = "" + | maps_string s f (x :: xs) = + let + val s1 = f x; + val s2 = maps_string s f xs; + in if s1 = "" then s2 + else if s2 = "" then s1 + else s1 ^ s ^ s2 + end; + +fun plain_text (XML.Elem (_, xs)) = implode (map plain_text xs) + | plain_text (XML.Text s) = s + +fun format presentation_names width = + Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) + #> YXML.parse_body + #> (if null presentation_names then implode o map plain_text + else maps_string "\n\n" (filter_presentation presentation_names false)) + #> suffix "\n"; (** names and variable name contexts **) @@ -395,28 +404,4 @@ val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst; - -(** module name spaces **) - -val dest_name = - apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; - -fun mk_name_module reserved module_prefix module_alias program = - let - fun mk_alias name = case module_alias name - of SOME name' => name' - | NONE => name - |> Long_Name.explode - |> map (fn name => (the_single o fst) (Name.variants [name] reserved)) - |> Long_Name.implode; - fun mk_prefix name = case module_prefix - of SOME module_prefix => Long_Name.append module_prefix name - | NONE => name; - val tab = - Symtab.empty - |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) - o fst o dest_name o fst) - program - in the o Symtab.lookup tab end; - end; (*struct*) diff -r c51e80de9b7e -r 928c5a5bdc93 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Thu Sep 02 15:48:32 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Sep 02 17:02:00 2010 +0200 @@ -317,7 +317,8 @@ val implicits = filter (is_classinst o Graph.get_node program) (Graph.imm_succs program name); in union (op =) implicits end; - fun modify_stmt (_, Code_Thingol.Datatypecons _) = NONE + fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE + | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE | modify_stmt (_, Code_Thingol.Classrel _) = NONE | modify_stmt (_, Code_Thingol.Classparam _) = NONE | modify_stmt (_, stmt) = SOME stmt; @@ -329,7 +330,7 @@ fun serialize_scala { labelled_name, reserved_syms, includes, module_alias, class_syntax, tyco_syntax, const_syntax, program, - names, presentation_names } = + names } = let (* build program *) @@ -368,21 +369,15 @@ in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end; fun print_node _ (_, Code_Namespace.Dummy) = NONE | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) = - if null presentation_names - orelse member (op =) presentation_names name - then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)) - else NONE + SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))) | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) = - if null presentation_names - then - let - val prefix_fragments' = prefix_fragments @ [name_fragment]; - in - Option.map (print_module name_fragment - (map_filter (print_implicit prefix_fragments') implicits)) - (print_nodes prefix_fragments' nodes) - end - else print_nodes [] nodes + let + val prefix_fragments' = prefix_fragments @ [name_fragment]; + in + Option.map (print_module name_fragment + (map_filter (print_implicit prefix_fragments') implicits)) + (print_nodes prefix_fragments' nodes) + end and print_nodes prefix_fragments nodes = let val ps = map_filter (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name))) @@ -390,10 +385,9 @@ in if null ps then NONE else SOME (Pretty.chunks2 ps) end; (* serialization *) - val p_includes = if null presentation_names then map snd includes else []; - val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program)); - fun write width NONE = writeln o format false width - | write width (SOME p) = File.write p o format false width; + val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program)); + fun write width NONE = writeln o format [] width + | write width (SOME p) = File.write p o format [] width; in Code_Target.serialization write (rpair [] ooo format) p end; diff -r c51e80de9b7e -r 928c5a5bdc93 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Sep 02 15:48:32 2010 +0200 +++ b/src/Tools/Code/code_target.ML Thu Sep 02 17:02:00 2010 +0200 @@ -8,6 +8,7 @@ sig val cert_tyco: theory -> string -> string val read_tyco: theory -> string -> string + val read_const_exprs: theory -> string list -> string list val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit @@ -42,7 +43,7 @@ type serialization val parse_args: 'a parser -> Token.T list -> 'a val serialization: (int -> Path.T option -> 'a -> unit) - -> (bool -> int -> 'a -> string * string option list) + -> (string list -> int -> 'a -> string * string option list) -> 'a -> serialization val set_default_code_width: int -> theory -> theory @@ -72,12 +73,9 @@ datatype destination = Export of Path.T option | Produce | Present of string list; type serialization = int -> destination -> (string * string option list) option; -fun stmt_names_of_destination (Present stmt_names) = stmt_names - | stmt_names_of_destination _ = []; - fun serialization output _ content width (Export some_path) = (output width some_path content; NONE) - | serialization _ string content width Produce = SOME (string false width content) - | serialization _ string content width (Present _) = SOME (string false width content); + | serialization _ string content width Produce = SOME (string [] width content) + | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content); fun export some_path f = (f (Export some_path); ()); fun produce f = the (f Produce); @@ -116,8 +114,7 @@ tyco_syntax: string -> Code_Printer.tyco_syntax option, const_syntax: string -> Code_Printer.activated_const_syntax option, program: Code_Thingol.program, - names: string list, - presentation_names: string list } + names: string list } -> serialization; datatype description = Fundamental of { serializer: serializer, @@ -308,7 +305,7 @@ fun invoke_serializer thy abortable serializer literals reserved abs_includes module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax - module_name args naming proto_program (names, presentation_names) = + module_name args naming proto_program names = let val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) = activate_symbol_syntax thy literals naming @@ -325,19 +322,15 @@ tyco_syntax = Symtab.lookup tyco_syntax, const_syntax = Symtab.lookup const_syntax, program = program, - names = names, - presentation_names = presentation_names } + names = names } end; -fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination = +fun mount_serializer thy target some_width module_name args naming proto_program names = let val (default_width, abortable, data, program) = activate_target_for thy target naming proto_program; val serializer = case the_description data of Fundamental seri => #serializer seri; - val presentation_names = stmt_names_of_destination destination; - val module_name = if null presentation_names - then raw_module_name else "Code"; val reserved = the_reserved data; fun select_include names_all (name, (content, cs)) = if null cs then SOME (name, content) @@ -354,7 +347,7 @@ in invoke_serializer thy abortable serializer literals reserved includes module_alias class instance tyco const module_name args - naming program (names, presentation_names) width destination + naming program names width end; fun assert_module_name "" = error ("Empty module name not allowed.")