--- a/src/Pure/IsaMakefile Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/IsaMakefile Wed Aug 11 20:25:44 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 \
--- a/src/Pure/Isar/class.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/class.ML Wed Aug 11 20:25:44 2010 +0200
@@ -1,351 +1,640 @@
(* 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 =
+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 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_prefix class))
- $> Element.satisfy_morphism (the_list wit);
- val eq_morph = Element.eq_morphism thy (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 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 (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)
- (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
- #> 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 (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) (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 = 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 =) (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_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)
- #> 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 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;
+
+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;
+
+
+(* 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 define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
+ (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
+ ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
+ ##> Local_Theory.target synchronize_inst_syntax;
+
+fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ case instantiation_param lthy b
+ of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+ else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun pretty lthy =
+ let
+ val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
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);
+ 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.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
+
+fun conclude 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;
- 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 (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 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
+ |> Local_Theory.init NONE ""
+ {define = Generic_Target.define 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 = pretty,
+ exit = Local_Theory.target_of o conclude}
+ end;
+
+fun instantiation_cmd arities thy =
+ instantiation (read_multi_arity thy arities) thy;
+
+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;
-fun user_proof after_qed some_prop =
- Element.witness_proof (after_qed o try the_single o the_single)
- [the_list some_prop];
+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 tactic_proof tac after_qed some_prop ctxt =
- after_qed (Option.map
- (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt;
+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;
+
+
+(* simplified instantiation interface with no class parameter *)
-in
+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 **)
-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 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;
-end; (*local*)
+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;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/class_declaration.ML Wed Aug 11 20:25:44 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;
--- a/src/Pure/Isar/class_target.ML Wed Aug 11 18:44:06 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,659 +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 register: class -> class list -> ((string * typ) * (string * typ)) list
- -> sort -> morphism -> morphism -> thm option -> thm option -> thm
- -> theory -> theory
-
- val is_class: theory -> class -> bool
- val base_sort: theory -> class -> sort
- val rules: theory -> class -> thm option * thm
- val these_params: theory -> sort -> (string * (class * (string * typ))) list
- val these_defs: theory -> sort -> thm list
- val these_operations: theory -> sort
- -> (string * (class * (typ * term))) list
- val print_classes: theory -> unit
-
- val begin: class list -> sort -> Proof.context -> Proof.context
- 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
- val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
-
- (*instances*)
- val init_instantiation: string list * (string * sort) list * sort
- -> theory -> Proof.context
- val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
- 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 conclude_instantiation: local_theory -> local_theory
- val instantiation_param: local_theory -> binding -> string option
- val confirm_declaration: binding -> local_theory -> local_theory
- val pretty_instantiation: local_theory -> Pretty.T
- 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
-
- (*subclasses*)
- val register_subclass: class * class -> morphism option -> Element.witness option
- -> morphism -> theory -> theory
- 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;
-
-structure Class_Target : 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;
-
--- a/src/Pure/Isar/isar_syn.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Aug 11 20:25:44 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
--- a/src/Pure/Isar/local_theory.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML Wed Aug 11 20:25:44 2010 +0200
@@ -50,7 +50,6 @@
val const_alias: binding -> string -> local_theory -> local_theory
val init: serial option -> string -> operations -> Proof.context -> local_theory
val restore: local_theory -> local_theory
- val reinit: local_theory -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
@@ -75,7 +74,6 @@
declaration: bool -> declaration -> local_theory -> local_theory,
syntax_declaration: bool -> declaration -> local_theory -> local_theory,
pretty: local_theory -> Pretty.T list,
- reinit: local_theory -> local_theory,
exit: local_theory -> Proof.context};
datatype lthy = LThy of
@@ -260,8 +258,6 @@
let val {naming, theory_prefix, operations, target} = get_lthy lthy
in init (Name_Space.get_group naming) theory_prefix operations target end;
-val reinit = checkpoint o operation #reinit;
-
(* exit *)
--- a/src/Pure/Isar/named_target.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/named_target.ML Wed Aug 11 20:25:44 2010 +0200
@@ -22,7 +22,13 @@
fun make_target target is_locale is_class =
Target {target = target, is_locale = is_locale, is_class = is_class};
-val global_target = make_target "" false false;
+val global_target = Target {target = "", is_locale = false, is_class = false};
+
+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.is_class thy locale}
+ else error ("No such locale: " ^ quote locale);
structure Data = Proof_Data
(
@@ -63,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 ?
@@ -82,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 *)
@@ -96,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, ...}) =
@@ -135,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);
@@ -168,18 +174,18 @@
pretty_thy ctxt target is_class;
-(* init various targets *)
+(* init *)
local
-fun init_data (Target {target, is_locale, is_class}) =
+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
- |> init_data ta
+ |> init_context ta
|> Data.put ta
|> Local_Theory.init NONE (Long_Name.base_name target)
{define = Generic_Target.define (target_foundation ta),
@@ -190,15 +196,8 @@
syntax_declaration = fn pervasive => target_declaration ta
{ syntax = true, pervasive = pervasive },
pretty = pretty ta,
- reinit = init_target ta o ProofContext.theory_of,
exit = Local_Theory.target_of};
-fun named_target _ NONE = global_target
- | named_target thy (SOME target) =
- if Locale.defined thy target
- then make_target target true (Class_Target.is_class thy target)
- else error ("No such locale: " ^ quote target);
-
in
fun init target thy = init_target (named_target thy target) thy;
--- a/src/Pure/Isar/overloading.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Aug 11 20:25:44 2010 +0200
@@ -6,14 +6,6 @@
signature OVERLOADING =
sig
- val init: (string * (string * typ) * bool) list -> theory -> Proof.context
- val conclude: local_theory -> local_theory
- val declare: string * typ -> theory -> term * theory
- val confirm: binding -> local_theory -> local_theory
- val define: bool -> binding -> string * term -> theory -> thm * theory
- val operation: Proof.context -> binding -> (string * bool) option
- val pretty: Proof.context -> Pretty.T
-
type improvable_syntax
val add_improvable_syntax: Proof.context -> Proof.context
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
@@ -121,27 +113,22 @@
(** overloading target **)
-(* bookkeeping *)
-
-structure OverloadingData = Proof_Data
+structure Data = Proof_Data
(
type T = ((string * typ) * (string * bool)) list;
fun init _ = [];
);
-val get_overloading = OverloadingData.get o Local_Theory.target_of;
-val map_overloading = Local_Theory.target o OverloadingData.map;
+val get_overloading = Data.get o Local_Theory.target_of;
+val map_overloading = Local_Theory.target o Data.map;
fun operation lthy b = get_overloading lthy
|> get_first (fn ((c, _), (v, checked)) =>
- if Binding.name_of b = v then SOME (c, checked) else NONE);
-
-
-(* target *)
+ if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
fun synchronize_syntax ctxt =
let
- val overloading = OverloadingData.get ctxt;
+ val overloading = Data.get ctxt;
fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
of SOME (v, _) => SOME (ty, Free (v, ty))
| NONE => NONE;
@@ -152,38 +139,20 @@
|> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
end
-fun init raw_overloading thy =
- let
- val _ = if null raw_overloading then error "At least one parameter must be given" else ();
- val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
- in
- thy
- |> Theory.checkpoint
- |> ProofContext.init_global
- |> OverloadingData.put overloading
- |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
- |> add_improvable_syntax
- |> synchronize_syntax
- end;
-
-fun declare c_ty = pair (Const c_ty);
+fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
+ Local_Theory.theory_result
+ (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+ ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
+ ##> Local_Theory.target synchronize_syntax
+ #-> (fn (_, def) => pair (Const (c, U), def))
-fun define checked b (c, t) =
- Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
- #>> snd;
-
-fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
- #> Local_Theory.target synchronize_syntax
-
-fun conclude lthy =
- let
- val overloading = get_overloading lthy;
- val _ = if null overloading then () else
- error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
- o Syntax.string_of_term lthy o Const o fst) overloading));
- in
- lthy
- end;
+fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ case operation lthy b
+ of SOME (c, (v, checked)) => if mx <> NoSyn
+ then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+ else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
fun pretty lthy =
let
@@ -192,32 +161,32 @@
fun pr_operation ((c, ty), (v, _)) =
(Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
- in
- (Pretty.block o Pretty.fbreaks)
- (Pretty.str "overloading" :: map pr_operation overloading)
- end;
-
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+ in Pretty.str "overloading" :: map pr_operation overloading end;
-fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case operation lthy b
- of SOME (c, checked) => if mx <> NoSyn then syntax_error c
- else lthy |> Local_Theory.theory_result (declare (c, U)
- ##>> define checked b_def (c, rhs))
- ||> confirm b
- | NONE => lthy |>
- Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+fun conclude lthy =
+ let
+ val overloading = get_overloading lthy;
+ val _ = if null overloading then () else
+ error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
+ o Syntax.string_of_term lthy o Const o fst) overloading));
+ in lthy end;
-fun gen_overloading prep_const raw_ops thy =
+fun gen_overloading prep_const raw_overloading thy =
let
val ctxt = ProofContext.init_global thy;
- val ops = raw_ops |> map (fn (name, const, checked) =>
- (name, Term.dest_Const (prep_const ctxt const), checked));
+ val _ = if null raw_overloading then error "At least one parameter must be given" else ();
+ val overloading = raw_overloading |> map (fn (v, const, checked) =>
+ (Term.dest_Const (prep_const ctxt const), (v, checked)));
in
thy
- |> init ops
+ |> Theory.checkpoint
+ |> ProofContext.init_global
+ |> Data.put overloading
+ |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+ |> add_improvable_syntax
+ |> synchronize_syntax
|> Local_Theory.init NONE ""
- {define = Generic_Target.define overloading_foundation,
+ {define = Generic_Target.define foundation,
notes = Generic_Target.notes
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
abbrev = Generic_Target.abbrev
@@ -225,8 +194,7 @@
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,
- reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
+ pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;
--- a/src/Pure/Isar/toplevel.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 20:25:44 2010 +0200
@@ -111,8 +111,10 @@
fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
| loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
- | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
- Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
+ | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
+ val target_name = #target (Named_Target.peek lthy);
+ val target = if target_name = "" then NONE else SOME target_name;
+ in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
(* datatype node *)
--- a/src/Pure/ROOT.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Aug 11 20:25:44 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";
--- a/src/Pure/axclass.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/axclass.ML Wed Aug 11 20:25:44 2010 +0200
@@ -406,7 +406,7 @@
in
thy
|> Thm.add_def false false (b', prop)
- |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
+ |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
end;