# HG changeset patch # User haftmann # Date 1281535323 -7200 # Node ID 67d71449e85ba993e8a3bece93f676417b4e9d3b # Parent 0b6fa86110e7b7e1fc4e08d367e517aa6646315e more convenient split of class modules: class and class_declaration diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Aug 11 15:45:15 2010 +0200 +++ b/src/Pure/IsaMakefile Wed Aug 11 16:02:03 2010 +0200 @@ -111,7 +111,7 @@ Isar/auto_bind.ML \ Isar/calculation.ML \ Isar/class.ML \ - Isar/class_target.ML \ + Isar/class_declaration.ML \ Isar/code.ML \ Isar/constdefs.ML \ Isar/context_rules.ML \ diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Aug 11 15:45:15 2010 +0200 +++ b/src/Pure/Isar/class.ML Wed Aug 11 16:02:03 2010 +0200 @@ -1,351 +1,651 @@ (* Title: Pure/Isar/class.ML Author: Florian Haftmann, TU Muenchen -Type classes derived from primitive axclasses and locales -- interfaces. +Type classes derived from primitive axclasses and locales. *) signature CLASS = sig - include CLASS_TARGET - (*FIXME the split into class_target.ML, named_target.ML and - class.ML is artificial*) + (*classes*) + val is_class: theory -> class -> bool + val these_params: theory -> sort -> (string * (class * (string * typ))) list + val base_sort: theory -> class -> sort + val rules: theory -> class -> thm option * thm + val these_defs: theory -> sort -> thm list + val these_operations: theory -> sort + -> (string * (class * (typ * term))) list + val print_classes: theory -> unit + val init: class -> theory -> Proof.context + val begin: class list -> sort -> Proof.context -> Proof.context + val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory + val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory + val refresh_syntax: class -> Proof.context -> Proof.context + val redeclare_operations: theory -> sort -> Proof.context -> Proof.context + val class_prefix: string -> string + val register: class -> class list -> ((string * typ) * (string * typ)) list + -> sort -> morphism -> morphism -> thm option -> thm option -> thm + -> theory -> theory - val class: binding -> class list -> Element.context_i list - -> theory -> string * local_theory - val class_cmd: binding -> xstring list -> Element.context list - -> theory -> string * local_theory - val prove_subclass: tactic -> class -> local_theory -> local_theory - val subclass: class -> local_theory -> Proof.state - val subclass_cmd: xstring -> local_theory -> Proof.state + (*instances*) + val instantiation: string list * (string * sort) list * sort -> theory -> local_theory + val instantiation_instance: (local_theory -> local_theory) + -> local_theory -> Proof.state + val prove_instantiation_instance: (Proof.context -> tactic) + -> local_theory -> local_theory + val prove_instantiation_exit: (Proof.context -> tactic) + -> local_theory -> theory + val prove_instantiation_exit_result: (morphism -> 'a -> 'b) + -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory + val read_multi_arity: theory -> xstring list * xstring list * xstring + -> string list * (string * sort) list * sort + val type_name: string -> string + val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory + val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state + + (*subclasses*) + val classrel: class * class -> theory -> Proof.state + val classrel_cmd: xstring * xstring -> theory -> Proof.state + val register_subclass: class * class -> morphism option -> Element.witness option + -> morphism -> theory -> theory + + (*tactics*) + val intro_classes_tac: thm list -> tactic + val default_intro_tac: Proof.context -> thm list -> tactic end; structure Class: CLASS = struct -open Class_Target; +(** class data **) + +datatype class_data = ClassData of { + + (* static part *) + consts: (string * string) list + (*locale parameter ~> constant name*), + base_sort: sort, + base_morph: morphism + (*static part of canonical morphism*), + export_morph: morphism, + assm_intro: thm option, + of_class: thm, + axiom: thm option, + + (* dynamic part *) + defs: thm list, + operations: (string * (class * (typ * term))) list + +}; + +fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), + (defs, operations)) = + ClassData { consts = consts, base_sort = base_sort, + base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, + of_class = of_class, axiom = axiom, defs = defs, operations = operations }; +fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro, + of_class, axiom, defs, operations }) = + make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), + (defs, operations))); +fun merge_class_data _ (ClassData { consts = consts, + base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, + of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, + ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, + of_class = _, axiom = _, defs = defs2, operations = operations2 }) = + make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), + (Thm.merge_thms (defs1, defs2), + AList.merge (op =) (K true) (operations1, operations2))); + +structure ClassData = Theory_Data +( + type T = class_data Graph.T + val empty = Graph.empty; + val extend = I; + val merge = Graph.join merge_class_data; +); + + +(* queries *) + +fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class + of SOME (ClassData data) => SOME data + | NONE => NONE; + +fun the_class_data thy class = case lookup_class_data thy class + of NONE => error ("Undeclared class " ^ quote class) + | SOME data => data; + +val is_class = is_some oo lookup_class_data; + +val ancestry = Graph.all_succs o ClassData.get; +val heritage = Graph.all_preds o ClassData.get; + +fun these_params thy = + let + fun params class = + let + val const_typs = (#params o AxClass.get_info thy) class; + val const_names = (#consts o the_class_data thy) class; + in + (map o apsnd) + (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names + end; + in maps params o ancestry thy end; + +val base_sort = #base_sort oo the_class_data; + +fun rules thy class = + let val { axiom, of_class, ... } = the_class_data thy class + in (axiom, of_class) end; + +fun all_assm_intros thy = + Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm) + (the_list assm_intro)) (ClassData.get thy) []; + +fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; +fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; + +val base_morphism = #base_morph oo the_class_data; +fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class]) + of SOME eq_morph => base_morphism thy class $> eq_morph + | NONE => base_morphism thy class; +val export_morphism = #export_morph oo the_class_data; + +fun print_classes thy = + let + val ctxt = ProofContext.init_global thy; + 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) + (Sorts.arities_of algebra); + val the_arities = these o Symtab.lookup arities; + fun mk_arity class tyco = + let + val Ss = Sorts.mg_domain algebra tyco [class]; + in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; + fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " + ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); + fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ + (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), + (SOME o Pretty.block) [Pretty.str "supersort: ", + (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes 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_info 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 register class sups params base_sort base_morph export_morph + axiom assm_intro of_class thy = + let + val operations = map (fn (v_ty as (_, ty), (c, _)) => + (c, (class, (ty, Free v_ty)))) params; + val add_class = Graph.new_node (class, + make_class_data (((map o pairself) fst params, base_sort, + base_morph, export_morph, assm_intro, of_class, axiom), ([], operations))) + #> fold (curry Graph.add_edge class) sups; + in ClassData.map add_class thy end; + +fun activate_defs class thms thy = case Element.eq_morphism thy thms + of SOME eq_morph => fold (fn cls => fn thy => + Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) + (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy + | NONE => thy; -(** class definitions **) +fun register_operation class (c, (t, some_def)) thy = + let + val base_sort = base_sort thy class; + val prep_typ = map_type_tfree + (fn (v, sort) => if Name.aT = v + then TFree (v, base_sort) else TVar ((v, 0), sort)); + val t' = map_types prep_typ t; + val ty' = Term.fastype_of t'; + in + thy + |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) + (fn (defs, operations) => + (fold cons (the_list some_def) defs, + (c, (class, (ty', t'))) :: operations)) + |> activate_defs class (the_list some_def) + end; + +fun register_subclass (sub, sup) some_dep_morph some_wit export thy = + let + val intros = (snd o rules thy) sup :: map_filter I + [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, + (fst o rules thy) sub]; + val tac = EVERY (map (TRYALL o Tactic.rtac) intros); + val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) + (K tac); + val diff_sort = Sign.complete_sort thy [sup] + |> subtract (op =) (Sign.complete_sort thy [sub]) + |> filter (is_class thy); + val add_dependency = case some_dep_morph + of SOME dep_morph => Locale.add_dependency sub + (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export + | NONE => I + in + thy + |> AxClass.add_classrel classrel + |> ClassData.map (Graph.add_edge (sub, sup)) + |> activate_defs sub (these_defs thy diff_sort) + |> add_dependency + end; + + +(** classes and class target **) + +(* class context syntax *) + +fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) + o these_operations thy; + +fun redeclare_const thy c = + let val b = Long_Name.base_name c + in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; + +fun synchronize_class_syntax sort base_sort ctxt = + let + val thy = ProofContext.theory_of ctxt; + val algebra = Sign.classes_of thy; + val operations = these_operations thy sort; + fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); + val primary_constraints = + (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; + val secondary_constraints = + (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; + fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c + of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty + of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) + of SOME (_, ty' as TVar (vi, sort)) => + if Type_Infer.is_param vi + andalso Sorts.sort_le algebra (base_sort, sort) + then SOME (ty', TFree (Name.aT, base_sort)) + else NONE + | _ => NONE) + | NONE => NONE) + | NONE => NONE) + fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); + val unchecks = these_unchecks thy sort; + in + ctxt + |> fold (redeclare_const thy o fst) primary_constraints + |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), + (((improve, subst), true), unchecks)), false)) + |> Overloading.set_primary_constraints + end; + +fun refresh_syntax class ctxt = + let + val thy = ProofContext.theory_of ctxt; + val base_sort = base_sort thy class; + in synchronize_class_syntax [class] base_sort ctxt end; + +fun redeclare_operations thy sort = + fold (redeclare_const thy o fst) (these_operations thy sort); + +fun begin sort base_sort ctxt = + ctxt + |> Variable.declare_term + (Logic.mk_type (TFree (Name.aT, base_sort))) + |> synchronize_class_syntax sort base_sort + |> Overloading.add_improvable_syntax; + +fun init class thy = + thy + |> Locale.init class + |> begin [class] (base_sort thy class); + + +(* class target *) + +val class_prefix = Logic.const_of_class o Long_Name.base_name; + +fun declare class ((c, mx), (type_params, dict)) thy = + let + val morph = morphism thy class; + val b = Morphism.binding morph c; + val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); + val c' = Sign.full_name thy b; + val dict' = Morphism.term morph dict; + val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict'; + val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') + |> map_types Type.strip_sorts; + in + thy + |> Sign.declare_const ((b, Type.strip_sorts ty'), mx) + |> snd + |> Thm.add_def false false (b_def, def_eq) + |>> apsnd Thm.varifyT_global + |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) + #> snd + #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) + |> Sign.add_const_constraint (c', SOME ty') + end; + +fun abbrev class prmode ((c, mx), rhs) thy = + let + val morph = morphism thy class; + val unchecks = these_unchecks thy [class]; + val b = Morphism.binding morph c; + val c' = Sign.full_name thy b; + val rhs' = Pattern.rewrite_term thy unchecks [] rhs; + val ty' = Term.fastype_of rhs'; + val rhs'' = map_types Logic.varifyT_global rhs'; + in + thy + |> Sign.add_abbrev (#1 prmode) (b, rhs'') + |> snd + |> Sign.add_const_constraint (c', SOME ty') + |> Sign.notation true prmode [(Const (c', ty'), mx)] + |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) + end; + + +(* simple subclasses *) local -(* calculating class-related rules including canonical interpretation *) - -fun calculate thy class sups base_sort param_map assm_axiom = - let - val empty_ctxt = ProofContext.init_global thy; - - (* instantiation of canonical interpretation *) - val aT = TFree (Name.aT, base_sort); - val param_map_const = (map o apsnd) Const param_map; - val param_map_inst = (map o apsnd) - (Const o apsnd (map_atyps (K aT))) param_map; - val const_morph = Element.inst_morphism thy - (Symtab.empty, Symtab.make param_map_inst); - val typ_morph = Element.inst_morphism thy - (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty); - val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt - |> Expression.cert_goal_expression ([(class, (("", false), - Expression.Named param_map_const))], []); - val (props, inst_morph) = if null param_map - then (raw_props |> map (Morphism.term typ_morph), - raw_inst_morph $> typ_morph) - else (raw_props, raw_inst_morph); (*FIXME proper handling in - locale.ML / expression.ML would be desirable*) - - (* witness for canonical interpretation *) - val prop = try the_single props; - val wit = Option.map (fn prop => let - val sup_axioms = map_filter (fst o Class_Target.rules thy) sups; - val loc_intro_tac = case Locale.intros_of thy class - of (_, NONE) => all_tac - | (_, SOME intro) => ALLGOALS (Tactic.rtac intro); - val tac = loc_intro_tac - THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom)) - in Element.prove_witness empty_ctxt prop tac end) prop; - val axiom = Option.map Element.conclude_witness wit; - - (* canonical interpretation *) - val base_morph = inst_morph - $> Morphism.binding_morphism (Binding.prefix false (Class_Target.class_prefix class)) - $> Element.satisfy_morphism (the_list wit); - val eq_morph = Element.eq_morphism thy (Class_Target.these_defs thy sups); - - (* assm_intro *) - fun prove_assm_intro thm = - let - val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; - val const_eq_morph = case eq_morph - of SOME eq_morph => const_morph $> eq_morph - | NONE => const_morph - val thm'' = Morphism.thm const_eq_morph thm'; - val tac = ALLGOALS (ProofContext.fact_tac [thm'']); - in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; - val assm_intro = Option.map prove_assm_intro - (fst (Locale.intros_of thy class)); - - (* of_class *) - val of_class_prop_concl = Logic.mk_of_class (aT, class); - val of_class_prop = case prop of NONE => of_class_prop_concl - | SOME prop => Logic.mk_implies (Morphism.term const_morph - ((map_types o map_atyps) (K aT) prop), of_class_prop_concl); - val sup_of_classes = map (snd o Class_Target.rules thy) sups; - val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); - val axclass_intro = #intro (AxClass.get_info thy class); - val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort); - val tac = REPEAT (SOMEGOAL - (Tactic.match_tac (axclass_intro :: sup_of_classes - @ loc_axiom_intros @ base_sort_trivs) - ORELSE' Tactic.assume_tac)); - val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac); - - in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end; - - -(* reading and processing class specifications *) - -fun prep_class_elems prep_decl thy sups raw_elems = +fun gen_classrel mk_prop classrel thy = let - - (* user space type system: only permits 'a type variable, improves towards 'a *) - val algebra = Sign.classes_of thy; - val inter_sort = curry (Sorts.inter_sort algebra); - val proto_base_sort = if null sups then Sign.defaultS thy - else fold inter_sort (map (Class_Target.base_sort thy) sups) []; - val base_constraints = (map o apsnd) - (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd) - (Class_Target.these_operations thy sups); - val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) => - if v = Name.aT then T - else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") - | T => T); - fun singleton_fixate Ts = - let - fun extract f = (fold o fold_atyps) f Ts []; - val tfrees = extract - (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I); - val inferred_sort = extract - (fn TVar (_, sort) => inter_sort sort | _ => I); - val fixate_sort = if null tfrees then inferred_sort - else case tfrees - of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort) - then inter_sort a_sort inferred_sort - else error ("Type inference imposes additional sort constraint " - ^ Syntax.string_of_sort_global thy inferred_sort - ^ " of type parameter " ^ Name.aT ^ " of sort " - ^ Syntax.string_of_sort_global thy a_sort ^ ".") - | _ => error "Multiple type variables in class specification."; - in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end; - fun add_typ_check level name f = Context.proof_map - (Syntax.add_typ_check level name (fn xs => fn ctxt => - let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); - - (* preprocessing elements, retrieving base sort from type-checked elements *) - val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints - #> Class_Target.redeclare_operations thy sups - #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc - #> add_typ_check ~10 "singleton_fixate" singleton_fixate; - val raw_supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional []))) sups, []); - val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy - |> prep_decl raw_supexpr init_class_body raw_elems; - fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs - | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs - | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => - fold_types f t #> (fold o fold_types) f ts) o snd) assms - | fold_element_types f (Element.Defines _) = - error ("\"defines\" element not allowed in class specification.") - | fold_element_types f (Element.Notes _) = - error ("\"notes\" element not allowed in class specification."); - val base_sort = if null inferred_elems then proto_base_sort else - case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] - of [] => error "No type variable in class specification" - | [(_, sort)] => sort - | _ => error "Multiple type variables in class specification"; - val supparams = map (fn ((c, T), _) => - (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams; - val supparam_names = map fst supparams; - fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c); - val supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups, - map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams); - - in (base_sort, supparam_names, supexpr, inferred_elems) end; - -val cert_class_elems = prep_class_elems Expression.cert_declaration; -val read_class_elems = prep_class_elems Expression.cert_read_declaration; - -fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems = - let - - (* prepare import *) - val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); - val sups = map (prep_class thy) raw_supclasses - |> Sign.minimize_sort thy; - val _ = case filter_out (Class_Target.is_class thy) sups - of [] => () - | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes)); - val raw_supparams = (map o apsnd) (snd o snd) (Class_Target.these_params thy sups); - val raw_supparam_names = map fst raw_supparams; - val _ = if has_duplicates (op =) raw_supparam_names - then error ("Duplicate parameter(s) in superclasses: " - ^ (commas o map quote o duplicates (op =)) raw_supparam_names) - else (); - - (* infer types and base sort *) - val (base_sort, supparam_names, supexpr, inferred_elems) = - prep_class_elems thy sups raw_elems; - val sup_sort = inter_sort base_sort sups; - - (* process elements as class specification *) - val class_ctxt = Class_Target.begin sups base_sort (ProofContext.init_global thy); - val ((_, _, syntax_elems), _) = class_ctxt - |> Expression.cert_declaration supexpr I inferred_elems; - fun check_vars e vs = if null vs - then error ("No type variable in part of specification element " - ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) - else (); - fun check_element (e as Element.Fixes fxs) = - map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs - | check_element (e as Element.Assumes assms) = - maps (fn (_, ts_pss) => map - (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms - | check_element e = [()]; - val _ = map check_element syntax_elems; - fun fork_syn (Element.Fixes xs) = - fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs - #>> Element.Fixes - | fork_syn x = pair x; - val (elems, global_syntax) = fold_map fork_syn syntax_elems []; - - in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end; - -val cert_class_spec = prep_class_spec (K I) cert_class_elems; -val read_class_spec = prep_class_spec Sign.intern_class read_class_elems; - - -(* class establishment *) - -fun add_consts class base_sort sups supparam_names global_syntax thy = - let - (*FIXME simplify*) - val supconsts = supparam_names - |> AList.make (snd o the o AList.lookup (op =) (Class_Target.these_params thy sups)) - |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); - val all_params = Locale.params_of thy class; - val raw_params = (snd o chop (length supparam_names)) all_params; - fun add_const ((raw_c, raw_ty), _) thy = - let - val b = Binding.name raw_c; - val c = Sign.full_name thy b; - val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; - val ty0 = Type.strip_sorts ty; - val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; - val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b; - in - thy - |> Sign.declare_const ((b, ty0), syn) - |> snd - |> pair ((Name.of_binding b, ty), (c, ty')) - end; + fun after_qed results = + ProofContext.theory ((fold o fold) AxClass.add_classrel results); in thy - |> Sign.add_path (Class_Target.class_prefix class) - |> fold_map add_const raw_params - ||> Sign.restore_naming thy - |-> (fn params => pair (supconsts @ (map o apfst) fst params, params)) - end; - -fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy = - let - (*FIXME simplify*) - fun globalize param_map = map_aterms - (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) - | t => t); - val raw_pred = Locale.intros_of thy class - |> fst - |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); - fun get_axiom thy = case (#axioms o AxClass.get_info thy) class - of [] => NONE - | [thm] => SOME thm; - in - thy - |> add_consts class base_sort sups supparam_names global_syntax - |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) - (map (fst o snd) params) - [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)] - #> snd - #> `get_axiom - #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params - #> pair (param_map, params, assm_axiom))) - end; - -fun gen_class prep_class_spec b raw_supclasses raw_elems thy = - let - val class = Sign.full_name thy b; - val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) = - prep_class_spec thy raw_supclasses raw_elems; - in - thy - |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems - |> snd |> Local_Theory.exit_global - |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax - ||> Theory.checkpoint - |-> (fn (param_map, params, assm_axiom) => - `(fn thy => calculate thy class sups base_sort param_map assm_axiom) - #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => - Context.theory_map (Locale.add_registration (class, base_morph) - (Option.map (rpair true) eq_morph) export_morph) - #> Class_Target.register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) - |> Named_Target.init (SOME class) - |> pair class + |> ProofContext.init_global + |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] end; in -val class = gen_class cert_class_spec; -val class_cmd = gen_class read_class_spec; +val classrel = + gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); +val classrel_cmd = + gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); end; (*local*) -(** subclass relations **) +(** instantiation target **) + +(* bookkeeping *) + +datatype instantiation = Instantiation of { + arities: string list * (string * sort) list * sort, + params: ((string * string) * (string * typ)) list + (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) +} + +structure Instantiation = Proof_Data +( + type T = instantiation + fun init _ = Instantiation { arities = ([], [], []), params = [] }; +); + +fun mk_instantiation (arities, params) = + Instantiation { arities = arities, params = params }; +fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) + of Instantiation data => data; +fun map_instantiation f = (Local_Theory.target o Instantiation.map) + (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); -local +fun the_instantiation lthy = case get_instantiation lthy + of { arities = ([], [], []), ... } => error "No instantiation target" + | data => data; + +val instantiation_params = #params o get_instantiation; + +fun instantiation_param lthy b = instantiation_params lthy + |> find_first (fn (_, (v, _)) => Binding.name_of b = v) + |> Option.map (fst o fst); -fun gen_subclass prep_class do_proof raw_sup lthy = +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = + let + val ctxt = ProofContext.init_global thy; + val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt + (raw_tyco, raw_sorts, raw_sort)) raw_tycos; + val tycos = map #1 all_arities; + val (_, sorts, sort) = hd all_arities; + val vs = Name.names Name.context Name.aT sorts; + in (tycos, vs, sort) end; + + +(* syntax *) + +fun synchronize_inst_syntax ctxt = let - val thy = ProofContext.theory_of lthy; - val proto_sup = prep_class thy raw_sup; - val proto_sub = case Named_Target.peek lthy - of {is_class = false, ...} => error "Not in a class context" - | {target, ...} => target; - val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); + val Instantiation { params, ... } = Instantiation.get ctxt; + + val lookup_inst_param = AxClass.lookup_inst_param + (Sign.consts_of (ProofContext.theory_of ctxt)) params; + fun subst (c, ty) = case lookup_inst_param (c, ty) + of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) + | NONE => NONE; + val unchecks = + map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; + in + ctxt + |> Overloading.map_improvable_syntax + (fn (((primary_constraints, _), (((improve, _), _), _)), _) => + (((primary_constraints, []), (((improve, subst), false), unchecks)), false)) + end; + + +(* target *) + +val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) + let + fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s + orelse s = "'" orelse s = "_"; + val is_junk = not o is_valid andf Symbol.is_regular; + val junk = Scan.many is_junk; + val scan_valids = Symbol.scanner "Malformed input" + ((junk |-- + (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) + --| junk)) + ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); + in + explode #> scan_valids #> implode + end; + +val type_name = sanitize_name o Long_Name.base_name; + +fun resort_terms pp algebra consts constraints ts = + let + fun matchings (Const (c_ty as (c, _))) = (case constraints c + of NONE => I + | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) + (Consts.typargs consts c_ty) sorts) + | matchings _ = I + val tvartab = (fold o fold_aterms) matchings ts Vartab.empty + handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); + val inst = map_type_tvar + (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); + in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; - val expr = ([(sup, (("", false), Expression.Positional []))], []); - val (([props], deps, export), goal_ctxt) = - Expression.cert_goal_expression expr lthy; - val some_prop = try the_single props; - val some_dep_morph = try the_single (map snd deps); - fun after_qed some_wit = - ProofContext.theory (Class_Target.register_subclass (sub, sup) - some_dep_morph some_wit export) - #> ProofContext.theory_of #> Named_Target.init (SOME sub); - in do_proof after_qed some_prop goal_ctxt end; +fun init_instantiation (tycos, vs, sort) thy = + let + val _ = if null tycos then error "At least one arity must be given" else (); + val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); + fun get_param tyco (param, (_, (c, ty))) = + if can (AxClass.param_of_inst thy) (c, tyco) + then NONE else SOME ((c, tyco), + (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); + val params = map_product get_param tycos class_params |> map_filter I; + val primary_constraints = map (apsnd + (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; + val pp = Syntax.pp_global thy; + val algebra = Sign.classes_of thy + |> fold (fn tyco => Sorts.add_arities pp + (tyco, map (fn class => (class, map snd vs)) sort)) tycos; + val consts = Sign.consts_of thy; + val improve_constraints = AList.lookup (op =) + (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); + fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts + of NONE => NONE + | SOME ts' => SOME (ts', ctxt); + val lookup_inst_param = AxClass.lookup_inst_param consts params; + val typ_instance = Type.typ_instance (Sign.tsig_of thy); + fun improve (c, ty) = case lookup_inst_param (c, ty) + of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE + | NONE => NONE; + in + thy + |> Theory.checkpoint + |> ProofContext.init_global + |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) + |> fold (Variable.declare_typ o TFree) vs + |> fold (Variable.declare_names o Free o snd) params + |> (Overloading.map_improvable_syntax o apfst) + (K ((primary_constraints, []), (((improve, K NONE), false), []))) + |> Overloading.add_improvable_syntax + |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) + |> synchronize_inst_syntax + end; + +fun confirm_declaration b = (map_instantiation o apsnd) + (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) + #> Local_Theory.target synchronize_inst_syntax + +fun gen_instantiation_instance do_proof after_qed lthy = + let + val (tycos, vs, sort) = (#arities o the_instantiation) lthy; + val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; + fun after_qed' results = + Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) + #> after_qed; + in + lthy + |> do_proof after_qed' arities_proof + end; + +val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => + Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); + +fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => + fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t + (fn {context, ...} => tac context)) ts) lthy) I; + +fun prove_instantiation_exit tac = prove_instantiation_instance tac + #> Local_Theory.exit_global; + +fun prove_instantiation_exit_result f tac x lthy = + let + val morph = ProofContext.export_morphism lthy + (ProofContext.init_global (ProofContext.theory_of lthy)); + val y = f morph x; + in + lthy + |> prove_instantiation_exit (fn ctxt => tac ctxt y) + |> pair y + end; -fun user_proof after_qed some_prop = - Element.witness_proof (after_qed o try the_single o the_single) - [the_list some_prop]; +fun conclude_instantiation lthy = + let + val (tycos, vs, sort) = (#arities o the_instantiation) lthy; + val thy = ProofContext.theory_of lthy; + val _ = map (fn tyco => if Sign.of_sort thy + (Type (tyco, map TFree vs), sort) + then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) + tycos; + in lthy end; -fun tactic_proof tac after_qed some_prop ctxt = - after_qed (Option.map - (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt; +fun pretty_instantiation lthy = + let + val { arities = (tycos, vs, sort), params } = the_instantiation lthy; + val thy = ProofContext.theory_of lthy; + fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); + fun pr_param ((c, _), (v, ty)) = + (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", + (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; + in + (Pretty.block o Pretty.fbreaks) + (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) + end; + +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); + +fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = + case instantiation_param lthy b + of SOME c => if mx <> NoSyn then syntax_error c + else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U) + ##>> AxClass.define_overloaded b_def (c, rhs)) + ||> confirm_declaration b + | NONE => lthy |> + Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); -in +fun instantiation arities thy = + thy + |> init_instantiation arities + |> Local_Theory.init NONE "" + {define = Generic_Target.define instantiation_foundation, + notes = Generic_Target.notes + (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), + abbrev = Generic_Target.abbrev + (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), + declaration = K Generic_Target.theory_declaration, + syntax_declaration = K Generic_Target.theory_declaration, + pretty = single o pretty_instantiation, + reinit = instantiation arities o ProofContext.theory_of, + exit = Local_Theory.target_of o conclude_instantiation}; + +fun instantiation_cmd arities thy = + instantiation (read_multi_arity thy arities) thy; + + +(* simplified instantiation interface with no class parameter *) -val subclass = gen_subclass (K I) user_proof; -fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof; +fun instance_arity_cmd raw_arities thy = + let + val (tycos, vs, sort) = read_multi_arity thy raw_arities; + val sorts = map snd vs; + val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; + fun after_qed results = ProofContext.theory + ((fold o fold) AxClass.add_arity results); + in + thy + |> ProofContext.init_global + |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) + end; + + +(** tactics and methods **) -end; (*local*) +fun intro_classes_tac facts st = + let + val thy = Thm.theory_of_thm st; + val classes = Sign.all_classes thy; + val class_trivs = map (Thm.class_triv thy) classes; + val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; + val assm_intros = all_assm_intros thy; + in + Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st + end; + +fun default_intro_tac ctxt [] = + intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] + | default_intro_tac _ _ = no_tac; + +fun default_tac rules ctxt facts = + HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE + default_intro_tac ctxt facts; + +val _ = Context.>> (Context.map_theory + (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) + "back-chain introduction rules of classes" #> + Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) + "apply some intro/elim rule")); end; + diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/Isar/class_declaration.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/class_declaration.ML Wed Aug 11 16:02:03 2010 +0200 @@ -0,0 +1,345 @@ +(* Title: Pure/Isar/class_declaration.ML + Author: Florian Haftmann, TU Muenchen + +Declaring classes and subclass relations. +*) + +signature CLASS_DECLARATION = +sig + val class: binding -> class list -> Element.context_i list + -> theory -> string * local_theory + val class_cmd: binding -> xstring list -> Element.context list + -> theory -> string * local_theory + val prove_subclass: tactic -> class -> local_theory -> local_theory + val subclass: class -> local_theory -> Proof.state + val subclass_cmd: xstring -> local_theory -> Proof.state +end; + +structure Class_Declaration: CLASS_DECLARATION = +struct + +(** class definitions **) + +local + +(* calculating class-related rules including canonical interpretation *) + +fun calculate thy class sups base_sort param_map assm_axiom = + let + val empty_ctxt = ProofContext.init_global thy; + + (* instantiation of canonical interpretation *) + val aT = TFree (Name.aT, base_sort); + val param_map_const = (map o apsnd) Const param_map; + val param_map_inst = (map o apsnd) + (Const o apsnd (map_atyps (K aT))) param_map; + val const_morph = Element.inst_morphism thy + (Symtab.empty, Symtab.make param_map_inst); + val typ_morph = Element.inst_morphism thy + (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty); + val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt + |> Expression.cert_goal_expression ([(class, (("", false), + Expression.Named param_map_const))], []); + val (props, inst_morph) = if null param_map + then (raw_props |> map (Morphism.term typ_morph), + raw_inst_morph $> typ_morph) + else (raw_props, raw_inst_morph); (*FIXME proper handling in + locale.ML / expression.ML would be desirable*) + + (* witness for canonical interpretation *) + val prop = try the_single props; + val wit = Option.map (fn prop => let + val sup_axioms = map_filter (fst o Class.rules thy) sups; + val loc_intro_tac = case Locale.intros_of thy class + of (_, NONE) => all_tac + | (_, SOME intro) => ALLGOALS (Tactic.rtac intro); + val tac = loc_intro_tac + THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom)) + in Element.prove_witness empty_ctxt prop tac end) prop; + val axiom = Option.map Element.conclude_witness wit; + + (* canonical interpretation *) + val base_morph = inst_morph + $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class)) + $> Element.satisfy_morphism (the_list wit); + val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups); + + (* assm_intro *) + fun prove_assm_intro thm = + let + val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; + val const_eq_morph = case eq_morph + of SOME eq_morph => const_morph $> eq_morph + | NONE => const_morph + val thm'' = Morphism.thm const_eq_morph thm'; + val tac = ALLGOALS (ProofContext.fact_tac [thm'']); + in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; + val assm_intro = Option.map prove_assm_intro + (fst (Locale.intros_of thy class)); + + (* of_class *) + val of_class_prop_concl = Logic.mk_of_class (aT, class); + val of_class_prop = case prop of NONE => of_class_prop_concl + | SOME prop => Logic.mk_implies (Morphism.term const_morph + ((map_types o map_atyps) (K aT) prop), of_class_prop_concl); + val sup_of_classes = map (snd o Class.rules thy) sups; + val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); + val axclass_intro = #intro (AxClass.get_info thy class); + val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort); + val tac = REPEAT (SOMEGOAL + (Tactic.match_tac (axclass_intro :: sup_of_classes + @ loc_axiom_intros @ base_sort_trivs) + ORELSE' Tactic.assume_tac)); + val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac); + + in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end; + + +(* reading and processing class specifications *) + +fun prep_class_elems prep_decl thy sups raw_elems = + let + + (* user space type system: only permits 'a type variable, improves towards 'a *) + val algebra = Sign.classes_of thy; + val inter_sort = curry (Sorts.inter_sort algebra); + val proto_base_sort = if null sups then Sign.defaultS thy + else fold inter_sort (map (Class.base_sort thy) sups) []; + val base_constraints = (map o apsnd) + (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd) + (Class.these_operations thy sups); + val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) => + if v = Name.aT then T + else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") + | T => T); + fun singleton_fixate Ts = + let + fun extract f = (fold o fold_atyps) f Ts []; + val tfrees = extract + (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I); + val inferred_sort = extract + (fn TVar (_, sort) => inter_sort sort | _ => I); + val fixate_sort = if null tfrees then inferred_sort + else case tfrees + of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort) + then inter_sort a_sort inferred_sort + else error ("Type inference imposes additional sort constraint " + ^ Syntax.string_of_sort_global thy inferred_sort + ^ " of type parameter " ^ Name.aT ^ " of sort " + ^ Syntax.string_of_sort_global thy a_sort ^ ".") + | _ => error "Multiple type variables in class specification."; + in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end; + fun add_typ_check level name f = Context.proof_map + (Syntax.add_typ_check level name (fn xs => fn ctxt => + let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); + + (* preprocessing elements, retrieving base sort from type-checked elements *) + val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints + #> Class.redeclare_operations thy sups + #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc + #> add_typ_check ~10 "singleton_fixate" singleton_fixate; + val raw_supexpr = (map (fn sup => (sup, (("", false), + Expression.Positional []))) sups, []); + val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy + |> prep_decl raw_supexpr init_class_body raw_elems; + fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs + | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs + | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => + fold_types f t #> (fold o fold_types) f ts) o snd) assms + | fold_element_types f (Element.Defines _) = + error ("\"defines\" element not allowed in class specification.") + | fold_element_types f (Element.Notes _) = + error ("\"notes\" element not allowed in class specification."); + val base_sort = if null inferred_elems then proto_base_sort else + case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] + of [] => error "No type variable in class specification" + | [(_, sort)] => sort + | _ => error "Multiple type variables in class specification"; + val supparams = map (fn ((c, T), _) => + (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams; + val supparam_names = map fst supparams; + fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c); + val supexpr = (map (fn sup => (sup, (("", false), + Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups, + map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams); + + in (base_sort, supparam_names, supexpr, inferred_elems) end; + +val cert_class_elems = prep_class_elems Expression.cert_declaration; +val read_class_elems = prep_class_elems Expression.cert_read_declaration; + +fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems = + let + + (* prepare import *) + val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); + val sups = map (prep_class thy) raw_supclasses + |> Sign.minimize_sort thy; + val _ = case filter_out (Class.is_class thy) sups + of [] => () + | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes)); + val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups); + val raw_supparam_names = map fst raw_supparams; + val _ = if has_duplicates (op =) raw_supparam_names + then error ("Duplicate parameter(s) in superclasses: " + ^ (commas o map quote o duplicates (op =)) raw_supparam_names) + else (); + + (* infer types and base sort *) + val (base_sort, supparam_names, supexpr, inferred_elems) = + prep_class_elems thy sups raw_elems; + val sup_sort = inter_sort base_sort sups; + + (* process elements as class specification *) + val class_ctxt = Class.begin sups base_sort (ProofContext.init_global thy); + val ((_, _, syntax_elems), _) = class_ctxt + |> Expression.cert_declaration supexpr I inferred_elems; + fun check_vars e vs = if null vs + then error ("No type variable in part of specification element " + ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) + else (); + fun check_element (e as Element.Fixes fxs) = + map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs + | check_element (e as Element.Assumes assms) = + maps (fn (_, ts_pss) => map + (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms + | check_element e = [()]; + val _ = map check_element syntax_elems; + fun fork_syn (Element.Fixes xs) = + fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs + #>> Element.Fixes + | fork_syn x = pair x; + val (elems, global_syntax) = fold_map fork_syn syntax_elems []; + + in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end; + +val cert_class_spec = prep_class_spec (K I) cert_class_elems; +val read_class_spec = prep_class_spec Sign.intern_class read_class_elems; + + +(* class establishment *) + +fun add_consts class base_sort sups supparam_names global_syntax thy = + let + (*FIXME simplify*) + val supconsts = supparam_names + |> AList.make (snd o the o AList.lookup (op =) (Class.these_params thy sups)) + |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); + val all_params = Locale.params_of thy class; + val raw_params = (snd o chop (length supparam_names)) all_params; + fun add_const ((raw_c, raw_ty), _) thy = + let + val b = Binding.name raw_c; + val c = Sign.full_name thy b; + val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; + val ty0 = Type.strip_sorts ty; + val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; + val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b; + in + thy + |> Sign.declare_const ((b, ty0), syn) + |> snd + |> pair ((Name.of_binding b, ty), (c, ty')) + end; + in + thy + |> Sign.add_path (Class.class_prefix class) + |> fold_map add_const raw_params + ||> Sign.restore_naming thy + |-> (fn params => pair (supconsts @ (map o apfst) fst params, params)) + end; + +fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy = + let + (*FIXME simplify*) + fun globalize param_map = map_aterms + (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) + | t => t); + val raw_pred = Locale.intros_of thy class + |> fst + |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); + fun get_axiom thy = case (#axioms o AxClass.get_info thy) class + of [] => NONE + | [thm] => SOME thm; + in + thy + |> add_consts class base_sort sups supparam_names global_syntax + |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) + (map (fst o snd) params) + [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)] + #> snd + #> `get_axiom + #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params + #> pair (param_map, params, assm_axiom))) + end; + +fun gen_class prep_class_spec b raw_supclasses raw_elems thy = + let + val class = Sign.full_name thy b; + val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) = + prep_class_spec thy raw_supclasses raw_elems; + in + thy + |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems + |> snd |> Local_Theory.exit_global + |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax + ||> Theory.checkpoint + |-> (fn (param_map, params, assm_axiom) => + `(fn thy => calculate thy class sups base_sort param_map assm_axiom) + #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => + Context.theory_map (Locale.add_registration (class, base_morph) + (Option.map (rpair true) eq_morph) export_morph) + #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) + |> Named_Target.init (SOME class) + |> pair class + end; + +in + +val class = gen_class cert_class_spec; +val class_cmd = gen_class read_class_spec; + +end; (*local*) + + +(** subclass relations **) + +local + +fun gen_subclass prep_class do_proof raw_sup lthy = + let + val thy = ProofContext.theory_of lthy; + val proto_sup = prep_class thy raw_sup; + val proto_sub = case Named_Target.peek lthy + of {is_class = false, ...} => error "Not in a class context" + | {target, ...} => target; + val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); + + val expr = ([(sup, (("", false), Expression.Positional []))], []); + val (([props], deps, export), goal_ctxt) = + Expression.cert_goal_expression expr lthy; + val some_prop = try the_single props; + val some_dep_morph = try the_single (map snd deps); + fun after_qed some_wit = + ProofContext.theory (Class.register_subclass (sub, sup) + some_dep_morph some_wit export) + #> ProofContext.theory_of #> Named_Target.init (SOME sub); + in do_proof after_qed some_prop goal_ctxt end; + +fun user_proof after_qed some_prop = + Element.witness_proof (after_qed o try the_single o the_single) + [the_list some_prop]; + +fun tactic_proof tac after_qed some_prop ctxt = + after_qed (Option.map + (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt; + +in + +val subclass = gen_subclass (K I) user_proof; +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); +val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof; + +end; (*local*) + +end; diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Wed Aug 11 15:45:15 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,657 +0,0 @@ -(* Title: Pure/Isar/class_target.ML - Author: Florian Haftmann, TU Muenchen - -Type classes derived from primitive axclasses and locales -- mechanisms. -*) - -signature CLASS_TARGET = -sig - (*classes*) - val is_class: theory -> class -> bool - val these_params: theory -> sort -> (string * (class * (string * typ))) list - val print_classes: theory -> unit - - val init: class -> theory -> Proof.context - val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory - val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory - val class_prefix: string -> string - val refresh_syntax: class -> Proof.context -> Proof.context - - (*instances*) - val instantiation_instance: (local_theory -> local_theory) - -> local_theory -> Proof.state - val prove_instantiation_instance: (Proof.context -> tactic) - -> local_theory -> local_theory - val prove_instantiation_exit: (Proof.context -> tactic) - -> local_theory -> theory - val prove_instantiation_exit_result: (morphism -> 'a -> 'b) - -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory - val read_multi_arity: theory -> xstring list * xstring list * xstring - -> string list * (string * sort) list * sort - val type_name: string -> string - val instantiation: string list * (string * sort) list * sort -> theory -> local_theory - val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory - val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state - - (*subclasses*) - val classrel: class * class -> theory -> Proof.state - val classrel_cmd: xstring * xstring -> theory -> Proof.state - - (*tactics*) - val intro_classes_tac: thm list -> tactic - val default_intro_tac: Proof.context -> thm list -> tactic -end; - -signature PRIVATE_CLASS_TARGET = -sig - include CLASS_TARGET - val register: class -> class list -> ((string * typ) * (string * typ)) list - -> sort -> morphism -> morphism -> thm option -> thm option -> thm - -> theory -> theory - val register_subclass: class * class -> morphism option -> Element.witness option - -> morphism -> theory -> theory - val base_sort: theory -> class -> sort - val rules: theory -> class -> thm option * thm - val these_defs: theory -> sort -> thm list - val these_operations: theory -> sort - -> (string * (class * (typ * term))) list - val begin: class list -> sort -> Proof.context -> Proof.context - val redeclare_operations: theory -> sort -> Proof.context -> Proof.context -end; - -structure Class_Target: PRIVATE_CLASS_TARGET = -struct - -(** class data **) - -datatype class_data = ClassData of { - - (* static part *) - consts: (string * string) list - (*locale parameter ~> constant name*), - base_sort: sort, - base_morph: morphism - (*static part of canonical morphism*), - export_morph: morphism, - assm_intro: thm option, - of_class: thm, - axiom: thm option, - - (* dynamic part *) - defs: thm list, - operations: (string * (class * (typ * term))) list - -}; - -fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), - (defs, operations)) = - ClassData { consts = consts, base_sort = base_sort, - base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, - of_class = of_class, axiom = axiom, defs = defs, operations = operations }; -fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro, - of_class, axiom, defs, operations }) = - make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), - (defs, operations))); -fun merge_class_data _ (ClassData { consts = consts, - base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, - of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, - ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, - of_class = _, axiom = _, defs = defs2, operations = operations2 }) = - make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), - (Thm.merge_thms (defs1, defs2), - AList.merge (op =) (K true) (operations1, operations2))); - -structure ClassData = Theory_Data -( - type T = class_data Graph.T - val empty = Graph.empty; - val extend = I; - val merge = Graph.join merge_class_data; -); - - -(* queries *) - -fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class - of SOME (ClassData data) => SOME data - | NONE => NONE; - -fun the_class_data thy class = case lookup_class_data thy class - of NONE => error ("Undeclared class " ^ quote class) - | SOME data => data; - -val is_class = is_some oo lookup_class_data; - -val ancestry = Graph.all_succs o ClassData.get; -val heritage = Graph.all_preds o ClassData.get; - -fun these_params thy = - let - fun params class = - let - val const_typs = (#params o AxClass.get_info thy) class; - val const_names = (#consts o the_class_data thy) class; - in - (map o apsnd) - (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names - end; - in maps params o ancestry thy end; - -val base_sort = #base_sort oo the_class_data; - -fun rules thy class = - let val { axiom, of_class, ... } = the_class_data thy class - in (axiom, of_class) end; - -fun all_assm_intros thy = - Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm) - (the_list assm_intro)) (ClassData.get thy) []; - -fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; -fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; - -val base_morphism = #base_morph oo the_class_data; -fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class]) - of SOME eq_morph => base_morphism thy class $> eq_morph - | NONE => base_morphism thy class; -val export_morphism = #export_morph oo the_class_data; - -fun print_classes thy = - let - val ctxt = ProofContext.init_global thy; - 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) - (Sorts.arities_of algebra); - val the_arities = these o Symtab.lookup arities; - fun mk_arity class tyco = - let - val Ss = Sorts.mg_domain algebra tyco [class]; - in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; - fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " - ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); - fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ - (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), - (SOME o Pretty.block) [Pretty.str "supersort: ", - (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes 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_info 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 register class sups params base_sort base_morph export_morph - axiom assm_intro of_class thy = - let - val operations = map (fn (v_ty as (_, ty), (c, _)) => - (c, (class, (ty, Free v_ty)))) params; - val add_class = Graph.new_node (class, - make_class_data (((map o pairself) fst params, base_sort, - base_morph, export_morph, assm_intro, of_class, axiom), ([], operations))) - #> fold (curry Graph.add_edge class) sups; - in ClassData.map add_class thy end; - -fun activate_defs class thms thy = case Element.eq_morphism thy thms - of SOME eq_morph => fold (fn cls => fn thy => - Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) - (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy - | NONE => thy; - -fun register_operation class (c, (t, some_def)) thy = - let - val base_sort = base_sort thy class; - val prep_typ = map_type_tfree - (fn (v, sort) => if Name.aT = v - then TFree (v, base_sort) else TVar ((v, 0), sort)); - val t' = map_types prep_typ t; - val ty' = Term.fastype_of t'; - in - thy - |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) - (fn (defs, operations) => - (fold cons (the_list some_def) defs, - (c, (class, (ty', t'))) :: operations)) - |> activate_defs class (the_list some_def) - end; - -fun register_subclass (sub, sup) some_dep_morph some_wit export thy = - let - val intros = (snd o rules thy) sup :: map_filter I - [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, - (fst o rules thy) sub]; - val tac = EVERY (map (TRYALL o Tactic.rtac) intros); - val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) - (K tac); - val diff_sort = Sign.complete_sort thy [sup] - |> subtract (op =) (Sign.complete_sort thy [sub]) - |> filter (is_class thy); - val add_dependency = case some_dep_morph - of SOME dep_morph => Locale.add_dependency sub - (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export - | NONE => I - in - thy - |> AxClass.add_classrel classrel - |> ClassData.map (Graph.add_edge (sub, sup)) - |> activate_defs sub (these_defs thy diff_sort) - |> add_dependency - end; - - -(** classes and class target **) - -(* class context syntax *) - -fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) - o these_operations thy; - -fun redeclare_const thy c = - let val b = Long_Name.base_name c - in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; - -fun synchronize_class_syntax sort base_sort ctxt = - let - val thy = ProofContext.theory_of ctxt; - val algebra = Sign.classes_of thy; - val operations = these_operations thy sort; - fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); - val primary_constraints = - (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; - val secondary_constraints = - (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; - fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c - of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty - of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) - of SOME (_, ty' as TVar (vi, sort)) => - if Type_Infer.is_param vi - andalso Sorts.sort_le algebra (base_sort, sort) - then SOME (ty', TFree (Name.aT, base_sort)) - else NONE - | _ => NONE) - | NONE => NONE) - | NONE => NONE) - fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); - val unchecks = these_unchecks thy sort; - in - ctxt - |> fold (redeclare_const thy o fst) primary_constraints - |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), - (((improve, subst), true), unchecks)), false)) - |> Overloading.set_primary_constraints - end; - -fun refresh_syntax class ctxt = - let - val thy = ProofContext.theory_of ctxt; - val base_sort = base_sort thy class; - in synchronize_class_syntax [class] base_sort ctxt end; - -fun redeclare_operations thy sort = - fold (redeclare_const thy o fst) (these_operations thy sort); - -fun begin sort base_sort ctxt = - ctxt - |> Variable.declare_term - (Logic.mk_type (TFree (Name.aT, base_sort))) - |> synchronize_class_syntax sort base_sort - |> Overloading.add_improvable_syntax; - -fun init class thy = - thy - |> Locale.init class - |> begin [class] (base_sort thy class); - - -(* class target *) - -val class_prefix = Logic.const_of_class o Long_Name.base_name; - -fun declare class ((c, mx), (type_params, dict)) thy = - let - val morph = morphism thy class; - val b = Morphism.binding morph c; - val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); - val c' = Sign.full_name thy b; - val dict' = Morphism.term morph dict; - val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict'; - val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') - |> map_types Type.strip_sorts; - in - thy - |> Sign.declare_const ((b, Type.strip_sorts ty'), mx) - |> snd - |> Thm.add_def false false (b_def, def_eq) - |>> apsnd Thm.varifyT_global - |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) - #> snd - #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) - |> Sign.add_const_constraint (c', SOME ty') - end; - -fun abbrev class prmode ((c, mx), rhs) thy = - let - val morph = morphism thy class; - val unchecks = these_unchecks thy [class]; - val b = Morphism.binding morph c; - val c' = Sign.full_name thy b; - val rhs' = Pattern.rewrite_term thy unchecks [] rhs; - val ty' = Term.fastype_of rhs'; - val rhs'' = map_types Logic.varifyT_global rhs'; - in - thy - |> Sign.add_abbrev (#1 prmode) (b, rhs'') - |> snd - |> Sign.add_const_constraint (c', SOME ty') - |> Sign.notation true prmode [(Const (c', ty'), mx)] - |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) - end; - - -(* simple subclasses *) - -local - -fun gen_classrel mk_prop classrel thy = - let - fun after_qed results = - ProofContext.theory ((fold o fold) AxClass.add_classrel results); - in - thy - |> ProofContext.init_global - |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] - end; - -in - -val classrel = - gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); -val classrel_cmd = - gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); - -end; (*local*) - - -(** instantiation target **) - -(* bookkeeping *) - -datatype instantiation = Instantiation of { - arities: string list * (string * sort) list * sort, - params: ((string * string) * (string * typ)) list - (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) -} - -structure Instantiation = Proof_Data -( - type T = instantiation - fun init _ = Instantiation { arities = ([], [], []), params = [] }; -); - -fun mk_instantiation (arities, params) = - Instantiation { arities = arities, params = params }; -fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) - of Instantiation data => data; -fun map_instantiation f = (Local_Theory.target o Instantiation.map) - (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); - -fun the_instantiation lthy = case get_instantiation lthy - of { arities = ([], [], []), ... } => error "No instantiation target" - | data => data; - -val instantiation_params = #params o get_instantiation; - -fun instantiation_param lthy b = instantiation_params lthy - |> find_first (fn (_, (v, _)) => Binding.name_of b = v) - |> Option.map (fst o fst); - -fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = - let - val ctxt = ProofContext.init_global thy; - val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt - (raw_tyco, raw_sorts, raw_sort)) raw_tycos; - val tycos = map #1 all_arities; - val (_, sorts, sort) = hd all_arities; - val vs = Name.names Name.context Name.aT sorts; - in (tycos, vs, sort) end; - - -(* syntax *) - -fun synchronize_inst_syntax ctxt = - let - val Instantiation { params, ... } = Instantiation.get ctxt; - - val lookup_inst_param = AxClass.lookup_inst_param - (Sign.consts_of (ProofContext.theory_of ctxt)) params; - fun subst (c, ty) = case lookup_inst_param (c, ty) - of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) - | NONE => NONE; - val unchecks = - map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; - in - ctxt - |> Overloading.map_improvable_syntax - (fn (((primary_constraints, _), (((improve, _), _), _)), _) => - (((primary_constraints, []), (((improve, subst), false), unchecks)), false)) - end; - - -(* target *) - -val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) - let - fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s - orelse s = "'" orelse s = "_"; - val is_junk = not o is_valid andf Symbol.is_regular; - val junk = Scan.many is_junk; - val scan_valids = Symbol.scanner "Malformed input" - ((junk |-- - (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) - --| junk)) - ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); - in - explode #> scan_valids #> implode - end; - -val type_name = sanitize_name o Long_Name.base_name; - -fun resort_terms pp algebra consts constraints ts = - let - fun matchings (Const (c_ty as (c, _))) = (case constraints c - of NONE => I - | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) - (Consts.typargs consts c_ty) sorts) - | matchings _ = I - val tvartab = (fold o fold_aterms) matchings ts Vartab.empty - handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); - val inst = map_type_tvar - (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); - in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; - -fun init_instantiation (tycos, vs, sort) thy = - let - val _ = if null tycos then error "At least one arity must be given" else (); - val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); - fun get_param tyco (param, (_, (c, ty))) = - if can (AxClass.param_of_inst thy) (c, tyco) - then NONE else SOME ((c, tyco), - (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); - val params = map_product get_param tycos class_params |> map_filter I; - val primary_constraints = map (apsnd - (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; - val pp = Syntax.pp_global thy; - val algebra = Sign.classes_of thy - |> fold (fn tyco => Sorts.add_arities pp - (tyco, map (fn class => (class, map snd vs)) sort)) tycos; - val consts = Sign.consts_of thy; - val improve_constraints = AList.lookup (op =) - (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); - fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts - of NONE => NONE - | SOME ts' => SOME (ts', ctxt); - val lookup_inst_param = AxClass.lookup_inst_param consts params; - val typ_instance = Type.typ_instance (Sign.tsig_of thy); - fun improve (c, ty) = case lookup_inst_param (c, ty) - of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE - | NONE => NONE; - in - thy - |> Theory.checkpoint - |> ProofContext.init_global - |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) - |> fold (Variable.declare_typ o TFree) vs - |> fold (Variable.declare_names o Free o snd) params - |> (Overloading.map_improvable_syntax o apfst) - (K ((primary_constraints, []), (((improve, K NONE), false), []))) - |> Overloading.add_improvable_syntax - |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) - |> synchronize_inst_syntax - end; - -fun confirm_declaration b = (map_instantiation o apsnd) - (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) - #> Local_Theory.target synchronize_inst_syntax - -fun gen_instantiation_instance do_proof after_qed lthy = - let - val (tycos, vs, sort) = (#arities o the_instantiation) lthy; - val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; - fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) - #> after_qed; - in - lthy - |> do_proof after_qed' arities_proof - end; - -val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => - Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); - -fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => - fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t - (fn {context, ...} => tac context)) ts) lthy) I; - -fun prove_instantiation_exit tac = prove_instantiation_instance tac - #> Local_Theory.exit_global; - -fun prove_instantiation_exit_result f tac x lthy = - let - val morph = ProofContext.export_morphism lthy - (ProofContext.init_global (ProofContext.theory_of lthy)); - val y = f morph x; - in - lthy - |> prove_instantiation_exit (fn ctxt => tac ctxt y) - |> pair y - end; - -fun conclude_instantiation lthy = - let - val (tycos, vs, sort) = (#arities o the_instantiation) lthy; - val thy = ProofContext.theory_of lthy; - val _ = map (fn tyco => if Sign.of_sort thy - (Type (tyco, map TFree vs), sort) - then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) - tycos; - in lthy end; - -fun pretty_instantiation lthy = - let - val { arities = (tycos, vs, sort), params } = the_instantiation lthy; - val thy = ProofContext.theory_of lthy; - fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); - fun pr_param ((c, _), (v, ty)) = - (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", - (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; - in - (Pretty.block o Pretty.fbreaks) - (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) - end; - -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); - -fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = - case instantiation_param lthy b - of SOME c => if mx <> NoSyn then syntax_error c - else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U) - ##>> AxClass.define_overloaded b_def (c, rhs)) - ||> confirm_declaration b - | NONE => lthy |> - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); - -fun instantiation arities thy = - thy - |> init_instantiation arities - |> Local_Theory.init NONE "" - {define = Generic_Target.define instantiation_foundation, - notes = Generic_Target.notes - (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), - abbrev = Generic_Target.abbrev - (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), - declaration = K Generic_Target.theory_declaration, - syntax_declaration = K Generic_Target.theory_declaration, - pretty = single o pretty_instantiation, - reinit = instantiation arities o ProofContext.theory_of, - exit = Local_Theory.target_of o conclude_instantiation}; - -fun instantiation_cmd arities thy = - instantiation (read_multi_arity thy arities) thy; - - -(* simplified instantiation interface with no class parameter *) - -fun instance_arity_cmd raw_arities thy = - let - val (tycos, vs, sort) = read_multi_arity thy raw_arities; - val sorts = map snd vs; - val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; - fun after_qed results = ProofContext.theory - ((fold o fold) AxClass.add_arity results); - in - thy - |> ProofContext.init_global - |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) - end; - - -(** tactics and methods **) - -fun intro_classes_tac facts st = - let - val thy = Thm.theory_of_thm st; - val classes = Sign.all_classes thy; - val class_trivs = map (Thm.class_triv thy) classes; - val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; - val assm_intros = all_assm_intros thy; - in - Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st - end; - -fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] - | default_intro_tac _ _ = no_tac; - -fun default_tac rules ctxt facts = - HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE - default_intro_tac ctxt facts; - -val _ = Context.>> (Context.map_theory - (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) - "back-chain introduction rules of classes" #> - Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) - "apply some intro/elim rule")); - -end; - diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Aug 11 15:45:15 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Aug 11 16:02:03 2010 +0200 @@ -462,11 +462,11 @@ (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin >> (fn ((name, (supclasses, elems)), begin) => (begin ? Toplevel.print) o Toplevel.begin_local_theory begin - (Class.class_cmd name supclasses elems #> snd))); + (Class_Declaration.class_cmd name supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal - (Parse.xname >> Class.subclass_cmd); + (Parse.xname >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Wed Aug 11 15:45:15 2010 +0200 +++ b/src/Pure/Isar/named_target.ML Wed Aug 11 16:02:03 2010 +0200 @@ -27,7 +27,7 @@ fun named_target _ NONE = global_target | named_target thy (SOME locale) = if Locale.defined thy locale - then Target {target = locale, is_locale = true, is_class = Class_Target.is_class thy locale} + then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale} else error ("No such locale: " ^ quote locale); structure Data = Proof_Data @@ -69,7 +69,7 @@ val is_canonical_class = is_class andalso (Binding.eq_name (b, b') andalso not (null prefix') - andalso List.last prefix' = (Class_Target.class_prefix target, false) + andalso List.last prefix' = (Class.class_prefix target, false) orelse same_shape); in not is_canonical_class ? @@ -88,7 +88,7 @@ fun class_target (Target {target, ...}) f = Local_Theory.raw_theory f #> - Local_Theory.target (Class_Target.refresh_syntax target); + Local_Theory.target (Class.refresh_syntax target); (* define *) @@ -102,7 +102,7 @@ (((b, U), mx), (b_def, rhs)) (type_params, term_params) = Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) - #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs))) + #> class_target ta (Class.declare target ((b, mx), (type_params, lhs))) #> pair (lhs, def)) fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = @@ -141,7 +141,7 @@ if is_locale then lthy |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs - |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t')) + |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t')) else lthy |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); @@ -181,7 +181,7 @@ fun init_context (Target {target, is_locale, is_class}) = if not is_locale then ProofContext.init_global else if not is_class then Locale.init target - else Class_Target.init target; + else Class.init target; fun init_target (ta as Target {target, ...}) thy = thy diff -r 0b6fa86110e7 -r 67d71449e85b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 11 15:45:15 2010 +0200 +++ b/src/Pure/ROOT.ML Wed Aug 11 16:02:03 2010 +0200 @@ -209,10 +209,10 @@ use "Isar/generic_target.ML"; use "Isar/overloading.ML"; use "axclass.ML"; -use "Isar/class_target.ML"; +use "Isar/class.ML"; use "Isar/named_target.ML"; use "Isar/expression.ML"; -use "Isar/class.ML"; +use "Isar/class_declaration.ML"; use "simplifier.ML";