# HG changeset patch # User haftmann # Date 1167420903 -3600 # Node ID ffeb00290397651e4308fd75a8b3d7d0e9739dd9 # Parent ab834c5c38585bedb0b23bb7937a65678c9296d2 major restructurings diff -r ab834c5c3858 -r ffeb00290397 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Dec 29 20:35:02 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Dec 29 20:35:03 2006 +0100 @@ -7,31 +7,22 @@ signature CLASS_PACKAGE = sig - val class: bstring -> class list -> Element.context Locale.element list -> theory -> - string * Proof.context - val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory -> + val class: bstring -> class list -> Element.context_i Locale.element list -> theory -> string * Proof.context - val instance_arity: ((bstring * string list) * string) list - -> ((bstring * Attrib.src list) * string) list - -> theory -> Proof.state - val instance_arity_i: ((bstring * sort list) * sort) list + val instance_arity: ((bstring * sort list) * sort) list -> ((bstring * attribute list) * term) list -> theory -> Proof.state val prove_instance_arity: tactic -> ((string * sort list) * sort) list -> ((bstring * attribute list) * term) list -> theory -> theory - val instance_sort: string * string -> theory -> Proof.state - val instance_sort_i: class * sort -> theory -> Proof.state + val instance_sort: class * sort -> theory -> Proof.state val prove_instance_sort: tactic -> class * sort -> theory -> theory - val certify_class: theory -> class -> class - val certify_sort: theory -> sort -> sort - val read_class: theory -> xstring -> class - val read_sort: theory -> string -> sort val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a (*'a must not keep any reference to theory*) + (* experimental class target *) val add_def: class * thm -> theory -> theory val export_typ: theory -> class -> typ -> typ val export_def: theory -> class -> term -> term @@ -45,172 +36,59 @@ structure ClassPackage : CLASS_PACKAGE = struct - -(** theory data **) +(** axclasses with implicit parameter handling **) -datatype class_data = ClassData of { - locale: string, - var: string, - consts: (string * (string * typ)) list - (*locale parameter ~> toplevel theory constant*), - propnames: string list, - defs: thm list -}; +(* axclass instances *) -fun rep_classdata (ClassData c) = c; +local -structure ClassData = TheoryDataFun ( - struct - val name = "Pure/classes"; - type T = class_data Symtab.table; - val empty = Symtab.empty; - val copy = I; - val extend = I; - fun merge _ = Symtab.merge (K true); - fun print _ _ = (); - end -); +fun gen_instance mk_prop add_thm after_qed insts thy = + let + fun after_qed' results = + ProofContext.theory ((fold o fold) add_thm results #> after_qed); + in + thy + |> ProofContext.init + |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts) + end; -val _ = Context.add_setup ClassData.init; +in + +val axclass_instance_arity = + gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; +val axclass_instance_sort = + gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) + AxClass.add_classrel I o single; + +end; (* local *) -(* queries *) - -val lookup_class_data = Option.map rep_classdata oo Symtab.lookup o ClassData.get; - -fun the_class_data thy class = - case lookup_class_data thy class - of NONE => error ("undeclared constructive class " ^ quote class) - | SOME data => data; - -fun the_ancestry thy classes = - let - fun proj_class class = - if is_some (lookup_class_data thy class) - then [class] - else (Sign.certify_sort thy o maps proj_class o Sign.super_classes thy) class; - fun ancestry class anc = - anc - |> insert (op =) class - |> fold ancestry ((maps proj_class o Sign.super_classes thy) class); - in fold ancestry classes [] end; - -val the_parm_map = #consts oo the_class_data; - -val the_propnames = #propnames oo the_class_data; - -fun subst_clsvar v ty_subst = - map_type_tfree (fn u as (w, _) => - if w = v then ty_subst else TFree u); +(* introducing axclasses with implicit parameter handling *) -fun print_classes thy = +fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms thy = let - val algebra = Sign.classes_of thy; - val arities = - Symtab.empty - |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => - Symtab.map_default (class, []) (insert (op =) tyco)) arities) - ((#arities o Sorts.rep_algebra) algebra); - val the_arities = these o Symtab.lookup arities; - fun mk_arity class tyco = - let - val Ss = Sorts.mg_domain algebra tyco [class]; - in Sign.pretty_arity thy (tyco, Ss, [class]) end; - fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " - ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty); - fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ - (SOME o Pretty.str) ("class " ^ class ^ ":"), - (SOME o Pretty.block) [Pretty.str "supersort: ", - (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class], - Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class), - ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param - o these o Option.map #params o try (AxClass.get_definition thy)) class, - (SOME o Pretty.block o Pretty.breaks) [ - Pretty.str "instances:", - Pretty.list "" "" (map (mk_arity class) (the_arities class)) - ] - ] + val superclasses = map (Sign.certify_class thy) raw_superclasses; + val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; + fun add_const ((c, ty), syn) = + Sign.add_consts_authentic [(c, ty, syn)] #> pair (Sign.full_name thy 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_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); in - (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes) - algebra + thy + |> fold_map add_const consts + |-> (fn cs => mk_axioms cs + #-> (fn axioms => AxClass.define_class_i (name, superclasses) (map fst cs) axioms + #-> (fn class => `(fn thy => AxClass.get_definition thy class) + #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs + #> pair (class, ((intro, axioms), cs)))))) end; -(* updaters *) - -fun add_class_data (class, (locale, var, consts, propnames)) = - ClassData.map ( - Symtab.update_new (class, ClassData { - locale = locale, - var = var, - consts = consts, - propnames = propnames, - defs = []}) - ); - -fun add_def (class, thm) = - (ClassData.map o Symtab.map_entry class) - (fn ClassData { locale, - var, consts, propnames, defs } => ClassData { locale = locale, - var = var, - consts = consts, propnames = propnames, defs = thm :: defs }); - - -(* experimental class target *) - -fun export_typ thy loc = - let - val class = loc (*FIXME*); - val (v, _) = AxClass.params_of_class thy class; - in - Term.map_type_tfree (fn var as (w, sort) => - if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy) - (sort, [class])) else TFree var) - end; - -fun export_def thy loc = - let - val class = loc (*FIXME*); - val data = the_class_data thy class; - val consts = #consts data; - val v = #var data; - val subst_typ = Term.map_type_tfree (fn var as (w, sort) => - if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy) - (sort, [class])) else TFree var) - fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v - of SOME c_ty => Const c_ty - | NONE => t) - | subst t = t; - in - Term.map_aterms subst #> map_types subst_typ - end; - -fun export_thm thy loc = - let - val class = loc (*FIXME*); - val thms = (#defs o the_class_data thy) class; - in - MetaSimplifier.rewrite_rule thms - end; - - -(* certification and reading *) - -fun certify_class thy class = - (fn class => (the_class_data thy class; class)) (Sign.certify_class thy class); - -fun certify_sort thy sort = - map (fn class => (the_class_data thy class; class)) (Sign.certify_sort thy sort); - -fun read_class thy = - certify_class thy o Sign.intern_class thy; - -fun read_sort thy = - certify_sort thy o Sign.read_sort thy; - - - -(** contexts with arity assumptions **) +(* contexts with arity assumptions *) fun assume_arities_of_sort thy arities ty_sort = let @@ -227,172 +105,7 @@ in f thy_read end; - -(** tactics and methods **) - -fun intro_classes_tac facts st = - (ALLGOALS (Method.insert_tac facts THEN' - REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st)))) - THEN Tactic.distinct_subgoals_tac) st; - -fun default_intro_classes_tac [] = intro_classes_tac [] - | default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) - -fun default_tac rules ctxt facts = - 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 **) - -local - -fun gen_instance mk_prop add_thm after_qed insts thy = - let - fun after_qed' results = - ProofContext.theory ((fold o fold) add_thm results #> after_qed); - in - thy - |> ProofContext.init - |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts) - end; - -in - -val axclass_instance_arity = - gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity; -val axclass_instance_arity_i = - gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; -val axclass_instance_sort = - gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) - AxClass.add_classrel I o single; - -end; - - - -(** classes and instances **) - -local - -fun add_axclass_i (name, supsort) params axs thy = - let - val (c, thy') = thy - |> AxClass.define_class_i (name, supsort) params axs; - val {intro, axioms, ...} = AxClass.get_definition thy' c; - in ((c, (intro, axioms)), thy') end; - -(*FIXME proper locale interface*) -fun prove_interpretation_i (prfx, atts) expr insts tac thy = - let - fun ad_hoc_term (Const (c, ty)) = - let - val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty; - val s = c ^ "::" ^ Pretty.output p; - in s end - | ad_hoc_term t = - let - val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t; - val s = Pretty.output p; - in s end; - in - thy - |> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts) - |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) - |> ProofContext.theory_of - end; - -fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = - let - val (elems, exprs) = fold_rev (fn Locale.Elem e => apfst (cons e) - | Locale.Expr e => apsnd (cons e)) - raw_elems ([], []); - val supclasses = map (prep_class thy) raw_supclasses; - val supsort = - supclasses - |> Sign.certify_sort thy - |> (fn [] => Sign.defaultS thy | S => S); (* FIXME Why syntax defaultS? *) - val expr_supclasses = Locale.Merge - (map (Locale.Locale o #locale o the_class_data thy) supclasses); - val expr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses - @ exprs); - val mapp_sup = AList.make - (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_supclasses); - fun extract_tyvar_consts thy name_locale = - let - fun extract_classvar ((c, ty), _) w = - (case Term.add_tfreesT ty [] - of [(v, _)] => (case w - of SOME u => if u = v then w else error ("Additonal type variable in type signature of constant " ^ quote c) - | NONE => SOME v) - | [] => error ("No type variable in type signature of constant " ^ quote c) - | _ => error ("More than one type variable in type signature of constant " ^ quote c)); - val consts1 = - Locale.parameters_of thy name_locale - |> map (apsnd (TheoryTarget.fork_mixfix false true #> fst)) - val SOME v = fold extract_classvar consts1 NONE; - val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1; - in (v, chop (length mapp_sup) consts2) end; - fun add_consts v raw_cs_sup raw_cs_this thy = - let - fun add_global_const ((c, ty), syn) thy = - ((c, (Sign.full_name thy c, ty)), - thy - |> Sign.add_consts_authentic [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]); - in - thy - |> fold_map add_global_const raw_cs_this - end; - fun extract_assumes thy name_locale cs_mapp = - let - val subst_assume = - map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty) - | t => t) - fun prep_asm ((name, atts), ts) = - ((NameSpace.base name, map (Attrib.attribute thy) atts), map subst_assume ts) - in - (map prep_asm o Locale.local_asms_of thy) name_locale - end; - fun add_global_constraint v class (_, (c, ty)) thy = - thy - |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty)); - fun mk_const thy class v (c, ty) = - Const (c, subst_clsvar v (TFree (v, [class])) ty); - in - thy - |> add_locale bname expr elems - |-> (fn name_locale => ProofContext.theory - (`(fn thy => extract_tyvar_consts thy name_locale) - #-> (fn (v, (raw_cs_sup, raw_cs_this)) => - add_consts v raw_cs_sup raw_cs_this - #-> (fn mapp_this => - `(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this)) - #-> (fn loc_axioms => - add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms - #-> (fn (name_axclass, (_, ax_axioms)) => - fold (add_global_constraint v name_axclass) mapp_this - #> add_class_data (name_locale, (name_locale, v, mapp_this, - map (fst o fst) loc_axioms)) - #> prove_interpretation_i (Logic.const_of_class bname, []) - (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) - ((ALLGOALS o ProofContext.fact_tac) ax_axioms) - ))))) #> pair name_locale) - end; - -in - -val class = gen_class (Locale.add_locale false) read_class; -val class_i = gen_class (Locale.add_locale_i false) certify_class; - -end; (*local*) +(* instances with implicit parameter handling *) local @@ -407,8 +120,8 @@ | _ => SOME raw_name; in (c, (insts, ((name, t), atts))) end; -fun read_def thy = gen_read_def thy Attrib.attribute read_axm; -fun read_def_i thy = gen_read_def thy (K I) (K I); +fun read_def_e thy = gen_read_def thy Attrib.attribute read_axm; +fun read_def thy = gen_read_def thy (K I) (K I); fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities raw_defs theory = let @@ -420,9 +133,10 @@ of [] => () | dupl_tycos => error ("type constructors occur more than once in arities: " ^ (commas o map quote) dupl_tycos); + val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory fun get_consts_class tyco ty class = let - val (_, cs) = AxClass.params_of_class theory class; + val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class; val subst_ty = map_type_tfree (K ty); in map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs @@ -430,7 +144,7 @@ fun get_consts_sort (tyco, asorts, sort) = let val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts)) - in maps (get_consts_class tyco ty) (the_ancestry theory sort) end; + in maps (get_consts_class tyco ty) (super_sort sort) end; val cs = maps get_consts_sort arities; fun mk_typnorm thy (ty, ty_sc) = case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty @@ -474,22 +188,339 @@ theory |> fold_map get_remove_contraint (map fst cs |> distinct (op =)) ||>> add_defs defs - |-> (fn (cs, def_thms) => do_proof (after_qed cs) arities) + |-> (fn (cs, _) => do_proof (after_qed cs) arities) end; -fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute +fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute + read_def_e do_proof; +fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity (K I) read_def do_proof; -fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I) - read_def_i do_proof; fun tactic_proof tac after_qed arities = fold (fn arity => AxClass.prove_arity arity tac) arities #> after_qed; in -val instance_arity = instance_arity' axclass_instance_arity_i; -val instance_arity_i = instance_arity_i' axclass_instance_arity_i; -val prove_instance_arity = instance_arity_i' o tactic_proof; +val instance_arity_e = instance_arity_e' axclass_instance_arity; +val instance_arity = instance_arity' axclass_instance_arity; +val prove_instance_arity = instance_arity' o tactic_proof; + +end; (* local *) + + + +(** combining locales and axclasses **) + +(* theory data *) + +datatype class_data = ClassData of { + locale: string, + consts: (string * string) list + (*locale parameter ~> toplevel theory constant*), + propnames: string list, + defs: thm list + (*for experimental class target*) +}; + +fun rep_classdata (ClassData c) = c; + +structure ClassData = TheoryDataFun ( + struct + val name = "Pure/classes"; + type T = class_data Graph.T; + val empty = Graph.empty; + val copy = I; + val extend = I; + fun merge _ = Graph.merge (K true); + fun print _ _ = (); + end +); + +val _ = Context.add_setup ClassData.init; + + +(* queries *) + +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o ClassData.get; +val is_class = can o Graph.get_node o ClassData.get; +fun the_class_data thy class = + case lookup_class_data thy class + of NONE => error ("undeclared class " ^ quote class) + | SOME data => data; + +fun the_ancestry thy = Graph.all_succs (ClassData.get thy); + +fun the_parm_map thy class = + let + val const_typs = (#params o AxClass.get_definition thy) class; + val const_names = (#consts o the_class_data thy) class; + in + map (apsnd (fn c => (c, (the o AList.lookup (op =) const_typs) c))) const_names + end; + +val the_propnames = #propnames oo the_class_data; + +fun print_classes thy = + let + val algebra = Sign.classes_of thy; + val arities = + Symtab.empty + |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => + Symtab.map_default (class, []) (insert (op =) tyco)) arities) + ((#arities o Sorts.rep_algebra) algebra); + val the_arities = these o Symtab.lookup arities; + fun mk_arity class tyco = + let + val Ss = Sorts.mg_domain algebra tyco [class]; + in Sign.pretty_arity thy (tyco, Ss, [class]) end; + fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " + ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty); + fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ + (SOME o Pretty.str) ("class " ^ class ^ ":"), + (SOME o Pretty.block) [Pretty.str "supersort: ", + (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class], + Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class), + ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param + o these o Option.map #params o try (AxClass.get_definition thy)) class, + (SOME o Pretty.block o Pretty.breaks) [ + Pretty.str "instances:", + Pretty.list "" "" (map (mk_arity class) (the_arities class)) + ] + ] + in + (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes) + algebra + end; + + +(* updaters *) + +fun add_class_data ((class, superclasses), (locale, consts, propnames)) = + ClassData.map ( + Graph.new_node (class, ClassData { + locale = locale, + consts = consts, + propnames = propnames, + defs = []}) + #> fold (curry Graph.add_edge class) superclasses + ); + +fun add_def (class, thm) = + (ClassData.map o Graph.map_node class) + (fn ClassData { locale, + consts, propnames, defs } => ClassData { locale = locale, + consts = consts, propnames = propnames, defs = thm :: defs }); + + +(* tactics and methods *) + +fun intro_classes_tac facts st = + (ALLGOALS (Method.insert_tac facts THEN' + REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st)))) + THEN Tactic.distinct_subgoals_tac) st; + +fun default_intro_classes_tac [] = intro_classes_tac [] + | default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) + +fun default_tac rules ctxt facts = + 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")]); + + +(* classes and instances *) + +local + +fun add_axclass (name, supsort) params axs thy = + let + val (c, thy') = thy + |> AxClass.define_class_i (name, supsort) params axs; + val {intro, axioms, ...} = AxClass.get_definition thy' c; + in ((c, (intro, axioms)), thy') end; + +fun certify_class thy class = + tap (the_class_data thy) (Sign.certify_class thy class); + +fun read_class thy = + certify_class thy o Sign.intern_class thy; + +(*FIXME proper locale interface*) +fun prove_interpretation (prfx, atts) expr insts tac thy = + let + fun ad_hoc_term (Const (c, ty)) = + let + val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty; + val s = c ^ "::" ^ Pretty.output p; + in s end + | ad_hoc_term t = + let + val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t; + val s = Pretty.output p; + in s end; + in + thy + |> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts) + |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) + |> ProofContext.theory_of + end; + +(* +fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = + let + val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems []; + val supclasses = map (prep_class thy) raw_supclasses; + val supsort = + supclasses + |> Sign.certify_sort thy + |> (fn [] => Sign.defaultS thy | S => S); (* FIXME Why syntax defaultS? *) + val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses); + val supconsts = AList.make + (the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses)) + ((map (fst o fst) o Locale.parameters_of_expr thy) supexpr); + fun check_locale thy name_locale = + let + val tfrees = + [] + |> fold (fold Term.add_tfrees o snd) (Locale.global_asms_of thy name_locale) + |> fold (Term.add_tfreesT o snd o fst) (Locale.parameters_of thy name_locale); + in case tfrees + of [(_, _)] => () + (*| [(_, sort)] => error ("Additional sort constraint on class variable: " + ^ Sign.string_of_sort thy sort) FIXME what to do about this?*) + | [] => error ("No type variable in class specification") + | tfrees => error ("More than one type variable in class specification: " ^ + (commas o map fst) tfrees) + end; + fun extract_params thy name_locale = + Locale.parameters_of thy name_locale + |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, []))) + |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst) + |> chop (length supconsts) + |> snd; + val LOC_AXIOMS = ref [] : string list ref; + fun extract_assumes name_locale params thy cs = + let + val consts = supconsts @ (map (fst o fst) params ~~ cs); + (*FIXME is this type handling correct?*) + fun subst (Free (c, ty)) = + Const ((fst o the o AList.lookup (op =) consts) c, ty); + fun prep_asm ((name, atts), ts) = + (*FIXME*) + ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts); + in + Locale.local_asms_of thy name_locale + |> map prep_asm + |> tap (fn assms => LOC_AXIOMS := map (fst o fst) assms) + end; + fun mk_const thy class (c, ty) = + Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty); + in + thy + |> add_locale bname supexpr elems + |-> (fn name_locale => ProofContext.theory_result ( + tap (fn thy => check_locale thy name_locale) + #> `(fn thy => extract_params thy name_locale) + #-> (fn params => + axclass_params (bname, supsort) params (extract_assumes name_locale params) + #-> (fn (name_axclass, ((_, ax_axioms), consts)) => + add_class_data ((name_axclass, supclasses), (name_locale, map (fst o fst) params ~~ map fst consts, + ! LOC_AXIOMS)) + #> prove_interpretation (Logic.const_of_class bname, []) + (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts)) + ((ALLGOALS o ProofContext.fact_tac) ax_axioms) + #> pair name_axclass + )))) + end; +*) + +fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = + let + val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems []; + val supclasses = map (prep_class thy) raw_supclasses; + val supsort = + supclasses + |> Sign.certify_sort thy + |> (fn [] => Sign.defaultS thy | S => S); (* FIXME Why syntax defaultS? *) + val expr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses); + val mapp_sup = AList.make + (the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses)) + ((map (fst o fst) o Locale.parameters_of_expr thy) expr); + fun extract_consts thy name_locale = + let + val tfrees = + [] + |> fold (fold Term.add_tfrees o snd) (Locale.global_asms_of thy name_locale) + |> fold (Term.add_tfreesT o snd o fst) (Locale.parameters_of thy name_locale); + val _ = case tfrees + of [(_, _)] => () + (*| [(_, sort)] => error ("Additional sort constraint on class variable: " + ^ Sign.string_of_sort thy sort) FIXME what to do about this?*) + | [] => error ("No type variable in class specification") + | tfrees => error ("More than one type variable in class specification: " ^ + (commas o map fst) tfrees); + val consts = + Locale.parameters_of thy name_locale + |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, []))) + |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst); + in chop (length mapp_sup) consts |> snd end; + fun add_consts raw_cs_this thy = + let + fun add_global_const ((c, ty), syn) thy = + ((c, (Sign.full_name thy c, ty)), + thy + |> Sign.add_consts_authentic + [(c, ty |> Term.map_type_tfree (fn (v, _) => TFree (v, Sign.defaultS thy)), syn)]); + in + thy + |> fold_map add_global_const raw_cs_this + end; + fun extract_assumes thy name_locale cs_mapp = + let + val subst_assume = + map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty) + | t => t) + fun prep_asm ((name, atts), ts) = + (*FIXME*) + ((NameSpace.base name, map (Attrib.attribute thy) atts), map subst_assume ts) + in + (map prep_asm o Locale.local_asms_of thy) name_locale + end; + fun add_global_constraint class (_, (c, ty)) thy = + thy + |> Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); + fun mk_const thy class (c, ty) = + Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty); + in + thy + |> add_locale bname expr elems + |-> (fn name_locale => ProofContext.theory + (`(fn thy => extract_consts thy name_locale) + #-> (fn raw_cs_this => + add_consts raw_cs_this + #-> (fn mapp_this => + `(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this)) + #-> (fn loc_axioms => + add_axclass (bname, supsort) (map (fst o snd) mapp_this) loc_axioms + #-> (fn (name_axclass, (_, ax_axioms)) => + fold (add_global_constraint name_axclass) mapp_this + #> add_class_data ((name_axclass, supclasses), (name_locale, map (apsnd fst) mapp_this, + map (fst o fst) loc_axioms)) + #> prove_interpretation (Logic.const_of_class bname, []) + (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd (mapp_sup @ mapp_this))) + ((ALLGOALS o ProofContext.fact_tac) ax_axioms) + ))))) #> pair name_locale) + end; + +in + +val class_e = gen_class (Locale.add_locale false) read_class; +val class = gen_class (Locale.add_locale_i false) certify_class; end; (*local*) @@ -502,14 +533,12 @@ |> ProofContext.theory_of; (*FIXME very ad-hoc, needs proper locale interface*) -fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory = +fun instance_sort' do_proof (class, sort) theory = let - val class = prep_class theory raw_class; - val sort = prep_sort theory raw_sort; val loc_name = (#locale o the_class_data theory) class; val loc_expr = (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort; - val const_names = (map (NameSpace.base o fst o snd) + val const_names = (map (NameSpace.base o snd) o maps (#consts o the_class_data theory) o the_ancestry theory) [class]; fun get_thms thy = @@ -532,20 +561,68 @@ |> do_proof after_qed (loc_name, loc_expr) end; -fun instance_sort' do_proof = gen_instance_sort read_class read_sort do_proof; -fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof; -val setup_proof = Locale.interpretation_in_locale o ProofContext.theory; -val tactic_proof = prove_interpretation_in; +val prove_instance_sort = instance_sort' o prove_interpretation_in; + +fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory = + let + val class = prep_class theory raw_class; + val sort = prep_sort theory raw_sort; + in if is_class theory class andalso forall (is_class theory) sort then + theory + |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort) + else case sort + of [class'] => + theory + |> axclass_instance_sort (class, class') + | _ => error ("Exactly one class expected: " ^ Sign.string_of_sort theory sort) + end; in -val instance_sort = instance_sort' setup_proof; -val instance_sort_i = instance_sort_i' setup_proof; -val prove_instance_sort = instance_sort_i' o tactic_proof; +val instance_sort_e = gen_instance_sort Sign.read_class Sign.read_sort; +val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort; +val prove_instance_sort = prove_instance_sort; end; (* local *) +(** experimental class target **) + +fun export_typ thy loc = + let + val class = loc (*FIXME*); + val (v, _) = AxClass.params_of_class thy class; + in + Term.map_type_tfree (fn var as (w, sort) => + if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy) + (sort, [class])) else TFree var) + end; + +fun export_def thy loc = + let + val class = loc (*FIXME*); + val consts = the_parm_map thy class; + val subst_typ = Term.map_type_tfree (fn var as (w, sort) => + if w = AxClass.param_tyvarname then TFree (w, Sorts.inter_sort (Sign.classes_of thy) + (sort, [class])) else TFree var) + fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v + of SOME c_ty => Const c_ty + | NONE => t) + | subst t = t; + in + Term.map_aterms subst #> map_types subst_typ + end; + +fun export_thm thy loc = + let + val class = loc (*FIXME*); + val thms = (#defs o the_class_data thy) class; + in + MetaSimplifier.rewrite_rule thms + end; + + + (** toplevel interface **) local @@ -557,11 +634,6 @@ val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes") -fun wrap_add_instance_sort (class, sort) thy = - (if forall (is_some o lookup_class_data thy) (Sign.read_sort thy sort) - andalso (is_some o lookup_class_data thy) (Sign.intern_class thy class) - then instance_sort else axclass_instance_sort) (class, sort) thy; - val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::); val class_bodyP = P.!!! (Scan.repeat1 P.locale_element); @@ -579,14 +651,14 @@ -- P.opt_begin >> (fn ((bname, (supclasses, elems)), begin) => Toplevel.begin_local_theory begin - (class bname supclasses elems #-> TheoryTarget.begin true))); + (class_e bname supclasses elems #-> TheoryTarget.begin true))); val instanceP = OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( - P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_sort + P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) + >> instance_sort_e || P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop) - >> (fn ([((tyco, asorts), sort)], []) => axclass_instance_arity I [(tyco, asorts, sort)] - | (arities, defs) => instance_arity arities defs) + >> (fn (arities, defs) => instance_arity_e arities defs) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); val print_classesP =