--- a/NEWS Mon Feb 10 21:51:15 2014 +0100
+++ b/NEWS Mon Feb 10 23:24:44 2014 +0100
@@ -44,6 +44,16 @@
*** Pure ***
+* Low-level type-class commands 'classes', 'classrel', 'arities' have
+been discontinued to avoid the danger of non-trivial axiomatization
+that is not immediately visible. INCOMPATIBILITY, use regular
+'instance' with proof. The required OFCLASS(...) theorem might be
+postulated via 'axiomatization' beforehand, or the proof finished
+trivially if the underlying class definition is made vacuous (without
+any assumptions). See also Isabelle/ML operations
+Axclass.axiomatize_class, Axclass.axiomatize_classrel,
+Axclass.axiomatize_arity.
+
* Attributes "where" and "of" allow an optional context of local
variables ('for' declaration): these variables become schematic in the
instantiated theorem.
--- a/etc/isar-keywords-ZF.el Mon Feb 10 21:51:15 2014 +0100
+++ b/etc/isar-keywords-ZF.el Mon Feb 10 23:24:44 2014 +0100
@@ -24,7 +24,6 @@
"also"
"apply"
"apply_end"
- "arities"
"assume"
"attribute_setup"
"axiomatization"
@@ -37,8 +36,6 @@
"chapter"
"class"
"class_deps"
- "classes"
- "classrel"
"codatatype"
"code_datatype"
"coinductive"
@@ -346,13 +343,10 @@
'("ML"
"ML_file"
"abbreviation"
- "arities"
"attribute_setup"
"axiomatization"
"bundle"
"class"
- "classes"
- "classrel"
"codatatype"
"code_datatype"
"coinductive"
--- a/etc/isar-keywords.el Mon Feb 10 21:51:15 2014 +0100
+++ b/etc/isar-keywords.el Mon Feb 10 23:24:44 2014 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-FP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -25,7 +25,6 @@
"also"
"apply"
"apply_end"
- "arities"
"assume"
"atom_decl"
"attribute_setup"
@@ -45,24 +44,16 @@
"chapter"
"class"
"class_deps"
- "classes"
- "classrel"
"codatatype"
- "code_class"
- "code_const"
"code_datatype"
"code_deps"
"code_identifier"
- "code_include"
- "code_instance"
- "code_modulename"
"code_monad"
"code_pred"
"code_printing"
"code_reflect"
"code_reserved"
"code_thms"
- "code_type"
"coinductive"
"coinductive_set"
"commit"
@@ -487,7 +478,6 @@
"ML_file"
"abbreviation"
"adhoc_overloading"
- "arities"
"atom_decl"
"attribute_setup"
"axiomatization"
@@ -496,21 +486,13 @@
"bundle"
"case_of_simps"
"class"
- "classes"
- "classrel"
"codatatype"
- "code_class"
- "code_const"
"code_datatype"
"code_identifier"
- "code_include"
- "code_instance"
- "code_modulename"
"code_monad"
"code_printing"
"code_reflect"
"code_reserved"
- "code_type"
"coinductive"
"coinductive_set"
"consts"
--- a/src/CCL/CCL.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/CCL/CCL.thy Mon Feb 10 23:24:44 2014 +0100
@@ -16,13 +16,13 @@
being defined which contains only executable terms.
*}
-classes prog < "term"
+class prog = "term"
default_sort prog
-arities "fun" :: (prog, prog) prog
+instance "fun" :: (prog, prog) prog ..
typedecl i
-arities i :: prog
+instance i :: prog ..
consts
--- a/src/CCL/Set.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/CCL/Set.thy Mon Feb 10 23:24:44 2014 +0100
@@ -7,7 +7,7 @@
declare [[eta_contract]]
typedecl 'a set
-arities set :: ("term") "term"
+instance set :: ("term") "term" ..
consts
Collect :: "['a => o] => 'a set" (*comprehension*)
--- a/src/Doc/Classes/Classes.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Doc/Classes/Classes.thy Mon Feb 10 23:24:44 2014 +0100
@@ -356,19 +356,14 @@
consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
text {*
- \noindent The connection to the type system is done by means
- of a primitive type class
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-classes %quote idem < type
-(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
-setup %invisible {* Sign.parent_path *}(*>*)
-
-text {* \noindent together with a corresponding interpretation: *}
+ \noindent The connection to the type system is done by means of a
+ primitive type class @{text "idem"}, together with a corresponding
+ interpretation:
+*}
interpretation %quote idem_class:
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
-(*<*)proof qed (rule idem)(*>*)
+(*<*)sorry(*>*)
text {*
\noindent This gives you the full power of the Isabelle module system;
--- a/src/Doc/IsarRef/Spec.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy Mon Feb 10 23:24:44 2014 +0100
@@ -1085,36 +1085,19 @@
section {* Primitive specification elements *}
-subsection {* Type classes and sorts \label{sec:classes} *}
+subsection {* Sorts *}
text {*
\begin{matharray}{rcll}
- @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
@{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}
@{rail \<open>
- @@{command classes} (@{syntax classdecl} +)
- ;
- @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
- ;
@@{command default_sort} @{syntax sort}
\<close>}
\begin{description}
- \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
- @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
- Isabelle implicitly maintains the transitive closure of the class
- hierarchy. Cyclic class structures are not permitted.
-
- \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
- relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
- This is done axiomatically! The @{command_ref "subclass"} and
- @{command_ref "instance"} commands (see \secref{sec:class}) provide
- a way to introduce proven class relations.
-
\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).
@@ -1138,15 +1121,12 @@
\begin{matharray}{rcll}
@{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
@{rail \<open>
@@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
;
@@{command typedecl} @{syntax typespec} @{syntax mixfix}?
- ;
- @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
\<close>}
\begin{description}
@@ -1161,14 +1141,7 @@
\item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
type constructor @{text t}. If the object-logic defines a base sort
@{text s}, then the constructor is declared to operate on that, via
- the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
- s)s"}.
-
- \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
- Isabelle's order-sorted signature of types by new type constructor
- arities. This is done axiomatically! The @{command_ref "instantiation"}
- target (see \secref{sec:class}) provides a way to introduce
- proven type arities.
+ the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
\end{description}
*}
--- a/src/Doc/ROOT Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Doc/ROOT Mon Feb 10 23:24:44 2014 +0100
@@ -1,7 +1,7 @@
chapter Doc
session Classes (doc) in "Classes" = HOL +
- options [document_variants = "classes"]
+ options [document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
theories Classes
files
--- a/src/FOL/IFOL.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/IFOL.thy Mon Feb 10 23:24:44 2014 +0100
@@ -24,7 +24,7 @@
setup Pure_Thy.old_appl_syntax_setup
-classes "term"
+class "term"
default_sort "term"
typedecl o
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Feb 10 23:24:44 2014 +0100
@@ -8,7 +8,9 @@
imports FOL
begin
-typedecl int arities int :: "term"
+typedecl int
+instance int :: "term" ..
+
consts plus :: "int => int => int" (infixl "+" 60)
zero :: int ("0")
minus :: "int => int" ("- _")
--- a/src/FOL/ex/Nat.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Nat.thy Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
begin
typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
axiomatization
Zero :: nat ("0") and
--- a/src/FOL/ex/Natural_Numbers.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy Mon Feb 10 23:24:44 2014 +0100
@@ -14,7 +14,7 @@
*}
typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
axiomatization
Zero :: nat ("0") and
--- a/src/FOL/ex/Prolog.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOL/ex/Prolog.thy Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
begin
typedecl 'a list
-arities list :: ("term") "term"
+instance list :: ("term") "term" ..
axiomatization
Nil :: "'a list" and
--- a/src/FOLP/IFOLP.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOLP/IFOLP.thy Mon Feb 10 23:24:44 2014 +0100
@@ -13,7 +13,7 @@
setup Pure_Thy.old_appl_syntax_setup
-classes "term"
+class "term"
default_sort "term"
typedecl p
--- a/src/FOLP/ex/Nat.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/FOLP/ex/Nat.thy Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
begin
typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
axiomatization
Zero :: nat ("0") and
--- a/src/HOL/HOL.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/HOL.thy Mon Feb 10 23:24:44 2014 +0100
@@ -45,13 +45,15 @@
subsubsection {* Core syntax *}
-classes type
+setup {* Axclass.axiomatize_class (@{binding type}, []) *}
default_sort type
setup {* Object_Logic.add_base_sort @{sort type} *}
-arities
- "fun" :: (type, type) type
- itself :: (type) type
+axiomatization where fun_arity: "OFCLASS('a \<Rightarrow> 'b, type_class)"
+instance "fun" :: (type, type) type by (rule fun_arity)
+
+axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
+instance itself :: (type) type by (rule itself_arity)
typedecl bool
--- a/src/HOL/HOLCF/ex/Focus_ex.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy Mon Feb 10 23:24:44 2014 +0100
@@ -103,7 +103,8 @@
begin
typedecl ('a, 'b) tc
-arities tc:: (pcpo, pcpo) pcpo
+axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)"
+instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)
axiomatization
Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
--- a/src/HOL/Statespace/DistinctTreeProver.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Mon Feb 10 23:24:44 2014 +0100
@@ -632,82 +632,4 @@
ML_file "distinct_tree_prover.ML"
-(* Uncomment for profiling or debugging *)
-(*
-ML {*
-(*
-val nums = (0 upto 10000);
-val nums' = (200 upto 3000);
-*)
-val nums = (0 upto 10000);
-val nums' = (0 upto 3000);
-val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
-
-val consts = sort Term_Ord.fast_term_ord
- (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort Term_Ord.fast_term_ord
- (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
-
-val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
-
-
-val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
-
-
-val dist =
- HOLogic.Trueprop$
- (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
-
-val dist' =
- HOLogic.Trueprop$
- (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
-
-val da = Unsynchronized.ref refl;
-
-*}
-
-setup {*
-Theory.add_consts_i const_decls
-#> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy
- in (da := thm; thy') end)
-*}
-
-
-ML {*
- val ct' = cterm_of @{theory} t';
-*}
-
-ML {*
- timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);()))
-*}
-
-(* 590 s *)
-
-ML {*
-
-
-val p1 =
- the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
-val p2 =
- the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
-*}
-
-
-ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
- p1
- p2)*}
-
-
-ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
-
-
-
-
-ML {*
-val cdist' = cterm_of @{theory} dist';
-DistinctTreeProver.distinct_implProver (!da) cdist';
-*}
-
-*)
-
end
--- a/src/HOL/TLA/Action.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Action.thy Mon Feb 10 23:24:44 2014 +0100
@@ -15,7 +15,7 @@
type_synonym 'a trfun = "(state * state) => 'a"
type_synonym action = "bool trfun"
-arities prod :: (world, world) world
+instance prod :: (world, world) world ..
consts
(** abstract syntax **)
--- a/src/HOL/TLA/Init.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Init.thy Mon Feb 10 23:24:44 2014 +0100
@@ -12,7 +12,7 @@
begin
typedecl behavior
-arities behavior :: world
+instance behavior :: world ..
type_synonym temporal = "behavior form"
--- a/src/HOL/TLA/Intensional.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy Mon Feb 10 23:24:44 2014 +0100
@@ -10,8 +10,7 @@
imports Main
begin
-classes world
-classrel world < type
+class world
(** abstract syntax **)
--- a/src/HOL/TLA/Stfun.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/TLA/Stfun.thy Mon Feb 10 23:24:44 2014 +0100
@@ -10,8 +10,7 @@
begin
typedecl state
-
-arities state :: world
+instance state :: world ..
type_synonym 'a stfun = "state => 'a"
type_synonym stpred = "bool stfun"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Feb 10 23:24:44 2014 +0100
@@ -285,7 +285,7 @@
|> Sign.add_consts_i
(map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
dst_preds)
- |> fold_map Specification.axiom
+ |> fold_map Specification.axiom (* FIXME !?!?!?! *)
(map_index (fn (j, (predname, t)) =>
((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
(maps (uncurry (map o pair)) (prednames ~~ intr_tss)))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Feb 10 23:24:44 2014 +0100
@@ -118,8 +118,9 @@
val new_defs = map mk_def srs
val (definition, thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> fold_map Specification.axiom (map_index
- (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
+ |> fold_map Specification.axiom (* FIXME !?!?!?! *)
+ (map_index (fn (i, t) =>
+ ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
in
(lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
end
--- a/src/HOL/ex/Higher_Order_Logic.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy Mon Feb 10 23:24:44 2014 +0100
@@ -18,13 +18,12 @@
subsection {* Pure Logic *}
-classes type
+class type
default_sort type
typedecl o
-arities
- o :: type
- "fun" :: (type, type) type
+instance o :: type ..
+instance "fun" :: (type, type) type ..
subsubsection {* Basic logical connectives *}
--- a/src/LCF/LCF.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/LCF/LCF.thy Mon Feb 10 23:24:44 2014 +0100
@@ -13,7 +13,7 @@
subsection {* Natural Deduction Rules for LCF *}
-classes cpo < "term"
+class cpo = "term"
default_sort cpo
typedecl tr
@@ -21,12 +21,11 @@
typedecl ('a,'b) prod (infixl "*" 6)
typedecl ('a,'b) sum (infixl "+" 5)
-arities
- "fun" :: (cpo, cpo) cpo
- prod :: (cpo, cpo) cpo
- sum :: (cpo, cpo) cpo
- tr :: cpo
- void :: cpo
+instance "fun" :: (cpo, cpo) cpo ..
+instance prod :: (cpo, cpo) cpo ..
+instance sum :: (cpo, cpo) cpo ..
+instance tr :: cpo ..
+instance void :: cpo ..
consts
UU :: "'a"
--- a/src/Pure/General/output.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/General/output.ML Mon Feb 10 23:24:44 2014 +0100
@@ -25,19 +25,6 @@
val physical_stderr: output -> unit
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
- structure Internal:
- sig
- val writeln_fn: (output -> unit) Unsynchronized.ref
- val urgent_message_fn: (output -> unit) Unsynchronized.ref
- val tracing_fn: (output -> unit) Unsynchronized.ref
- val warning_fn: (output -> unit) Unsynchronized.ref
- val error_message_fn: (serial * output -> unit) Unsynchronized.ref
- val prompt_fn: (output -> unit) Unsynchronized.ref
- val status_fn: (output -> unit) Unsynchronized.ref
- val report_fn: (output -> unit) Unsynchronized.ref
- val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
- val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
- end
val urgent_message: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
@@ -49,7 +36,22 @@
val try_protocol_message: Properties.T -> string -> unit
end;
-structure Output: OUTPUT =
+signature PRIVATE_OUTPUT =
+sig
+ include OUTPUT
+ val writeln_fn: (output -> unit) Unsynchronized.ref
+ val urgent_message_fn: (output -> unit) Unsynchronized.ref
+ val tracing_fn: (output -> unit) Unsynchronized.ref
+ val warning_fn: (output -> unit) Unsynchronized.ref
+ val error_message_fn: (serial * output -> unit) Unsynchronized.ref
+ val prompt_fn: (output -> unit) Unsynchronized.ref
+ val status_fn: (output -> unit) Unsynchronized.ref
+ val report_fn: (output -> unit) Unsynchronized.ref
+ val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+ val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+end;
+
+structure Output: PRIVATE_OUTPUT =
struct
(** print modes **)
@@ -92,33 +94,30 @@
exception Protocol_Message of Properties.T;
-structure Internal =
-struct
- val writeln_fn = Unsynchronized.ref physical_writeln;
- val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*)
- val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
- val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
- val error_message_fn =
- Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
- val prompt_fn = Unsynchronized.ref physical_stdout;
- val status_fn = Unsynchronized.ref (fn _: output => ());
- val report_fn = Unsynchronized.ref (fn _: output => ());
- val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
- val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
- Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
-end;
+val writeln_fn = Unsynchronized.ref physical_writeln;
+val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*)
+val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
+val error_message_fn =
+ Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
+val prompt_fn = Unsynchronized.ref physical_stdout;
+val status_fn = Unsynchronized.ref (fn _: output => ());
+val report_fn = Unsynchronized.ref (fn _: output => ());
+val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
+val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+ Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
-fun writeln s = ! Internal.writeln_fn (output s);
-fun urgent_message s = ! Internal.urgent_message_fn (output s); (*Proof General legacy*)
-fun tracing s = ! Internal.tracing_fn (output s);
-fun warning s = ! Internal.warning_fn (output s);
-fun error_message' (i, s) = ! Internal.error_message_fn (i, output s);
+fun writeln s = ! writeln_fn (output s);
+fun urgent_message s = ! urgent_message_fn (output s); (*Proof General legacy*)
+fun tracing s = ! tracing_fn (output s);
+fun warning s = ! warning_fn (output s);
+fun error_message' (i, s) = ! error_message_fn (i, output s);
fun error_message s = error_message' (serial (), s);
-fun prompt s = ! Internal.prompt_fn (output s);
-fun status s = ! Internal.status_fn (output s);
-fun report s = ! Internal.report_fn (output s);
-fun result props s = ! Internal.result_fn props (output s);
-fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
+fun prompt s = ! prompt_fn (output s);
+fun status s = ! status_fn (output s);
+fun report s = ! report_fn (output s);
+fun result props s = ! result_fn props (output s);
+fun protocol_message props s = ! protocol_message_fn props (output s);
fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Feb 10 23:24:44 2014 +0100
@@ -73,19 +73,7 @@
(** theory commands **)
-(* classes and sorts *)
-
-val _ =
- Outer_Syntax.command @{command_spec "classes"} "declare type classes"
- (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
- Parse.!!! (Parse.list1 Parse.class)) [])
- >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
- (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
- |-- Parse.!!! Parse.class))
- >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
+(* sorts *)
val _ =
Outer_Syntax.local_theory @{command_spec "default_sort"}
@@ -111,10 +99,6 @@
"declare syntactic type constructors (grammar nonterminal symbols)"
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
-val _ =
- Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
- (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
-
(* consts and syntax *)
--- a/src/Pure/Pure.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Pure.thy Mon Feb 10 23:24:44 2014 +0100
@@ -25,10 +25,9 @@
and "subsect" :: prf_heading3 % "proof"
and "subsubsect" :: prf_heading4 % "proof"
and "txt" "txt_raw" :: prf_decl % "proof"
- and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
- "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
- "translations" "no_translations" "defs" "definition"
- "abbreviation" "type_notation" "no_type_notation" "notation"
+ and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment"
+ "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
+ "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "ML" :: thy_decl % "ML"
--- a/src/Pure/ROOT.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/ROOT.ML Mon Feb 10 23:24:44 2014 +0100
@@ -306,6 +306,8 @@
use "Tools/named_thms.ML";
use "Tools/proof_general.ML";
+structure Output: OUTPUT = Output; (*seal system channels!*)
+
(* ML toplevel pretty printing *)
--- a/src/Pure/System/isabelle_process.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML Mon Feb 10 23:24:44 2014 +0100
@@ -111,19 +111,19 @@
message name
(fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
in
- Output.Internal.status_fn := standard_message [] Markup.statusN;
- Output.Internal.report_fn := standard_message [] Markup.reportN;
- Output.Internal.result_fn :=
+ Output.status_fn := standard_message [] Markup.statusN;
+ Output.report_fn := standard_message [] Markup.reportN;
+ Output.result_fn :=
(fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
- Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
- Output.Internal.tracing_fn :=
+ Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
+ Output.tracing_fn :=
(fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
- Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
- Output.Internal.error_message_fn :=
+ Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
+ Output.error_message_fn :=
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
- Output.Internal.protocol_message_fn := message Markup.protocolN;
- Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
- Output.Internal.prompt_fn := ignore;
+ Output.protocol_message_fn := message Markup.protocolN;
+ Output.urgent_message_fn := ! Output.writeln_fn;
+ Output.prompt_fn := ignore;
message Markup.initN [] (Session.welcome ());
msg_channel
end;
--- a/src/Pure/System/isar.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/System/isar.ML Mon Feb 10 23:24:44 2014 +0100
@@ -157,7 +157,7 @@
(Context.set_thread_data NONE;
Multithreading.max_threads_update (Options.default_int "threads");
if do_init then init () else ();
- Output.Internal.protocol_message_fn := protocol_message;
+ Output.protocol_message_fn := protocol_message;
if welcome then writeln (Session.welcome ()) else ();
uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
--- a/src/Pure/System/session.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/System/session.ML Mon Feb 10 23:24:44 2014 +0100
@@ -57,6 +57,7 @@
Outer_Syntax.check_syntax ();
Future.shutdown ();
Event_Timer.shutdown ();
+ Future.shutdown ();
session_finished := true);
--- a/src/Pure/Tools/build.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Tools/build.ML Mon Feb 10 23:24:44 2014 +0100
@@ -166,7 +166,7 @@
theories |>
(List.app (use_theories_condition last_timing)
|> session_timing name verbose
- |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
+ |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
|> Multithreading.max_threads_setmp (Options.int options "threads")
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
--- a/src/Pure/Tools/proof_general.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/Tools/proof_general.ML Mon Feb 10 23:24:44 2014 +0100
@@ -264,14 +264,14 @@
| s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
fun setup_messages () =
- (Output.Internal.writeln_fn := message "" "" "";
- Output.Internal.status_fn := (fn _ => ());
- Output.Internal.report_fn := (fn _ => ());
- Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
- Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
- Output.Internal.warning_fn := message (special "K") (special "L") "### ";
- Output.Internal.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
- Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
+ (Output.writeln_fn := message "" "" "";
+ Output.status_fn := (fn _ => ());
+ Output.report_fn := (fn _ => ());
+ Output.urgent_message_fn := message (special "I") (special "J") "";
+ Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+ Output.warning_fn := message (special "K") (special "L") "### ";
+ Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
+ Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
(* notification *)
--- a/src/Pure/axclass.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/axclass.ML Mon Feb 10 23:24:44 2014 +0100
@@ -30,12 +30,9 @@
val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory
val define_class: binding * class list -> string list ->
(Thm.binding * term list) list -> theory -> class * theory
+ val axiomatize_classrel: (class * class) list -> theory -> theory
+ val axiomatize_arity: arity -> theory -> theory
val axiomatize_class: binding * class list -> theory -> theory
- val axiomatize_class_cmd: binding * xstring list -> theory -> theory
- val axiomatize_classrel: (class * class) list -> theory -> theory
- val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
- val axiomatize_arity: arity -> theory -> theory
- val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
end;
structure Axclass: AXCLASS =
@@ -596,38 +593,30 @@
|-> fold (add o Drule.export_without_context o snd)
end;
-fun ax_classrel prep =
- axiomatize (map o prep) (map Logic.mk_classrel)
- (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
-
-fun ax_arity prep =
- axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
- (map (prefix arity_prefix) o Logic.name_arities) add_arity;
-
fun class_const c =
(Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
-fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
+in
+
+val axiomatize_classrel =
+ axiomatize (map o cert_classrel) (map Logic.mk_classrel)
+ (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
+
+val axiomatize_arity =
+ axiomatize (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
+ (map (prefix arity_prefix) o Logic.name_arities) add_arity;
+
+fun axiomatize_class (bclass, raw_super) thy =
let
val class = Sign.full_name thy bclass;
- val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
+ val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
in
thy
|> Sign.primitive_class (bclass, super)
- |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
+ |> axiomatize_classrel (map (fn c => (class, c)) super)
|> Theory.add_deps_global "" (class_const class) (map class_const super)
end;
-in
-
-val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd =
- ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
-val axiomatize_classrel = ax_classrel cert_classrel;
-val axiomatize_classrel_cmd = ax_classrel read_classrel;
-val axiomatize_arity = ax_arity Proof_Context.cert_arity;
-val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
-
end;
end;
--- a/src/Pure/raw_simplifier.ML Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Mon Feb 10 23:24:44 2014 +0100
@@ -375,11 +375,7 @@
fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
-fun put_simpset ss = map_simpset (fn context_ss =>
- let
- val Simpset ({rules, prems, ...}, ss2) = ss; (* FIXME prems from context (!?) *)
- val Simpset ({depth, ...}, _) = context_ss;
- in Simpset (make_ss1 (rules, prems, depth), ss2) end);
+fun put_simpset ss = map_simpset (K ss);
val empty_simpset = put_simpset empty_ss;
--- a/src/Sequents/LK/Nat.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Sequents/LK/Nat.thy Mon Feb 10 23:24:44 2014 +0100
@@ -10,7 +10,7 @@
begin
typedecl nat
-arities nat :: "term"
+instance nat :: "term" ..
axiomatization
Zero :: nat ("0") and
--- a/src/Sequents/LK0.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/Sequents/LK0.thy Mon Feb 10 23:24:44 2014 +0100
@@ -12,7 +12,7 @@
imports Sequents
begin
-classes "term"
+class "term"
default_sort "term"
consts
--- a/src/ZF/ZF.thy Mon Feb 10 21:51:15 2014 +0100
+++ b/src/ZF/ZF.thy Mon Feb 10 23:24:44 2014 +0100
@@ -12,7 +12,7 @@
declare [[eta_contract = false]]
typedecl i
-arities i :: "term"
+instance i :: "term" ..
axiomatization
zero :: "i" ("0") --{*the empty set*} and