# HG changeset patch # User haftmann # Date 1271655515 -7200 # Node ID 4d220994f30ba5927dc68598614fb396bf1d66f9 # Parent 2e92aca73cab416a16fe21f68b29465064babcf8# Parent ead2db2be11a809f809f77f4f5ddf305857d0c9f merged diff -r ead2db2be11a -r 4d220994f30b Admin/isatest/isatest-makeall --- 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 diff -r ead2db2be11a -r 4d220994f30b Admin/isatest/isatest-makedist --- 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") diff -r ead2db2be11a -r 4d220994f30b NEWS --- 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. diff -r ead2db2be11a -r 4d220994f30b doc-src/Codegen/Thy/Program.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarImplementation/Thy/Logic.thy --- 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 "\"}-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! diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarImplementation/Thy/ML.thy --- 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. diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarImplementation/Thy/document/ML.tex --- 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. diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarRef/Thy/HOL_Specific.thy --- 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} diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarRef/Thy/Spec.thy --- 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 \ theory"} \\ + @{command_def "types"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "typedecl"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} @@ -1225,11 +1225,14 @@ \begin{matharray}{rcl} @{command_def "global"} & : & @{text "theory \ theory"} \\ @{command_def "local"} & : & @{text "theory \ theory"} \\ - @{command_def "hide"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_class"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_type"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_const"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_fact"} & : & @{text "theory \ 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} *} diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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} diff -r ead2db2be11a -r 4d220994f30b doc-src/IsarRef/Thy/document/Spec.tex --- 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% diff -r ead2db2be11a -r 4d220994f30b doc-src/Locales/Locales/Examples.thy --- 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 (* diff -r ead2db2be11a -r 4d220994f30b doc-src/Locales/Locales/document/Examples.tex --- 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 diff -r ead2db2be11a -r 4d220994f30b doc-src/System/Thy/Basics.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b doc-src/System/Thy/document/Basics.tex --- 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 diff -r ead2db2be11a -r 4d220994f30b doc-src/TutorialI/Datatype/Nested.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b doc-src/TutorialI/Documents/Documents.thy --- 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 \ bool \ bool" (infixl "\" 60) @@ -161,7 +161,7 @@ *} (*<*) -hide const xor +hide_const xor setup {* Sign.add_path "version2" *} (*>*) definition xor :: "bool \ bool \ bool" (infixl "[+]\" 60) diff -r ead2db2be11a -r 4d220994f30b doc-src/TutorialI/Misc/Option2.thy --- 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)}% diff -r ead2db2be11a -r 4d220994f30b doc-src/TutorialI/Types/Overloading.thy --- 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. *} diff -r ead2db2be11a -r 4d220994f30b doc-src/antiquote_setup.ML --- 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) "")) diff -r ead2db2be11a -r 4d220994f30b etc/isar-keywords-ZF.el --- 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" diff -r ead2db2be11a -r 4d220994f30b etc/isar-keywords.el --- 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" diff -r ead2db2be11a -r 4d220994f30b etc/settings --- 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 \ diff -r ead2db2be11a -r 4d220994f30b lib/scripts/getsettings --- 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 diff -r ead2db2be11a -r 4d220994f30b lib/scripts/isabelle-platform --- /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 + diff -r ead2db2be11a -r 4d220994f30b src/FOL/FOL.thy --- 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. *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Bali/Basis.thy --- 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) diff -r ead2db2be11a -r 4d220994f30b src/HOL/Bali/TypeSafe.thy --- 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\s0 \halloc oi\a\ s1" and diff -r ead2db2be11a -r 4d220994f30b src/HOL/Code_Evaluation.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Code_Numeral.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/DSequence.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Datatype.thy --- 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" diff -r ead2db2be11a -r 4d220994f30b src/HOL/Finite_Set.thy --- 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 \ 'a set)" setup {* Sign.parent_path *} -hide const finite +hide_const finite context finite begin diff -r ead2db2be11a -r 4d220994f30b src/HOL/Fun.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Groups.thy --- 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") diff -r ead2db2be11a -r 4d220994f30b src/HOL/HOL.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Imperative_HOL/Array.thy --- 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 \== liftM Code_Numeral.of_nat" -hide (open) const length' +hide_const (open) length' lemma [code]: "Array.length = Array.length' \== 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 \ 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 \ return a" by (simp add: upd'_def monad_simp upd_return) diff -r ead2db2be11a -r 4d220994f30b src/HOL/Imperative_HOL/Heap.thy --- 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 \ 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Imperative_HOL/Ref.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- 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\heap array \ nat \ nat \ unit Heap" where "swap a i j = (do diff -r ead2db2be11a -r 4d220994f30b src/HOL/Int.thy --- 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\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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Lattice/Bounds.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Lazy_Sequence.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Dlist.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Efficient_Nat.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Executable_Set.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Fset.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Mapping.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Multiset.thy --- 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\" 60) -hide (open) const bagify +hide_const (open) bagify subsection {* The multiset order *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Nested_Environment.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Quotient_List.thy --- 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: "\x y. R x y \ (\a b. R a b \ 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 \ length a" by fact + then have e: "\list_rel S x a" using list_rel_len by auto + have "length y \ length b" using d a c by simp + then have "\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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/RBT.thy --- 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) \ 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 (*>*) diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/RBT_Impl.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Library/Transitive_Closure_Table.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/List.thy --- 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 \ 'a list \ 'a list" where "insert x xs = (if x \ 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 \ 'a list \ '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 \ length ys = length zs \ length zs = length ws \ + P [] [] [] [] \ (\x xs y ys z zs w ws. length xs = length ys \ + length ys = length zs \ length zs = length ws \ P xs ys zs ws \ + P (x#xs) (y#ys) (z#zs) (w#ws)) \ 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': "\ P [] []; \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. *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/NSA/Filter.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Nat.thy --- 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 \ f ^^ n" @@ -1504,7 +1504,7 @@ lemma diff_diff_eq: "[| k \ m; k \ (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 \ m; k \ (n::nat) |] ==> (m-k = n-k) = (m=n)" by (auto split add: nat_diff_split) diff -r ead2db2be11a -r 4d220994f30b src/HOL/New_DSequence.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/New_Random_Sequence.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Nitpick.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Option.thy --- 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 \ 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") diff -r ead2db2be11a -r 4d220994f30b src/HOL/Predicate.thy --- 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 ("\") and bind (infixl "\=" 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- 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 *) diff -r ead2db2be11a -r 4d220994f30b src/HOL/Product_Type.thy --- 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] diff -r ead2db2be11a -r 4d220994f30b src/HOL/Quickcheck.thy --- 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 \ 'b) \ ('a randompred \ '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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Random.thy --- 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\" 60) diff -r ead2db2be11a -r 4d220994f30b src/HOL/Random_Sequence.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Record.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Statespace/state_fun.ML --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Statespace/state_space.ML --- 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 ***) diff -r ead2db2be11a -r 4d220994f30b src/HOL/String.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Sum_Type.thy --- 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 \ UNIV <+> UNIV \ u \ UNIV" by (cases u) auto qed -hide (open) const Suml Sumr Projl Projr +hide_const (open) Suml Sumr Projl Projr end diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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); diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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)); diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Datatype/datatype.ML --- 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') = diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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*); diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 *) diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/record.ML --- 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))); diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/typecopy.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/HOL/Tools/typedef.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/HOL/Typerep.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/Word/BinGeneral.thy --- 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" diff -r ead2db2be11a -r 4d220994f30b src/HOL/ex/Meson_Test.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/ex/Numeral.thy --- 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 *} diff -r ead2db2be11a -r 4d220994f30b src/HOL/ex/RPred.thy --- 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 \ 'b) \ ('a rpred \ '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 diff -r ead2db2be11a -r 4d220994f30b src/HOL/ex/SVC_Oracle.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/Domain.thy --- 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" diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/Fixrec.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/IOA/meta_theory/Automata.thy --- 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" diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/Tools/Domain/domain_theorems.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/Tools/pcpodef.ML --- 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); diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/Tools/repdef.ML --- 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); diff -r ead2db2be11a -r 4d220994f30b src/HOLCF/Universal.thy --- 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 diff -r ead2db2be11a -r 4d220994f30b src/Pure/Isar/isar_cmd.ML --- 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 *) diff -r ead2db2be11a -r 4d220994f30b src/Pure/Isar/isar_syn.ML --- 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 *) diff -r ead2db2be11a -r 4d220994f30b src/Pure/Isar/proof_context.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/Pure/Isar/typedecl.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/Pure/ML-Systems/polyml.ML --- 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 ())))))"; + diff -r ead2db2be11a -r 4d220994f30b src/Pure/ML-Systems/polyml_common.ML --- 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 **) diff -r ead2db2be11a -r 4d220994f30b src/Pure/ML-Systems/smlnj.ML --- 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 = diff -r ead2db2be11a -r 4d220994f30b src/Pure/ML/ml_antiquote.ML --- 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))); diff -r ead2db2be11a -r 4d220994f30b src/Pure/ML/ml_env.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/Pure/ProofGeneral/proof_general_pgip.ML --- 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)) diff -r ead2db2be11a -r 4d220994f30b src/Pure/System/cygwin.scala --- 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 diff -r ead2db2be11a -r 4d220994f30b src/Pure/System/gui_setup.scala --- 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") } diff -r ead2db2be11a -r 4d220994f30b src/Pure/System/isabelle_system.scala --- 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 { diff -r ead2db2be11a -r 4d220994f30b src/Pure/System/platform.scala --- 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 } diff -r ead2db2be11a -r 4d220994f30b src/Pure/System/standard_system.scala --- 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) + } } diff -r ead2db2be11a -r 4d220994f30b src/Pure/Thy/thy_output.ML --- 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; diff -r ead2db2be11a -r 4d220994f30b src/Pure/sign.ML --- 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 *)