--- 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))\\
--- 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\<Colon>bar) y \<longleftrightarrow> x = y"
+definition %quote "HOL.equal (x\<Colon>bar) y \<longleftrightarrow> 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 -)
--- 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.
*}
--- 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}.
*}
--- 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 \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}"
-values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}"
+values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
+values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
subsection {* Embedding into functional code within Isabelle/HOL *}
--- 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;
--- 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}%
--- 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%
--- 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%
%
--- 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%
%
--- 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}%
%
--- 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;\\
--- 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}%
--- 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;
}
--- 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))
--- 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;
--- 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);
--- 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*)
--- 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;
--- 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.")