--- a/Admin/isatest/isatest-makeall Mon Apr 19 07:38:08 2010 +0200
+++ b/Admin/isatest/isatest-makeall Mon Apr 19 07:38:35 2010 +0200
@@ -186,7 +186,7 @@
echo >> $ERRORLOG
FAIL="$FAIL$SHORT "
- (cd $ERRORDIR; ln -s $TESTLOG)
+ (cd $ERRORDIR; cp -a $TESTLOG .)
fi
rm -f $RUNNING/$SHORT.running
--- a/Admin/isatest/isatest-makedist Mon Apr 19 07:38:08 2010 +0200
+++ b/Admin/isatest/isatest-makedist Mon Apr 19 07:38:35 2010 +0200
@@ -55,6 +55,7 @@
echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
rm -rf $HOME/isabelle-*
+ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly"
echo "### building distribution" >> $DISTLOG 2>&1
mkdir -p $DISTPREFIX
@@ -81,6 +82,9 @@
cd $DISTPREFIX >> $DISTLOG 2>&1
$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
+ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \
+rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/.
+
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
--- a/NEWS Mon Apr 19 07:38:08 2010 +0200
+++ b/NEWS Mon Apr 19 07:38:35 2010 +0200
@@ -71,6 +71,10 @@
in subsequent goal refinement steps. Tracing may also still be
enabled or disabled via the ProofGeneral settings menu.
+* Separate commands 'hide_class', 'hide_type', 'hide_const',
+'hide_fact' replace the former 'hide' KIND command. Minor
+INCOMPATIBILITY.
+
*** Pure ***
@@ -97,9 +101,9 @@
within a local theory context, with explicit checking of the
constructors involved (in contrast to the raw 'syntax' versions).
-* Command 'typedecl' now works within a local theory context --
-without introducing dependencies on parameters or assumptions, which
-is not possible in Isabelle/Pure.
+* Commands 'types' and 'typedecl' now work within a local theory
+context -- without introducing dependencies on parameters or
+assumptions, which is not possible in Isabelle/Pure.
* Proof terms: Type substitutions on proof constants now use canonical
order of type variables. INCOMPATIBILITY: Tools working with proof
@@ -298,6 +302,10 @@
* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
syntax constant (cf. 'syntax' command).
+* Antiquotation @{make_string} inlines a function to print arbitrary
+values similar to the ML toplevel. The result is compiler dependent
+and may fall back on "?" in certain situations.
+
* Renamed old-style Drule.standard to Drule.export_without_context, to
emphasize that this is in no way a standard operation.
INCOMPATIBILITY.
--- a/doc-src/Codegen/Thy/Program.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Mon Apr 19 07:38:35 2010 +0200
@@ -430,7 +430,7 @@
subsection {* Inductive Predicates *}
(*<*)
-hide const append
+hide_const append
inductive append
where
--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Apr 19 07:38:35 2010 +0200
@@ -334,7 +334,7 @@
this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
- \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
+ \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
"\<alpha>"}-equivalence of two terms. This is the basic equality relation
on type @{ML_type term}; raw datatype equality should only be used
for operations related to parsing or printing!
--- a/doc-src/IsarImplementation/Thy/ML.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Apr 19 07:38:35 2010 +0200
@@ -209,7 +209,7 @@
options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
"string"} (see structure @{ML_struct Config} and @{ML
Attrib.config_bool} etc.), and lists of theorems (see functor
- @{ML_functor NamedThmsFun}).
+ @{ML_functor Named_Thms}).
\item Keep components with local state information
\emph{re-entrant}. Instead of poking initial values into (private)
@@ -623,7 +623,7 @@
whenever such pure finite mappings are neccessary.
The key type of tables must be given explicitly by instantiating
- the @{ML_functor TableFun} functor which takes the key type
+ the @{ML_functor Table} functor which takes the key type
together with its @{ML_type order}; for convience, we restrict
here to the @{ML_struct Symtab} instance with @{ML_type string}
as key type.
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Apr 19 07:38:35 2010 +0200
@@ -222,7 +222,7 @@
\secref{sec:context-data}) there are drop-in replacements that
emulate primitive references for common cases of \emph{configuration
options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
- \verb|NamedThmsFun|).
+ \verb|Named_Thms|).
\item Keep components with local state information
\emph{re-entrant}. Instead of poking initial values into (private)
@@ -763,7 +763,7 @@
whenever such pure finite mappings are neccessary.
The key type of tables must be given explicitly by instantiating
- the \verb|TableFun| functor which takes the key type
+ the \verb|Table| functor which takes the key type
together with its \verb|order|; for convience, we restrict
here to the \verb|Symtab| instance with \verb|string|
as key type.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Apr 19 07:38:35 2010 +0200
@@ -178,7 +178,7 @@
\end{matharray}
\begin{rail}
- 'record' typespec '=' (type '+')? (constdecl +)
+ 'record' typespecsorts '=' (type '+')? (constdecl +)
;
\end{rail}
--- a/doc-src/IsarRef/Thy/Spec.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon Apr 19 07:38:35 2010 +0200
@@ -953,7 +953,7 @@
text {*
\begin{matharray}{rcll}
- @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
@@ -1225,11 +1225,14 @@
\begin{matharray}{rcl}
@{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}
- 'hide' ('(open)')? name (nameref + )
+ ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
;
\end{rail}
@@ -1251,17 +1254,20 @@
Note that global names are prone to get hidden accidently later,
when qualified names of the same base name are introduced.
- \item @{command "hide"}~@{text "space names"} fully removes
- declarations from a given name space (which may be @{text "class"},
- @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
- "(open)"} option, only the base name is hidden. Global
- (unqualified) names may never be hidden.
-
+ \item @{command "hide_class"}~@{text names} fully removes class
+ declarations from a given name space; with the @{text "(open)"}
+ option, only the base name is hidden. Global (unqualified) names
+ may never be hidden.
+
Note that hiding name space accesses has no impact on logical
declarations --- they remain valid internally. Entities that are no
longer accessible to the user are printed with the special qualifier
``@{text "??"}'' prefixed to the full internal name.
+ \item @{command "hide_type"}, @{command "hide_const"}, and @{command
+ "hide_fact"} are similar to @{command "hide_class"}, but hide types,
+ constants, and facts, respectively.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Apr 19 07:38:35 2010 +0200
@@ -202,7 +202,7 @@
\end{matharray}
\begin{rail}
- 'record' typespec '=' (type '+')? (constdecl +)
+ 'record' typespecsorts '=' (type '+')? (constdecl +)
;
\end{rail}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Apr 19 07:38:35 2010 +0200
@@ -990,7 +990,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcll}
- \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
\end{matharray}
@@ -1268,11 +1268,14 @@
\begin{matharray}{rcl}
\indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+ \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\end{matharray}
\begin{rail}
- 'hide' ('(open)')? name (nameref + )
+ ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
;
\end{rail}
@@ -1292,16 +1295,19 @@
Note that global names are prone to get hidden accidently later,
when qualified names of the same base name are introduced.
- \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
- declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
- \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global
- (unqualified) names may never be hidden.
-
+ \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
+ declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
+ option, only the base name is hidden. Global (unqualified) names
+ may never be hidden.
+
Note that hiding name space accesses has no impact on logical
declarations --- they remain valid internally. Entities that are no
longer accessible to the user are printed with the special qualifier
``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
+ \item \hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}, \hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}, and \hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}} are similar to \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}, but hide types,
+ constants, and facts, respectively.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Locales/Locales/Examples.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Mon Apr 19 07:38:35 2010 +0200
@@ -2,7 +2,7 @@
imports Main
begin
-hide %invisible const Lattices.lattice
+hide_const %invisible Lattices.lattice
pretty_setmargin %invisible 65
(*
--- a/doc-src/Locales/Locales/document/Examples.tex Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex Mon Apr 19 07:38:35 2010 +0200
@@ -25,8 +25,8 @@
\endisadeliminvisible
%
\isataginvisible
-\isacommand{hide}\isamarkupfalse%
-\ const\ Lattices{\isachardot}lattice\isanewline
+\isacommand{hide{\isacharunderscore}const}\isamarkupfalse%
+\ Lattices{\isachardot}lattice\isanewline
\isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse%
\ {\isadigit{6}}{\isadigit{5}}%
\endisataginvisible
--- a/doc-src/System/Thy/Basics.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/System/Thy/Basics.thy Mon Apr 19 07:38:35 2010 +0200
@@ -162,6 +162,17 @@
some extend. In particular, site-wide defaults may be overridden by
a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
+ \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
+ set to a symbolic identifier for the underlying hardware and
+ operating system. The Isabelle platform identification always
+ refers to the 32 bit variant, even this is a 64 bit machine. Note
+ that the ML or Java runtime may have a different idea, depending on
+ which binaries are actually run.
+
+ \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
+ @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
+ on a platform that supports this; the value is empty for 32 bit.
+
\item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
names of the @{executable "isabelle-process"} and @{executable
--- a/doc-src/System/Thy/document/Basics.tex Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Mon Apr 19 07:38:35 2010 +0200
@@ -180,6 +180,17 @@
some extend. In particular, site-wide defaults may be overridden by
a private \verb|$ISABELLE_HOME_USER/etc/settings|.
+ \item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is automatically
+ set to a symbolic identifier for the underlying hardware and
+ operating system. The Isabelle platform identification always
+ refers to the 32 bit variant, even this is a 64 bit machine. Note
+ that the ML or Java runtime may have a different idea, depending on
+ which binaries are actually run.
+
+ \item[\indexdef{}{setting}{ISABELLE\_PLATFORM64}\hypertarget{setting.ISABELLE-PLATFORM64}{\hyperlink{setting.ISABELLE-PLATFORM64}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM{\isadigit{6}}{\isadigit{4}}}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is similar to
+ \hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}} but refers to the proper 64 bit variant
+ on a platform that supports this; the value is empty for 32 bit.
+
\item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively. Thus other tools and scripts
need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
--- a/doc-src/TutorialI/Datatype/Nested.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Mon Apr 19 07:38:35 2010 +0200
@@ -11,7 +11,7 @@
Consider the following model of terms
where function symbols can be applied to a list of arguments:
*}
-(*<*)hide const Var(*>*)
+(*<*)hide_const Var(*>*)
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
text{*\noindent
--- a/doc-src/TutorialI/Documents/Documents.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Mon Apr 19 07:38:35 2010 +0200
@@ -138,7 +138,7 @@
*}
(*<*)
-hide const xor
+hide_const xor
setup {* Sign.add_path "version1" *}
(*>*)
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
@@ -161,7 +161,7 @@
*}
(*<*)
-hide const xor
+hide_const xor
setup {* Sign.add_path "version2" *}
(*>*)
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
--- a/doc-src/TutorialI/Misc/Option2.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Mon Apr 19 07:38:35 2010 +0200
@@ -1,7 +1,7 @@
(*<*)
theory Option2 imports Main begin
-hide const None Some
-hide type option
+hide_const None Some
+hide_type option
(*>*)
text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
--- a/doc-src/TutorialI/Types/Overloading.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Mon Apr 19 07:38:35 2010 +0200
@@ -1,6 +1,6 @@
(*<*)theory Overloading imports Main Setup begin
-hide (open) "class" plus (*>*)
+hide_class (open) plus (*>*)
text {* Type classes allow \emph{overloading}; thus a constant may
have multiple definitions at non-overlapping types. *}
--- a/doc-src/antiquote_setup.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/doc-src/antiquote_setup.ML Mon Apr 19 07:38:35 2010 +0200
@@ -54,7 +54,7 @@
fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
-fun ml_functor _ = ""; (*no check!*)
+fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
fun index_ml name kind ml = ThyOutput.antiquotation name
(Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
--- a/etc/isar-keywords-ZF.el Mon Apr 19 07:38:08 2010 +0200
+++ b/etc/isar-keywords-ZF.el Mon Apr 19 07:38:35 2010 +0200
@@ -82,7 +82,10 @@
"header"
"help"
"hence"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_cases"
"init_toplevel"
@@ -372,7 +375,10 @@
"extract_type"
"finalconsts"
"global"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"instantiation"
"judgment"
--- a/etc/isar-keywords.el Mon Apr 19 07:38:08 2010 +0200
+++ b/etc/isar-keywords.el Mon Apr 19 07:38:35 2010 +0200
@@ -115,7 +115,10 @@
"header"
"help"
"hence"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_cases"
"inductive_set"
@@ -494,7 +497,10 @@
"fixrec"
"fun"
"global"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_set"
"instantiation"
--- a/etc/settings Mon Apr 19 07:38:08 2010 +0200
+++ b/etc/settings Mon Apr 19 07:38:35 2010 +0200
@@ -55,7 +55,7 @@
### JVM components (Scala or Java)
###
-ISABELLE_JAVA="java"
+ISABELLE_JAVA="${THIS_JAVA:-java}"
ISABELLE_SCALA="scala"
[ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \
--- a/lib/scripts/getsettings Mon Apr 19 07:38:08 2010 +0200
+++ b/lib/scripts/getsettings Mon Apr 19 07:38:35 2010 +0200
@@ -27,6 +27,9 @@
"$ISABELLE_TOOL" "$@"
}
+#platform
+. "$ISABELLE_HOME/lib/scripts/isabelle-platform"
+
#Isabelle distribution identifier -- filled in automatically!
ISABELLE_IDENTIFIER=""
@@ -53,7 +56,7 @@
if [ "$OSTYPE" = cygwin ]; then
CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
function jvmpath() { cygpath -w -p "$@"; }
- CYGWIN_ROOT="$(jvmpath "/")"
+ THIS_CYGWIN="$(jvmpath "/")"
else
function jvmpath() { echo "$@"; }
fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/isabelle-platform Mon Apr 19 07:38:35 2010 +0200
@@ -0,0 +1,63 @@
+#
+# determine general hardware and operating system type for Isabelle
+#
+# NOTE: The ML system or JVM may have their own idea about the platform!
+
+ISABELLE_PLATFORM="unknown-platform"
+ISABELLE_PLATFORM64=""
+
+case $(uname -s) in
+ Linux)
+ case $(uname -m) in
+ i?86)
+ ISABELLE_PLATFORM=x86-linux
+ ;;
+ x86_64)
+ ISABELLE_PLATFORM=x86-linux
+ ISABELLE_PLATFORM64=x86_64-linux
+ ;;
+ esac
+ ;;
+ Darwin)
+ case $(uname -m) in
+ i?86)
+ ISABELLE_PLATFORM=x86-darwin
+ if [ "$(sysctl -n hw.optional.x86_64 2>/dev/null)" = 1 ]; then
+ ISABELLE_PLATFORM64=x86_64-darwin
+ fi
+ ;;
+ Power* | power* | ppc)
+ ISABELLE_PLATFORM=ppc-darwin
+ ;;
+ esac
+ ;;
+ CYGWIN_NT*)
+ case $(uname -m) in
+ i?86)
+ ISABELLE_PLATFORM=x86-cygwin
+ ;;
+ esac
+ ;;
+ SunOS)
+ case $(uname -r) in
+ 5.*)
+ case $(uname -p) in
+ sparc)
+ ISABELLE_PLATFORM=sparc-solaris
+ ;;
+ i?86)
+ ISABELLE_PLATFORM=x86-solaris
+ ;;
+ esac
+ ;;
+ esac
+ ;;
+ FreeBSD|NetBSD)
+ case $(uname -m) in
+ i?86)
+ ISABELLE_PLATFORM=x86-bsd
+ ;;
+ esac
+ ;;
+esac
+
--- a/src/FOL/FOL.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/FOL/FOL.thy Mon Apr 19 07:38:35 2010 +0200
@@ -371,7 +371,7 @@
lemmas induct_rulify_fallback =
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
-hide const induct_forall induct_implies induct_equal induct_conj
+hide_const induct_forall induct_implies induct_equal induct_conj
text {* Method setup. *}
--- a/src/HOL/Bali/Basis.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Bali/Basis.thy Mon Apr 19 07:38:35 2010 +0200
@@ -176,7 +176,7 @@
section "sums"
-hide const In0 In1
+hide_const In0 In1
notation sum_case (infixr "'(+')"80)
--- a/src/HOL/Bali/TypeSafe.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Mon Apr 19 07:38:35 2010 +0200
@@ -9,7 +9,7 @@
section "error free"
-hide const field
+hide_const field
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
--- a/src/HOL/Code_Evaluation.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Mon Apr 19 07:38:35 2010 +0200
@@ -280,8 +280,8 @@
end
*}
-hide const dummy_term App valapp
-hide (open) const Const termify valtermify term_of term_of_num
+hide_const dummy_term App valapp
+hide_const (open) Const termify valtermify term_of term_of_num
subsection {* Tracing of generated and evaluated code *}
@@ -301,7 +301,7 @@
code_const "tracing :: String.literal => 'a => 'a"
(Eval "Code'_Evaluation.tracing")
-hide (open) const tracing
+hide_const (open) tracing
code_reserved Eval Code_Evaluation
subsection {* Evaluation setup *}
--- a/src/HOL/Code_Numeral.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Mon Apr 19 07:38:35 2010 +0200
@@ -278,7 +278,7 @@
then show ?thesis by (auto simp add: int_of_def mult_ac)
qed
-hide (open) const of_nat nat_of int_of
+hide_const (open) of_nat nat_of int_of
subsubsection {* Lazy Evaluation of an indexed function *}
@@ -289,7 +289,7 @@
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
-hide (open) const iterate_upto
+hide_const (open) iterate_upto
subsection {* Code generator setup *}
--- a/src/HOL/DSequence.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/DSequence.thy Mon Apr 19 07:38:35 2010 +0200
@@ -97,13 +97,13 @@
code_reserved Eval DSequence
(*
-hide type Sequence.seq
+hide_type Sequence.seq
-hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
+hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
*)
-hide (open) const empty single eval map_seq bind union if_seq not_seq map
-hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
+hide_const (open) empty single eval map_seq bind union if_seq not_seq map
+hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
if_seq_def not_seq_def map_def
end
--- a/src/HOL/Datatype.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Datatype.thy Mon Apr 19 07:38:35 2010 +0200
@@ -512,8 +512,8 @@
text {* hides popular names *}
-hide (open) type node item
-hide (open) const Push Node Atom Leaf Numb Lim Split Case
+hide_type (open) node item
+hide_const (open) Push Node Atom Leaf Numb Lim Split Case
use "Tools/Datatype/datatype.ML"
--- a/src/HOL/Finite_Set.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Finite_Set.thy Mon Apr 19 07:38:35 2010 +0200
@@ -513,7 +513,7 @@
class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
setup {* Sign.parent_path *}
-hide const finite
+hide_const finite
context finite
begin
--- a/src/HOL/Fun.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Fun.thy Mon Apr 19 07:38:35 2010 +0200
@@ -525,7 +525,7 @@
lemma bij_swap_iff: "bij (swap a b f) = bij f"
by (simp add: bij_def)
-hide (open) const swap
+hide_const (open) swap
subsection {* Inversion of injective functions *}
--- a/src/HOL/Groups.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Groups.thy Mon Apr 19 07:38:35 2010 +0200
@@ -88,7 +88,7 @@
class one =
fixes one :: 'a ("1")
-hide (open) const zero one
+hide_const (open) zero one
syntax
"_index1" :: index ("\<^sub>1")
--- a/src/HOL/HOL.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/HOL.thy Mon Apr 19 07:38:35 2010 +0200
@@ -1567,7 +1567,7 @@
lemma [induct_simp]: "(x = x) = True"
by (rule simp_thms)
-hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
+hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
use "~~/src/Tools/induct_tacs.ML"
setup InductTacs.setup
@@ -1886,8 +1886,8 @@
Nbe.add_const_alias @{thm equals_alias_cert}
*}
-hide (open) const eq
-hide const eq
+hide_const (open) eq
+hide_const eq
text {* Cases *}
--- a/src/HOL/Imperative_HOL/Array.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Mon Apr 19 07:38:35 2010 +0200
@@ -92,7 +92,7 @@
return a
done)"
-hide (open) const new map -- {* avoid clashed with some popular names *}
+hide_const (open) new map -- {* avoid clashed with some popular names *}
subsection {* Properties *}
@@ -115,28 +115,28 @@
definition new' where
[code del]: "new' = Array.new o Code_Numeral.nat_of"
-hide (open) const new'
+hide_const (open) new'
lemma [code]:
"Array.new = Array.new' o Code_Numeral.of_nat"
by (simp add: new'_def o_def)
definition of_list' where
[code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
-hide (open) const of_list'
+hide_const (open) of_list'
lemma [code]:
"Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
by (simp add: of_list'_def)
definition make' where
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
-hide (open) const make'
+hide_const (open) make'
lemma [code]:
"Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
by (simp add: make'_def o_def)
definition length' where
[code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
-hide (open) const length'
+hide_const (open) length'
lemma [code]:
"Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
by (simp add: length'_def monad_simp',
@@ -145,14 +145,14 @@
definition nth' where
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
-hide (open) const nth'
+hide_const (open) nth'
lemma [code]:
"Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
by (simp add: nth'_def)
definition upd' where
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
-hide (open) const upd'
+hide_const (open) upd'
lemma [code]:
"Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- a/src/HOL/Imperative_HOL/Heap.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Mon Apr 19 07:38:35 2010 +0200
@@ -432,6 +432,6 @@
"array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
by (simp add: array_present_def new_ref_def ref_def Let_def)
-hide (open) const empty array array_of_list upd length ref
+hide_const (open) empty array array_of_list upd length ref
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Apr 19 07:38:35 2010 +0200
@@ -405,7 +405,7 @@
lemmas MREC_rule = mrec.MREC_rule
lemmas MREC_pinduct = mrec.MREC_pinduct
-hide (open) const heap execute
+hide_const (open) heap execute
subsection {* Code generator setup *}
@@ -426,7 +426,7 @@
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
-hide (open) const Fail raise_exc
+hide_const (open) Fail raise_exc
subsubsection {* SML and OCaml *}
--- a/src/HOL/Imperative_HOL/Ref.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Mon Apr 19 07:38:35 2010 +0200
@@ -41,7 +41,7 @@
return y
done)"
-hide (open) const new lookup update change
+hide_const (open) new lookup update change
subsection {* Properties *}
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Apr 19 07:38:35 2010 +0200
@@ -8,7 +8,7 @@
imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
begin
-hide (open) const swap rev
+hide_const (open) swap rev
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
"swap a i j = (do
--- a/src/HOL/Int.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Int.thy Mon Apr 19 07:38:35 2010 +0200
@@ -2263,7 +2263,7 @@
lemma [code]: "nat i = nat_aux i 0"
by (simp add: nat_aux_def)
-hide (open) const nat_aux
+hide_const (open) nat_aux
lemma zero_is_num_zero [code, code_unfold_post]:
"(0\<Colon>int) = Numeral0"
@@ -2325,7 +2325,7 @@
quickcheck_params [default_type = int]
-hide (open) const Pls Min Bit0 Bit1 succ pred
+hide_const (open) Pls Min Bit0 Bit1 succ pred
subsection {* Legacy theorems *}
--- a/src/HOL/Lattice/Bounds.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Lattice/Bounds.thy Mon Apr 19 07:38:35 2010 +0200
@@ -6,7 +6,7 @@
theory Bounds imports Orders begin
-hide (open) const inf sup
+hide_const (open) inf sup
subsection {* Infimum and supremum *}
--- a/src/HOL/Lazy_Sequence.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Mon Apr 19 07:38:35 2010 +0200
@@ -212,8 +212,8 @@
where
"hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
-hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
-hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
+hide_type (open) lazy_sequence
+hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
+hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
end
--- a/src/HOL/Library/Dlist.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Apr 19 07:38:35 2010 +0200
@@ -247,6 +247,6 @@
end
-hide (open) const member fold empty insert remove map filter null member length fold
+hide_const (open) member fold empty insert remove map filter null member length fold
end
--- a/src/HOL/Library/Efficient_Nat.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon Apr 19 07:38:35 2010 +0200
@@ -496,6 +496,6 @@
code_modulename Haskell
Efficient_Nat Arith
-hide const int
+hide_const int
end
--- a/src/HOL/Library/Executable_Set.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy Mon Apr 19 07:38:35 2010 +0200
@@ -265,7 +265,7 @@
"Union (Coset []) = Coset []"
unfolding Union_def Sup_sup by simp_all
-hide (open) const is_empty empty remove
+hide_const (open) is_empty empty remove
set_eq subset_eq subset inter union subtract Inf Sup Inter Union
end
--- a/src/HOL/Library/Fset.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Fset.thy Mon Apr 19 07:38:35 2010 +0200
@@ -293,7 +293,7 @@
declare mem_def [simp del]
-hide (open) const is_empty insert remove map filter forall exists card
+hide_const (open) is_empty insert remove map filter forall exists card
Inter Union
end
--- a/src/HOL/Library/Mapping.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Apr 19 07:38:35 2010 +0200
@@ -146,6 +146,6 @@
by (cases m) simp
-hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
+hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
end
\ No newline at end of file
--- a/src/HOL/Library/Multiset.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Apr 19 07:38:35 2010 +0200
@@ -1001,7 +1001,7 @@
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
-hide (open) const bagify
+hide_const (open) bagify
subsection {* The multiset order *}
--- a/src/HOL/Library/Nested_Environment.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Mon Apr 19 07:38:35 2010 +0200
@@ -54,7 +54,7 @@
| "lookup_option None xs = None"
| "lookup_option (Some e) xs = lookup e xs"
-hide const lookup_option
+hide_const lookup_option
text {*
\medskip The characteristic cases of @{term lookup} are expressed by
@@ -262,7 +262,7 @@
| "update_option xs opt (Some e) =
(if xs = [] then opt else Some (update xs opt e))"
-hide const update_option
+hide_const update_option
text {*
\medskip The characteristic cases of @{term update} are expressed by
--- a/src/HOL/Library/Quotient_List.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy Mon Apr 19 07:38:35 2010 +0200
@@ -217,6 +217,52 @@
apply (simp_all)
done
+lemma list_rel_rsp:
+ assumes r: "\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b)"
+ and l1: "list_rel R x y"
+ and l2: "list_rel R a b"
+ shows "list_rel S x a = list_rel T y b"
+ proof -
+ have a: "length y = length x" by (rule list_rel_len[OF l1, symmetric])
+ have c: "length a = length b" by (rule list_rel_len[OF l2])
+ show ?thesis proof (cases "length x = length a")
+ case True
+ have b: "length x = length a" by fact
+ show ?thesis using a b c r l1 l2 proof (induct rule: list_induct4)
+ case Nil
+ show ?case using assms by simp
+ next
+ case (Cons h t)
+ then show ?case by auto
+ qed
+ next
+ case False
+ have d: "length x \<noteq> length a" by fact
+ then have e: "\<not>list_rel S x a" using list_rel_len by auto
+ have "length y \<noteq> length b" using d a c by simp
+ then have "\<not>list_rel T y b" using list_rel_len by auto
+ then show ?thesis using e by simp
+ qed
+ qed
+
+lemma[quot_respect]:
+ "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel"
+ by (simp add: list_rel_rsp)
+
+lemma[quot_preserve]:
+ assumes a: "Quotient R abs1 rep1"
+ shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel"
+ apply (simp add: expand_fun_eq)
+ apply clarify
+ apply (induct_tac xa xb rule: list_induct2')
+ apply (simp_all add: Quotient_abs_rep[OF a])
+ done
+
+lemma[quot_preserve]:
+ assumes a: "Quotient R abs1 rep1"
+ shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
+ by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
+
lemma list_rel_eq[id_simps]:
shows "(list_rel (op =)) = (op =)"
unfolding expand_fun_eq
--- a/src/HOL/Library/RBT.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/RBT.thy Mon Apr 19 07:38:35 2010 +0200
@@ -224,7 +224,7 @@
"HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
by (simp add: eq Mapping_def entries_lookup)
-hide (open) const impl_of lookup empty insert delete
+hide_const (open) impl_of lookup empty insert delete
entries keys bulkload map_entry map fold
(*>*)
--- a/src/HOL/Library/RBT_Impl.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Mon Apr 19 07:38:35 2010 +0200
@@ -1079,6 +1079,6 @@
then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
qed
-hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
+hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
end
--- a/src/HOL/Library/Transitive_Closure_Table.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Mon Apr 19 07:38:35 2010 +0200
@@ -227,8 +227,8 @@
value "test\<^sup>*\<^sup>* A C"
value "test\<^sup>*\<^sup>* C A"
-hide type ty
-hide const test A B C
+hide_type ty
+hide_const test A B C
end
--- a/src/HOL/List.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/List.thy Mon Apr 19 07:38:35 2010 +0200
@@ -172,7 +172,8 @@
insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insert x xs = (if x \<in> set xs then xs else x # xs)"
-hide (open) const insert hide (open) fact insert_def
+hide_const (open) insert
+hide_fact (open) insert_def
primrec
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -513,6 +514,17 @@
(cases zs, simp_all)
qed
+lemma list_induct4 [consumes 3, case_names Nil Cons]:
+ "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
+ P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
+ length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
+ P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
+proof (induct xs arbitrary: ys zs ws)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
+qed
+
lemma list_induct2':
"\<lbrakk> P [] [];
\<And>x xs. P (x#xs) [];
@@ -4579,7 +4591,7 @@
declare set_map [symmetric, code_unfold]
-hide (open) const length_unique
+hide_const (open) length_unique
text {* Code for bounded quantification and summation over nats. *}
--- a/src/HOL/NSA/Filter.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/NSA/Filter.thy Mon Apr 19 07:38:35 2010 +0200
@@ -403,6 +403,6 @@
lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
-hide (open) const filter
+hide_const (open) filter
end
--- a/src/HOL/Nat.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Nat.thy Mon Apr 19 07:38:35 2010 +0200
@@ -175,7 +175,7 @@
end
-hide (open) fact add_0 add_0_right diff_0
+hide_fact (open) add_0 add_0_right diff_0
instantiation nat :: comm_semiring_1_cancel
begin
@@ -1212,7 +1212,7 @@
"funpow (Suc n) f = f o funpow n f"
unfolding funpow_code_def by simp_all
-hide (open) const funpow
+hide_const (open) funpow
lemma funpow_add:
"f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
@@ -1504,7 +1504,7 @@
lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
by (simp split add: nat_diff_split)
-hide (open) fact diff_diff_eq
+hide_fact (open) diff_diff_eq
lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
by (auto split add: nat_diff_split)
--- a/src/HOL/New_DSequence.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/New_DSequence.thy Mon Apr 19 07:38:35 2010 +0200
@@ -91,12 +91,12 @@
None => Lazy_Sequence.hb_single ()
| Some ((), xq) => Lazy_Sequence.empty)"
-hide (open) type pos_dseq neg_dseq
+hide_type (open) pos_dseq neg_dseq
-hide (open) const
+hide_const (open)
pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
-hide (open) fact
+hide_fact (open)
pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
--- a/src/HOL/New_Random_Sequence.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/New_Random_Sequence.thy Mon Apr 19 07:38:35 2010 +0200
@@ -91,16 +91,16 @@
where
"neg_map f P = neg_bind P (neg_single o f)"
(*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
DSequence.map
*)
-hide (open) const
+hide_const (open)
pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
-hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
+hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
(* FIXME: hide facts *)
-(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
+(*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
end
\ No newline at end of file
--- a/src/HOL/Nitpick.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Nitpick.thy Mon Apr 19 07:38:35 2010 +0200
@@ -237,15 +237,15 @@
setup {* Nitpick_Isar.setup *}
-hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
+hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
less_eq_frac of_frac
-hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
+hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
-hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
+hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
--- a/src/HOL/Option.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Option.thy Mon Apr 19 07:38:35 2010 +0200
@@ -82,7 +82,7 @@
by (rule ext) (simp split: sum.split)
-hide (open) const set map
+hide_const (open) set map
subsubsection {* Code generator setup *}
@@ -102,7 +102,7 @@
"eq_class.eq x None \<longleftrightarrow> is_none x"
by (simp add: eq is_none_none)
-hide (open) const is_none
+hide_const (open) is_none
code_type option
(SML "_ option")
--- a/src/HOL/Predicate.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Predicate.thy Mon Apr 19 07:38:35 2010 +0200
@@ -934,8 +934,8 @@
bot ("\<bottom>") and
bind (infixl "\<guillemotright>=" 70)
-hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
+hide_type (open) pred seq
+hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
end
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Apr 19 07:38:35 2010 +0200
@@ -1168,7 +1168,7 @@
code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
-hide const a b
+hide_const a b
subsection {* Lambda *}
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Mon Apr 19 07:38:35 2010 +0200
@@ -150,7 +150,7 @@
quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
oops
-hide const a b
+hide_const a b
subsection {* Lexicographic order *}
(* TODO *)
--- a/src/HOL/Product_Type.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Apr 19 07:38:35 2010 +0200
@@ -637,7 +637,7 @@
use "Tools/split_rule.ML"
setup Split_Rule.setup
-hide const internal_split
+hide_const internal_split
lemmas prod_caseI = prod.cases [THEN iffD2, standard]
--- a/src/HOL/Quickcheck.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Quickcheck.thy Mon Apr 19 07:38:35 2010 +0200
@@ -203,9 +203,9 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
where "map f P = bind P (single o f)"
-hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
-hide (open) type randompred
-hide (open) const random collapse beyond random_fun_aux random_fun_lift
+hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
+hide_type (open) randompred
+hide_const (open) random collapse beyond random_fun_aux random_fun_lift
iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
end
--- a/src/HOL/Random.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Random.thy Mon Apr 19 07:38:35 2010 +0200
@@ -174,10 +174,10 @@
end;
*}
-hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" split_seed
+hide_type (open) seed
+hide_const (open) inc_shift minus_shift log "next" split_seed
iterate range select pick select_weight
-hide (open) fact range_def
+hide_fact (open) range_def
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Random_Sequence.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Random_Sequence.thy Mon Apr 19 07:38:35 2010 +0200
@@ -48,14 +48,14 @@
"map f P = bind P (single o f)"
(*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
DSequence.map
*)
-hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
+hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
-hide type DSequence.dseq random_dseq
-hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
+hide_type DSequence.dseq random_dseq
+hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
end
\ No newline at end of file
--- a/src/HOL/Record.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Record.thy Mon Apr 19 07:38:35 2010 +0200
@@ -455,7 +455,7 @@
use "Tools/record.ML"
setup Record.setup
-hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
+hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
iso_tuple_update_accessor_eq_assist tuple_iso_tuple
--- a/src/HOL/Statespace/state_fun.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Mon Apr 19 07:38:35 2010 +0200
@@ -193,7 +193,7 @@
(* mk_updterm returns
* - (orig-term-skeleton,simplified-term-skeleton, vars, b)
- * where boolean b tells if a simplification has occured.
+ * where boolean b tells if a simplification has occurred.
"orig-term-skeleton = simplified-term-skeleton" is
* the desired simplification rule.
* The algorithm first walks down the updates to the seed-state while
--- a/src/HOL/Statespace/state_space.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon Apr 19 07:38:35 2010 +0200
@@ -478,6 +478,21 @@
Type (name, Ts) => (Ts, name)
| T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
+fun read_typ ctxt raw_T env =
+ let
+ val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
+ val T = Syntax.read_typ ctxt' raw_T;
+ val env' = OldTerm.add_typ_tfrees (T, env);
+ in (T, env') end;
+
+fun cert_typ ctxt raw_T env =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val T = Type.no_tvars (Sign.certify_typ thy raw_T)
+ handle TYPE (msg, _, _) => error msg;
+ val env' = OldTerm.add_typ_tfrees (T, env);
+ in (T, env') end;
+
fun gen_define_statespace prep_typ state_space args name parents comps thy =
let (* - args distinct
- only args may occur in comps and parent-instantiations
@@ -500,7 +515,7 @@
val (Ts',env') = fold_map (prep_typ ctxt) Ts env
handle ERROR msg => cat_error msg
- ("The error(s) above occured in parent statespace specification "
+ ("The error(s) above occurred in parent statespace specification "
^ quote pname);
val err_insts = if length args <> length Ts' then
["number of type instantiation(s) does not match arguments of parent statespace "
@@ -539,7 +554,7 @@
fun prep_comp (n,T) env =
let val (T', env') = prep_typ ctxt T env handle ERROR msg =>
- cat_error msg ("The error(s) above occured in component " ^ quote n)
+ cat_error msg ("The error(s) above occurred in component " ^ quote n)
in ((n,T'), env') end;
val (comps',env') = fold_map prep_comp comps env;
@@ -579,8 +594,8 @@
end
handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
-val define_statespace = gen_define_statespace Record.read_typ NONE;
-val define_statespace_i = gen_define_statespace Record.cert_typ;
+val define_statespace = gen_define_statespace read_typ NONE;
+val define_statespace_i = gen_define_statespace cert_typ;
(*** parse/print - translations ***)
--- a/src/HOL/String.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/String.thy Mon Apr 19 07:38:35 2010 +0200
@@ -217,6 +217,6 @@
in Codegen.add_codegen "char_codegen" char_codegen end
*}
-hide (open) type literal
+hide_type (open) literal
end
\ No newline at end of file
--- a/src/HOL/Sum_Type.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Sum_Type.thy Mon Apr 19 07:38:35 2010 +0200
@@ -187,6 +187,6 @@
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
qed
-hide (open) const Suml Sumr Projl Projr
+hide_const (open) Suml Sumr Projl Projr
end
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Apr 19 07:38:35 2010 +0200
@@ -160,14 +160,22 @@
(* unregister ATP thread *)
-fun unregister message thread = Synchronized.change global_state
+fun unregister ({verbose, ...} : params) message thread =
+ Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
- SOME (_, _, description) =>
+ SOME (birth_time, _, description) =>
let
val active' = delete_thread thread active;
- val cancelling' = (thread, (Time.now (), description)) :: cancelling;
- val message' = description ^ "\n" ^ message;
+ val now = Time.now ()
+ val cancelling' = (thread, (now, description)) :: cancelling;
+ val message' =
+ description ^ "\n" ^ message ^
+ (if verbose then
+ "Total time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms.\n"
+ else
+ "")
val messages' = message' :: messages;
val store' = message' ::
(if length store <= message_store_limit then store
@@ -190,7 +198,7 @@
else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs)
end;
-fun check_thread_manager () = Synchronized.change global_state
+fun check_thread_manager params = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
else let val manager = SOME (Toplevel.thread false (fn () =>
@@ -223,7 +231,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister "Interrupted (reached timeout)");
+ |> List.app (unregister params "Timed out.");
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
@@ -233,7 +241,7 @@
(* register ATP thread *)
-fun register birth_time death_time (thread, desc) =
+fun register params birth_time death_time (thread, desc) =
(Synchronized.change global_state
(fn {manager, timeout_heap, active, cancelling, messages, store} =>
let
@@ -241,7 +249,7 @@
val active' = update_thread (thread, (birth_time, death_time, desc)) active;
val state' = make_state manager timeout_heap' active' cancelling messages store;
in state' end);
- check_thread_manager ());
+ check_thread_manager params);
@@ -336,7 +344,7 @@
val _ = Toplevel.thread true (fn () =>
let
- val _ = register birth_time death_time (Thread.self (), desc);
+ val _ = register params birth_time death_time (Thread.self (), desc)
val problem =
{subgoal = i, goal = (ctxt, (facts, goal)),
relevance_override = relevance_override, axiom_clauses = NONE,
@@ -345,7 +353,7 @@
handle Sledgehammer_HOL_Clause.TRIVIAL =>
metis_line i n []
| ERROR msg => ("Error: " ^ msg);
- val _ = unregister message (Thread.self ());
+ val _ = unregister params message (Thread.self ());
in () end);
in () end);
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Apr 19 07:38:35 2010 +0200
@@ -20,6 +20,7 @@
structure ATP_Wrapper : ATP_WRAPPER =
struct
+open Sledgehammer_Util
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
@@ -65,8 +66,8 @@
else SOME "Ill-formed ATP output"
| (failure :: _) => SOME failure
-fun generic_prover overlord get_facts prepare write cmd args failure_strs
- produce_answer name ({full_types, ...} : params)
+fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
+ produce_answer name ({debug, full_types, ...} : params)
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -100,7 +101,7 @@
if destdir' = "" then File.tmp_path probfile
else if File.exists (Path.explode destdir')
then Path.append (Path.explode destdir') probfile
- else error ("No such directory: " ^ destdir')
+ else error ("No such directory: " ^ destdir' ^ ".")
end;
(* write out problem file and call prover *)
@@ -127,25 +128,29 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write full_types probfile clauses
+ write_file debug full_types probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
- else error ("Bad executable: " ^ Path.implode cmd);
+ else error ("Bad executable: " ^ Path.implode cmd ^ ".");
- (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+ (* If the problem file has not been exported, remove it; otherwise, export
+ the proof file too. *)
fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
fun export probfile (((proof, _), _), _) =
- if destdir' = "" then ()
- else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
+ if destdir' = "" then
+ ()
+ else
+ File.write (Path.explode (Path.implode probfile ^ "_proof"))
+ ("% " ^ timestamp () ^ "\n" ^ proof)
val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
with_path cleanup export run_on (prob_pathname subgoal);
- (* check for success and print out some information on failure *)
+ (* Check for success and print out some information on failure. *)
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
val (message, relevant_thm_names) =
- if is_some failure then ("External prover failed.", [])
- else if rc <> 0 then ("External prover failed: " ^ proof, [])
+ if is_some failure then ("ATP failed to find a proof.\n", [])
+ else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
else
(produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
subgoal));
--- a/src/HOL/Tools/Datatype/datatype.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Apr 19 07:38:35 2010 +0200
@@ -682,7 +682,7 @@
(constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
- ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+ ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
" of datatype " ^ quote (Binding.str_of tname));
val (constrs', constr_syntax', sorts') =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Apr 19 07:38:35 2010 +0200
@@ -69,25 +69,25 @@
fun metis_lit b c args = (b, (c, args));
-fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
- | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
- | hol_type_to_fol (Comp (tc, tps)) =
- Metis.Term.Fn (tc, map hol_type_to_fol tps);
+fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
+ | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
+ | hol_type_to_fol (TyConstr ((s, _), tps)) =
+ Metis.Term.Fn (s, map hol_type_to_fol tps);
(*These two functions insert type literals before the real literals. That is the
opposite order from TPTP linkup, but maybe OK.*)
fun hol_term_to_fol_FO tm =
case strip_combterm_comb tm of
- (CombConst(c,_,tys), tms) =>
+ (CombConst ((c, _), _, tys), tms) =>
let val tyargs = map hol_type_to_fol tys
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
- | (CombVar(v,_), []) => Metis.Term.Var v
+ | (CombVar ((v, _), _), []) => Metis.Term.Var v
| _ => error "hol_term_to_fol_FO";
-fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
- | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
+fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
+ | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
| hol_term_to_fol_HO (CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
@@ -95,26 +95,26 @@
(*The fully-typed translation, to avoid type errors*)
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
-fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
- | hol_term_to_fol_FT (CombConst(a, ty, _)) =
+fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
+ | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
| hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
type_of_combterm tm);
fun hol_literal_to_fol FO (Literal (pol, tm)) =
- let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
+ let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
val tylits = if p = "equal" then [] else map hol_type_to_fol tys
val lits = map hol_term_to_fol_FO tms
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
| hol_literal_to_fol HO (Literal (pol, tm)) =
(case strip_combterm_comb tm of
- (CombConst("equal",_,_), tms) =>
+ (CombConst(("equal", _), _, _), tms) =>
metis_lit pol "=" (map hol_term_to_fol_HO tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
| hol_literal_to_fol FT (Literal (pol, tm)) =
(case strip_combterm_comb tm of
- (CombConst("equal",_,_), tms) =>
+ (CombConst(("equal", _), _, _), tms) =>
metis_lit pol "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Apr 19 07:38:35 2010 +0200
@@ -177,9 +177,8 @@
(*The frequency of a constant is the sum of those of all instances of its type.*)
fun const_frequency ctab (c, cts) =
- let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
- fun add ((cts',m), n) = if match_types cts cts' then m+n else n
- in List.foldl add 0 pairs end;
+ CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
+ (the (Symtab.lookup ctab c)) 0
(*Add in a constant's weight, as determined by its frequency.*)
fun add_ct_weight ctab ((c,T), w) =
@@ -253,40 +252,46 @@
end;
fun relevant_clauses ctxt convergence follow_defs max_new
- (relevance_override as {add, del, only}) thy ctab p
- rel_consts =
- let val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
- fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
- | relevant (newpairs,rejects) [] =
- let val (newrels,more_rejects) = take_best max_new newpairs
- val new_consts = maps #2 newrels
- val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
- val newp = p + (1.0-p) / convergence
+ (relevance_override as {add, del, only}) thy ctab =
+ let
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun iter p rel_consts =
+ let
+ fun relevant ([], _) [] = [] (* Nothing added this iteration *)
+ | relevant (newpairs,rejects) [] =
+ let
+ val (newrels, more_rejects) = take_best max_new newpairs
+ val new_consts = maps #2 newrels
+ val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
+ val newp = p + (1.0-p) / convergence
in
- trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
- map #1 newrels @
- relevant_clauses ctxt convergence follow_defs max_new
- relevance_override thy ctab newp rel_consts'
- (more_rejects @ rejects)
+ trace_msg (fn () => "relevant this iteration: " ^
+ Int.toString (length newrels));
+ map #1 newrels @ iter newp rel_consts' (more_rejects @ rejects)
end
- | relevant (newrels, rejects)
- ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+ | relevant (newrels, rejects)
+ ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
let
val weight = if member Thm.eq_thm del_thms thm then 0.0
else if member Thm.eq_thm add_thms thm then 1.0
else if only then 0.0
else clause_weight ctab rel_consts consts_typs
in
- if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
- then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight));
- relevant ((ax,weight)::newrels, rejects) axs)
- else relevant (newrels, ax::rejects) axs
+ if p <= weight orelse
+ (follow_defs andalso defines thy (#1 clsthm) rel_consts) then
+ (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
+ " passes: " ^ Real.toString weight);
+ relevant ((ax, weight) :: newrels, rejects) axs)
+ else
+ relevant (newrels, ax :: rejects) axs
end
- in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
- relevant ([],[])
- end;
+ in
+ trace_msg (fn () => "relevant_clauses, current pass mark: " ^
+ Real.toString p);
+ relevant ([], [])
+ end
+ in iter end
fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new
theory_const relevance_override thy axioms goals =
@@ -498,19 +503,23 @@
fun get_relevant_facts respect_no_atp relevance_threshold convergence
higher_order follow_defs max_new theory_const
- relevance_override (ctxt, (chain_ths, th)) goal_cls =
- let
- val thy = ProofContext.theory_of ctxt
- val is_FO = is_first_order thy higher_order goal_cls
- val included_cls = get_all_lemmas respect_no_atp ctxt
- |> cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy is_FO
- |> remove_unwanted_clauses
- in
- relevance_filter ctxt relevance_threshold convergence follow_defs max_new
- theory_const relevance_override thy included_cls
- (map prop_of goal_cls)
- end;
+ (relevance_override as {add, only, ...})
+ (ctxt, (chain_ths, th)) goal_cls =
+ if (only andalso null add) orelse relevance_threshold > 1.0 then
+ []
+ else
+ let
+ val thy = ProofContext.theory_of ctxt
+ val is_FO = is_first_order thy higher_order goal_cls
+ val included_cls = get_all_lemmas respect_no_atp ctxt
+ |> cnf_rules_pairs thy |> make_unique
+ |> restrict_to_logic thy is_FO
+ |> remove_unwanted_clauses
+ in
+ relevance_filter ctxt relevance_threshold convergence follow_defs max_new
+ theory_const relevance_override thy included_cls
+ (map prop_of goal_cls)
+ end
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Apr 19 07:38:35 2010 +0200
@@ -30,13 +30,19 @@
val make_fixed_const : bool -> string -> string
val make_fixed_type_const : bool -> string -> string
val make_type_class : string -> string
+ type name = string * string
+ type name_pool = string Symtab.table * string Symtab.table
+ val empty_name_pool : bool -> name_pool option
+ val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
+ val nice_name : name -> name_pool option -> string * name_pool option
datatype kind = Axiom | Conjecture
type axiom_name = string
datatype fol_type =
- AtomV of string
- | AtomF of string
- | Comp of string * fol_type list
- val string_of_fol_type : fol_type -> string
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * fol_type list
+ val string_of_fol_type :
+ fol_type -> name_pool option -> string * name_pool option
datatype type_literal = LTVar of string * string | LTFree of string * string
exception CLAUSE of string * term
val add_typs : typ list -> type_literal list
@@ -207,7 +213,66 @@
fun make_type_class clas = class_prefix ^ ascii_of clas;
-(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
+(**** name pool ****)
+
+type name = string * string
+type name_pool = string Symtab.table * string Symtab.table
+
+fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
+
+fun pool_map f xs =
+ fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
+ o pair []
+
+fun add_nice_name full_name nice_prefix j the_pool =
+ let
+ val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
+ in
+ case Symtab.lookup (snd the_pool) nice_name of
+ SOME full_name' =>
+ if full_name = full_name' then (nice_name, the_pool)
+ else add_nice_name full_name nice_prefix (j + 1) the_pool
+ | NONE =>
+ (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
+ Symtab.update_new (nice_name, full_name) (snd the_pool)))
+ end
+
+fun translate_first_char f s =
+ String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+
+fun clean_short_name full_name s =
+ let
+ val s = s |> Long_Name.base_name
+ |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
+ val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
+ val s' =
+ (s' |> rev
+ |> implode
+ |> String.translate
+ (fn c => if Char.isAlphaNum c then String.str c else ""))
+ ^ replicate_string (String.size s - length s') "_"
+ val s' =
+ if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
+ else s'
+ val s' = if s' = "op" then full_name else s'
+ in
+ case (Char.isLower (String.sub (full_name, 0)),
+ Char.isLower (String.sub (s', 0))) of
+ (true, false) => translate_first_char Char.toLower s'
+ | (false, true) => translate_first_char Char.toUpper s'
+ | _ => s'
+ end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+ | nice_name (full_name, desired_name) (SOME the_pool) =
+ case Symtab.lookup (fst the_pool) full_name of
+ SOME nice_name => (nice_name, SOME the_pool)
+ | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
+ 0 the_pool
+ |> apsnd SOME
+
+(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
+ format ****)
datatype kind = Axiom | Conjecture;
@@ -215,35 +280,24 @@
(**** Isabelle FOL clauses ****)
-(*FIXME: give the constructors more sensible names*)
-datatype fol_type = AtomV of string
- | AtomF of string
- | Comp of string * fol_type list;
+datatype fol_type =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * fol_type list
-fun string_of_fol_type (AtomV x) = x
- | string_of_fol_type (AtomF x) = x
- | string_of_fol_type (Comp(tcon,tps)) =
- tcon ^ (paren_pack (map string_of_fol_type tps));
+fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
+ | string_of_fol_type (TyFree sp) pool = nice_name sp pool
+ | string_of_fol_type (TyConstr (sp, tys)) pool =
+ let
+ val (s, pool) = nice_name sp pool
+ val (ss, pool) = pool_map string_of_fol_type tys pool
+ in (s ^ paren_pack ss, pool) end
(*First string is the type class; the second is a TVar or TFfree*)
datatype type_literal = LTVar of string * string | LTFree of string * string;
exception CLAUSE of string * term;
-fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
- | atomic_type (TVar (v,_)) = AtomV(make_schematic_type_var v);
-
-(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
- TVars it contains.*)
-fun type_of dfg (Type (a, Ts)) =
- let val (folTyps, ts) = types_of dfg Ts
- val t = make_fixed_type_const dfg a
- in (Comp(t,folTyps), ts) end
- | type_of dfg T = (atomic_type T, [T])
-and types_of dfg Ts =
- let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
- in (folTyps, union_all ts) end;
-
(*Make literals for sorted type variables*)
fun sorts_on_typs_aux (_, []) = []
| sorts_on_typs_aux ((x,i), s::ss) =
@@ -282,8 +336,6 @@
(**** Isabelle arities ****)
-exception ARCLAUSE of string;
-
datatype arLit = TConsLit of class * string * string list
| TVarLit of class * string;
@@ -401,10 +453,10 @@
(*** Find occurrences of functions in clauses ***)
-fun add_foltype_funcs (AtomV _, funcs) = funcs
- | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
- | add_foltype_funcs (Comp(a,tys), funcs) =
- List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
+fun add_foltype_funcs (TyVar _, funcs) = funcs
+ | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs
+ | add_foltype_funcs (TyConstr ((s, _), tys), funcs) =
+ List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys;
(*TFrees are recorded as constants*)
fun add_type_sort_funcs (TVar _, funcs) = funcs
@@ -495,22 +547,24 @@
(**** Produce TPTP files ****)
-(*Attach sign in TPTP syntax: false means negate.*)
fun tptp_sign true s = s
| tptp_sign false s = "~ " ^ s
-fun tptp_of_typeLit pos (LTVar (s,ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
- | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")");
+fun tptp_of_typeLit pos (LTVar (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+ | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+
+fun tptp_cnf name kind formula =
+ "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
-fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
- "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^
- tptp_pack (tylits@lits) ^ ").\n"
- | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
- "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^
- tptp_pack lits ^ ").\n";
+fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
+ tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
+ (tptp_pack (tylits @ lits))
+ | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
+ tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
+ (tptp_pack lits)
fun tptp_tfree_clause tfree_lit =
- "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
+ tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
fun tptp_of_arLit (TConsLit (c,t,args)) =
tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
@@ -518,14 +572,14 @@
tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
- "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
- tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
+ tptp_cnf (string_of_ar axiom_name) "axiom"
+ (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
fun tptp_classrelLits sub sup =
let val tvar = "(T)"
in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
- "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
+ tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 19 07:38:35 2010 +0200
@@ -6,6 +6,7 @@
signature SLEDGEHAMMER_HOL_CLAUSE =
sig
+ type name = Sledgehammer_FOL_Clause.name
type kind = Sledgehammer_FOL_Clause.kind
type fol_type = Sledgehammer_FOL_Clause.fol_type
type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
@@ -15,8 +16,8 @@
type hol_clause_id = int
datatype combterm =
- CombConst of string * fol_type * fol_type list (* Const and Free *) |
- CombVar of string * fol_type |
+ CombConst of name * fol_type * fol_type list (* Const and Free *) |
+ CombVar of name * fol_type |
CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
datatype hol_clause =
@@ -33,11 +34,11 @@
val get_helper_clauses : bool -> theory -> bool ->
hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
hol_clause list
- val write_tptp_file : bool -> Path.T ->
+ val write_tptp_file : bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
classrel_clause list * arity_clause list ->
int * int
- val write_dfg_file : bool -> Path.T ->
+ val write_dfg_file : bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
classrel_clause list * arity_clause list -> int * int
end
@@ -45,6 +46,7 @@
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
struct
+open Sledgehammer_Util
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
@@ -74,8 +76,8 @@
type hol_clause_id = int;
datatype combterm =
- CombConst of string * fol_type * fol_type list (* Const and Free *) |
- CombVar of string * fol_type |
+ CombConst of name * fol_type * fol_type list (* Const and Free *) |
+ CombVar of name * fol_type |
CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm;
@@ -89,11 +91,11 @@
(* convert a clause with type Term.term to a clause with type clause *)
(*********************************************************************)
-fun isFalse (Literal(pol, CombConst(c,_,_))) =
+fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
(pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
| isFalse _ = false;
-fun isTrue (Literal (pol, CombConst(c,_,_))) =
+fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
(pol andalso c = "c_True") orelse
(not pol andalso c = "c_False")
| isTrue _ = false;
@@ -101,19 +103,22 @@
fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
fun type_of dfg (Type (a, Ts)) =
- let val (folTypes,ts) = types_of dfg Ts
- in (Comp(make_fixed_type_const dfg a, folTypes), ts) end
- | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
- | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
+ let val (folTypes,ts) = types_of dfg Ts in
+ (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
+ end
+ | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+ | type_of _ (tp as TVar (x, _)) =
+ (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
and types_of dfg Ts =
let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
in (folTyps, union_all ts) end;
(* same as above, but no gathering of sort information *)
fun simp_type_of dfg (Type (a, Ts)) =
- Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
- | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
- | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
+ TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
+ | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+ | simp_type_of _ (TVar (x, _)) =
+ TyVar (make_schematic_type_var x, string_of_indexname x);
fun const_type_of dfg thy (c,t) =
@@ -123,15 +128,15 @@
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
fun combterm_of dfg thy (Const(c,t)) =
let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
- val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
+ val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
in (c',ts) end
| combterm_of dfg _ (Free(v,t)) =
let val (tp,ts) = type_of dfg t
- val v' = CombConst(make_fixed_var v, tp, [])
+ val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
| combterm_of dfg _ (Var(v,t)) =
let val (tp,ts) = type_of dfg t
- val v' = CombVar(make_schematic_var v,tp)
+ val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
in (v',ts) end
| combterm_of dfg thy (P $ Q) =
let val (P',tsP) = combterm_of dfg thy P
@@ -192,8 +197,8 @@
(**********************************************************************)
(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
- | result_type _ = error "result_type"
+fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2
+ | result_type _ = raise Fail "Non-function type"
fun type_of_combterm (CombConst (_, tp, _)) = tp
| type_of_combterm (CombVar (_, tp)) = tp
@@ -207,11 +212,20 @@
val type_wrapper = "ti";
-fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
+fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
+ needs_hBOOL const_needs_hBOOL c
| head_needs_hBOOL _ _ = true;
-fun wrap_type full_types (s, tp) =
- if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
+fun wrap_type full_types (s, ty) pool =
+ if full_types then
+ let val (s', pool) = string_of_fol_type ty pool in
+ (type_wrapper ^ paren_pack [s, s'], pool)
+ end
+ else
+ (s, pool)
+
+fun wrap_type_if full_types cnh (head, s, tp) =
+ if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
fun apply ss = "hAPP" ^ paren_pack ss;
@@ -220,105 +234,118 @@
fun string_apply (v, args) = rev_apply (v, rev args);
-(*Apply an operator to the argument strings, using either the "apply" operator or
- direct function application.*)
-fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
- let val c = if c = "equal" then "c_fequal" else c
- val nargs = min_arity_of cma c
- val args1 = List.take(args, nargs)
- handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
- Int.toString nargs ^ " but is applied to " ^
- space_implode ", " args)
- val args2 = List.drop(args, nargs)
- val targs = if full_types then [] else map string_of_fol_type tvars
- in
- string_apply (c ^ paren_pack (args1@targs), args2)
- end
- | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
- | string_of_applic _ _ _ = error "string_of_applic";
+(* Apply an operator to the argument strings, using either the "apply" operator
+ or direct function application. *)
+fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
+ pool =
+ let
+ val s = if s = "equal" then "c_fequal" else s
+ val nargs = min_arity_of cma s
+ val args1 = List.take (args, nargs)
+ handle Subscript =>
+ raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
+ " but is applied to " ^ commas (map quote args))
+ val args2 = List.drop (args, nargs)
+ val (targs, pool) = if full_types then ([], pool)
+ else pool_map string_of_fol_type tvars pool
+ val (s, pool) = nice_name (s, s') pool
+ in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
+ | string_of_application _ _ (CombVar (name, _), args) pool =
+ nice_name name pool |>> (fn s => string_apply (s, args))
-fun wrap_type_if full_types cnh (head, s, tp) =
- if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
-
-fun string_of_combterm (params as (full_types, cma, cnh)) t =
- let val (head, args) = strip_combterm_comb t
- in wrap_type_if full_types cnh (head,
- string_of_applic full_types cma
- (head, map (string_of_combterm (params)) args),
- type_of_combterm t)
- end;
+fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
+ let
+ val (head, args) = strip_combterm_comb t
+ val (ss, pool) = pool_map (string_of_combterm params) args pool
+ val (s, pool) = string_of_application full_types cma (head, ss) pool
+ in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
(*Boolean-valued terms are here converted to literals.*)
-fun boolify params t =
- "hBOOL" ^ paren_pack [string_of_combterm params t];
+fun boolify params c =
+ string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
-fun string_of_predicate (params as (_,_,cnh)) t =
+fun string_of_predicate (params as (_, _, cnh)) t =
case t of
- (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
- (*DFG only: new TPTP prefers infix equality*)
- ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
- | _ =>
- case #1 (strip_combterm_comb t) of
- CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
- | _ => boolify params t;
+ (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
+ (* DFG only: new TPTP prefers infix equality *)
+ pool_map (string_of_combterm params) [t1, t2]
+ #>> prefix "equal" o paren_pack
+ | _ =>
+ case #1 (strip_combterm_comb t) of
+ CombConst ((s, _), _, _) =>
+ (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
+ | _ => boolify params t
-(*** tptp format ***)
+(*** TPTP format ***)
-fun tptp_of_equality params pol (t1,t2) =
- let val eqop = if pol then " = " else " != "
- in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
-
-fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
- tptp_of_equality params pol (t1,t2)
- | tptp_literal params (Literal(pol,pred)) =
- tptp_sign pol (string_of_predicate params pred);
+fun tptp_of_equality params pos (t1, t2) =
+ pool_map (string_of_combterm params) [t1, t2]
+ #>> space_implode (if pos then " = " else " != ")
-(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
- the latter should only occur in conjecture clauses.*)
-fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
- (map (tptp_literal params) literals,
- map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
+fun tptp_literal params
+ (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
+ t2))) =
+ tptp_of_equality params pos (t1, t2)
+ | tptp_literal params (Literal (pos, pred)) =
+ string_of_predicate params pred #>> tptp_sign pos
+
+(* Given a clause, returns its literals paired with a list of literals
+ concerning TFrees; the latter should only occur in conjecture clauses. *)
+fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
+ pool_map (tptp_literal params) literals
+ #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts))
-fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
- let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
+fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
+ pool =
+let
+ val ((lits, tylits), pool) =
+ tptp_type_literals params (kind = Conjecture) cls pool
in
- (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
- end;
+ ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
+ end
-(*** dfg format ***)
+(*** DFG format ***)
-fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
+fun dfg_literal params (Literal (pos, pred)) =
+ string_of_predicate params pred #>> dfg_sign pos
-fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
- (map (dfg_literal params) literals,
- map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
+fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
+ pool_map (dfg_literal params) literals
+ #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts))
-fun get_uvars (CombConst _) vars = vars
- | get_uvars (CombVar(v,_)) vars = (v::vars)
- | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
+fun get_uvars (CombConst _) vars pool = (vars, pool)
+ | get_uvars (CombVar (name, _)) vars pool =
+ nice_name name pool |>> (fn var => var :: vars)
+ | get_uvars (CombApp (P, Q)) vars pool =
+ let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
-fun get_uvars_l (Literal(_,c)) = get_uvars c [];
+fun get_uvars_l (Literal (_, c)) = get_uvars c [];
-fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
+fun dfg_vars (HOLClause {literals, ...}) =
+ pool_map get_uvars_l literals #>> union_all
-fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
- ctypes_sorts, ...}) =
- let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
- val vars = dfg_vars cls
- val tvars = get_tvar_strs ctypes_sorts
+fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
+ ctypes_sorts, ...}) pool =
+ let
+ val ((lits, tylits), pool) =
+ dfg_type_literals params (kind = Conjecture) cls pool
+ val (vars, pool) = dfg_vars cls pool
+ val tvars = get_tvar_strs ctypes_sorts
in
- (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
- end;
+ ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
+ tylits), pool)
+ end
(** For DFG format: accumulate function and predicate declarations **)
fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
-fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
- if c = "equal" then (addtypes tvars funcs, preds)
+fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) =
+ if c = "equal" then
+ (addtypes tvars funcs, preds)
else
let val arity = min_arity_of cma c
val ntys = if not full_types then length tvars else 0
@@ -327,7 +354,7 @@
if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
else (addtypes tvars funcs, addit preds)
end
- | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
+ | add_decls _ (CombVar (_,ctp), (funcs, preds)) =
(add_foltype_funcs (ctp,funcs), preds)
| add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
@@ -368,7 +395,7 @@
Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
("c_COMBS", 0)];
-fun count_combterm (CombConst (c, _, _), ct) =
+fun count_combterm (CombConst ((c, _), _, _), ct) =
(case Symtab.lookup ct c of NONE => ct (*no counter*)
| SOME n => Symtab.update (c,n+1) ct)
| count_combterm (CombVar _, ct) = ct
@@ -416,7 +443,7 @@
val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
in
case head of
- CombConst (a,_,_) => (*predicate or function version of "equal"?*)
+ CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
let val a = if a="equal" andalso not toplev then "c_fequal" else a
val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
in
@@ -451,39 +478,54 @@
(* TPTP format *)
-fun write_tptp_file full_types file clauses =
+fun write_tptp_file debug full_types file clauses =
let
+ fun section _ [] = []
+ | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
+ val pool = empty_name_pool debug
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (full_types, cma, cnh)
- val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
+ val ((conjecture_clss, tfree_litss), pool) =
+ pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
+ val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
+ pool
+ val classrel_clss = map tptp_classrel_clause classrel_clauses
+ val arity_clss = map tptp_arity_clause arity_clauses
+ val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
+ helper_clauses pool
val _ =
File.write_list file (
- map (#1 o (clause2tptp params)) axclauses @
- tfree_clss @
- tptp_clss @
- map tptp_classrel_clause classrel_clauses @
- map tptp_arity_clause arity_clauses @
- map (#1 o (clause2tptp params)) helper_clauses)
- in (length axclauses + 1, length tfree_clss + length tptp_clss)
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
+ "% " ^ timestamp () ^ "\n" ::
+ section "Relevant fact" ax_clss @
+ section "Type variable" tfree_clss @
+ section "Conjecture" conjecture_clss @
+ section "Class relationship" classrel_clss @
+ section "Arity declaration" arity_clss @
+ section "Helper fact" helper_clss)
+ in (length axclauses + 1, length tfree_clss + length conjecture_clss)
end;
(* DFG format *)
-fun write_dfg_file full_types file clauses =
+fun write_dfg_file debug full_types file clauses =
let
+ val pool = empty_name_pool debug
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (full_types, cma, cnh)
- val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
+ val ((conjecture_clss, tfree_litss), pool) =
+ pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
and probname = Path.implode (Path.base file)
- val axstrs = map (#1 o (clause2dfg params)) axclauses
+ val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
- val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
+ val (helper_clauses_strs, pool) =
+ pool_map (apfst fst oo dfg_clause params) helper_clauses pool
val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
val _ =
@@ -492,21 +534,22 @@
string_of_descrip probname ::
string_of_symbols (string_of_funcs funcs)
(string_of_preds (cl_preds @ ty_preds)) ::
- "list_of_clauses(axioms,cnf).\n" ::
+ "list_of_clauses(axioms, cnf).\n" ::
axstrs @
map dfg_classrel_clause classrel_clauses @
map dfg_arity_clause arity_clauses @
helper_clauses_strs @
- ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
+ ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
tfree_clss @
- dfg_clss @
+ conjecture_clss @
["end_of_list.\n\n",
(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
- "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
+ "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
"end_problem.\n"])
- in (length axclauses + length classrel_clauses + length arity_clauses +
- length helper_clauses + 1, length tfree_clss + length dfg_clss)
- end;
+ in
+ (length axclauses + length classrel_clauses + length arity_clauses +
+ length helper_clauses + 1, length tfree_clss + length conjecture_clss)
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Apr 19 07:38:35 2010 +0200
@@ -27,13 +27,13 @@
{add = [], del = ns, only = false}
fun only_relevance_override ns : relevance_override =
{add = ns, del = [], only = true}
-val default_relevance_override = add_to_relevance_override []
+val no_relevance_override = add_to_relevance_override []
fun merge_relevance_override_pairwise (r1 : relevance_override)
(r2 : relevance_override) =
{add = #add r1 @ #add r2, del = #del r1 @ #del r2,
- only = #only r1 orelse #only r2}
+ only = #only r1 andalso #only r2}
fun merge_relevance_overrides rs =
- fold merge_relevance_override_pairwise rs default_relevance_override
+ fold merge_relevance_override_pairwise rs (only_relevance_override [])
type raw_param = string * string list
@@ -96,11 +96,19 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
+(* Don't even try to start ATPs that are not installed.
+ Hack: Should not rely on naming convention. *)
+val filter_atps =
+ space_explode " "
+ #> filter (fn s => String.isPrefix "remote_" s orelse
+ getenv (String.map Char.toUpper s ^ "_HOME") <> "")
+ #> space_implode " "
+
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
fun default_raw_params thy =
Data.get thy
|> fold (AList.default (op =))
- [("atps", [!atps]),
+ [("atps", [filter_atps (!atps)]),
("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
@@ -207,9 +215,6 @@
val refresh_tptpN = "refresh_tptp"
val helpN = "help"
-val addN = "add"
-val delN = "del"
-val onlyN = "only"
fun minimizize_raw_param_name "timeout" = "minimize_timeout"
| minimizize_raw_param_name name = name
@@ -270,14 +275,11 @@
(Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
|| (Args.del |-- Args.colon |-- parse_fact_refs
>> del_from_relevance_override)
- || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
+ || (parse_fact_refs >> only_relevance_override)
val parse_relevance_override =
- Scan.optional (Args.parens
- (Scan.optional (parse_fact_refs >> only_relevance_override)
- default_relevance_override
- -- Scan.repeat parse_relevance_chunk)
- >> op :: >> merge_relevance_overrides)
- default_relevance_override
+ Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
+ >> merge_relevance_overrides))
+ (add_to_relevance_override [])
val parse_sledgehammer_command =
(Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
-- Scan.option P.nat) #>> sledgehammer_trans
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Apr 19 07:38:35 2010 +0200
@@ -8,13 +8,16 @@
sig
val plural_s : int -> string
val serial_commas : string -> string list -> string list
+ val replace_all : string -> string -> string -> string
+ val remove_all : string -> string -> string
+ val timestamp : unit -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val hashw : word * word -> word
val hashw_char : Char.char * word -> word
val hashw_string : string * word -> word
end;
-
+
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
@@ -26,6 +29,20 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+fun replace_all bef aft =
+ let
+ fun aux seen "" = String.implode (rev seen)
+ | aux seen s =
+ if String.isPrefix bef s then
+ aux seen "" ^ aft ^ aux [] (unprefix bef s)
+ else
+ aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+ in aux [] end
+
+fun remove_all bef = replace_all bef ""
+
+val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+
fun parse_bool_option option name s =
(case s of
"smart" => if option then NONE else raise Option
--- a/src/HOL/Tools/record.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon Apr 19 07:38:35 2010 +0200
@@ -54,9 +54,9 @@
val print_records: theory -> unit
val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
- val add_record: bool -> string list * binding -> (typ list * string) option ->
+ val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
(binding * typ * mixfix) list -> theory -> theory
- val add_record_cmd: bool -> string list * binding -> string option ->
+ val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
(binding * string * mixfix) list -> theory -> theory
val setup: theory -> theory
end;
@@ -64,7 +64,8 @@
signature ISO_TUPLE_SUPPORT =
sig
- val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
+ val add_iso_tuple_type: bstring * (string * sort) list ->
+ typ * typ -> theory -> (term * term) * theory
val mk_cons_tuple: term * term -> term
val dest_cons_tuple: term -> term * term
val iso_tuple_intros_tac: int -> tactic
@@ -742,7 +743,7 @@
val varifyT = varifyT midx;
val vartypes = map varifyT types;
- val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty
+ val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
handle Type.TYPE_MATCH => err "type is no proper record (extension)";
val alphas' =
map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
@@ -872,11 +873,10 @@
apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
val (args', more) = split_last args;
val alphavars = map varifyT (but_last alphas);
- val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty;
+ val subst = Type.raw_matches (alphavars, args') Vartab.empty;
val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
in fields'' @ strip_fields more end
- handle Type.TYPE_MATCH => [("", T)]
- | Library.UnequalLengths => [("", T)])
+ handle Type.TYPE_MATCH => [("", T)])
| _ => [("", T)])
| _ => [("", T)])
| _ => [("", T)])
@@ -900,19 +900,18 @@
val midx = maxidx_of_typ T;
val varifyT = varifyT midx;
- fun mk_type_abbr subst name alphas =
- let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in
- Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
- end;
-
- fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
+ fun mk_type_abbr subst name args =
+ let val abbrT = Type (name, map (varifyT o TFree) args)
+ in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
+
+ fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
if ! print_record_type_abbr then
(case last_extT T of
SOME (name, _) =>
if name = last_ext then
let val subst = match schemeT T in
- if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS))))
+ if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
then mk_type_abbr subst abbr alphas
else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
@@ -1639,11 +1638,10 @@
val fields_moreTs = fieldTs @ [moreT];
val alphas_zeta = alphas @ [zeta];
- val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
val ext_binding = Binding.name (suffix extN base_name);
val ext_name = suffix extN name;
- val extT = Type (suffix ext_typeN name, alphas_zetaTs);
+ val extT = Type (suffix ext_typeN name, map TFree alphas_zeta);
val ext_type = fields_moreTs ---> extT;
@@ -1846,10 +1844,8 @@
(* record_definition *)
-fun record_definition (args, binding) parent (parents: parent_info list) raw_fields thy =
+fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
let
- val alphas = map fst args;
-
val name = Sign.full_name thy binding;
val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
@@ -1869,7 +1865,7 @@
val fields = map (apfst full) bfields;
val names = map fst fields;
val types = map snd fields;
- val alphas_fields = fold Term.add_tfree_namesT types [];
+ val alphas_fields = fold Term.add_tfreesT types [];
val alphas_ext = inter (op =) alphas_fields alphas;
val len = length fields;
val variants =
@@ -1885,9 +1881,8 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
-
- val zeta = Name.variant alphas "'z";
- val moreT = TFree (zeta, HOLogic.typeS);
+ val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
+ val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
val bfields_more = bfields @ [(Binding.name moreN, moreT)];
@@ -1976,11 +1971,6 @@
(* prepare definitions *)
- (*record (scheme) type abbreviation*)
- val recordT_specs =
- [(Binding.suffix_name schemeN binding, alphas @ [zeta], rec_schemeT0, NoSyn),
- (binding, alphas, recT0, NoSyn)];
-
val ext_defs = ext_def :: map #ext_def parents;
(*Theorems from the iso_tuple intros.
@@ -2064,7 +2054,9 @@
ext_thy
|> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
|> Sign.restore_naming thy
- |> Sign.add_tyabbrs_i recordT_specs
+ |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
+ |> Typedecl.abbrev_global
+ (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
|> Sign.qualified_path false binding
|> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
(sel_decls ~~ (field_syntax @ [NoSyn]))
@@ -2349,7 +2341,7 @@
((Binding.name "iffs", iffs), [iff_add])];
val info =
- make_record_info args parent fields extension
+ make_record_info alphas parent fields extension
ext_induct ext_inject ext_surjective ext_split ext_def
sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
@@ -2371,10 +2363,25 @@
(* add_record *)
-(*We do all preparations and error checks here, deferring the real
- work to record_definition.*)
-fun gen_add_record prep_typ prep_raw_parent quiet_mode
- (params, binding) raw_parent raw_fields thy =
+local
+
+fun read_parent NONE ctxt = (NONE, ctxt)
+ | read_parent (SOME raw_T) ctxt =
+ (case ProofContext.read_typ_abbrev ctxt raw_T of
+ Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
+ | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
+
+fun prep_field prep (x, T, mx) = (x, prep T, mx)
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x));
+
+fun read_field raw_field ctxt =
+ let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
+ in (field, Variable.declare_typ T ctxt) end;
+
+in
+
+fun add_record quiet_mode (params, binding) raw_parent raw_fields thy =
let
val _ = Theory.requires thy "Record" "record definitions";
val _ =
@@ -2382,40 +2389,19 @@
else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
val ctxt = ProofContext.init thy;
-
-
- (* parents *)
-
- fun prep_inst T = fst (cert_typ ctxt T []);
-
- val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent
- handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
+ fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
+ handle TYPE (msg, _, _) => error msg;
+
+
+ (* specification *)
+
+ val parent = Option.map (apfst (map cert_typ)) raw_parent
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in parent record specification");
+ val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
val parents = add_parents thy parent [];
- val init_env =
- (case parent of
- NONE => []
- | SOME (types, _) => fold Term.add_tfreesT types []);
-
-
- (* fields *)
-
- fun prep_field (x, raw_T, mx) env =
- let
- val (T, env') =
- prep_typ ctxt raw_T env handle ERROR msg =>
- cat_error msg ("The error(s) above occured in record field " ^ quote (Binding.str_of x));
- in ((x, T, mx), env') end;
-
- val (bfields, envir) = fold_map prep_field raw_fields init_env;
- val envir_names = map fst envir;
-
-
- (* args *)
-
- val defaultS = Sign.defaultS thy;
- val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
-
+ val bfields = map (prep_field cert_typ) raw_fields;
(* errors *)
@@ -2424,15 +2410,12 @@
if is_none (get_record thy name) then []
else ["Duplicate definition of record " ^ quote name];
- val err_dup_parms =
- (case duplicates (op =) params of
+ val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
+ val err_extra_frees =
+ (case subtract (op =) params spec_frees of
[] => []
- | dups => ["Duplicate parameter(s) " ^ commas dups]);
-
- val err_extra_frees =
- (case subtract (op =) params envir_names of
- [] => []
- | extras => ["Extra free type variable(s) " ^ commas extras]);
+ | extras => ["Extra free type variable(s) " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
val err_no_fields = if null bfields then ["No fields present"] else [];
@@ -2445,23 +2428,25 @@
if forall (not_equal moreN o Binding.name_of o #1) bfields then []
else ["Illegal field name " ^ quote moreN];
- val err_dup_sorts =
- (case duplicates (op =) envir_names of
- [] => []
- | dups => ["Inconsistent sort constraints for " ^ commas dups]);
-
val errs =
- err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
- err_dup_fields @ err_bad_fields @ err_dup_sorts;
-
+ err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> record_definition (args, binding) parent parents bfields
+ thy |> record_definition (params, binding) parent parents bfields
end
handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
-val add_record = gen_add_record cert_typ (K I);
-val add_record_cmd = gen_add_record read_typ read_raw_parent;
+fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
+ val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
+ val (parent, ctxt2) = read_parent raw_parent ctxt1;
+ val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
+ val params' = map (ProofContext.check_tfree ctxt3) params;
+ in thy |> add_record quiet_mode (params', binding) parent fields end;
+
+end;
(* setup theory *)
@@ -2479,7 +2464,7 @@
val _ =
OuterSyntax.command "record" "define extensible record" K.thy_decl
- (P.type_args -- P.binding --
+ (P.type_args_constrained -- P.binding --
(P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
--- a/src/HOL/Tools/typecopy.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML Mon Apr 19 07:38:35 2010 +0200
@@ -8,7 +8,7 @@
sig
type info = { vs: (string * sort) list, constr: string, typ: typ,
inject: thm, proj: string * typ, proj_def: thm }
- val typecopy: binding * string list -> typ -> (binding * binding) option
+ val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
-> theory -> (string * info) * theory
val get_info: theory -> string -> info option
val interpretation: (string -> theory -> theory) -> theory -> theory
@@ -52,8 +52,8 @@
fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
let
val ty = Sign.certify_typ thy raw_ty;
- val vs =
- AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
+ val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
+ val vs = map (ProofContext.check_tfree ctxt) raw_vs;
val tac = Tactic.rtac UNIV_witness 1;
fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
@@ -80,8 +80,7 @@
end
in
thy
- |> Typedef.add_typedef_global false (SOME raw_tyco)
- (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn) (* FIXME keep constraints!? *)
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
|-> (fn (tyco, info) => add_info tyco info)
end;
--- a/src/HOL/Tools/typedef.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Mon Apr 19 07:38:35 2010 +0200
@@ -135,9 +135,9 @@
(* rhs *)
- val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val set = prep_term tmp_lthy raw_set;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+ val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
val setT = Term.fastype_of set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
@@ -149,7 +149,7 @@
(* lhs *)
- val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val args = map (ProofContext.check_tfree tmp_ctxt') raw_args;
val (newT, typedecl_lthy) = lthy
|> Typedecl.typedecl (tname, args, mx)
||> Variable.declare_term set;
--- a/src/HOL/Typerep.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Typerep.thy Mon Apr 19 07:38:35 2010 +0200
@@ -90,6 +90,6 @@
code_reserved Eval Term
-hide (open) const typerep Typerep
+hide_const (open) typerep Typerep
end
--- a/src/HOL/Word/BinGeneral.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/Word/BinGeneral.thy Mon Apr 19 07:38:35 2010 +0200
@@ -28,7 +28,7 @@
lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
-hide (open) const B0 B1
+hide_const (open) B0 B1
lemma Min_ne_Pls [iff]:
"Int.Min ~= Int.Pls"
--- a/src/HOL/ex/Meson_Test.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy Mon Apr 19 07:38:35 2010 +0200
@@ -16,7 +16,7 @@
below and constants declared in HOL!
*}
-hide (open) const subset member quotient union inter
+hide_const (open) subset member quotient union inter
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/Numeral.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Apr 19 07:38:35 2010 +0200
@@ -879,7 +879,7 @@
declare zero_is_num_zero [code_unfold del]
declare one_is_num_one [code_unfold del]
-hide (open) const sub dup
+hide_const (open) sub dup
subsection {* Numeral equations as default simplification rules *}
--- a/src/HOL/ex/RPred.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/ex/RPred.thy Mon Apr 19 07:38:35 2010 +0200
@@ -47,6 +47,6 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
where "map f P = bind P (return o f)"
-hide (open) const return bind supp map
+hide_const (open) return bind supp map
end
\ No newline at end of file
--- a/src/HOL/ex/SVC_Oracle.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Mon Apr 19 07:38:35 2010 +0200
@@ -17,7 +17,7 @@
iff_keep :: "[bool, bool] => bool"
iff_unfold :: "[bool, bool] => bool"
-hide const iff_keep iff_unfold
+hide_const iff_keep iff_unfold
oracle svc_oracle = Svc.oracle
--- a/src/HOLCF/Domain.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/Domain.thy Mon Apr 19 07:38:35 2010 +0200
@@ -149,8 +149,8 @@
cfcomp2 sfst_defined_iff ssnd_defined_iff
lemmas take_con_rules =
- ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
- sprod_map_spair' sprod_map_strict u_map_up u_map_strict
+ ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
+ deflation_strict deflation_ID ID1 cfcomp2
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
--- a/src/HOLCF/Fixrec.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/Fixrec.thy Mon Apr 19 07:38:35 2010 +0200
@@ -608,7 +608,7 @@
(@{const_name UU}, @{const_name match_UU}) ]
*}
-hide (open) const return bind fail run cases
+hide_const (open) return bind fail run cases
lemmas [fixrec_simp] =
run_strict run_fail run_return
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Mon Apr 19 07:38:35 2010 +0200
@@ -59,7 +59,7 @@
(* hiding and restricting *)
hide_asig :: "['a signature, 'a set] => 'a signature"
- "hide" :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+ hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
restrict_asig :: "['a signature, 'a set] => 'a signature"
restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Apr 19 07:38:35 2010 +0200
@@ -184,8 +184,7 @@
val rhs = con_app2 con one_rhs args;
val goal = mk_trp (lhs === rhs);
val rules =
- [ax_abs_iso]
- @ @{thms take_con_rules ID1 cfcomp2 deflation_strict}
+ [ax_abs_iso] @ @{thms take_con_rules}
@ take_Suc_thms @ deflation_thms @ deflation_take_thms;
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
in pg con_appls goal (K tacs) end;
--- a/src/HOLCF/Tools/pcpodef.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Mon Apr 19 07:38:35 2010 +0200
@@ -169,18 +169,18 @@
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
(*rhs*)
- val (_, tmp_lthy) =
- thy |> Theory.copy |> Theory_Target.init NONE
- |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val set = prep_term tmp_lthy raw_set;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+ val tmp_ctxt =
+ ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
val setT = Term.fastype_of set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT));
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
--- a/src/HOLCF/Tools/repdef.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Mon Apr 19 07:38:35 2010 +0200
@@ -64,18 +64,18 @@
val _ = Theory.requires thy "Representable" "repdefs";
(*rhs*)
- val (_, tmp_lthy) =
- thy |> Theory.copy |> Theory_Target.init NONE
- |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val defl = prep_term tmp_lthy raw_defl;
- val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl;
+ val tmp_ctxt =
+ ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val defl = prep_term tmp_ctxt raw_defl;
+ val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
val deflT = Term.fastype_of defl;
val _ = if deflT = @{typ "udom alg_defl"} then ()
- else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT));
+ else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args;
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
val lhs_sorts = map snd lhs_tfrees;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
--- a/src/HOLCF/Universal.thy Mon Apr 19 07:38:08 2010 +0200
+++ b/src/HOLCF/Universal.thy Mon Apr 19 07:38:35 2010 +0200
@@ -809,7 +809,7 @@
apply (rule ubasis_until_less)
done
-hide (open) const
+hide_const (open)
node
choose
choose_pos
--- a/src/Pure/Isar/isar_cmd.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Apr 19 07:38:35 2010 +0200
@@ -19,7 +19,10 @@
val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
local_theory -> local_theory
- val hide_names: bool -> string * xstring list -> theory -> theory
+ val hide_class: bool -> xstring list -> theory -> theory
+ val hide_type: bool -> xstring list -> theory -> theory
+ val hide_const: bool -> xstring list -> theory -> theory
+ val hide_fact: bool -> xstring list -> theory -> theory
val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -196,23 +199,19 @@
(* hide names *)
-val hide_kinds =
- [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
- ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
- ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
- ("fact", (PureThy.intern_fact, PureThy.defined_fact, PureThy.hide_fact))];
+fun hide_names intern check hide fully xnames thy =
+ let
+ val names = map (intern thy) xnames;
+ val bads = filter_out (check thy) names;
+ in
+ if null bads then fold (hide fully) names thy
+ else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
+ end;
-fun hide_names b (kind, xnames) thy =
- (case AList.lookup (op =) hide_kinds kind of
- SOME (intern, check, hide) =>
- let
- val names = map (intern thy) xnames;
- val bads = filter_out (check thy) names;
- in
- if null bads then fold (hide b) names thy
- else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
- end
- | NONE => error ("Bad name space specification: " ^ quote kind));
+val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
+val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
+val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
+val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact;
(* goals *)
--- a/src/Pure/Isar/isar_syn.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Apr 19 07:38:35 2010 +0200
@@ -108,10 +108,10 @@
>> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
val _ =
- OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
+ OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
(P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
- >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+ >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
val _ =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
@@ -280,10 +280,15 @@
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
(Scan.succeed (Toplevel.theory Sign.local_path));
-val _ =
- OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
- ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
- (Toplevel.theory o uncurry IsarCmd.hide_names));
+fun hide_names name hide what =
+ OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
+ ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
+ (Toplevel.theory o uncurry hide));
+
+val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
+val _ = hide_names "hide_type" IsarCmd.hide_type "types";
+val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
+val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
(* use ML text *)
--- a/src/Pure/Isar/proof_context.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Apr 19 07:38:35 2010 +0200
@@ -62,6 +62,8 @@
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> string -> term
val allow_dummies: Proof.context -> Proof.context
+ val check_tvar: Proof.context -> indexname * sort -> indexname * sort
+ val check_tfree: Proof.context -> string * sort -> string * sort
val decode_term: Proof.context -> term -> term
val standard_infer_types: Proof.context -> term list -> term list
val read_term_pattern: Proof.context -> string -> term
@@ -606,19 +608,26 @@
(* types *)
-fun get_sort ctxt def_sort raw_env =
+fun get_sort ctxt raw_env =
let
val tsig = tsig_of ctxt;
fun eq ((xi, S), (xi', S')) =
Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
val env = distinct eq raw_env;
- val _ = (case duplicates (eq_fst (op =)) env of [] => ()
+ val _ =
+ (case duplicates (eq_fst (op =)) env of
+ [] => ()
| dups => error ("Inconsistent sort constraints for type variable(s) "
^ commas_quote (map (Term.string_of_vname' o fst) dups)));
+ fun lookup xi =
+ (case AList.lookup (op =) env xi of
+ NONE => NONE
+ | SOME S => if S = dummyS then NONE else SOME S);
+
fun get xi =
- (case (AList.lookup (op =) env xi, def_sort xi) of
+ (case (lookup xi, Variable.def_sort ctxt xi) of
(NONE, NONE) => Type.defaultS tsig
| (NONE, SOME S) => S
| (SOME S, NONE) => S
@@ -629,6 +638,9 @@
" for type variable " ^ quote (Term.string_of_vname' xi)));
in get end;
+fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
+fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
+
local
fun intern_skolem ctxt def_type x =
@@ -647,7 +659,7 @@
in
fun term_context ctxt =
- {get_sort = get_sort ctxt (Variable.def_sort ctxt),
+ {get_sort = get_sort ctxt,
map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
map_free = intern_skolem ctxt (Variable.def_type ctxt false)};
@@ -731,9 +743,8 @@
fun parse_typ ctxt text =
let
- val get_sort = get_sort ctxt (Variable.def_sort ctxt);
val (syms, pos) = Syntax.parse_token Markup.typ text;
- val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+ val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
in T end;
--- a/src/Pure/Isar/typedecl.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Mon Apr 19 07:38:35 2010 +0200
@@ -1,21 +1,29 @@
(* Title: Pure/Isar/typedecl.ML
Author: Makarius
-Type declarations (within the object logic).
+Type declarations (with object-logic arities) and type abbreviations.
*)
signature TYPEDECL =
sig
val read_constraint: Proof.context -> string option -> sort
- val predeclare_constraints: binding * (string * sort) list * mixfix ->
- local_theory -> string * local_theory
+ val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
+ val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
+ val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
+ val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
end;
structure Typedecl: TYPEDECL =
struct
+(* constraints *)
+
+fun read_constraint _ NONE = dummyS
+ | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
+
(* primitives *)
fun object_logic_arity name thy =
@@ -23,46 +31,44 @@
NONE => thy
| SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
-fun basic_typedecl (b, n, mx) lthy =
+fun basic_decl decl (b, n, mx) lthy =
let val name = Local_Theory.full_name lthy b in
lthy
- |> Local_Theory.theory (Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name)
+ |> Local_Theory.theory (decl name)
|> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
|> Local_Theory.type_alias b name
|> pair name
end;
-
-(* syntactic version -- useful for internalizing additional types/terms beforehand *)
-
-fun read_constraint _ NONE = dummyS
- | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
-
-fun predeclare_constraints (b, raw_args, mx) =
- basic_typedecl (b, length raw_args, mx) ##>
- fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args;
+fun basic_typedecl (b, n, mx) =
+ basic_decl (fn name => Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name) (b, n, mx);
-(* regular version -- without dependencies on type parameters of the context *)
+(* global type -- without dependencies on type parameters of the context *)
-fun typedecl (b, raw_args, mx) lthy =
+fun global_type lthy (b, raw_args) =
let
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
- val args = raw_args
- |> map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort lthy (a, ~1) else S));
- val T = Type (Local_Theory.full_name lthy b, map TFree args);
+ val args = map (TFree o ProofContext.check_tfree lthy) raw_args;
+ val T = Type (Local_Theory.full_name lthy b, args);
val bad_args =
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
|> filter_out Term.is_TVar;
- val _ = not (null bad_args) andalso
+ val _ = null bad_args orelse
err ("Locally fixed type arguments " ^
commas_quote (map (Syntax.string_of_typ lthy) bad_args));
- in
+ in T end;
+
+
+(* type declarations *)
+
+fun typedecl (b, raw_args, mx) lthy =
+ let val T = global_type lthy (b, raw_args) in
lthy
- |> basic_typedecl (b, length args, mx)
+ |> basic_typedecl (b, length raw_args, mx)
|> snd
|> Variable.declare_typ T
|> pair T
@@ -73,5 +79,28 @@
#> typedecl decl
#> Local_Theory.exit_result_global Morphism.typ;
+
+(* type abbreviations *)
+
+fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
+ let
+ val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
+ val rhs = prep_typ lthy raw_rhs
+ handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
+ in
+ lthy
+ |> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx)
+ |> snd
+ |> pair name
+ end;
+
+val abbrev = gen_abbrev ProofContext.cert_typ_syntax;
+val abbrev_cmd = gen_abbrev ProofContext.read_typ_syntax;
+
+fun abbrev_global decl rhs =
+ Theory_Target.init NONE
+ #> abbrev decl rhs
+ #> Local_Theory.exit_result_global (K I);
+
end;
--- a/src/Pure/ML-Systems/polyml.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Mon Apr 19 07:38:35 2010 +0200
@@ -66,3 +66,6 @@
use_text context (1, "pp") false
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+val ml_make_string =
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
+
--- a/src/Pure/ML-Systems/polyml_common.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Mon Apr 19 07:38:35 2010 +0200
@@ -55,7 +55,7 @@
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-(* print depth *)
+(* toplevel printing *)
local
val depth = Unsynchronized.ref 10;
@@ -66,6 +66,8 @@
val error_depth = PolyML.error_depth;
+val ml_make_string = "PolyML.makestring";
+
(** interrupts **)
--- a/src/Pure/ML-Systems/smlnj.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Apr 19 07:38:35 2010 +0200
@@ -61,6 +61,8 @@
Control.Print.printLength := dest_int n);
end;
+val ml_make_string = "(fn _ => \"?\")";
+
(*prompts*)
fun ml_prompts p1 p2 =
--- a/src/Pure/ML/ml_antiquote.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Mon Apr 19 07:38:35 2010 +0200
@@ -59,6 +59,8 @@
structure P = OuterParse;
+val _ = inline "make_string" (Scan.succeed ml_make_string);
+
val _ = value "binding"
(Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
--- a/src/Pure/ML/ml_env.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/ML/ml_env.ML Mon Apr 19 07:38:35 2010 +0200
@@ -9,6 +9,7 @@
val inherit: Context.generic -> Context.generic -> Context.generic
val name_space: ML_Name_Space.T
val local_context: use_context
+ val check_functor: string -> unit
end
structure ML_Env: ML_ENV =
@@ -88,5 +89,11 @@
print = writeln,
error = error};
+val is_functor = is_some o #lookupFunct name_space;
+
+fun check_functor name =
+ if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
+ else error ("Unknown ML functor: " ^ quote name);
+
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Apr 19 07:38:35 2010 +0200
@@ -955,7 +955,7 @@
end)
| _ => raise PGIP "Invalid PGIP packet received")
handle PGIP msg =>
- (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
+ (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
(XML.string_of xml));
true))
--- a/src/Pure/System/cygwin.scala Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/System/cygwin.scala Mon Apr 19 07:38:35 2010 +0200
@@ -91,9 +91,9 @@
def check_root(): String =
{
- val root_env = java.lang.System.getenv("CYGWIN_ROOT")
+ val this_cygwin = java.lang.System.getenv("THIS_CYGWIN")
val root =
- if (root_env != null && root_env != "") root_env
+ if (this_cygwin != null && this_cygwin != "") this_cygwin
else
query_registry(CYGWIN_SETUP1, "rootdir") orElse
query_registry(CYGWIN_SETUP2, "rootdir") getOrElse
--- a/src/Pure/System/gui_setup.scala Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/System/gui_setup.scala Mon Apr 19 07:38:35 2010 +0200
@@ -43,19 +43,16 @@
}
// values
- Platform.defaults match {
- case None =>
- case Some((name, None)) => text.append("Platform: " + name + "\n")
- case Some((name1, Some(name2))) =>
- text.append("Main platform: " + name1 + "\n")
- text.append("Alternative platform: " + name2 + "\n")
- }
- if (Platform.is_windows) {
+ text.append("JVM platform: " + Platform.jvm_platform() + "\n")
+ if (Platform.is_windows)
text.append("Cygwin root: " + Cygwin.check_root() + "\n")
- }
try {
val isabelle_system = new Isabelle_System
text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
+ text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
+ val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
+ if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
+ text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
} catch {
case e: RuntimeException => text.append(e.getMessage + "\n")
}
--- a/src/Pure/System/isabelle_system.scala Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Apr 19 07:38:35 2010 +0200
@@ -26,7 +26,8 @@
{
import scala.collection.JavaConversions._
- val env0 = Map(java.lang.System.getenv.toList: _*)
+ val env0 = Map(java.lang.System.getenv.toList: _*) +
+ ("THIS_JAVA" -> this_java())
val isabelle_home =
env0.get("ISABELLE_HOME") match {
--- a/src/Pure/System/platform.scala Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/System/platform.scala Mon Apr 19 07:38:35 2010 +0200
@@ -19,37 +19,37 @@
val is_windows = System.getProperty("os.name").startsWith("Windows")
- /* Isabelle platform identifiers */
+ /* Platform identifiers */
private val Solaris = new Regex("SunOS|Solaris")
private val Linux = new Regex("Linux")
private val Darwin = new Regex("Mac OS X")
- private val Cygwin = new Regex("Windows.*")
+ private val Windows = new Regex("Windows.*")
private val X86 = new Regex("i.86|x86")
private val X86_64 = new Regex("amd64|x86_64")
private val Sparc = new Regex("sparc")
private val PPC = new Regex("PowerPC|ppc")
- // main default, optional 64bit variant
- val defaults: Option[(String, Option[String])] =
+ def jvm_platform(): String =
{
- (java.lang.System.getProperty("os.name") match {
- case Solaris() => Some("solaris")
- case Linux() => Some("linux")
- case Darwin() => Some("darwin")
- case Cygwin() => Some("cygwin")
- case _ => None
- }) match {
- case Some(name) =>
- java.lang.System.getProperty("os.arch") match {
- case X86() => Some(("x86-" + name, None))
- case X86_64() => Some(("x86-" + name, if (is_windows) None else Some("x86_64-" + name)))
- case Sparc() => Some(("sparc-" + name, None))
- case PPC() => Some(("ppc-" + name, None))
- }
- case None => None
- }
+ val arch =
+ java.lang.System.getProperty("os.arch") match {
+ case X86() => "x86"
+ case X86_64() => "x86_64"
+ case Sparc() => "sparc"
+ case PPC() => "ppc"
+ case _ => error("Failed to determine CPU architecture")
+ }
+ val os =
+ java.lang.System.getProperty("os.name") match {
+ case Solaris() => "solaris"
+ case Linux() => "linux"
+ case Darwin() => "darwin"
+ case Windows() => "windows"
+ case _ => error("Failed to determine operating system platform")
+ }
+ arch + "-" + os
}
--- a/src/Pure/System/standard_system.scala Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/System/standard_system.scala Mon Apr 19 07:38:35 2010 +0200
@@ -211,4 +211,17 @@
}
}
else jvm_path
+
+
+ /* this_java executable */
+
+ def this_java(): String =
+ {
+ val java_home = System.getProperty("java.home")
+ val java_exe =
+ if (Platform.is_windows) new File(java_home + "\\bin\\java.exe")
+ else new File(java_home + "/bin/java")
+ if (!java_exe.isFile) error("Expected this Java executable: " + java_exe.toString)
+ posix_path(java_exe.getAbsolutePath)
+ }
}
--- a/src/Pure/Thy/thy_output.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Apr 19 07:38:35 2010 +0200
@@ -599,7 +599,7 @@
val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
-val _ = ml_text "ML_functor" (K ""); (*no check!*)
+val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
val _ = ml_text "ML_text" (K "");
end;
--- a/src/Pure/sign.ML Mon Apr 19 07:38:08 2010 +0200
+++ b/src/Pure/sign.ML Mon Apr 19 07:38:35 2010 +0200
@@ -72,8 +72,7 @@
val add_defsort_i: sort -> theory -> theory
val add_types: (binding * int * mixfix) list -> theory -> theory
val add_nonterminals: binding list -> theory -> theory
- val add_tyabbrs: (binding * string list * string * mixfix) list -> theory -> theory
- val add_tyabbrs_i: (binding * string list * typ * mixfix) list -> theory -> theory
+ val add_type_abbrev: binding * string list * typ -> theory -> theory
val add_syntax: (string * string * mixfix) list -> theory -> theory
val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
@@ -346,42 +345,25 @@
(* add type constructors *)
-val type_syntax = Syntax.mark_type oo full_name;
-
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' =
- Syntax.update_type_gram true Syntax.mode_default
- (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
- val decls = map (fn (a, n, _) => (a, n)) types;
- val tsig' = fold (Type.add_type naming) decls tsig;
+ fun type_syntax (b, n, mx) =
+ (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
+ val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
+ val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
in (naming, syn', tsig', consts) end);
(* add nonterminals *)
-fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
- let
- val tsig' = fold (Type.add_nonterminal naming) ns tsig;
- in (naming, syn, tsig', consts) end);
+fun add_nonterminals ns = map_sign (fn (naming, syn, tsig, consts) =>
+ (naming, syn, fold (Type.add_nonterminal naming) ns tsig, consts));
(* add type abbreviations *)
-fun gen_add_tyabbr parse_typ (b, vs, rhs, mx) thy =
- thy |> map_sign (fn (naming, syn, tsig, consts) =>
- let
- val ctxt = ProofContext.init thy;
- val syn' =
- Syntax.update_type_gram true Syntax.mode_default
- [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
- val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
- handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
- val tsig' = Type.add_abbrev naming abbr tsig;
- in (naming, syn', tsig', consts) end);
-
-val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
-val add_tyabbrs_i = fold (gen_add_tyabbr (K I));
+fun add_type_abbrev abbr = map_sign (fn (naming, syn, tsig, consts) =>
+ (naming, syn, Type.add_abbrev naming abbr tsig, consts));
(* modify syntax *)