# HG changeset patch # User wenzelm # Date 1192111535 -7200 # Node ID 526df61afe9756c9602a381e2620daa3cb10f71f # Parent c04ec061ac2bcb5fff4ff3a497f3b849870e82a4 moved define_class_params to Isar/class.ML; removed obsolete params_of_class, print_axclasses; moved ProofContext.pp to Syntax.pp; misc tuning; diff -r c04ec061ac2b -r 526df61afe97 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Oct 11 16:05:33 2007 +0200 +++ b/src/Pure/axclass.ML Thu Oct 11 16:05:35 2007 +0200 @@ -2,28 +2,22 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Type classes as parameter records and predicates, with explicit -definitions and proofs. +Type classes defined as predicates, associated with a record of +parameters. *) signature AX_CLASS = sig val define_class: bstring * class list -> string list -> ((bstring * attribute list) * term list) list -> theory -> class * theory - val define_class_params: bstring * class list -> ((bstring * typ) * mixfix) list -> - (theory -> (string * typ) list -> ((bstring * attribute list) * term list) list) -> - string list -> theory -> - (class * ((string * typ) list * thm list)) * theory val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory val prove_classrel: class * class -> tactic -> theory -> theory val prove_arity: string * sort list * sort -> tactic -> theory -> theory - val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list, - params: (string * typ) list} + val get_info: theory -> class -> + {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} val class_intros: theory -> thm list val class_of_param: theory -> string -> class option - val params_of_class: theory -> class -> string * (string * typ) list - val print_axclasses: theory -> unit val cert_classrel: theory -> class * class -> class * class val read_classrel: theory -> xstring * xstring -> class * class val axiomatize_class: bstring * class list -> theory -> theory @@ -133,10 +127,7 @@ fun params_of thy c = get_params thy (fn c' => c' = c); fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); -fun class_of_param thy = - AList.lookup (op =) (#2 (get_axclasses thy)); - -fun params_of_class thy class = (Name.aT, #params (get_info thy class)); +fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy)); (* maintain instances *) @@ -165,24 +156,6 @@ (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th)))); -(* print data *) - -fun print_axclasses thy = - let - val axclasses = #1 (get_axclasses thy); - val ctxt = ProofContext.init thy; - - fun pretty_axclass (class, AxClass {def, intro, axioms, params}) = - Pretty.block (Pretty.fbreaks - [Pretty.block - [Pretty.str "class ", Syntax.pretty_sort ctxt [class], Pretty.str ":"], - Pretty.strs ("parameters:" :: params_of thy class), - ProofContext.pretty_fact ctxt ("def", [def]), - ProofContext.pretty_fact ctxt (introN, [intro]), - ProofContext.pretty_fact ctxt (axiomsN, axioms)]); - in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end; - - (** instances **) @@ -281,29 +254,48 @@ (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; in (intro, dests) end; -fun define_class (bclass, raw_super) params raw_specs thy = +fun define_class (bclass, raw_super) raw_params raw_specs thy = let val ctxt = ProofContext.init thy; - val pp = ProofContext.pp ctxt; + val pp = Syntax.pp ctxt; - (* prepare specification *) + (* class *) val bconst = Logic.const_of_class bclass; val class = Sign.full_name thy bclass; val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); + fun check_constraint (a, S) = + if Sign.subsort thy (super, S) then () + else error ("Sort constraint of type variable " ^ + setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ + " needs to be weaker than " ^ Pretty.string_of_sort pp super); + + + (* params *) + + val params = raw_params |> map (fn p => + let + val T = Sign.the_const_type thy p; + val _ = + (case Term.add_tvarsT T [] of + [((a, _), S)] => check_constraint (a, S) + | _ => error ("Exactly one type variable expected in class parameter " ^ quote p)); + val T' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) T; + in (p, T') end); + + + (* axioms *) + fun prep_axiom t = (case Term.add_tfrees t [] of - [(a, S)] => - if Sign.subsort thy (super, S) then t - else error ("Sort constraint of type variable " ^ - setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ - " needs to be weaker than " ^ Pretty.string_of_sort pp super) - | [] => t - | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t)) - |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) - |> Logic.close_form; + [(a, S)] => check_constraint (a, S) + | [] => () + | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t); + t + |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) + |> Logic.close_form); val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; val name_atts = map fst raw_specs; @@ -333,21 +325,10 @@ ((superN, []), [(map Drule.standard raw_classrel, [])]), ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; - (* params *) - - val params_typs = map (fn param => - let - val ty = Sign.the_const_type thy param; - val _ = case Term.typ_tvars ty - of [_] => () - | _ => error ("Exactly one type variable required in parameter " ^ quote param); - val ty' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) ty; - in (param, ty') end) params; - (* result *) - val axclass = make_axclass ((def, intro, axioms), params_typs); + val axclass = make_axclass ((def, intro, axioms), params); val result_thy = facts_thy |> fold put_classrel (map (pair class) super ~~ classrel) @@ -356,46 +337,12 @@ |> Sign.restore_naming facts_thy |> map_axclasses (fn (axclasses, parameters) => (Symtab.update (class, axclass) axclasses, - fold (fn x => add_param pp (x, class)) params parameters)); + fold (fn (x, _) => add_param pp (x, class)) params parameters)); in (class, result_thy) end; -(** axclasses with implicit parameter handling **) - -fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy = - let - val superclasses = map (Sign.certify_class thy) raw_superclasses; - val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; - val prefix = Logic.const_of_class name; - fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix) - (Sign.full_name thy c); - fun add_const ((c, ty), syn) = - Sign.add_consts_authentic [] [(c, ty, syn)] - #> pair (mk_const_name c, ty); - fun mk_axioms cs thy = - raw_dep_axioms thy cs - |> (map o apsnd o map) (Sign.cert_prop thy) - |> rpair thy; - fun add_constraint class (c, ty) = - Sign.add_const_constraint (c, SOME - (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); - in - thy - |> Sign.add_path prefix - |> fold_map add_const consts - ||> Sign.restore_naming thy - |-> (fn cs => mk_axioms cs - #-> (fn axioms_prop => define_class (name, superclasses) - (map fst cs @ other_consts) axioms_prop - #-> (fn class => `(fn thy => get_info thy class) - #-> (fn {axioms, ...} => fold (add_constraint class) cs - #> pair (class, (cs, axioms)))))) - end; - - - (** axiomatizations **) local