| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 28 Apr 2010 14:01:13 +0200 | |
| changeset 36466 | 14de0767dc7e |
| parent 36465 | 15e834a03509 (current diff) |
| parent 36461 | e741ba542b61 (diff) |
| child 36467 | 0e2300856d7d |
--- a/NEWS Wed Apr 28 13:29:40 2010 +0200 +++ b/NEWS Wed Apr 28 14:01:13 2010 +0200 @@ -84,6 +84,8 @@ *** Pure *** +* Empty class specifications observe default sort. INCOMPATIBILITY. + * Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY. * Code generator: simple concept for abstract datatypes obeying invariants. @@ -116,6 +118,9 @@ context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure. +* Command 'defaultsort' is renamed to 'default_sort', it works within +a local theory context. Minor INCOMPATIBILITY. + * Proof terms: Type substitutions on proof constants now use canonical order of type variables. INCOMPATIBILITY: Tools working with proof terms may need to be adapted.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 28 14:01:13 2010 +0200 @@ -897,98 +897,6 @@ *} -section {* Invoking automated reasoning tools --- The Sledgehammer *} - -text {* - Isabelle/HOL includes a generic \emph{ATP manager} that allows - external automated reasoning tools to crunch a pending goal. - Supported provers include E\footnote{\url{http://www.eprover.org}}, - SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire. - There is also a wrapper to invoke provers remotely via the - SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}} - web service. - - The problem passed to external provers consists of the goal together - with a smart selection of lemmas from the current theory context. - The result of a successful proof search is some source text that - usually reconstructs the proof within Isabelle, without requiring - external provers again. The Metis - prover\footnote{\url{http://www.gilith.com/software/metis/}} that is - integrated into Isabelle/HOL is being used here. - - In this mode of operation, heavy means of automated reasoning are - used as a strong relevance filter, while the main proof checking - works via explicit inferences going through the Isabelle kernel. - Moreover, rechecking Isabelle proof texts with already specified - auxiliary facts is much faster than performing fully automated - search over and over again. - - \begin{matharray}{rcl} - @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\ - @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ - @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ - @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ - @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ - @{method_def (HOL) metis} & : & @{text method} \\ - \end{matharray} - - \begin{rail} - 'sledgehammer' ( nameref * ) - ; - 'atp\_messages' ('(' nat ')')? - ; - - 'metis' thmrefs - ; - \end{rail} - - \begin{description} - - \item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> prover\<^sub>n"} - invokes the specified automated theorem provers on the first - subgoal. Provers are run in parallel, the first successful result - is displayed, and the other attempts are terminated. - - Provers are defined in the theory context, see also @{command (HOL) - print_atps}. If no provers are given as arguments to @{command - (HOL) sledgehammer}, the system refers to the default defined as - ``ATP provers'' preference by the user interface. - - There are additional preferences for timeout (default: 60 seconds), - and the maximum number of independent prover processes (default: 5); - excessive provers are automatically terminated. - - \item @{command (HOL) print_atps} prints the list of automated - theorem provers available to the @{command (HOL) sledgehammer} - command. - - \item @{command (HOL) atp_info} prints information about presently - running provers, including elapsed runtime, and the remaining time - until timeout. - - \item @{command (HOL) atp_kill} terminates all presently running - provers. - - \item @{command (HOL) atp_messages} displays recent messages issued - by automated theorem provers. This allows to examine results that - might have got lost due to the asynchronous nature of default - @{command (HOL) sledgehammer} output. An optional message limit may - be specified (default 5). - - \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover - with the given facts. Metis is an automated proof tool of medium - strength, but is fully integrated into Isabelle/HOL, with explicit - inferences going through the kernel. Thus its results are - guaranteed to be ``correct by construction''. - - Note that all facts used with Metis need to be specified as explicit - arguments. There are no rule declarations as for other Isabelle - provers, like @{method blast} or @{method fast}. - - \end{description} -*} - - section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *} text {*
--- a/doc-src/IsarRef/Thy/Spec.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Wed Apr 28 14:01:13 2010 +0200 @@ -902,7 +902,7 @@ \begin{matharray}{rcll} @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\ @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\ - @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\ + @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ \end{matharray} @@ -911,7 +911,7 @@ ; 'classrel' (nameref ('<' | subseteq) nameref + 'and') ; - 'defaultsort' sort + 'default\_sort' sort ; \end{rail} @@ -929,7 +929,7 @@ (see \secref{sec:class}) provide a way to introduce proven class relations. - \item @{command "defaultsort"}~@{text s} makes sort @{text s} the + \item @{command "default_sort"}~@{text s} makes sort @{text s} the new default sort for any type variable that is given explicitly in the text, but lacks a sort constraint (wrt.\ the current context). Type variables generated by type inference are not affected.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 28 13:29:40 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 28 14:01:13 2010 +0200 @@ -915,98 +915,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Invoking automated reasoning tools --- The Sledgehammer% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Isabelle/HOL includes a generic \emph{ATP manager} that allows - external automated reasoning tools to crunch a pending goal. - Supported provers include E\footnote{\url{http://www.eprover.org}}, - SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire. - There is also a wrapper to invoke provers remotely via the - SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}} - web service. - - The problem passed to external provers consists of the goal together - with a smart selection of lemmas from the current theory context. - The result of a successful proof search is some source text that - usually reconstructs the proof within Isabelle, without requiring - external provers again. The Metis - prover\footnote{\url{http://www.gilith.com/software/metis/}} that is - integrated into Isabelle/HOL is being used here. - - In this mode of operation, heavy means of automated reasoning are - used as a strong relevance filter, while the main proof checking - works via explicit inferences going through the Isabelle kernel. - Moreover, rechecking Isabelle proof texts with already specified - auxiliary facts is much faster than performing fully automated - search over and over again. - - \begin{matharray}{rcl} - \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ - \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\ - \end{matharray} - - \begin{rail} - 'sledgehammer' ( nameref * ) - ; - 'atp\_messages' ('(' nat ')')? - ; - - 'metis' thmrefs - ; - \end{rail} - - \begin{description} - - \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}} - invokes the specified automated theorem provers on the first - subgoal. Provers are run in parallel, the first successful result - is displayed, and the other attempts are terminated. - - Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}. If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as - ``ATP provers'' preference by the user interface. - - There are additional preferences for timeout (default: 60 seconds), - and the maximum number of independent prover processes (default: 5); - excessive provers are automatically terminated. - - \item \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}} prints the list of automated - theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} - command. - - \item \hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}} prints information about presently - running provers, including elapsed runtime, and the remaining time - until timeout. - - \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running - provers. - - \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued - by automated theorem provers. This allows to examine results that - might have got lost due to the asynchronous nature of default - \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may - be specified (default 5). - - \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover - with the given facts. Metis is an automated proof tool of medium - strength, but is fully integrated into Isabelle/HOL, with explicit - inferences going through the kernel. Thus its results are - guaranteed to be ``correct by construction''. - - Note that all facts used with Metis need to be specified as explicit - arguments. There are no rule declarations as for other Isabelle - provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}% } \isamarkuptrue%
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Apr 28 13:29:40 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Apr 28 14:01:13 2010 +0200 @@ -937,7 +937,7 @@ \begin{matharray}{rcll} \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ - \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ + \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ \end{matharray} @@ -946,7 +946,7 @@ ; 'classrel' (nameref ('<' | subseteq) nameref + 'and') ; - 'defaultsort' sort + 'default\_sort' sort ; \end{rail} @@ -964,7 +964,7 @@ (see \secref{sec:class}) provide a way to introduce proven class relations. - \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the + \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the new default sort for any type variable that is given explicitly in the text, but lacks a sort constraint (wrt.\ the current context). Type variables generated by type inference are not affected.
--- a/etc/isar-keywords-ZF.el Wed Apr 28 13:29:40 2010 +0200 +++ b/etc/isar-keywords-ZF.el Wed Apr 28 14:01:13 2010 +0200 @@ -57,7 +57,7 @@ "declaration" "declare" "def" - "defaultsort" + "default_sort" "defer" "definition" "defs" @@ -372,7 +372,7 @@ "datatype" "declaration" "declare" - "defaultsort" + "default_sort" "definition" "defs" "extract"
--- a/etc/isar-keywords.el Wed Apr 28 13:29:40 2010 +0200 +++ b/etc/isar-keywords.el Wed Apr 28 14:01:13 2010 +0200 @@ -30,10 +30,6 @@ "arities" "assume" "atom_decl" - "atp_info" - "atp_kill" - "atp_messages" - "atp_minimize" "attribute_setup" "automaton" "ax_specification" @@ -81,7 +77,7 @@ "declaration" "declare" "def" - "defaultsort" + "default_sort" "defer" "defer_recdef" "definition" @@ -172,7 +168,6 @@ "print_abbrevs" "print_antiquotations" "print_ast_translation" - "print_atps" "print_attributes" "print_binds" "print_cases" @@ -362,10 +357,6 @@ '("ML_command" "ML_val" "ProofGeneral\\.pr" - "atp_info" - "atp_kill" - "atp_messages" - "atp_minimize" "boogie_status" "cd" "class_deps" @@ -389,7 +380,6 @@ "prf" "print_abbrevs" "print_antiquotations" - "print_atps" "print_attributes" "print_binds" "print_cases" @@ -487,7 +477,7 @@ "datatype" "declaration" "declare" - "defaultsort" + "default_sort" "defer_recdef" "definition" "defs"
--- a/src/CCL/CCL.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/CCL/CCL.thy Wed Apr 28 14:01:13 2010 +0200 @@ -17,7 +17,7 @@ *} classes prog < "term" -defaultsort prog +default_sort prog arities "fun" :: (prog, prog) prog
--- a/src/FOL/IFOL.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/FOL/IFOL.thy Wed Apr 28 14:01:13 2010 +0200 @@ -31,7 +31,7 @@ global classes "term" -defaultsort "term" +default_sort "term" typedecl o
--- a/src/FOLP/IFOLP.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/FOLP/IFOLP.thy Wed Apr 28 14:01:13 2010 +0200 @@ -15,7 +15,7 @@ global classes "term" -defaultsort "term" +default_sort "term" typedecl p typedecl o
--- a/src/HOL/HOL.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOL/HOL.thy Wed Apr 28 14:01:13 2010 +0200 @@ -40,7 +40,7 @@ subsubsection {* Core syntax *} classes type -defaultsort type +default_sort type setup {* Object_Logic.add_base_sort @{sort type} *} arities
--- a/src/HOL/ex/Higher_Order_Logic.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOL/ex/Higher_Order_Logic.thy Wed Apr 28 14:01:13 2010 +0200 @@ -20,7 +20,7 @@ subsection {* Pure Logic *} classes type -defaultsort type +default_sort type typedecl o arities
--- a/src/HOLCF/Adm.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Adm.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Cont begin -defaultsort cpo +default_sort cpo subsection {* Definitions *}
--- a/src/HOLCF/Algebraic.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Algebraic.thy Wed Apr 28 14:01:13 2010 +0200 @@ -297,7 +297,7 @@ subsection {* Type constructor for finite deflations *} -defaultsort profinite +default_sort profinite typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}" by (fast intro: finite_deflation_approx)
--- a/src/HOLCF/Cfun.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Cfun.thy Wed Apr 28 14:01:13 2010 +0200 @@ -9,7 +9,7 @@ imports Pcpodef Ffun Product_Cpo begin -defaultsort cpo +default_sort cpo subsection {* Definition of continuous function type *} @@ -511,7 +511,7 @@ subsection {* Strictified functions *} -defaultsort pcpo +default_sort pcpo definition strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
--- a/src/HOLCF/CompactBasis.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/CompactBasis.thy Wed Apr 28 14:01:13 2010 +0200 @@ -10,7 +10,7 @@ subsection {* Compact bases of bifinite domains *} -defaultsort profinite +default_sort profinite typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}" by (fast intro: compact_approx)
--- a/src/HOLCF/Cont.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Cont.thy Wed Apr 28 14:01:13 2010 +0200 @@ -14,7 +14,7 @@ of default class po *} -defaultsort po +default_sort po subsection {* Definitions *}
--- a/src/HOLCF/Cprod.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Cprod.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Bifinite begin -defaultsort cpo +default_sort cpo subsection {* Continuous case function for unit type *}
--- a/src/HOLCF/Deflation.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Deflation.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Cfun begin -defaultsort cpo +default_sort cpo subsection {* Continuous deflations *}
--- a/src/HOLCF/Domain.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Domain.thy Wed Apr 28 14:01:13 2010 +0200 @@ -16,7 +16,7 @@ ("Tools/Domain/domain_extender.ML") begin -defaultsort pcpo +default_sort pcpo subsection {* Casedist *}
--- a/src/HOLCF/FOCUS/Fstream.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Wed Apr 28 14:01:13 2010 +0200 @@ -12,7 +12,7 @@ imports "../ex/Stream" begin -defaultsort type +default_sort type types 'a fstream = "'a lift stream"
--- a/src/HOLCF/FOCUS/Fstreams.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/FOCUS/Fstreams.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ theory Fstreams imports "../ex/Stream" begin -defaultsort type +default_sort type types 'a fstream = "('a lift) stream"
--- a/src/HOLCF/Fix.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Fix.thy Wed Apr 28 14:01:13 2010 +0200 @@ -9,7 +9,7 @@ imports Cfun begin -defaultsort pcpo +default_sort pcpo subsection {* Iteration *}
--- a/src/HOLCF/Fixrec.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Fixrec.thy Wed Apr 28 14:01:13 2010 +0200 @@ -13,7 +13,7 @@ subsection {* Maybe monad type *} -defaultsort cpo +default_sort cpo pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set" by simp_all @@ -463,7 +463,7 @@ subsection {* Match functions for built-in types *} -defaultsort pcpo +default_sort pcpo definition match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
--- a/src/HOLCF/HOLCF.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/HOLCF.thy Wed Apr 28 14:01:13 2010 +0200 @@ -12,7 +12,7 @@ Sum_Cpo begin -defaultsort pcpo +default_sort pcpo text {* Legacy theorem names *}
--- a/src/HOLCF/IOA/Storage/Correctness.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/Storage/Correctness.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports SimCorrectness Spec Impl begin -defaultsort type +default_sort type definition sim_relation :: "((nat * bool) * (nat set * bool)) set" where
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Wed Apr 28 14:01:13 2010 +0200 @@ -9,7 +9,7 @@ uses ("automaton.ML") begin -defaultsort type +default_sort type definition cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Asig begin -defaultsort type +default_sort type types ('a, 's) transition = "'s * 'a * 's"
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports TLS begin -defaultsort type +default_sort type types ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Main begin -defaultsort type +default_sort type types 'a predicate = "'a => bool"
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Traces begin -defaultsort type +default_sort type definition move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Seq begin -defaultsort type +default_sort type types 'a Seq = "'a::type lift seq"
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports RefCorrectness begin -defaultsort type +default_sort type definition is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
--- a/src/HOLCF/IOA/meta_theory/TL.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/TL.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Pred Sequence begin -defaultsort type +default_sort type types 'a temporal = "'a Seq predicate"
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports IOA TL begin -defaultsort type +default_sort type types ('a, 's) ioa_temp = "('a option,'s)transition temporal"
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Sequence Automata begin -defaultsort type +default_sort type types ('a,'s)pairs = "('a * 's) Seq"
--- a/src/HOLCF/Lift.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Lift.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Discrete Up Countable begin -defaultsort type +default_sort type pcpodef 'a lift = "UNIV :: 'a discr u set" by simp_all
--- a/src/HOLCF/Product_Cpo.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Product_Cpo.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Adm begin -defaultsort cpo +default_sort cpo subsection {* Unit type is a pcpo *}
--- a/src/HOLCF/Representable.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Representable.thy Wed Apr 28 14:01:13 2010 +0200 @@ -42,7 +42,7 @@ @{term rep}, unless specified otherwise. *} -defaultsort rep +default_sort rep subsection {* Representations of types *}
--- a/src/HOLCF/Sprod.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Sprod.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Bifinite begin -defaultsort pcpo +default_sort pcpo subsection {* Definition of strict product type *}
--- a/src/HOLCF/Ssum.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Ssum.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Tr begin -defaultsort pcpo +default_sort pcpo subsection {* Definition of strict sum type *}
--- a/src/HOLCF/Tr.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Tr.thy Wed Apr 28 14:01:13 2010 +0200 @@ -62,7 +62,7 @@ subsection {* Case analysis *} -defaultsort pcpo +default_sort pcpo definition trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
--- a/src/HOLCF/Universal.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Universal.thy Wed Apr 28 14:01:13 2010 +0200 @@ -340,7 +340,7 @@ subsection {* Universality of \emph{udom} *} -defaultsort bifinite +default_sort bifinite subsubsection {* Choosing a maximal element from a finite set *}
--- a/src/HOLCF/Up.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/Up.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports Bifinite begin -defaultsort cpo +default_sort cpo subsection {* Definition of new type for lifting *}
--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports HOLCF begin -defaultsort rep +default_sort rep (*
--- a/src/HOLCF/ex/Letrec.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/ex/Letrec.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports HOLCF begin -defaultsort pcpo +default_sort pcpo definition CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
--- a/src/HOLCF/ex/New_Domain.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/ex/New_Domain.thy Wed Apr 28 14:01:13 2010 +0200 @@ -13,7 +13,7 @@ i.e. types in class @{text rep}. *} -defaultsort rep +default_sort rep text {* Provided that @{text rep} is the default sort, the @{text new_domain}
--- a/src/HOLCF/ex/Powerdomain_ex.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/HOLCF/ex/Powerdomain_ex.thy Wed Apr 28 14:01:13 2010 +0200 @@ -8,7 +8,7 @@ imports HOLCF begin -defaultsort bifinite +default_sort bifinite subsection {* Monadic sorting example *}
--- a/src/LCF/LCF.thy Wed Apr 28 13:29:40 2010 +0200 +++ b/src/LCF/LCF.thy Wed Apr 28 14:01:13 2010 +0200 @@ -14,7 +14,7 @@ subsection {* Natural Deduction Rules for LCF *} classes cpo < "term" -defaultsort cpo +default_sort cpo typedecl tr typedecl void
--- a/src/Pure/Isar/class.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/Isar/class.ML Wed Apr 28 14:01:13 2010 +0200 @@ -100,10 +100,14 @@ (* reading and processing class specifications *) -fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems = +fun prep_class_elems prep_decl thy sups raw_elems = let (* user space type system: only permits 'a type variable, improves towards 'a *) + val algebra = Sign.classes_of thy; + val inter_sort = curry (Sorts.inter_sort algebra); + val proto_base_sort = if null sups then Sign.defaultS thy + else fold inter_sort (map (base_sort thy) sups) []; val base_constraints = (map o apsnd) (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd) (these_operations thy sups); @@ -111,17 +115,17 @@ if v = Name.aT then T else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") | T => T); - fun singleton_fixate thy algebra Ts = + fun singleton_fixate Ts = let fun extract f = (fold o fold_atyps) f Ts []; val tfrees = extract (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I); val inferred_sort = extract - (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I); + (fn TVar (_, sort) => inter_sort sort | _ => I); val fixate_sort = if null tfrees then inferred_sort else case tfrees of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort) - then Sorts.inter_sort algebra (a_sort, inferred_sort) + then inter_sort a_sort inferred_sort else error ("Type inference imposes additional sort constraint " ^ Syntax.string_of_sort_global thy inferred_sort ^ " of type parameter " ^ Name.aT ^ " of sort " @@ -136,7 +140,7 @@ val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints #> redeclare_operations thy sups #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc - #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy)); + #> add_typ_check ~10 "singleton_fixate" singleton_fixate; val raw_supexpr = (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy @@ -183,11 +187,10 @@ then error ("Duplicate parameter(s) in superclasses: " ^ (commas o map quote o duplicates (op =)) raw_supparam_names) else (); - val given_basesort = fold inter_sort (map (base_sort thy) sups) []; (* infer types and base sort *) val (base_sort, supparam_names, supexpr, inferred_elems) = - prep_class_elems thy sups given_basesort raw_elems; + prep_class_elems thy sups raw_elems; val sup_sort = inter_sort base_sort sups; (* process elements as class specification *)
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Apr 28 14:01:13 2010 +0200 @@ -96,8 +96,9 @@ >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); val _ = - OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl - (P.sort >> (Toplevel.theory o Sign.add_defsort)); + OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables" + K.thy_decl + (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); (* types *)
--- a/src/Pure/Isar/local_theory.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/Isar/local_theory.ML Wed Apr 28 14:01:13 2010 +0200 @@ -40,6 +40,7 @@ local_theory -> (string * thm list) list * local_theory val declaration: bool -> declaration -> local_theory -> local_theory val syntax_declaration: bool -> declaration -> local_theory -> local_theory + val set_defsort: sort -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val class_alias: binding -> class -> local_theory -> local_theory @@ -183,7 +184,7 @@ fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy)); -(* basic operations *) +(* primitive operations *) fun operation f lthy = f (#operations (get_lthy lthy)) lthy; fun operation1 f x = operation (fn ops => f ops x); @@ -196,9 +197,16 @@ val declaration = checkpoint ooo operation2 #declaration; val syntax_declaration = checkpoint ooo operation2 #syntax_declaration; + + +(** basic derived operations **) + val notes = notes_kind ""; fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single; +fun set_defsort S = + syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (ProofContext.set_defsort S))); + (* notation *) @@ -224,6 +232,9 @@ val const_alias = alias Sign.const_alias ProofContext.const_alias; + +(** init and exit **) + (* init *) fun init group theory_prefix operations target =
--- a/src/Pure/Isar/proof_context.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Apr 28 14:01:13 2010 +0200 @@ -28,6 +28,7 @@ val full_name: Proof.context -> binding -> string val syn_of: Proof.context -> Syntax.syntax val tsig_of: Proof.context -> Type.tsig + val set_defsort: sort -> Proof.context -> Proof.context val default_sort: Proof.context -> indexname -> sort val consts_of: Proof.context -> Consts.T val the_const_constraint: Proof.context -> string -> typ @@ -178,17 +179,17 @@ datatype ctxt = Ctxt of - {mode: mode, (*inner syntax mode*) - naming: Name_Space.naming, (*local naming conventions*) - syntax: Local_Syntax.T, (*local syntax*) - tsigs: Type.tsig * Type.tsig, (*local/global type signature -- local name space only*) - consts: Consts.T * Consts.T, (*local/global consts -- local name space/abbrevs only*) - facts: Facts.T, (*local facts*) + {mode: mode, (*inner syntax mode*) + naming: Name_Space.naming, (*local naming conventions*) + syntax: Local_Syntax.T, (*local syntax*) + tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) + consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) + facts: Facts.T, (*local facts*) cases: (string * (Rule_Cases.T * bool)) list}; (*named case contexts*) -fun make_ctxt (mode, naming, syntax, tsigs, consts, facts, cases) = +fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) = Ctxt {mode = mode, naming = naming, syntax = syntax, - tsigs = tsigs, consts = consts, facts = facts, cases = cases}; + tsig = tsig, consts = consts, facts = facts, cases = cases}; val local_naming = Name_Space.default_naming |> Name_Space.add_path "local"; @@ -204,39 +205,39 @@ fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args); fun map_context f = - ContextData.map (fn Ctxt {mode, naming, syntax, tsigs, consts, facts, cases} => - make_ctxt (f (mode, naming, syntax, tsigs, consts, facts, cases))); + ContextData.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} => + make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases))); -fun set_mode mode = map_context (fn (_, naming, syntax, tsigs, consts, facts, cases) => - (mode, naming, syntax, tsigs, consts, facts, cases)); +fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) => + (mode, naming, syntax, tsig, consts, facts, cases)); fun map_mode f = - map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsigs, consts, facts, cases) => - (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsigs, consts, facts, cases)); + map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) => + (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases)); fun map_naming f = - map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) => - (mode, f naming, syntax, tsigs, consts, facts, cases)); + map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + (mode, f naming, syntax, tsig, consts, facts, cases)); fun map_syntax f = - map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) => - (mode, naming, f syntax, tsigs, consts, facts, cases)); + map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + (mode, naming, f syntax, tsig, consts, facts, cases)); -fun map_tsigs f = - map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) => - (mode, naming, syntax, f tsigs, consts, facts, cases)); +fun map_tsig f = + map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + (mode, naming, syntax, f tsig, consts, facts, cases)); fun map_consts f = - map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) => - (mode, naming, syntax, tsigs, f consts, facts, cases)); + map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + (mode, naming, syntax, tsig, f consts, facts, cases)); fun map_facts f = - map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) => - (mode, naming, syntax, tsigs, consts, f facts, cases)); + map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + (mode, naming, syntax, tsig, consts, f facts, cases)); fun map_cases f = - map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) => - (mode, naming, syntax, tsigs, consts, facts, f cases)); + map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) => + (mode, naming, syntax, tsig, consts, facts, f cases)); val get_mode = #mode o rep_context; val restore_mode = set_mode o get_mode; @@ -254,7 +255,8 @@ val set_syntax_mode = map_syntax o Local_Syntax.set_mode; val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; -val tsig_of = #1 o #tsigs o rep_context; +val tsig_of = #1 o #tsig o rep_context; +val set_defsort = map_tsig o apfst o Type.set_defsort; fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; val consts_of = #1 o #consts o rep_context; @@ -268,10 +270,10 @@ fun transfer_syntax thy ctxt = ctxt |> map_syntax (Local_Syntax.rebuild thy) |> - map_tsigs (fn tsigs as (local_tsig, global_tsig) => + map_tsig (fn tsig as (local_tsig, global_tsig) => let val thy_tsig = Sign.tsig_of thy in - if Type.eq_tsig (thy_tsig, global_tsig) then tsigs - else (Type.merge_tsigs (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig) + if Type.eq_tsig (thy_tsig, global_tsig) then tsig + else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig) end) |> map_consts (fn consts as (local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in @@ -608,22 +610,19 @@ (* types *) -fun get_sort ctxt raw_env = +fun get_sort ctxt raw_text = let - val thy = theory_of ctxt; 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 text = distinct (op =) (map (apsnd (Type.minimize_sort tsig)) raw_text); val _ = - (case duplicates (eq_fst (op =)) env of + (case duplicates (eq_fst (op =)) text 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 + (case AList.lookup (op =) text xi of NONE => NONE | SOME S => if S = dummyS then NONE else SOME S); @@ -637,7 +636,7 @@ else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^ " for type variable " ^ quote (Term.string_of_vname' xi))); - in Sign.minimize_sort thy o get end; + 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)); @@ -737,11 +736,10 @@ fun parse_sort ctxt text = let - val thy = theory_of ctxt; val (syms, pos) = Syntax.parse_token Markup.sort text; val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos) handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos) - in Sign.minimize_sort thy S end; + in Type.minimize_sort (tsig_of ctxt) S end; fun parse_typ ctxt text = let @@ -1144,8 +1142,8 @@ (* aliases *) -fun class_alias b c ctxt = (map_tsigs o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; -fun type_alias b c ctxt = (map_tsigs o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; +fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; +fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
--- a/src/Pure/Proof/proof_syntax.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Wed Apr 28 14:01:13 2010 +0200 @@ -45,7 +45,7 @@ thy |> Theory.copy |> Sign.root_path - |> Sign.add_defsort_i [] + |> Sign.set_defsort [] |> Sign.add_types [(Binding.name "proof", 0, NoSyn)] |> fold (snd oo Sign.declare_const) [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
--- a/src/Pure/Syntax/type_ext.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/Syntax/type_ext.ML Wed Apr 28 14:01:13 2010 +0200 @@ -110,8 +110,7 @@ fun decode_term get_sort map_const map_free tm = let - val sort_env = term_sorts tm; - val decodeT = typ_of_term (get_sort sort_env); + val decodeT = typ_of_term (get_sort (term_sorts tm)); fun decode (Const ("_constrain", _) $ t $ typ) = type_constraint (decodeT typ) (decode t)
--- a/src/Pure/sign.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/sign.ML Wed Apr 28 14:01:13 2010 +0200 @@ -25,6 +25,7 @@ val super_classes: theory -> class -> class list val minimize_sort: theory -> sort -> sort val complete_sort: theory -> sort -> sort + val set_defsort: sort -> theory -> theory val defaultS: theory -> sort val subsort: theory -> sort * sort -> bool val of_sort: theory -> typ * sort -> bool @@ -68,8 +69,6 @@ val cert_prop: theory -> term -> term val no_frees: Pretty.pp -> term -> term val no_vars: Pretty.pp -> term -> term - val add_defsort: string -> theory -> theory - 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_type_abbrev: binding * string list * typ -> theory -> theory @@ -156,7 +155,7 @@ val naming = Name_Space.default_naming; val syn = Syntax.merge_syntaxes syn1 syn2; - val tsig = Type.merge_tsigs pp (tsig1, tsig2); + val tsig = Type.merge_tsig pp (tsig1, tsig2); val consts = Consts.merge (consts1, consts2); in make_sign (naming, syn, tsig, consts) end; ); @@ -198,6 +197,7 @@ val minimize_sort = Sorts.minimize_sort o classes_of; val complete_sort = Sorts.complete_sort o classes_of; +val set_defsort = map_tsig o Type.set_defsort; val defaultS = Type.defaultS o tsig_of; val subsort = Type.subsort o tsig_of; val of_sort = Type.of_sort o tsig_of; @@ -334,15 +334,6 @@ (** signature extension functions **) (*exception ERROR/TYPE*) -(* add default sort *) - -fun gen_add_defsort prep_sort s thy = - thy |> map_tsig (Type.set_defsort (prep_sort thy s)); - -val add_defsort = gen_add_defsort Syntax.read_sort_global; -val add_defsort_i = gen_add_defsort certify_sort; - - (* add type constructors *) fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
--- a/src/Pure/type.ML Wed Apr 28 13:29:40 2010 +0200 +++ b/src/Pure/type.ML Wed Apr 28 14:01:13 2010 +0200 @@ -32,6 +32,7 @@ val inter_sort: tsig -> sort * sort -> sort val cert_class: tsig -> class -> class val cert_sort: tsig -> sort -> sort + val minimize_sort: tsig -> sort -> sort val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list type mode val mode_default: mode @@ -88,7 +89,7 @@ val hide_type: bool -> string -> tsig -> tsig val add_arity: Pretty.pp -> arity -> tsig -> tsig val add_classrel: Pretty.pp -> class * class -> tsig -> tsig - val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig + val merge_tsig: Pretty.pp -> tsig * tsig -> tsig end; structure Type: TYPE = @@ -159,6 +160,7 @@ fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes); fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes); +fun minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes); fun witness_sorts (TSig {classes, log_types, ...}) = Sorts.witness_sorts (#2 classes) log_types; @@ -619,7 +621,7 @@ (* merge type signatures *) -fun merge_tsigs pp (tsig1, tsig2) = +fun merge_tsig pp (tsig1, tsig2) = let val (TSig {classes = (space1, classes1), default = default1, types = types1, log_types = _}) = tsig1;