# HG changeset patch # User haftmann # Date 1192454983 -7200 # Node ID 522abf8a5f87d76bf736efb1b31d857d1d9ccd8a # Parent d6a3dec2375d752bfa5f45cc9349cd7d65ff286d canonical interpretation interface diff -r d6a3dec2375d -r 522abf8a5f87 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Oct 15 15:29:41 2007 +0200 +++ b/src/Pure/Isar/class.ML Mon Oct 15 15:29:43 2007 +0200 @@ -19,11 +19,12 @@ val class_cmd: bstring -> xstring list -> Element.context Locale.element list -> xstring list -> theory -> string * Proof.context val init: class -> Proof.context -> Proof.context; - val add_const_in_class: string -> (string * mixfix) * term -> theory -> string * theory - val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term -> theory -> - string * theory + val add_const_in_class: string -> (string * mixfix) * (string * term) + -> theory -> string * theory + val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term) + -> theory -> string * theory val remove_constraint: class -> string -> Proof.context -> Proof.context - val is_class: theory -> string -> bool + val is_class: theory -> class -> bool val these_params: theory -> sort -> (string * (string * typ)) list val intro_classes_tac: thm list -> tactic val default_intro_classes_tac: thm list -> tactic @@ -83,6 +84,15 @@ | NONE => thm; in strip end; +fun get_remove_global_constraint c thy = + let + val ty = Sign.the_const_constraint thy c; + in + thy + |> Sign.add_const_constraint (c, NONE) + |> pair (c, Logic.unvarifyT ty) + end; + (** axclass command **) @@ -232,14 +242,6 @@ of [] => () | dupl_tycos => error ("Type constructors occur more than once in arities: " ^ commas_quote dupl_tycos); - fun get_remove_constraint c thy = - let - val ty = Sign.the_const_constraint thy c; - in - thy - |> Sign.add_const_constraint (c, NONE) - |> pair (c, Logic.unvarifyT ty) - end; fun get_consts_class tyco ty class = let val cs = (these o try (#params o AxClass.get_info theory)) class; @@ -283,7 +285,7 @@ #> after_qed defs; in theory - |> fold_map get_remove_constraint (map fst cs |> distinct (op =)) + |> fold_map get_remove_global_constraint (map fst cs |> distinct (op =)) ||>> fold_map add_def defs ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs) @@ -311,12 +313,11 @@ (** class data **) datatype class_data = ClassData of { - locale: string, consts: (string * string) list (*locale parameter ~> constant name*), local_sort: sort, - inst: typ Symtab.table * term Symtab.table - (*canonical interpretation*), + inst: (typ option list * term option list) * term Symtab.table + (*canonical interpretation FIXME*), intro: thm, defs: thm list, operations: (string * (term * (typ * int))) list @@ -326,50 +327,46 @@ }; fun rep_class_data (ClassData d) = d; -fun mk_class_data ((locale, consts, local_sort, inst, intro), +fun mk_class_data ((consts, local_sort, inst, intro), (defs, operations, operations_rev)) = - ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, + ClassData { consts = consts, local_sort = local_sort, inst = inst, intro = intro, defs = defs, operations = operations, operations_rev = operations_rev }; -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, +fun map_class_data f (ClassData { consts, local_sort, inst, intro, defs, operations, operations_rev }) = - mk_class_data (f ((locale, consts, local_sort, inst, intro), + mk_class_data (f ((consts, local_sort, inst, intro), (defs, operations, operations_rev))); -fun merge_class_data _ (ClassData { locale = locale, consts = consts, +fun merge_class_data _ (ClassData { consts = consts, local_sort = local_sort, inst = inst, intro = intro, defs = defs1, operations = operations1, operations_rev = operations_rev1 }, - ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, + ClassData { consts = _, local_sort = _, inst = _, intro = _, defs = defs2, operations = operations2, operations_rev = operations_rev2 }) = - mk_class_data ((locale, consts, local_sort, inst, intro), + mk_class_data ((consts, local_sort, inst, intro), (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2), AList.merge (op =) (K true) (operations_rev1, operations_rev2))); -fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); - structure ClassData = TheoryDataFun ( - type T = class_data Graph.T * class Symtab.table - (*locale name ~> class name*); - val empty = (Graph.empty, Symtab.empty); + type T = class_data Graph.T + val empty = Graph.empty; val copy = I; val extend = I; - fun merge _ = merge_pair (Graph.join merge_class_data) (Symtab.merge (K true)); + fun merge _ = Graph.join merge_class_data; ); (* queries *) -val is_class = Symtab.defined o snd o ClassData.get; - -val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node - o fst o ClassData.get; +val lookup_class_data = Option.map rep_class_data oo try 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; -val ancestry = Graph.all_succs o fst o ClassData.get; +val is_class = is_some oo lookup_class_data; + +val ancestry = Graph.all_succs o ClassData.get; fun these_params thy = let @@ -386,7 +383,7 @@ fun these_intros thy = Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data)) - ((fst o ClassData.get) thy) []; + (ClassData.get thy) []; fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; @@ -428,7 +425,7 @@ (SOME o Pretty.str) ("class " ^ class ^ ":"), (SOME o Pretty.block) [Pretty.str "supersort: ", (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], - Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class), + if is_class thy class then (SOME o Pretty.str) ("locale: " ^ class) else NONE, ((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_info thy)) class, (SOME o Pretty.block o Pretty.breaks) [ @@ -444,21 +441,29 @@ (* updaters *) -fun add_class_data ((class, superclasses), (locale, cs, local_sort, inst, intro)) = +fun add_class_data ((class, superclasses), (cs, local_sort, inst, intro)) thy = let + (*FIXME*) + val is_empty = null (fold (fn ((_, ty), _) => fold_atyps cons ty) cs []) + andalso null ((fold o fold_types o fold_atyps) cons + (maps snd (Locale.global_asms_of thy class)) []); + (*FIXME*) + val inst_params = map + (SOME o the o Symtab.lookup inst o fst o fst) + (Locale.parameters_of_expr thy (Locale.Locale class)); + val instT = if is_empty then [] else [SOME (TFree (Name.aT, [class]))]; + val inst' = ((instT, inst_params), inst); val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs; val cs = (map o pairself) fst cs; - val add_class = Graph.new_node (class, mk_class_data ((locale, - cs, local_sort, inst, intro), - ([], operations, []))) + val add_class = Graph.new_node (class, + mk_class_data ((cs, local_sort, inst', intro), ([], operations, []))) #> fold (curry Graph.add_edge class) superclasses; - val add_locale = Symtab.update (locale, class); in - ClassData.map (fn (gr, tab) => (add_class gr, add_locale tab)) + ClassData.map add_class thy end; fun register_operation class (entry, some_def) = - (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd) + (ClassData.map o Graph.map_node class o map_class_data o apsnd) (fn (defs, operations, operations_rev) => (case some_def of NONE => defs | SOME def => def :: defs, entry :: operations, (*FIXME*)operations_rev)); @@ -468,13 +473,13 @@ val class_prefix = Logic.const_of_class o Sign.base_name; -fun class_intro thy locale class sups = +fun class_intro thy class sups = let fun class_elim class = case (#axioms o AxClass.get_info thy) class of [thm] => SOME (Drule.unconstrainTs thm) | [] => NONE; - val pred_intro = case Locale.intros thy locale + val pred_intro = case Locale.intros thy class of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME | ([intro], []) => SOME intro | ([], [intro]) => SOME intro @@ -499,30 +504,17 @@ fun class_interpretation class facts defs thy = let - val inst = #inst (the_class_data thy class); + val params = these_params thy [class]; + val { inst = ((_, inst), _), ... } = the_class_data thy class; + (*val _ = tracing ("interpreting with " ^ cat_lines (map (setmp show_sorts true makestring) + (map_filter I inst)));*) val tac = ALLGOALS (ProofContext.fact_tac facts); + val prfx = class_prefix class; in - prove_interpretation tac ((false, class_prefix class), []) (Locale.Locale class) - (inst, defs) thy - end; - -fun interpretation_in_rule thy (class1, class2) = - let - val ctxt = ProofContext.init thy; - fun mk_axioms class = - let - val { locale, inst = (_, insttab), ... } = the_class_data thy class; - in - Locale.global_asms_of thy locale - |> maps snd - |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup insttab) s | t => t) - |> (map o map_types o map_atyps) (fn TFree _ => TFree (Name.aT, [class1]) | T => T) - |> map (ObjectLogic.ensure_propT thy) - end; - val (prems, concls) = pairself mk_axioms (class1, class2); - in - Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls) - (Locale.intro_locales_tac true ctxt) + thy + |> fold_map (get_remove_global_constraint o fst o snd) params + ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs) + |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs) end; fun intro_classes_tac facts st = @@ -643,7 +635,7 @@ val supclasses = map (prep_class thy) raw_supclasses; val (sups, local_sort) = sups_local_sort thy supclasses; val supsort = Sign.minimize_sort thy supclasses; - val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups; + val suplocales = map Locale.Locale sups; val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); val supexpr = Locale.Merge suplocales; @@ -695,18 +687,17 @@ fun gen_class prep_spec prep_param bname raw_supclasses raw_includes_elems raw_other_consts thy = let + val class = Sign.full_name thy bname; val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) = prep_spec thy raw_supclasses raw_includes_elems; val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts; - fun mk_instT class = Symtab.empty - |> Symtab.update (Name.aT, TFree (Name.aT, [class])); fun mk_inst class param_names cs = Symtab.empty |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs; - fun extract_params thy name_locale = + fun extract_params thy = let - val params = Locale.parameters_of thy name_locale; + val params = Locale.parameters_of thy class; val _ = if Sign.subsort thy (supsort, local_sort) then () else error ("Sort " ^ Sign.string_of_sort thy local_sort ^ " is less general than permitted least general sort " @@ -718,7 +709,7 @@ |> chop (length supconsts) |> snd) end; - fun extract_assumes name_locale params thy cs = + fun extract_assumes params thy cs = let val consts = supconsts @ (map (fst o fst) params ~~ cs); fun subst (Free (c, ty)) = @@ -728,32 +719,32 @@ ((Sign.base_name name, map (Attrib.attribute_i thy) atts), (map o map_aterms) subst ts); in - Locale.global_asms_of thy name_locale + Locale.global_asms_of thy class |> map prep_asm end; - fun note_intro name_axclass class_intro = - PureThy.note_thmss_qualified "" (class_prefix name_axclass) + fun note_intro class_intro = + PureThy.note_thmss_qualified "" (class_prefix class) [(("intro", []), [([class_intro], [])])] #> snd in thy |> Locale.add_locale_i (SOME "") bname mergeexpr elems - |-> (fn name_locale => ProofContext.theory_result ( - `(fn thy => extract_params thy name_locale) + |> snd + |> ProofContext.theory (`extract_params #-> (fn (globals, params) => define_class_params (bname, supsort) params - (extract_assumes name_locale params) other_consts - #-> (fn (name_axclass, (consts, axioms)) => - `(fn thy => class_intro thy name_locale name_axclass sups) + (extract_assumes params) other_consts + #-> (fn (_, (consts, axioms)) => + `(fn thy => class_intro thy class sups) #-> (fn class_intro => - add_class_data ((name_axclass, sups), - (name_locale, map fst params ~~ consts, local_sort, - (mk_instT name_axclass, mk_inst name_axclass (map fst globals) - (map snd supconsts @ consts)), class_intro)) - #> note_intro name_axclass class_intro - #> class_interpretation name_axclass axioms [] - #> pair name_axclass - ))))) + add_class_data ((class, sups), + (map fst params ~~ consts, local_sort, + mk_inst class (map fst globals) (map snd supconsts @ consts), + class_intro)) + #> note_intro class_intro + #> class_interpretation class axioms [] + )))) + |> pair class end; in @@ -782,8 +773,9 @@ val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs; in (c, (rhs, (ty, typidx))) end; -fun add_const_in_class class ((c, mx), rhs) thy = +fun add_const_in_class class ((c, mx), (c_loc, rhs)) thy = let + val _ = tracing c_loc; val prfx = class_prefix class; val thy' = thy |> Sign.add_path prfx; @@ -793,6 +785,7 @@ val ty' = Term.fastype_of rhs'; val ty'' = subst_typ ty'; val c' = Sign.full_name thy' c; + val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c; val def = (c, Logic.mk_equals (Const (c', ty'), rhs')); val (mx', _) = fork_mixfix true true mx; fun interpret def thy = @@ -808,6 +801,7 @@ end; in thy' + |> Sign.hide_consts_i false [c''] |> Sign.declare_const [] (c, ty', mx') |> snd |> Sign.parent_path |> Sign.sticky_prefix prfx @@ -820,10 +814,12 @@ (* abbreviation in class target *) -fun add_abbrev_in_class class prmode ((c, mx), rhs) thy = +fun add_abbrev_in_class class prmode ((c, mx), (c_loc, rhs)) thy = let + val _ = tracing c_loc; val prfx = class_prefix class; - val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx; (* FIXME !? *) + val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx; + (*FIXME*) val c' = NameSpace.full naming c; val rhs' = export_fixes thy class rhs; val ty' = Term.fastype_of rhs'; diff -r d6a3dec2375d -r 522abf8a5f87 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Oct 15 15:29:41 2007 +0200 +++ b/src/Pure/Isar/locale.ML Mon Oct 15 15:29:43 2007 +0200 @@ -99,7 +99,7 @@ val interpretation_i: (Proof.context -> Proof.context) -> (bool * string) * Attrib.src list -> expr -> - (typ Symtab.table * term Symtab.table) * term list -> + term option list * term list -> theory -> Proof.state val interpretation: (Proof.context -> Proof.context) -> (bool * string) * Attrib.src list -> expr -> @@ -109,7 +109,7 @@ xstring * expr -> theory -> Proof.state val interpret_i: (Proof.state -> Proof.state Seq.seq) -> (bool * string) * Attrib.src list -> expr -> - (typ Symtab.table * term Symtab.table) * term list -> + term option list * term list -> bool -> Proof.state -> Proof.state val interpret: (Proof.state -> Proof.state Seq.seq) -> (bool * string) * Attrib.src list -> expr -> @@ -2077,14 +2077,22 @@ add_local_equation x; -fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) = +fun prep_instantiations prep_term prep_prop ctxt parms (insts, eqns) = let (* parameters *) val (parm_names, parm_types) = parms |> split_list ||> map (TypeInfer.paramify_vars o Logic.varifyT); - val type_parms = fold Term.add_tvarsT parm_types [] |> map TVar; + val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar); val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst; + (*(* type instantiations *) + val dT = length type_parms - length instsT; + val instsT = + if dT < 0 then error "More type arguments than type parameters in instantiation." + else instsT @ replicate dT NONE; + val type_terms = map2 (fn t => fn SOME T => TypeInfer.constrain (Term.itselfT T) t + | NONE => t) type_parms instsT;*) + (* parameter instantiations *) val d = length parms - length insts; val insts = @@ -2098,12 +2106,12 @@ val (given_parm_names, given_parm_types) = given_ps |> split_list; (* prepare insts / eqns *) - val given_insts' = map (parse_term ctxt) given_insts; - val eqns' = map (parse_prop ctxt) eqns; + val given_insts' = map (prep_term ctxt) given_insts; + val eqns' = map (prep_prop ctxt) eqns; (* infer types *) val res = Syntax.check_terms ctxt - (map Logic.mk_type type_parms @ + (type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns'); val ctxt' = ctxt |> fold Variable.auto_fixes res; @@ -2116,9 +2124,8 @@ val standard = Variable.export_morphism ctxt' ctxt; in ((instT, inst), eqns'') end; - val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop; -val check_instantiations = prep_instantiations (K I) (K I); +val cert_instantiations = prep_instantiations (K I) (K I); fun gen_prep_registration mk_ctxt test_reg activate prep_attr prep_expr prep_insts @@ -2200,21 +2207,13 @@ val prep_global_registration = gen_prep_global_registration Attrib.intern_src intern_expr read_instantiations; -(* FIXME: NEW val prep_global_registration_i = gen_prep_global_registration - (K I) (K I) check_instantiations; -*) -val prep_global_registration_i = gen_prep_global_registration - (K I) (K I) ((K o K) I); + (K I) (K I) cert_instantiations; val prep_local_registration = gen_prep_local_registration Attrib.intern_src intern_expr read_instantiations; -(* FIXME: NEW val prep_local_registration_i = gen_prep_local_registration - (K I) (K I) check_instantiations; -*) -val prep_local_registration_i = gen_prep_local_registration - (K I) (K I) ((K o K) I); + (K I) (K I) cert_instantiations; fun prep_registration_in_locale target expr thy = (* target already in internal form *)