# HG changeset patch # User haftmann # Date 1232577623 -3600 # Node ID 564ea783ace87fedcba4b65ca859b11fdd0c447a # Parent 4f980382962525a54e95798d73af12f069597dcc no base sort in class import diff -r 4f9803829625 -r 564ea783ace8 NEWS --- a/NEWS Wed Jan 21 18:37:44 2009 +0100 +++ b/NEWS Wed Jan 21 23:40:23 2009 +0100 @@ -66,6 +66,12 @@ *** Pure *** +* Class declaration: sc. "base sort" must not be given in import list +any longer but is inferred from the specification. Particularly in HOL, +write + + class foo = ... instead of class foo = type + ... + * Type Binding.T gradually replaces formerly used type bstring for names to be bound. Name space interface for declarations has been simplified: diff -r 4f9803829625 -r 564ea783ace8 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/HOL.thy Wed Jan 21 23:40:23 2009 +0100 @@ -208,34 +208,34 @@ subsubsection {* Generic classes and algebraic operations *} -class default = type + +class default = fixes default :: 'a -class zero = type + +class zero = fixes zero :: 'a ("0") -class one = type + +class one = fixes one :: 'a ("1") hide (open) const zero one -class plus = type + +class plus = fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) -class minus = type + +class minus = fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) -class uminus = type + +class uminus = fixes uminus :: "'a \ 'a" ("- _" [81] 80) -class times = type + +class times = fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) -class inverse = type + +class inverse = fixes inverse :: "'a \ 'a" and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) -class abs = type + +class abs = fixes abs :: "'a \ 'a" begin @@ -247,10 +247,10 @@ end -class sgn = type + +class sgn = fixes sgn :: "'a \ 'a" -class ord = type + +class ord = fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" begin @@ -1675,7 +1675,7 @@ text {* Equality *} -class eq = type + +class eq = fixes eq :: "'a \ 'a \ bool" assumes eq_equals: "eq x y \ x = y" begin diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Int.thy Wed Jan 21 23:40:23 2009 +0100 @@ -599,7 +599,7 @@ Bit1 :: "int \ int" where [code del]: "Bit1 k = 1 + k + k" -class number = type + -- {* for numeric types: nat, int, real, \dots *} +class number = -- {* for numeric types: nat, int, real, \dots *} fixes number_of :: "int \ 'a" use "Tools/numeral.ML" diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Library/Eval_Witness.thy --- a/src/HOL/Library/Eval_Witness.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Library/Eval_Witness.thy Wed Jan 21 23:40:23 2009 +0100 @@ -32,7 +32,7 @@ with the oracle. *} -class ml_equiv = type +class ml_equiv text {* Instances of @{text "ml_equiv"} should only be declared for those types, diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Library/Quotient.thy --- a/src/HOL/Library/Quotient.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Library/Quotient.thy Wed Jan 21 23:40:23 2009 +0100 @@ -21,7 +21,7 @@ "\ :: 'a => 'a => bool"}. *} -class eqv = type + +class eqv = fixes eqv :: "'a \ 'a \ bool" (infixl "\" 50) class equiv = eqv + diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Nat.thy Wed Jan 21 23:40:23 2009 +0100 @@ -1515,7 +1515,7 @@ subsection {* size of a datatype value *} -class size = type + +class size = fixes size :: "'a \ nat" -- {* see further theory @{text Wellfounded} *} end diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Nominal/Examples/W.thy --- a/src/HOL/Nominal/Examples/W.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Nominal/Examples/W.thy Wed Jan 21 23:40:23 2009 +0100 @@ -49,7 +49,7 @@ text {* free type variables *} -class ftv = type + +class ftv = fixes ftv :: "'a \ tvar list" instantiation * :: (ftv, ftv) ftv diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Parity.thy Wed Jan 21 23:40:23 2009 +0100 @@ -8,7 +8,7 @@ imports Plain Presburger begin -class even_odd = type + +class even_odd = fixes even :: "'a \ bool" abbreviation diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Power.thy Wed Jan 21 23:40:23 2009 +0100 @@ -11,7 +11,7 @@ imports Nat begin -class power = type + +class power = fixes power :: "'a \ nat \ 'a" (infixr "^" 80) subsection{*Powers for Arbitrary Monoids*} diff -r 4f9803829625 -r 564ea783ace8 src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/RealVector.thy Wed Jan 21 23:40:23 2009 +0100 @@ -124,7 +124,7 @@ subsection {* Real vector spaces *} -class scaleR = type + +class scaleR = fixes scaleR :: "real \ 'a \ 'a" (infixr "*\<^sub>R" 75) begin @@ -418,7 +418,7 @@ subsection {* Real normed vector spaces *} -class norm = type + +class norm = fixes norm :: "'a \ real" instantiation real :: norm diff -r 4f9803829625 -r 564ea783ace8 src/HOL/SizeChange/Kleene_Algebras.thy --- a/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 23:40:23 2009 +0100 @@ -11,7 +11,7 @@ text {* A type class of kleene algebras *} -class star = type + +class star = fixes star :: "'a \ 'a" class idem_add = ab_semigroup_add + diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Typedef.thy Wed Jan 21 23:40:23 2009 +0100 @@ -123,7 +123,7 @@ text {* This class is just a workaround for classes without parameters; it shall disappear as soon as possible. *} -class itself = type + +class itself = fixes itself :: "'a itself" setup {* diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Word/BitSyntax.thy --- a/src/HOL/Word/BitSyntax.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Word/BitSyntax.thy Wed Jan 21 23:40:23 2009 +0100 @@ -12,7 +12,7 @@ imports BinGeneral begin -class bit = type + +class bit = fixes bitNOT :: "'a \ 'a" ("NOT _" [70] 71) and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) and bitOR :: "'a \ 'a \ 'a" (infixr "OR" 59) diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Word/Size.thy --- a/src/HOL/Word/Size.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Word/Size.thy Wed Jan 21 23:40:23 2009 +0100 @@ -18,7 +18,7 @@ some duplication with the definitions in @{text "Numeral_Type"}. *} -class len0 = type + +class len0 = fixes len_of :: "'a itself \ nat" text {* diff -r 4f9803829625 -r 564ea783ace8 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOLCF/Porder.thy Wed Jan 21 23:40:23 2009 +0100 @@ -10,7 +10,7 @@ subsection {* Type class for partial orders *} -class sq_ord = type + +class sq_ord = fixes sq_le :: "'a \ 'a \ bool" notation diff -r 4f9803829625 -r 564ea783ace8 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Jan 21 18:37:44 2009 +0100 +++ b/src/Pure/Isar/class.ML Wed Jan 21 23:40:23 2009 +0100 @@ -92,8 +92,8 @@ fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt => let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); -fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) => - if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort) +val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) => + if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort) else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi) (*FIXME does not occur*) | T as TFree (v, sort) => @@ -119,11 +119,12 @@ let (* prepare import *) val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); - val (sups, others_basesort) = map (prep_class thy) raw_supclasses - |> Sign.minimize_sort thy - |> List.partition (is_class thy); - - val supparams = (map o apsnd) (snd o snd) (these_params thy sups); + val sups = map (prep_class thy) raw_supclasses + |> Sign.minimize_sort thy; + val _ = case filter_out (is_class thy) sups + of [] => () + | no_classes => error ("These are not classes: " ^ commas (map quote no_classes)); + val supparams = (map o apsnd) (snd o snd) (these_params thy sups); val supparam_names = map fst supparams; val _ = if has_duplicates (op =) supparam_names then error ("Duplicate parameter(s) in superclasses: " @@ -131,7 +132,7 @@ else (); val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); - val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort; + val given_basesort = fold inter_sort (map (base_sort thy) sups) []; (* infer types and base sort *) val base_constraints = (map o apsnd) @@ -139,10 +140,9 @@ (these_operations thy sups); val ((_, _, inferred_elems), _) = ProofContext.init thy |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints - |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort)) + |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param |> add_typ_check ~2 "singleton_fixate" singleton_fixate |> prep_decl supexpr raw_elems; - (*FIXME propagation of given base sort into class spec broken*) (*FIXME check for *all* side conditions here, extra check function for elements, less side-condition checks in check phase*) val base_sort = if null inferred_elems then given_basesort else @@ -170,45 +170,6 @@ val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration; -(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems = - let - (*FIXME 2009 simplify*) - val supclasses = map (prep_class thy) raw_supclasses; - val supsort = Sign.minimize_sort thy supclasses; - val (sups, bases) = List.partition (is_class thy) supsort; - val base_sort = if null sups then supsort else - Library.foldr (Sorts.inter_sort (Sign.classes_of thy)) - (map (base_sort thy) sups, bases); - val supparams = (map o apsnd) (snd o snd) (these_params thy sups); - val supparam_names = map fst supparams; - val _ = if has_duplicates (op =) supparam_names - then error ("Duplicate parameter(s) in superclasses: " - ^ (commas o map quote o duplicates (op =)) supparam_names) - else (); - - val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional []))) - sups, []); - val constrain = Element.Constrains ((map o apsnd o map_atyps) - (K (TFree (Name.aT, base_sort))) supparams); - (*FIXME 2009 perhaps better: control type variable by explicit - parameter instantiation of import expression*) - val begin_ctxt = begin sups base_sort - #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps) - (K (TFree (Name.aT, base_sort))) supparams) (*FIXME - should constraints be issued in begin?*) - val ((_, _, syntax_elems), _) = ProofContext.init thy - |> begin_ctxt - |> process_decl supexpr raw_elems; - fun fork_syn (Element.Fixes xs) = - fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs - #>> Element.Fixes - | fork_syn x = pair x; - val (elems, global_syntax) = fold_map fork_syn syntax_elems []; - in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end; - -val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration; -val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*) - fun add_consts bname class base_sort sups supparams global_syntax thy = let (*FIXME 2009 simplify*)