# HG changeset patch # User wenzelm # Date 1145996638 -7200 # Node ID 0afdd5023bfcda4626f40c2b9ce9a54bfe51b9a6 # Parent d75570e8aa976e417540f9dd500a21246401c3ce Sign.arity_sorts; tuned; diff -r d75570e8aa97 -r 0afdd5023bfc src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Apr 25 22:23:50 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Tue Apr 25 22:23:58 2006 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Type classes, simulated by locales. +Type classes derived from primitive axclasses and locales. *) signature CLASS_PACKAGE = @@ -112,7 +112,7 @@ ] in (Pretty.writeln o Pretty.chunks o map (pretty_class gr) - o AList.make (Graph.get_node gr) o Library.flat o Graph.strong_conn) gr + o AList.make (Graph.get_node gr) o flat o Graph.strong_conn) gr end; end ); @@ -147,7 +147,7 @@ else operational_sort_of thy (Sign.super_classes thy class); in map get_sort sort - |> Library.flat + |> flat |> Sign.certify_sort thy end; @@ -193,13 +193,10 @@ val data = the_class_data thy class in (#var data, (map snd o #consts) data) end; -fun mg_domain thy tyco class = - Sorts.mg_domain (Sign.classes_of thy, Sign.arities_of thy) tyco [class]; - fun the_inst_sign thy (class, tyco) = let val _ = if is_operational_class thy class then () else error ("no operational class: " ^ class); - val arity = mg_domain thy tyco class; + val arity = Sign.arity_sorts thy tyco [class]; val clsvar = (#var o the_class_data thy) class; val const_sign = (snd o the_consts_sign thy) class; fun add_var sort used = @@ -289,6 +286,12 @@ HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE default_intro_classes_tac facts; +val _ = Context.add_setup (Method.add_methods + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), + "back-chain introduction rules of classes"), + ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), + "apply some intro/elim rule")]); + (* axclass instances *) @@ -325,15 +328,15 @@ else fish_thm (name ^ "_axioms") end; -fun add_locale opn name expr body thy = +fun add_locale name expr body thy = thy - |> Locale.add_locale opn name expr body + |> Locale.add_locale true name expr body ||>> `(fn thy => intro_incr thy name expr) |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt)); -fun add_locale_i opn name expr body thy = +fun add_locale_i name expr body thy = thy - |> Locale.add_locale_i opn name expr body + |> Locale.add_locale_i true name expr body ||>> `(fn thy => intro_incr thy name expr) |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt)); @@ -372,21 +375,18 @@ val supsort = supclasses |> map (#name_axclass o the_class_data thy) - |> Sorts.certify_sort (Sign.classes_of thy) + |> Sign.certify_sort thy |> null ? K (Sign.defaultS thy); - val expr = if null supclasses - then Locale.empty - else - (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses; + val expr = (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses; val mapp_sup = AList.make - (the o AList.lookup (op =) ((Library.flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) + (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) ((map (fst o fst) o Locale.parameters_of_expr thy) expr); fun extract_tyvar_consts thy name_locale = let fun extract_tyvar_name thy tys = fold (curry add_typ_tfrees) tys [] |> (fn [(v, sort)] => - if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort)) + if Sign.subsort thy (supsort, sort) then v else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort) | [] => error ("no class type variable") @@ -445,8 +445,8 @@ in -val class = gen_class (add_locale true) intern_class; -val class_i = gen_class (add_locale_i true) certify_class; +val class = gen_class add_locale intern_class; +val class_i = gen_class add_locale_i certify_class; end; (* local *) @@ -501,7 +501,7 @@ val subst_ty = map_type_tfree (fn (var as (v, _)) => if #var data = v then ty_inst else TFree var) in (map (apsnd subst_ty o snd) o #consts) data end; - val cs = (Library.flat o map get_consts) classes; + val cs = (flat o map get_consts) classes; fun get_remove_contraint c thy = let val ty = Sign.the_const_constraint thy c; @@ -609,15 +609,13 @@ val class = prep_class theory raw_class; val sort = prep_sort theory raw_sort; val loc_name = (#name_locale o the_class_data theory) class; - val loc_expr = if null sort - then Locale.empty - else - (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort; + val loc_expr = + (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort; fun after_qed thmss thy = - (writeln "---"; (Pretty.writeln o Display.pretty_thms o Library.flat) thmss; writeln "---"; fold (fn supclass => + (writeln "---"; (Pretty.writeln o Display.pretty_thms o flat) thmss; writeln "---"; fold (fn supclass => AxClass.prove_classrel (class, supclass) (ALLGOALS (K (intro_classes_tac [])) THEN - (ALLGOALS o resolve_tac o Library.flat) thmss) + (ALLGOALS o resolve_tac o flat) thmss) ) sort thy) in theory @@ -673,7 +671,7 @@ fun mk_lookup (sort_def, (Type (tyco, tys))) = map (fn class => Instance ((class, tyco), map2 (curry mk_lookup) - (map (operational_sort_of thy) (mg_domain thy tyco class)) + (map (operational_sort_of thy) (Sign.arity_sorts thy tyco [class])) tys) ) sort_def | mk_lookup (sort_def, TVar ((vname, _), sort_use)) = @@ -784,11 +782,6 @@ val _ = OuterSyntax.add_parsers [classP, instanceP]; -val _ = Context.add_setup (Method.add_methods - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), - "back-chain introduction rules of classes"), - ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]); - end; (* local *) end; (* struct *)