# HG changeset patch # User haftmann # Date 1138605570 -3600 # Node ID 05a16861d3a5d00db1bb4bdd8159e80e4c7712f2 # Parent 4ed69fe8f8870cead9cccaa354b432ae581e7994 added three times overloaded Isar instance command diff -r 4ed69fe8f887 -r 05a16861d3a5 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Mon Jan 30 08:18:51 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Mon Jan 30 08:19:30 2006 +0100 @@ -17,7 +17,8 @@ val add_instance_arity_i: (string * sort list) * sort -> ((bstring * term) * attribute list) list -> theory -> Proof.state - val add_classentry: class -> xstring list -> xstring list -> theory -> theory + val add_classentry: class -> xstring list -> theory -> theory + val add_classinsts: class -> xstring list -> theory -> theory val intern_class: theory -> xstring -> string val extern_class: theory -> string -> xstring @@ -152,6 +153,13 @@ fun gen_add_class add_locale prep_class bname raw_supclasses raw_body thy = let val supclasses = map (prep_class thy) raw_supclasses; + fun get_allcs class = + let + val data = get_class_data thy class + in + Library.flat (map get_allcs (#superclasses data) @ [#consts data]) + end; + val supcs = Library.flat (map get_allcs supclasses) val supsort = case map (#name_axclass o get_class_data thy) supclasses of [] => Sign.defaultS thy | sort => Sorts.certify_sort (Sign.classes_of thy) sort; @@ -159,22 +167,18 @@ of [] => Locale.empty | _ => (Locale.Merge o map (Locale.Locale o #name_locale o get_class_data thy)) supclasses; - fun extract_assumes c_adds elems = - let - fun subst_free ts = - let - val get_ty = the o AList.lookup (op =) (fold Term.add_frees ts []); - val subst_map = map (fn (c, (c', _)) => - (Free (c, get_ty c), Const (c', get_ty c))) c_adds; - in map (subst_atomic subst_map) ts end; - in - elems - |> (map o List.mapPartial) - (fn (Element.Assumes asms) => (SOME o map (map fst o snd)) asms - | _ => NONE) - |> Library.flat o Library.flat o Library.flat - |> subst_free - end; + fun mk_c_lookup c_global supcs c_adds = + map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds + fun extract_assumes v c_lookup elems = + elems + |> (map o List.mapPartial) + (fn (Element.Assumes asms) => (SOME o map (map fst o snd)) asms + | _ => NONE) + |> Library.flat o Library.flat o Library.flat + |> (map o map_aterms) (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup) c, ty) + | t => t) + |> tap (fn ts => writeln ("(1) axclass axioms: " ^ + (commas o map (Sign.string_of_term thy)) ts)); fun extract_tyvar_name thy tys = fold (curry add_typ_tfrees) tys [] |> (fn [(v, sort)] => @@ -211,8 +215,7 @@ fun interpret name_locale cs ax_axioms thy = thy |> Locale.interpretation (NameSpace.base name_locale, []) - (Locale.Locale name_locale) - (map (fn ((c, _), _) => SOME (Sign.intern_const thy c)) cs) + (Locale.Locale name_locale) (map (SOME o fst) cs) |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE); fun print_ctxt ctxt elem = map Pretty.writeln (Element.pretty_ctxt ctxt elem) @@ -227,7 +230,7 @@ fold_map (add_global_const v) c_defs #-> (fn c_adds => AxClass.add_axclass_i (bname, supsort) - (map (Thm.no_attributes o pair "") (extract_assumes c_adds (import_elems @ body_elems))) + (map (Thm.no_attributes o pair "") (extract_assumes v (mk_c_lookup c_global supcs c_adds) body_elems)) #-> (fn { axioms = ax_axioms : thm list, ...} => `(fn thy => Sign.intern_class thy bname) #-> (fn name_axclass => @@ -235,7 +238,7 @@ #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds)) #> tap (fn _ => (map o map) (print_ctxt ctxt) import_elems) #> tap (fn _ => (map o map) (print_ctxt ctxt) body_elems) - #> interpret name_locale (c_global @ c_defs) ax_axioms + #> interpret name_locale (supcs @ (map (fn ((c, ty), _) => (Sign.intern_const thy c, ty)) c_defs)) ax_axioms )))))) end; @@ -270,9 +273,15 @@ fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs; fun check_defs c_given c_req thy = let - fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2 - andalso Sign.typ_instance thy (ty1, ty2) - andalso Sign.typ_instance thy (ty2, ty1); + fun eq_c ((c1, ty1), (c2, ty2)) = + let + val ty1' = Type.varifyT ty1; + val ty2' = Type.varifyT ty2; + in + c1 = c2 + andalso Sign.typ_instance thy (ty1', ty2') + andalso Sign.typ_instance thy (ty2', ty1') + end; val _ = case fold (remove eq_c) c_req c_given of [] => () | cs => error ("superfluous definition(s) given for " @@ -427,7 +436,7 @@ (* intermediate auxiliary *) -fun add_classentry raw_class raw_cs raw_insts thy = +fun add_classentry raw_class raw_cs thy = let val class = Sign.intern_class thy raw_class; val cs_proto = @@ -446,14 +455,20 @@ then TFree (v, []) else TVar var ) ty)); - val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts; in thy |> add_class_data (class, ([], "", class, v, cs)) + end; + +fun add_classinsts raw_class raw_insts thy = + let + val class = Sign.intern_class thy raw_class; + val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts; + in + thy |> fold (curry add_inst_data class) insts end; - (* toplevel interface *) local @@ -463,22 +478,23 @@ in -val (classK, instanceK) = ("class", "class_instance") +val (classK, instanceK) = ("class", "instance") val classP = - OuterSyntax.command classK "operational type classes" K.thy_decl - (P.name --| P.$$$ "=" - -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) [] - -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) [] + OuterSyntax.command classK "operational type classes" K.thy_decl ( + P.name --| P.$$$ "=" + -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) [] + -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) [] >> (Toplevel.theory_context o (fn ((bname, supclasses), elems) => add_class bname supclasses elems))); val instanceP = - OuterSyntax.command instanceK "declare instance for operational type class" K.thy_goal - (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) - -- Scan.repeat1 P.spec_name - >> (Toplevel.print oo Toplevel.theory_to_proof - o (fn ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs))); + OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( + P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass + || P.xname -- (P.$$$ "::" |-- P.!!! P.arity) -- Scan.repeat P.spec_name + >> (fn ((tyco, (asorts, sort)), []) => AxClass.instance_arity I (tyco, asorts, sort) + | ((tyco, (asorts, sort)), defs) => add_instance_arity ((tyco, asorts), sort) defs) + ) >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [classP, instanceP];