--- a/Admin/isatest/settings/cygwin-poly-e Thu Sep 02 14:34:08 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e Thu Sep 02 18:45:23 2010 +0200
@@ -24,6 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
-# Disable while Jasmin is on vacation
-unset KODKODI
-#init_component "$HOME/contrib_devel/kodkodi"
+init_component "$HOME/contrib_devel/kodkodi"
--- a/NEWS Thu Sep 02 14:34:08 2010 +0200
+++ b/NEWS Thu Sep 02 18:45:23 2010 +0200
@@ -23,7 +23,7 @@
at the cost of clarity of file dependencies. Recall that Isabelle/ML
files exclusively use the .ML extension. Minor INCOMPATIBILTY.
-* Various options that affect document antiquotations are now properly
+* Various options that affect pretty printing etc. are now properly
handled within the context via configuration options, instead of
unsynchronized references. There are both ML Config.T entities and
Isar declaration attributes to access these.
@@ -36,15 +36,11 @@
Thy_Output.source thy_output_source
Thy_Output.break thy_output_break
+ show_question_marks show_question_marks
+
Note that the corresponding "..._default" references may be only
changed globally at the ROOT session setup, but *not* within a theory.
-* ML structure Unsynchronized never opened, not even in Isar
-interaction mode as before. Old Unsynchronized.set etc. have been
-discontinued -- use plain := instead. This should be *rare* anyway,
-since modern tools always work via official context data, notably
-configuration options.
-
*** Pure ***
@@ -220,6 +216,15 @@
*** ML ***
+* Configuration option show_question_marks only affects regular pretty
+printing of types and terms, not raw Term.string_of_vname.
+
+* ML structure Unsynchronized never opened, not even in Isar
+interaction mode as before. Old Unsynchronized.set etc. have been
+discontinued -- use plain := instead. This should be *rare* anyway,
+since modern tools always work via official context data, notably
+configuration options.
+
* ML antiquotations @{theory} and @{theory_ref} refer to named
theories from the ancestry of the current context, not any accidental
theory loader state as before. Potential INCOMPATIBILITY, subtle
--- a/doc-src/Classes/Thy/document/Classes.tex Thu Sep 02 14:34:08 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Thu Sep 02 18:45:23 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 14:34:08 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs Thu Sep 02 18:45:23 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/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Sep 02 18:45:23 2010 +0200
@@ -108,7 +108,7 @@
@{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
- @{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
+ @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
\end{mldecls}
These global ML variables control the detail of information that is
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Sep 02 14:34:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Sep 02 18:45:23 2010 +0200
@@ -130,7 +130,7 @@
\indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
- \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\
+ \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
\end{mldecls}
These global ML variables control the detail of information that is
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Sep 02 18:45:23 2010 +0200
@@ -132,19 +132,19 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-@{ML "show_question_marks := false"}\verb!;!
+@{ML "show_question_marks_default := false"}\verb!;!
\end{quote}
at the beginning of your file \texttt{ROOT.ML}.
The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Setting \verb!show_question_marks! to \texttt{false} only
+Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
suppresses question marks; variables that end in digits,
e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
e.g. @{text"x1.0"}, their internal index. This can be avoided by
turning the last digit into a subscript: write \verb!x\<^isub>1! and
obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML "show_question_marks := false"(*>*)
+(*<*)declare [[show_question_marks = false]](*>*)
subsection {*Qualified names*}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Sep 02 14:34:08 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Sep 02 18:45:23 2010 +0200
@@ -164,7 +164,7 @@
\begin{isamarkuptext}%
If you print anything, especially theorems, containing
schematic variables they are prefixed with a question mark:
-\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}. Most of the time
+\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time
you would rather not see the question marks. There is an attribute
\verb!no_vars! that you can attach to the theorem that turns its
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
@@ -173,12 +173,12 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-\verb|show_question_marks := false|\verb!;!
+\verb|show_question_marks_default := false|\verb!;!
\end{quote}
at the beginning of your file \texttt{ROOT.ML}.
The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Setting \verb!show_question_marks! to \texttt{false} only
+Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
suppresses question marks; variables that end in digits,
e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}},
e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by
@@ -187,19 +187,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
\isamarkupsubsection{Qualified names%
}
\isamarkuptrue%
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Thu Sep 02 18:45:23 2010 +0200
@@ -348,6 +348,6 @@
let
fun rewr (_, (t, _)) = vc_of_term (f thy t)
|> (fn vc => (vc, (t, thm_of thy vc)))
- in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
+ in VCs.map (Option.map (fn (vcs, _) => (Symtab.map (K rewr) vcs, g))) thy end
end
--- a/src/HOL/HOL.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/HOL.thy Thu Sep 02 18:45:23 2010 +0200
@@ -32,6 +32,7 @@
("Tools/recfun_codegen.ML")
"Tools/async_manager.ML"
"Tools/try.ML"
+ ("Tools/cnf_funcs.ML")
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -1645,7 +1646,6 @@
"(\<not> \<not>(P)) = P"
by blast+
-
subsection {* Basic ML bindings *}
ML {*
@@ -1699,6 +1699,7 @@
val trans = @{thm trans}
*}
+use "Tools/cnf_funcs.ML"
subsection {* Code generator setup *}
@@ -1931,6 +1932,10 @@
code_reserved Scala
Boolean
+code_modulename SML Pure HOL
+code_modulename OCaml Pure HOL
+code_modulename Haskell Pure HOL
+
text {* using built-in Haskell equality *}
code_class equal
--- a/src/HOL/Hilbert_Choice.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Sep 02 18:45:23 2010 +0200
@@ -7,7 +7,8 @@
theory Hilbert_Choice
imports Nat Wellfounded Plain
-uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
+uses ("Tools/meson.ML")
+ ("Tools/choice_specification.ML")
begin
subsection {* Hilbert's epsilon *}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 02 18:45:23 2010 +0200
@@ -578,7 +578,7 @@
(map o pairself) imp_monad_bind pats),
imp_monad_bind t0);
- in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
+ in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
in
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Sep 02 18:45:23 2010 +0200
@@ -124,10 +124,10 @@
fun vector_cmul c (v:vector) =
let val n = dim v
in if c =/ rat_0 then vector_0 n
- else (n,FuncUtil.Intfunc.map (fn x => c */ x) (snd v))
+ else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v))
end;
-fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.map Rat.neg (snd v)) :vector;
+fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.map (K Rat.neg) (snd v)) :vector;
fun vector_add (v1:vector) (v2:vector) =
let val m = dim v1
@@ -167,11 +167,11 @@
fun matrix_cmul c (m:matrix) =
let val (i,j) = dimensions m
in if c =/ rat_0 then matrix_0 (i,j)
- else ((i,j),FuncUtil.Intpairfunc.map (fn x => c */ x) (snd m))
+ else ((i,j),FuncUtil.Intpairfunc.map (fn _ => fn x => c */ x) (snd m))
end;
fun matrix_neg (m:matrix) =
- (dimensions m, FuncUtil.Intpairfunc.map Rat.neg (snd m)) :matrix;
+ (dimensions m, FuncUtil.Intpairfunc.map (K Rat.neg) (snd m)) :matrix;
fun matrix_add (m1:matrix) (m2:matrix) =
let val d1 = dimensions m1
@@ -229,14 +229,14 @@
fun monomial_pow m k =
if k = 0 then monomial_1
- else FuncUtil.Ctermfunc.map (fn x => k * x) m;
+ else FuncUtil.Ctermfunc.map (fn _ => fn x => k * x) m;
fun monomial_divides m1 m2 =
FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
fun monomial_div m1 m2 =
let val m = FuncUtil.Ctermfunc.combine Integer.add
- (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2)
+ (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn _ => fn x => ~ x) m2)
in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
else error "monomial_div: non-divisible"
end;
@@ -270,9 +270,9 @@
fun poly_cmul c p =
if c =/ rat_0 then poly_0
- else FuncUtil.Monomialfunc.map (fn x => c */ x) p;
+ else FuncUtil.Monomialfunc.map (fn _ => fn x => c */ x) p;
-fun poly_neg p = FuncUtil.Monomialfunc.map Rat.neg p;;
+fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;;
fun poly_add p1 p2 =
FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
@@ -282,7 +282,7 @@
fun poly_cmmul (c,m) p =
if c =/ rat_0 then poly_0
else if FuncUtil.Ctermfunc.is_empty m
- then FuncUtil.Monomialfunc.map (fn d => c */ d) p
+ then FuncUtil.Monomialfunc.map (fn _ => fn d => c */ d) p
else FuncUtil.Monomialfunc.fold (fn (m', d) => fn a => (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
fun poly_mul p1 p2 =
@@ -596,13 +596,13 @@
let
val cd1 = fold_rev (common_denominator FuncUtil.Intpairfunc.fold) mats (rat_1)
val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) (rat_1)
- val mats' = map (FuncUtil.Intpairfunc.map (fn x => cd1 */ x)) mats
+ val mats' = map (FuncUtil.Intpairfunc.map (fn _ => fn x => cd1 */ x)) mats
val obj' = vector_cmul cd2 obj
val max1 = fold_rev (maximal_element FuncUtil.Intpairfunc.fold) mats' (rat_0)
val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
val scal1 = pow2 (20 - trunc(Math.ln (float_of_rat max1) / Math.ln 2.0))
val scal2 = pow2 (20 - trunc(Math.ln (float_of_rat max2) / Math.ln 2.0))
- val mats'' = map (FuncUtil.Intpairfunc.map (fn x => x */ scal1)) mats'
+ val mats'' = map (FuncUtil.Intpairfunc.map (fn _ => fn x => x */ scal1)) mats'
val obj'' = vector_cmul scal2 obj'
in solver obj'' mats''
end
@@ -629,13 +629,13 @@
let
val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj) (rat_1)
- val mats' = map (Inttriplefunc.map (fn x => cd1 */ x)) mats
+ val mats' = map (Inttriplefunc.map (fn _ => fn x => cd1 */ x)) mats
val obj' = vector_cmul cd2 obj
val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0)
val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
- val mats'' = map (Inttriplefunc.map (fn x => x */ scal1)) mats'
+ val mats'' = map (Inttriplefunc.map (fn _ => fn x => x */ scal1)) mats'
val obj'' = vector_cmul scal2 obj'
in solver obj'' mats''
end
@@ -655,7 +655,7 @@
(* Stuff for "equations" ((int*int*int)->num functions). *)
fun tri_equation_cmul c eq =
- if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn d => c */ d) eq;
+ if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
fun tri_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
@@ -686,7 +686,7 @@
in if b =/ rat_0 then e else
tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
end
- in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map elim dun)) (map elim oeqs)
+ in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map (K elim) dun)) (map elim oeqs)
end)
handle Failure _ => eliminate vs dun eqs)
in
@@ -724,7 +724,7 @@
in if b =/ rat_0 then e
else tri_equation_add e (tri_equation_cmul (Rat.neg b // a) eq)
end
- in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map elim dun))
+ in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
(map elim oeqs)
end
in fn eqs =>
@@ -744,7 +744,7 @@
(Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
val ass =
Inttriplefunc.combine (curry op +/) (K false)
- (Inttriplefunc.map (tri_equation_eval vfn) assigs) vfn
+ (Inttriplefunc.map (K (tri_equation_eval vfn)) assigs) vfn
in if forall (fn e => tri_equation_eval ass e =/ rat_0) eqs
then Inttriplefunc.delete_safe one ass else raise Sanity
end;
@@ -762,7 +762,7 @@
(* Usual operations on equation-parametrized poly. *)
fun tri_epoly_cmul c l =
- if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (tri_equation_cmul c) l;;
+ if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (K (tri_equation_cmul c)) l;;
val tri_epoly_neg = tri_epoly_cmul (Rat.rat_of_int ~1);
@@ -773,7 +773,7 @@
(* Stuff for "equations" ((int*int)->num functions). *)
fun pi_equation_cmul c eq =
- if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn d => c */ d) eq;
+ if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
fun pi_equation_add eq1 eq2 = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0) eq1 eq2;
@@ -804,7 +804,7 @@
in if b =/ rat_0 then e else
pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
end
- in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map elim dun)) (map elim oeqs)
+ in eliminate vs (Inttriplefunc.update (v,eq') (Inttriplefunc.map (K elim) dun)) (map elim oeqs)
end
handle Failure _ => eliminate vs dun eqs
in
@@ -842,7 +842,7 @@
in if b =/ rat_0 then e
else pi_equation_add e (pi_equation_cmul (Rat.neg b // a) eq)
end
- in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map elim dun))
+ in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
(map elim oeqs)
end
in fn eqs =>
@@ -862,7 +862,7 @@
(Inttriplefunc.onefunc(one, Rat.rat_of_int ~1))
val ass =
Inttriplefunc.combine (curry op +/) (K false)
- (Inttriplefunc.map (pi_equation_eval vfn) assigs) vfn
+ (Inttriplefunc.map (K (pi_equation_eval vfn)) assigs) vfn
in if forall (fn e => pi_equation_eval ass e =/ rat_0) eqs
then Inttriplefunc.delete_safe one ass else raise Sanity
end;
@@ -880,7 +880,7 @@
(* Usual operations on equation-parametrized poly. *)
fun pi_epoly_cmul c l =
- if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (pi_equation_cmul c) l;;
+ if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (K (pi_equation_cmul c)) l;;
val pi_epoly_neg = pi_epoly_cmul (Rat.rat_of_int ~1);
@@ -1035,7 +1035,7 @@
val bmatrix_add = Inttriplefunc.combine (curry op +/) (fn x => x =/ rat_0);
fun bmatrix_cmul c bm =
if c =/ rat_0 then Inttriplefunc.empty
- else Inttriplefunc.map (fn x => c */ x) bm;
+ else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
fun bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
--- a/src/HOL/Library/positivstellensatz.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Thu Sep 02 18:45:23 2010 +0200
@@ -549,7 +549,7 @@
(* A linear arithmetic prover *)
local
val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
- fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
+ fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
val one_tm = @{cterm "1::real"}
fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
--- a/src/HOL/Multivariate_Analysis/normarith.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Thu Sep 02 18:45:23 2010 +0200
@@ -32,16 +32,16 @@
(Thm.dest_arg t) acc
| _ => augment_norm true t acc
- val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg
+ val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
fun cterm_lincomb_cmul c t =
- if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t
+ if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
- val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg
+ val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
fun int_lincomb_cmul c t =
- if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t
+ if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
--- a/src/HOL/SAT.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/SAT.thy Thu Sep 02 18:45:23 2010 +0200
@@ -10,7 +10,6 @@
theory SAT
imports Refute
uses
- "Tools/cnf_funcs.ML"
"Tools/sat_funcs.ML"
begin
--- a/src/HOL/Sledgehammer.thy Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Sep 02 18:45:23 2010 +0200
@@ -26,6 +26,9 @@
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
+lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by simp
+
definition skolem_id :: "'a \<Rightarrow> 'a" where
[no_atp]: "skolem_id = (\<lambda>x. x)"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 02 18:45:23 2010 +0200
@@ -310,7 +310,7 @@
val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
val intros_graph_of =
- Graph.map_nodes (#intros o rep_pred_data) o PredData.get o ProofContext.theory_of
+ Graph.map (K (#intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
(* diagnostic display functions *)
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Thu Sep 02 18:45:23 2010 +0200
@@ -133,7 +133,7 @@
fun complete (vT as (v, _)) subst =
subst
|> not (Vartab.defined subst v) ? Vartab.update vT
- |> Vartab.map (apsnd (Term.map_atyps (replace vT)))
+ |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Thu Sep 02 18:45:23 2010 +0200
@@ -191,7 +191,7 @@
fun cert @{term True} = @{cterm "~False"}
| cert t = certify ctxt' t
- in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end
+ in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Thu Sep 02 18:45:23 2010 +0200
@@ -823,7 +823,7 @@
fun result (p, (cx, _)) = (thm_of p, cx)
in
- (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map Unproved ptab)))
+ (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
end
fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt =
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 18:45:23 2010 +0200
@@ -10,7 +10,8 @@
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
- val cnf_axiom: theory -> thm -> thm list
+ val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
+ val cnf_axiom : theory -> thm -> thm list
end;
structure Clausifier : CLAUSIFIER =
@@ -228,19 +229,26 @@
|> Meson.make_nnf ctxt
in (th3, ctxt) end
+fun to_definitional_cnf_with_quantifiers thy th =
+ let
+ val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = eqth RS @{thm eq_reflection}
+ val eqth = eqth RS @{thm TruepropI}
+ in Thm.equal_elim eqth th end
+
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
fun cnf_axiom thy th =
let
val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val sko_ths = map (skolem_theorem_of_def thy)
- (assume_skolem_funs nnfth)
- val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
+ val (nnf_th, ctxt) = to_nnf th ctxt0
+ val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
+ val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
+ val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
in
- cnfs |> map introduce_combinators_in_theorem
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation
+ cnf_ths |> map introduce_combinators_in_theorem
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation
end
handle THM _ => []
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 18:45:23 2010 +0200
@@ -795,13 +795,15 @@
fun generic_metis_tac mode ctxt ths i st0 =
let
+ val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (maps neg_clausify)
+ Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
+ (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end
--- a/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 18:45:23 2010 +0200
@@ -430,7 +430,7 @@
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
+ | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
+ | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()
--- a/src/HOL/Tools/meson.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Sep 02 18:45:23 2010 +0200
@@ -25,7 +25,9 @@
val depth_prolog_tac: thm list -> tactic
val gocls: thm list -> thm list
val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
- val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic
+ val MESON:
+ (int -> tactic) -> (thm list -> thm list) -> (thm list -> tactic)
+ -> Proof.context -> int -> tactic
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
val safe_best_meson_tac: Proof.context -> int -> tactic
val depth_meson_tac: Proof.context -> int -> tactic
@@ -315,8 +317,8 @@
(nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
fun resop nf [prem] = resolve_tac (nf prem) 1;
-(*Any need to extend this list with
- "HOL.type_class","HOL.eq_class","Pure.term"?*)
+(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
+ and "Pure.term"? *)
val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
fun apply_skolem_theorem (th, rls) =
@@ -573,7 +575,8 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+fun make_clauses_unsorted ths = fold_rev add_clauses ths []
+handle exn => error (ML_Compiler.exn_message exn) (*###*)
val make_clauses = sort_clauses o make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
@@ -598,20 +601,22 @@
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)
-fun MESON mkcl cltac ctxt i st =
+fun MESON preskolem_tac mkcl cltac ctxt i st =
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac 1,
rtac ccontr 1,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [skolemize_prems_tac ctxt negs,
+ EVERY1 [preskolem_tac,
+ skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
+
(** Best-first search versions **)
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
fun best_meson_tac sizef =
- MESON make_clauses
+ MESON (K all_tac) make_clauses
(fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
(has_fewer_prems 1, sizef)
@@ -625,7 +630,7 @@
(** Depth-first search version **)
val depth_meson_tac =
- MESON make_clauses
+ MESON (K all_tac) make_clauses
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
@@ -645,7 +650,7 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
-fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON (K all_tac) make_clauses
(fn cls =>
(case (gocls (cls @ ths)) of
[] => no_tac (*no goal clauses*)
--- a/src/Pure/General/graph.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/General/graph.ML Thu Sep 02 18:45:23 2010 +0200
@@ -21,7 +21,7 @@
val maximals: 'a T -> key list
val subgraph: (key -> bool) -> 'a T -> 'a T
val get_entry: 'a T -> key -> 'a * (key list * key list) (*exception UNDEF*)
- val map_nodes: ('a -> 'b) -> 'a T -> 'b T
+ val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
@@ -114,7 +114,7 @@
(* nodes *)
-fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
+fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
fun get_node G = #1 o get_entry G;
@@ -161,7 +161,7 @@
fun del_nodes xs (Graph tab) =
Graph (tab
|> fold Table.delete xs
- |> Table.map (fn (i, (preds, succs)) =>
+ |> Table.map (fn _ => fn (i, (preds, succs)) =>
(i, (fold remove_key xs preds, fold remove_key xs succs))));
fun del_node x (G as Graph tab) =
@@ -206,13 +206,13 @@
fun join f (G1 as Graph tab1, G2 as Graph tab2) =
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
if pointer_eq (G1, G2) then G1
- else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2)))
+ else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2)))
end;
fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
if pointer_eq (G1, G2) then G1
- else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2)))
+ else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2)))
end;
fun merge eq GG = gen_merge add_edge eq GG;
@@ -286,6 +286,7 @@
(*final declarations of this structure!*)
+val map = map_nodes;
val fold = fold_graph;
end;
--- a/src/Pure/General/table.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/General/table.ML Thu Sep 02 18:45:23 2010 +0200
@@ -20,8 +20,7 @@
exception UNDEF of key
val empty: 'a table
val is_empty: 'a table -> bool
- val map: ('a -> 'b) -> 'a table -> 'b table
- val map': (key -> 'a -> 'b) -> 'a table -> 'b table
+ val map: (key -> 'a -> 'b) -> 'a table -> 'b table
val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
val dest: 'a table -> (key * 'a) list
@@ -403,8 +402,7 @@
(*final declarations of this structure!*)
-fun map f = map_table (K f);
-val map' = map_table;
+val map = map_table;
val fold = fold_table;
val fold_rev = fold_rev_table;
--- a/src/Pure/Isar/attrib.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Sep 02 18:45:23 2010 +0200
@@ -392,7 +392,8 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (register_config Unify.trace_bound_value #>
+ (register_config show_question_marks_value #>
+ register_config Unify.trace_bound_value #>
register_config Unify.search_bound_value #>
register_config Unify.trace_simp_value #>
register_config Unify.trace_types_value #>
--- a/src/Pure/Isar/code.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/Isar/code.ML Thu Sep 02 18:45:23 2010 +0200
@@ -282,7 +282,7 @@
then NONE
else thy
|> (Code_Data.map o apfst)
- ((map_functions o Symtab.map) (fn ((changed, current), history) =>
+ ((map_functions o Symtab.map) (fn _ => fn ((changed, current), history) =>
((false, current),
if changed then (serial (), current) :: history else history))
#> map_history_concluded (K true))
--- a/src/Pure/Isar/proof_context.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Sep 02 18:45:23 2010 +0200
@@ -413,8 +413,7 @@
SOME (x, i) =>
(case try Name.dest_skolem x of
NONE => Pretty.mark Markup.var (Pretty.str s)
- | SOME x' => Pretty.mark Markup.skolem
- (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
+ | SOME x' => Pretty.mark Markup.skolem (Pretty.str (Term.string_of_vname (x', i))))
| NONE => Pretty.mark Markup.var (Pretty.str s));
fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
@@ -536,14 +535,16 @@
fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
(not (abbrev_mode ctxt)) (consts_of ctxt);
-fun reject_schematic (Var (xi, _)) =
- error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
- | reject_schematic (Abs (_, _, t)) = reject_schematic t
- | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
- | reject_schematic _ = ();
+fun expand_binds ctxt =
+ let
+ val Mode {pattern, schematic, ...} = get_mode ctxt;
-fun expand_binds ctxt =
- let val Mode {pattern, schematic, ...} = get_mode ctxt in
+ fun reject_schematic (t as Var _) =
+ error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t)
+ | reject_schematic (Abs (_, _, t)) = reject_schematic t
+ | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
+ | reject_schematic _ = ();
+ in
if pattern then I
else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic)
end;
@@ -576,9 +577,9 @@
val _ =
pattern orelse schematic orelse
T |> Term.exists_subtype
- (fn TVar (xi, _) =>
+ (fn T as TVar (xi, _) =>
not (Type_Infer.is_param xi) andalso
- error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
+ error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T)
| _ => false)
in T end;
--- a/src/Pure/ProofGeneral/preferences.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Thu Sep 02 18:45:23 2010 +0200
@@ -141,7 +141,7 @@
"prems-limit"
"Setting for maximum number of premises printed",
print_depth_pref,
- bool_pref show_question_marks
+ bool_pref show_question_marks_default
"show-question-marks"
"Show leading question mark of variable name"];
--- a/src/Pure/Syntax/printer.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Thu Sep 02 18:45:23 2010 +0200
@@ -12,6 +12,9 @@
val show_no_free_types: bool Unsynchronized.ref
val show_all_types: bool Unsynchronized.ref
val show_structs: bool Unsynchronized.ref
+ val show_question_marks_default: bool Unsynchronized.ref
+ val show_question_marks_value: Config.value Config.T
+ val show_question_marks: bool Config.T
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
@@ -52,6 +55,11 @@
val show_all_types = Unsynchronized.ref false;
val show_structs = Unsynchronized.ref false;
+val show_question_marks_default = Unsynchronized.ref true;
+val show_question_marks_value =
+ Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
+val show_question_marks = Config.bool show_question_marks_value;
+
fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
@@ -72,15 +80,18 @@
(* simple_ast_of *)
-fun simple_ast_of (Const (c, _)) = Ast.Constant c
- | simple_ast_of (Free (x, _)) = Ast.Variable x
- | simple_ast_of (Var (xi, _)) = Ast.Variable (Term.string_of_vname xi)
- | simple_ast_of (t as _ $ _) =
- let val (f, args) = strip_comb t in
- Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
- end
- | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
- | simple_ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+fun simple_ast_of ctxt =
+ let
+ val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
+ fun ast_of (Const (c, _)) = Ast.Constant c
+ | ast_of (Free (x, _)) = Ast.Variable x
+ | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
+ | ast_of (t as _ $ _) =
+ let val (f, args) = strip_comb t
+ in Ast.mk_appl (ast_of f) (map ast_of args) end
+ | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
+ | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+ in ast_of end;
@@ -88,14 +99,14 @@
fun ast_of_termT ctxt trf tm =
let
- fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
- | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
+ | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
| ast_of (Const (a, _)) = trans a []
| ast_of (t as _ $ _) =
(case strip_comb t of
(Const (a, _), args) => trans a args
| (f, args) => Ast.Appl (map ast_of (f :: args)))
- | ast_of t = simple_ast_of t
+ | ast_of t = simple_ast_of ctxt t
and trans a args =
ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
@@ -168,7 +179,7 @@
if show_all_types
then Ast.mk_appl (constrain const T) (map ast_of ts)
else trans c T ts
- | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
+ | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args =
ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
@@ -176,9 +187,9 @@
and constrain t T =
if show_types andalso T <> dummyT then
- Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
+ Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
- else simple_ast_of t;
+ else simple_ast_of ctxt t;
in
tm
|> Syn_Trans.prop_tr'
--- a/src/Pure/Thy/thy_info.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Sep 02 18:45:23 2010 +0200
@@ -346,6 +346,6 @@
(* finish all theories *)
-fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
+fun finish () = change_thys (Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
end;
--- a/src/Pure/Thy/thy_output.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Thu Sep 02 18:45:23 2010 +0200
@@ -447,7 +447,7 @@
val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
-val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks o boolean);
+val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
--- a/src/Pure/context.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/context.ML Thu Sep 02 18:45:23 2010 +0200
@@ -137,7 +137,7 @@
val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
in k end;
-val extend_data = Datatab.map' invoke_extend;
+val extend_data = Datatab.map invoke_extend;
fun merge_data pp (data1, data2) =
Datatab.keys (Datatab.merge (K true) (data1, data2))
@@ -476,7 +476,7 @@
| NONE => raise Fail "Invalid proof data identifier");
fun init_data thy =
- Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
+ Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
fun init_new_data data thy =
Datatab.merge (K true) (data, init_data thy);
--- a/src/Pure/proofterm.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/proofterm.ML Thu Sep 02 18:45:23 2010 +0200
@@ -515,7 +515,7 @@
| remove_types t = t;
fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
- Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
+ Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv};
fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
--- a/src/Pure/sorts.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/sorts.ML Thu Sep 02 18:45:23 2010 +0200
@@ -321,7 +321,7 @@
| NONE => NONE)
else NONE;
val classes' = classes |> Graph.subgraph P;
- val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
+ val arities' = arities |> Symtab.map (map_filter o restrict_arity);
in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
--- a/src/Pure/term.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Pure/term.ML Thu Sep 02 18:45:23 2010 +0200
@@ -114,7 +114,6 @@
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
- val show_question_marks: bool Unsynchronized.ref
end;
signature TERM =
@@ -983,11 +982,8 @@
(* display variables *)
-val show_question_marks = Unsynchronized.ref true;
-
fun string_of_vname (x, i) =
let
- val question_mark = if ! show_question_marks then "?" else "";
val idx = string_of_int i;
val dot =
(case rev (Symbol.explode x) of
@@ -996,9 +992,9 @@
| c :: _ => Symbol.is_digit c
| _ => true);
in
- if dot then question_mark ^ x ^ "." ^ idx
- else if i <> 0 then question_mark ^ x ^ idx
- else question_mark ^ x
+ if dot then "?" ^ x ^ "." ^ idx
+ else if i <> 0 then "?" ^ x ^ idx
+ else "?" ^ x
end;
fun string_of_vname' (x, ~1) = x
--- a/src/Tools/Code/code_haskell.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Sep 02 18:45:23 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,13 +396,13 @@
val _ = File.mkdir_leaf (Path.dir pathname);
in File.write pathname
("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
- ^ string_of_pretty width content)
+ ^ format [] width content)
end
- | write_module width NONE (_, content) = writeln_pretty 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))
- (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
+ (fn present => fn width => rpair [] o format present width o Pretty.chunks o map snd)
(map (uncurry print_module) includes
@ map serialize_module (Symtab.dest hs_program))
end;
--- a/src/Tools/Code/code_ml.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Sep 02 18:45:23 2010 +0200
@@ -707,73 +707,39 @@
(** SML/OCaml generic part **)
-local
-
-datatype ml_node =
- Dummy of string
- | Stmt of string * ml_stmt
- | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
-
-in
-
-fun ml_node_of_program labelled_name reserved module_alias program =
+fun ml_program_of_program labelled_name reserved module_alias program =
let
- val reserved = Name.make_context reserved;
- val empty_module = ((reserved, reserved), Graph.empty);
- fun map_node [] f = f
- | map_node (m::ms) f =
- Graph.default_node (m, Module (m, empty_module))
- #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
- Module (module_name, (nsp, map_node ms f nodes)));
- fun map_nsp_yield [] f (nsp, nodes) =
- let
- val (x, nsp') = f nsp
- in (x, (nsp', nodes)) end
- | map_nsp_yield (m::ms) f (nsp, nodes) =
- let
- val (x, nodes') =
- nodes
- |> Graph.default_node (m, Module (m, empty_module))
- |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
- let
- val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
- in (x, Module (d_module_name, nsp_nodes')) end)
- in (x, (nsp, nodes')) end;
- fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
+ fun namify_const upper base (nsp_const, nsp_type) =
+ let
+ val (base', nsp_const') = yield_singleton Name.variants
+ (if upper then first_upper base else base) nsp_const
+ in (base', (nsp_const', nsp_type)) end;
+ fun namify_type base (nsp_const, nsp_type) =
let
- val (x, nsp_fun') = f nsp_fun
- in (x, (nsp_fun', nsp_typ)) end;
- fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
- let
- val (x, nsp_typ') = f nsp_typ
- in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = mk_name_module reserved NONE module_alias program;
- fun mk_name_stmt upper name nsp =
- let
- val (_, base) = dest_name name;
- val base' = if upper then first_upper base else base;
- val ([base''], nsp') = Name.variants [base'] nsp;
- in (base'', nsp') end;
- fun deps_of names =
- []
- |> fold (fold (insert (op =)) o Graph.imm_succs program) names
- |> subtract (op =) names
- |> filter_out (Code_Thingol.is_case o Graph.get_node program);
+ val (base', nsp_type') = yield_singleton Name.variants base nsp_type
+ in (base', (nsp_const, nsp_type')) end;
+ fun namify_stmt (Code_Thingol.Fun _) = namify_const false
+ | namify_stmt (Code_Thingol.Datatype _) = namify_type
+ | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
+ | namify_stmt (Code_Thingol.Class _) = namify_type
+ | namify_stmt (Code_Thingol.Classrel _) = namify_const false
+ | namify_stmt (Code_Thingol.Classparam _) = namify_const false
+ | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
let
val eqs = filter (snd o snd) raw_eqs;
- val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
+ val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
| _ => (eqs, NONE)
else (eqs, NONE)
- in (ML_Function (name, (tysm, eqs')), is_value) end
+ in (ML_Function (name, (tysm, eqs')), some_value_name) end
| ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
(ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
| ml_binding_of_stmt (name, _) =
error ("Binding block containing illegal statement: " ^ labelled_name name)
- fun add_fun (name, stmt) =
+ fun modify_fun (name, stmt) =
let
val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
val ml_stmt = case binding
@@ -784,157 +750,73 @@
of NONE => ML_Funs ([binding], [])
| SOME (name, true) => ML_Funs ([binding], [name])
| SOME (name, false) => ML_Val binding
- in
- map_nsp_fun_yield (mk_name_stmt false name)
- #>> (fn name' => ([name'], ml_stmt))
- end;
- fun add_funs stmts =
- let
- val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
- in
- fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
- #>> rpair ml_stmt
- end;
- fun add_datatypes stmts =
- fold_map
- (fn (name, Code_Thingol.Datatype (_, stmt)) =>
- map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
- | (name, Code_Thingol.Datatypecons _) =>
- map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
- | (name, _) =>
- error ("Datatype block containing illegal statement: " ^ labelled_name name)
- ) stmts
- #>> (split_list #> apsnd (map_filter I
- #> (fn [] => error ("Datatype block without data statement: "
- ^ (Library.commas o map (labelled_name o fst)) stmts)
- | stmts => ML_Datas stmts)));
- fun add_class stmts =
- fold_map
- (fn (name, Code_Thingol.Class (_, stmt)) =>
- map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
- | (name, Code_Thingol.Classrel _) =>
- map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
- | (name, Code_Thingol.Classparam _) =>
- map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
- | (name, _) =>
- error ("Class block containing illegal statement: " ^ labelled_name name)
- ) stmts
- #>> (split_list #> apsnd (map_filter I
- #> (fn [] => error ("Class block without class statement: "
- ^ (Library.commas o map (labelled_name o fst)) stmts)
- | [stmt] => ML_Class stmt)));
- fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
- add_fun stmt
- | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
- add_funs stmts
- | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
- add_datatypes stmts
- | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
- add_datatypes stmts
- | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
- add_class stmts
- | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
- add_class stmts
- | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
- add_class stmts
- | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
- add_fun stmt
- | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
- add_funs stmts
- | add_stmts stmts = error ("Illegal mutual dependencies: " ^
+ in SOME ml_stmt end;
+ fun modify_funs stmts = single (SOME
+ (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
+ fun modify_datatypes stmts = single (SOME
+ (ML_Datas (map_filter
+ (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
+ 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, 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 (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 _)::_)) =
+ modify_datatypes stmts
+ | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
+ modify_class stmts
+ | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
+ modify_class stmts
+ | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
+ modify_class stmts
+ | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
+ [modify_fun stmt]
+ | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+ modify_funs stmts
+ | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
(Library.commas o map (labelled_name o fst)) stmts);
- fun add_stmts' stmts nsp_nodes =
- let
- val names as (name :: names') = map fst stmts;
- val deps = deps_of names;
- val (module_names, _) = (split_list o map dest_name) names;
- val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
- handle Empty =>
- error ("Different namespace prefixes for mutual dependencies:\n"
- ^ Library.commas (map labelled_name names)
- ^ "\n"
- ^ Library.commas module_names);
- val module_name_path = Long_Name.explode module_name;
- fun add_dep name name' =
- let
- val module_name' = (mk_name_module o fst o dest_name) name';
- in if module_name = module_name' then
- map_node module_name_path (Graph.add_edge (name, name'))
- else let
- val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
- (module_name_path, Long_Name.explode module_name');
- in
- map_node common
- (fn node => Graph.add_edge_acyclic (diff1, diff2) node
- handle Graph.CYCLES _ => error ("Dependency "
- ^ quote name ^ " -> " ^ quote name'
- ^ " would result in module dependency cycle"))
- end end;
- in
- nsp_nodes
- |> map_nsp_yield module_name_path (add_stmts stmts)
- |-> (fn (base' :: bases', stmt') =>
- apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
- #> fold2 (fn name' => fn base' =>
- Graph.new_node (name', (Dummy base'))) names' bases')))
- |> apsnd (fold (fn name => fold (add_dep name) deps) names)
- |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
- end;
- val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program))
- |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false);
- val (_, nodes) = fold add_stmts' stmts empty_module;
- fun deresolver prefix name =
- let
- val module_name = (fst o dest_name) name;
- val module_name' = (Long_Name.explode o mk_name_module) module_name;
- val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
- val stmt_name =
- nodes
- |> fold (fn name => fn node => case Graph.get_node node name
- of Module (_, (_, node)) => node) module_name'
- |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
- | Dummy stmt_name => stmt_name);
- in
- Long_Name.implode (remainder @ [stmt_name])
- end handle Graph.UNDEF _ =>
- error ("Unknown statement name: " ^ labelled_name name);
- in (deresolver, nodes) end;
+ in
+ Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
+ empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
+ cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
+ end;
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, nodes) = ml_node_of_program labelled_name
- reserved_syms module_alias program;
- val reserved = make_vars reserved_syms;
- fun print_node prefix (Dummy _) =
+ 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 (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 reserved is_cons (deresolver prefix) stmt)
- | print_node prefix (Module (module_name, (_, nodes))) =
+ | 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 @ [module_name]) nodes;
- val p = if is_presentation then Pretty.chunks2 body
- else print_module module_name (if with_signatures then SOME decls else NONE) body;
+ val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
+ val p = print_module name_fragment
+ (if with_signatures then SOME decls else NONE) body;
in SOME ([], p) end
- and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
+ and print_nodes prefix_fragments nodes = (map_filter
+ (fn name => print_node prefix_fragments (name, snd (Graph.get_node nodes name)))
o rev o flat o Graph.strong_conn) nodes
|> split_list
|> (fn (decls, body) => (flat decls, body))
val names' = map (try (deresolver [])) names;
- val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
- fun write width NONE = writeln_pretty width
- | write width (SOME p) = File.write p o string_of_pretty width;
+ val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
+ fun write width NONE = writeln o format [] width
+ | write width (SOME p) = File.write p o format [] width;
in
- Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
+ Code_Target.serialization write (rpair names' ooo format) p
end;
-end; (*local*)
-
val serializer_sml : Code_Target.serializer =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
>> (fn with_signatures => serialize_ml target_SML
--- a/src/Tools/Code/code_namespace.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Tools/Code/code_namespace.ML Thu Sep 02 18:45:23 2010 +0200
@@ -6,31 +6,46 @@
signature CODE_NAMESPACE =
sig
- datatype 'a node =
+ val dest_name: string -> string * string
+ datatype ('a, 'b) node =
Dummy
- | Stmt of Code_Thingol.stmt
- | Module of ('a * (string * 'a node) Graph.T);
+ | Stmt of 'a
+ | Module of ('b * (string * ('a, 'b) node) Graph.T);
val hierarchical_program: (string -> string) -> { module_alias: string -> string option,
- reserved: Name.context, empty_nsp: 'b, namify_module: string -> 'b -> string * 'b,
- namify_stmt: Code_Thingol.stmt -> string -> 'b -> string * 'b,
- cyclic_modules: bool, empty_data: 'a, memorize_data: string -> 'a -> 'a }
+ reserved: Name.context, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
+ namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
+ cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b,
+ modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
-> Code_Thingol.program
-> { deresolver: string list -> string -> string,
- hierarchical_program: (string * 'a node) Graph.T }
+ hierarchical_program: (string * ('a, 'b) node) Graph.T }
end;
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 node =
+datatype ('a, 'b) node =
Dummy
- | Stmt of Code_Thingol.stmt
- | Module of ('a * (string * 'a node) Graph.T);
+ | Stmt of 'a
+ | Module of ('b * (string * ('a, 'b) node) Graph.T);
+
+fun map_module_content f (Module content) = Module (f content);
+
+fun map_module [] = I
+ | map_module (name_fragment :: name_fragments) =
+ apsnd o Graph.map_node name_fragment o apsnd o map_module_content
+ o map_module name_fragments;
fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
- namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data } program =
+ namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
let
(* building module name hierarchy *)
@@ -38,18 +53,13 @@
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);
- fun map_module f (Module content) = Module (f content);
- fun change_module [] = I
- | change_module (name_fragment :: name_fragments) =
- apsnd o Graph.map_node name_fragment o apsnd o map_module
- o change_module name_fragments;
fun ensure_module name_fragment (data, nodes) =
if can (Graph.get_node nodes) name_fragment then (data, nodes)
else (data,
@@ -57,7 +67,7 @@
fun allocate_module [] = I
| allocate_module (name_fragment :: name_fragments) =
ensure_module name_fragment
- #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+ #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
fragments_tab empty_module;
@@ -66,8 +76,7 @@
let
val (name_fragments, base) = dest_name name;
in
- change_module name_fragments (fn (data, nodes) =>
- (memorize_data name data, Graph.new_node (name, (base, Stmt stmt)) nodes))
+ (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
end;
fun add_dependency name name' =
let
@@ -75,42 +84,47 @@
val (name_fragments', base') = dest_name name';
val (name_fragments_common, (diff, diff')) =
chop_prefix (op =) (name_fragments, name_fragments');
- val (is_module, dep) = if null diff then (false, (name, name'))
- else (true, (hd diff, hd diff'))
+ val is_module = not (null diff andalso null diff');
+ val dep = pairself hd (diff @ [name], diff' @ [name']);
val add_edge = if is_module andalso not cyclic_modules
then (fn node => Graph.add_edge_acyclic dep node
handle Graph.CYCLES _ => error ("Dependency "
^ quote name ^ " -> " ^ quote name'
^ " would result in module dependency cycle"))
else Graph.add_edge dep
- in (change_module name_fragments_common o apsnd) add_edge end;
+ in (map_module name_fragments_common o apsnd) add_edge end;
val proto_program = empty_program
|> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
|> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
- (* name declarations *)
+ (* name declarations, data and statement modifications *)
fun make_declarations nsps (data, nodes) =
let
val (module_fragments, stmt_names) = List.partition
(fn name_fragment => case Graph.get_node nodes name_fragment
of (_, Module _) => true | _ => false) (Graph.keys nodes);
- fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
- | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
- | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
- | modify_stmt stmt = stmt;
- fun declare namify modify name (nsps, nodes) =
+ fun declare namify name (nsps, nodes) =
let
val (base, node) = Graph.get_node nodes name;
val (base', nsps') = namify node base nsps;
- val nodes' = Graph.map_node name (K (base', modify node)) nodes;
+ val nodes' = Graph.map_node name (K (base', node)) nodes;
in (nsps', nodes') end;
val (nsps', nodes') = (nsps, nodes)
- |> fold (declare (K namify_module) I) module_fragments
- |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
- val nodes'' = nodes'
- |> fold (fn name_fragment => (Graph.map_node name_fragment
- o apsnd o map_module) (make_declarations nsps')) module_fragments;
- in (data, nodes'') end;
+ |> fold (declare (K namify_module)) module_fragments
+ |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
+ fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
+ fun select_names names = case filter (member (op =) stmt_names) names
+ of [] => NONE
+ | xs => SOME xs;
+ val modify_stmts' = AList.make (snd o Graph.get_node nodes)
+ #> split_list
+ ##> map (fn Stmt stmt => stmt)
+ #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts)));
+ val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes;
+ val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
+ | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
+ val data' = fold memorize_data stmt_names data;
+ in (data', nodes'') end;
val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
(* deresolving *)
--- a/src/Tools/Code/code_printer.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Sep 02 18:45:23 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 string_of_pretty: int -> Pretty.T -> string
- val writeln_pretty: int -> Pretty.T -> unit
+ 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 =
@@ -104,9 +99,16 @@
open Code_Thingol;
+(** generic nonsense *)
+
fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
| eqn_error NONE s = error s;
+val code_presentationN = "code_presentation";
+val stmt_nameN = "stmt_name";
+val _ = Markup.add_mode code_presentationN YXML.output_markup;
+
+
(** assembling and printing text pieces **)
infixr 5 @@;
@@ -125,8 +127,35 @@
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
-fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
-fun writeln_pretty width p = writeln (string_of_pretty width p);
+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 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 **)
@@ -375,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 14:34:08 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Sep 02 18:45:23 2010 +0200
@@ -193,8 +193,7 @@
str "match", str "{"], str "}")
(map print_clause eqs)
end;
- val print_method = str o Library.enclose "`" "`" o space_implode "+"
- o Long_Name.explode o deresolve_full;
+ val print_method = str o Library.enclose "`" "`" o deresolve_full;
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
print_def name (vs, ty) (filter (snd o snd) raw_eqs)
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
@@ -318,21 +317,25 @@
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.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;
in
Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
- cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits } program
+ cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
end;
fun serialize_scala { labelled_name, reserved_syms, includes,
module_alias, class_syntax, tyco_syntax, const_syntax, program,
- names, presentation_names } =
+ names } =
let
(* build program *)
- val reserved = fold (insert (op =) o fst) includes reserved_syms;
val { deresolver, hierarchical_program = sca_program } =
- scala_program_of_program labelled_name (Name.make_context reserved) module_alias program;
+ scala_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
(* print statements *)
fun lookup_constr tyco constr = case Graph.get_node program tyco
@@ -352,7 +355,7 @@
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
- (make_vars reserved) args_num is_singleton_constr;
+ (make_vars reserved_syms) args_num is_singleton_constr;
(* print nodes *)
fun print_module base implicit_ps p = Pretty.chunks2
@@ -364,23 +367,17 @@
let
val s = deresolver prefix_fragments implicit;
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
- fun print_node _ (_, Dummy) = NONE
+ 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)))
@@ -388,12 +385,11 @@
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_pretty width
- | write width (SOME p) = File.write p o string_of_pretty 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 [] oo string_of_pretty) p
+ Code_Target.serialization write (rpair [] ooo format) p
end;
val serializer : Code_Target.serializer =
--- a/src/Tools/Code/code_target.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Sep 02 18:45:23 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)
- -> (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 width content)
- | serialization _ string content width (Present _) = SOME (string 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.")
--- a/src/Tools/WWW_Find/find_theorems.ML Thu Sep 02 14:34:08 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Thu Sep 02 18:45:23 2010 +0200
@@ -143,9 +143,9 @@
fun html_thm ctxt (n, (thmref, thm)) =
let
- val string_of_thm =
+ val output_thm =
Output.output o Pretty.string_of_margin 100 o
- setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
+ Display.pretty_thm (Config.put show_question_marks false ctxt);
in
tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
[
@@ -153,7 +153,7 @@
[span' (sorry_class thm)
[raw_text (Facts.string_of_ref thmref)]
],
- tag' "td" (class "thm") [pre noid (string_of_thm thm)]
+ tag' "td" (class "thm") [pre noid (output_thm thm)]
]
end;
@@ -236,7 +236,7 @@
end;
in
-val () = show_question_marks := false;
+val () = show_question_marks_default := false;
val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
end;