diff --git a/src/Pure/Isar/class.ML b/src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML +++ b/src/Pure/Isar/class.ML @@ -1,844 +1,844 @@ (* Title: Pure/Isar/class.ML Author: Florian Haftmann, TU Muenchen Type classes derived from primitive axclasses and locales. *) signature CLASS = sig (*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) * bool))) list val print_classes: Proof.context -> unit val init: class -> theory -> Proof.context val begin: class list -> sort -> Proof.context -> Proof.context val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory 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 (*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 instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state val theory_map_result: string list * (string * sort) list * sort -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> (Proof.context -> 'b -> tactic) -> theory -> 'b * theory (*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 -> local_theory -> local_theory (*tactics*) val intro_classes_tac: Proof.context -> thm list -> tactic val standard_intro_classes_tac: Proof.context -> thm list -> tactic (*diagnostics*) val pretty_specification: theory -> class -> Pretty.T list end; structure Class: CLASS = struct (** class data **) datatype class_data = Class_Data 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) * bool))) list (* n.b. params = logical parameters of class operations = operations participating in user-space type system *) }; fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), (defs, operations)) = Class_Data {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 (Class_Data {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 _ (Class_Data {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}, Class_Data {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 Class_Data = 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 (Class_Data.get thy)) class of SOME (Class_Data 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 Class_Data.get; val heritage = Graph.all_preds o Class_Data.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 (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm) (the_list assm_intro)) (Class_Data.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 pretty_param ctxt (c, ty) = Pretty.block [Name_Space.pretty ctxt (Proof_Context.const_space ctxt) c, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt ty]; fun print_classes ctxt = let val thy = Proof_Context.theory_of ctxt; val algebra = Sign.classes_of thy; val class_space = Proof_Context.class_space ctxt; val type_space = Proof_Context.type_space ctxt; val arities = Symtab.empty |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => Symtab.map_default (class, []) (insert (op =) tyco)) arities) (Sorts.arities_of algebra); fun prt_supersort class = Syntax.pretty_sort ctxt (Sign.minimize_sort thy (Sign.super_classes thy class)); fun prt_arity class tyco = let val Ss = Sorts.mg_domain algebra tyco [class]; in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; fun prt_param (c, ty) = pretty_param ctxt (c, Type.strip_sorts_dummy ty); fun prt_entry class = Pretty.block ([Pretty.keyword1 "class", Pretty.brk 1, Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @ (case (these o Option.map #params o try (Axclass.get_info thy)) class of [] => [] | params => [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @ (case (these o Symtab.lookup arities) class of [] => [] | ars => [Pretty.fbrk, Pretty.big_list "instances:" (map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))])); in Sorts.all_classes algebra |> sort (Name_Space.extern_ord ctxt class_space) |> map prt_entry |> Pretty.writeln_chunks2 end; (* updaters *) fun register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class thy = let val operations = map (fn (v_ty as (_, ty), (c, _)) => (c, (class, ((ty, Free v_ty), false)))) params; val add_class = Graph.new_node (class, make_class_data (((map o apply2) fst params, base_sort, base_morph, export_morph, Option.map Thm.trim_context some_assm_intro, Thm.trim_context of_class, Option.map Thm.trim_context some_axiom), ([], operations))) #> fold (curry Graph.add_edge class) sups; in Class_Data.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 {inst = (cls, base_morphism thy cls), mixin = SOME (eq_morph, true), export = export_morphism thy cls}) thy) (heritage thy [class]) thy | NONE => thy); fun register_operation class (c, t) input_only 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 |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apsnd) (cons (c, (class, ((ty', t'), input_only)))) end; fun register_def class def_thm thy = let val sym_thm = Thm.trim_context (Thm.symmetric def_thm) in thy |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apfst) (cons sym_thm) |> activate_defs class [sym_thm] end; (** classes and class target **) (* class context syntax *) fun make_rewrite t c_ty = let val vs = strip_abs_vars t; val vts = map snd vs |> Name.invent_names Name.context Name.uu |> map (fn (v, T) => Var ((v, 0), T)); in (betapplys (t, vts), betapplys (Const c_ty, vts)) end; fun these_unchecks thy = these_operations thy #> map_filter (fn (c, (_, ((ty, t), input_only))) => if input_only then NONE else SOME (make_rewrite t (c, ty))); fun these_unchecks_reversed thy = these_operations thy #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t)); 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 = Proof_Context.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 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', Term.aT base_sort) else NONE | _ => NONE) | NONE => NONE) | NONE => NONE); fun subst (c, _) = Option.map (fst o 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 = primary_constraints, secondary_constraints = secondary_constraints, improve = improve, subst = subst, no_subst_in_abbrev_mode = true, unchecks = unchecks}) |> Overloading.set_primary_constraints end; fun synchronize_class_syntax_target class lthy = lthy |> Local_Theory.map_contexts (K (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class))); 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 (Term.aT base_sort)) |> synchronize_class_syntax sort base_sort |> Overloading.activate_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 guess_morphism_identity (b, rhs) phi1 phi2 = let (*FIXME proper concept to identify morphism instead of educated guess*) val name_of_binding = Name_Space.full_name Name_Space.global_naming; val n1 = (name_of_binding o Morphism.binding phi1) b; val n2 = (name_of_binding o Morphism.binding phi2) b; val rhs1 = Morphism.term phi1 rhs; val rhs2 = Morphism.term phi2 rhs; in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end; fun target_const class phi0 prmode (b, rhs) lthy = let val export = Variable.export_morphism lthy (Local_Theory.target_of lthy); val guess_identity = guess_morphism_identity (b, rhs) export; val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0); in lthy |> Generic_Target.locale_target_const class (not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs) end; local fun dangling_params_for lthy class (type_params, term_params) = let val class_param_names = map fst (these_params (Proof_Context.theory_of lthy) [class]); val dangling_term_params = subtract (fn (v, Free (w, _)) => v = w | _ => false) class_param_names term_params; in (type_params, dangling_term_params) end; fun global_def (b, eq) thy = let val ((_, def_thm), thy') = thy |> Thm.add_def_global false false (b, eq); val def_thm' = def_thm |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 |> Thm.varifyT_global; val (_, thy'') = thy' |> Global_Theory.store_thm (b, def_thm'); in (def_thm', thy'') end; fun canonical_const class phi dangling_params ((b, mx), rhs) thy = let val b_def = Binding.suffix_name "_dict" b; val c = Sign.full_name thy b; val ty = map Term.fastype_of dangling_params ---> Term.fastype_of rhs; val def_eq = Logic.mk_equals (list_comb (Const (c, ty), dangling_params), rhs) |> map_types Type.strip_sorts; in thy |> Sign.declare_const_global ((b, Type.strip_sorts ty), mx) |> snd |> global_def (b_def, def_eq) |-> (fn def_thm => register_def class def_thm) |> null dangling_params ? register_operation class (c, rhs) false |> Sign.add_const_constraint (c, SOME ty) end; in fun const class ((b, mx), lhs) params lthy = let val phi = morphism (Proof_Context.theory_of lthy) class; val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params)); in lthy |> target_const class phi Syntax.mode_default (b, lhs) |> Local_Theory.raw_theory (canonical_const class phi dangling_params ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs)) |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other) Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs) |> synchronize_class_syntax_target class end; end; local fun canonical_abbrev class phi prmode with_syntax ((b, mx), rhs) thy = let val c = Sign.full_name thy b; val constrain = map_atyps (fn T as TFree (v, _) => if v = Name.aT then TFree (v, [class]) else T | T => T); val rhs' = map_types constrain rhs; in thy |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs') |> snd |> with_syntax ? Sign.notation true prmode [(Const (c, fastype_of rhs), mx)] |> with_syntax ? register_operation class (c, rhs) (#1 prmode = Print_Mode.input) |> Sign.add_const_constraint (c, SOME (fastype_of rhs')) end; fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy = let val thy = Proof_Context.theory_of lthy; val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) [])); val (global_rhs, (_, (_, term_params))) = Generic_Target.export_abbrev lthy preprocess rhs; val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx; in lthy |> Local_Theory.raw_theory (canonical_abbrev class phi prmode (null term_params) ((Morphism.binding phi b, mx'), Logic.unvarify_types_global global_rhs)) end; fun further_abbrev_target class phi prmode (b, mx) rhs params = Generic_Target.background_abbrev (b, rhs) (snd params) #-> (fn (lhs, _) => target_const class phi prmode (b, lhs) #> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), lhs)) in fun abbrev class prmode ((b, mx), rhs) lthy = let val thy = Proof_Context.theory_of lthy; val phi = morphism thy class; val rhs_generic = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs; in lthy |> canonical_abbrev_target class phi prmode ((b, mx), rhs) |> Generic_Target.abbrev (further_abbrev_target class phi) prmode ((b, mx), rhs_generic) ||> synchronize_class_syntax_target class end; end; (* subclasses *) fun register_subclass (sub, sup) some_dep_morph some_witn export lthy = let val thy = Proof_Context.theory_of lthy; val intros = (snd o rules thy) sup :: map_filter I [Option.map (Drule.export_without_context_open o Element.conclude_witness lthy) some_witn, (fst o rules thy) sub]; val classrel = Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup)) (fn {context = ctxt, ...} => EVERY (map (TRYALL o resolve_tac ctxt o single) intros)); 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 + Generic_Target.locale_dependency sub {inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)), mixin = NONE, export = export} | NONE => I); in lthy |> Local_Theory.raw_theory (Axclass.add_classrel classrel #> Class_Data.map (Graph.add_edge (sub, sup)) #> activate_defs sub (these_defs thy diff_sort)) |> add_dependency |> synchronize_class_syntax_target sub end; local fun gen_classrel mk_prop classrel thy = let fun after_qed results = Proof_Context.background_theory ((fold o fold) Axclass.add_classrel results); in thy |> Proof_Context.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)*) } fun make_instantiation (arities, params) = Instantiation {arities = arities, params = params}; val empty_instantiation = make_instantiation (([], [], []), []); structure Instantiation = Proof_Data ( type T = instantiation; fun init _ = empty_instantiation; ); val get_instantiation = (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of; fun map_instantiation f = (Local_Theory.target o Instantiation.map) (fn Instantiation {arities, params} => make_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 = Proof_Context.init_global thy; val all_arities = map (fn raw_tyco => Proof_Context.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.invent_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 (Proof_Context.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 = primary_constraints, secondary_constraints = [], improve = improve, subst = subst, no_subst_in_abbrev_mode = false, unchecks = unchecks}) end; fun resort_terms ctxt 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 (Context.Proof ctxt) 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 ts else (map o map_types) inst ts end; (* target *) fun define_overloaded (c, U) b (b_def, rhs) lthy = let val name = Binding.name_of b; val pos = Binding.pos_of b; val _ = if Context_Position.is_reported lthy pos then Position.report_text pos Markup.class_parameter (Pretty.string_of (Pretty.block [Pretty.keyword1 "class", Pretty.brk 1, Pretty.str "parameter", Pretty.brk 1, pretty_param lthy (c, U)])) else (); in lthy |> Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U) ##>> Axclass.define_overloaded b_def (c, rhs)) ||> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = name)) ||> Local_Theory.map_contexts (K synchronize_inst_syntax) end; fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case instantiation_param lthy b of SOME c => if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) b (b_def, rhs) else error ("Illegal mixfix syntax for overloaded constant " ^ quote c) | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let val {arities = (tycos, vs, sort), params} = the_instantiation lthy; fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); fun pr_param ((c, _), (v, ty)) = Pretty.block (Pretty.breaks [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c, Pretty.str "::", Syntax.pretty_typ lthy ty]); in [Pretty.block (Pretty.fbreaks (Pretty.keyword1 "instantiation" :: map pr_arity tycos @ map pr_param params))] end; fun conclude lthy = let val (tycos, vs, sort) = #arities (the_instantiation lthy); val thy = Proof_Context.theory_of lthy; val _ = tycos |> List.app (fn tyco => if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then () else error ("Missing instance proof for type " ^ quote (Proof_Context.markup_type lthy tyco))); in lthy end; fun registration thy_ctxt {inst, mixin, export} lthy = lthy - |> Locale.add_registration_theory + |> Generic_Target.theory_registration {inst = inst, mixin = mixin, export = export $> Proof_Context.export_morphism lthy thy_ctxt} (*handle fixed types variables on target context properly*); 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 ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); val params = map_product get_param tycos class_params |> map_filter I; val _ = if null params andalso forall (fn tyco => can (Sign.arity_sorts thy tyco) sort) tycos then error "No parameters and no pending instance proof obligations in instantiation." else (); val primary_constraints = map (apsnd (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; val algebra = Sign.classes_of thy |> fold (fn tyco => Sorts.add_arities (Context.Theory thy) (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 ctxt ts = resort_terms ctxt algebra consts improve_constraints ts; val lookup_inst_param = Axclass.lookup_inst_param consts params; fun improve (c, ty) = (case lookup_inst_param (c, ty) of SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE | NONE => NONE); in thy |> Local_Theory.init {background_naming = Sign.naming_of thy, setup = Proof_Context.init_global #> Instantiation.put (make_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) (K {primary_constraints = primary_constraints, secondary_constraints = [], improve = improve, subst = K NONE, no_subst_in_abbrev_mode = false, unchecks = []}) #> Overloading.activate_improvable_syntax #> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check) #> synchronize_inst_syntax, conclude = conclude} {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, declaration = K Generic_Target.theory_declaration, theory_registration = registration (Proof_Context.init_global thy), locale_dependency = fn _ => error "Not possible in instantiation target", pretty = pretty} 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.background_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 = Proof_Context.export_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy)); val y = f morph x; in lthy |> prove_instantiation_exit (fn ctxt => tac ctxt y) |> pair y end; fun theory_map_result arities f g tac = instantiation arities #> g #-> prove_instantiation_exit_result f tac; (* 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 = Proof_Context.background_theory ((fold o fold) Axclass.add_arity results); in thy |> Proof_Context.init_global |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) end; (** tactics and methods **) fun intro_classes_tac ctxt facts st = let val thy = Proof_Context.theory_of ctxt; 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 ctxt (class_trivs @ class_intros @ assm_intros) facts st end; fun standard_intro_classes_tac ctxt facts st = if null facts andalso not (Thm.no_prems st) then (intro_classes_tac ctxt [] ORELSE Locale.intro_locales_tac {strict = true, eager = true} ctxt []) st else no_tac st; fun standard_tac ctxt facts = HEADGOAL (Method.some_rule_tac ctxt [] facts) ORELSE standard_intro_classes_tac ctxt facts; val _ = Theory.setup (Method.setup \<^binding>\intro_classes\ (Scan.succeed (METHOD o intro_classes_tac)) "back-chain introduction rules of classes" #> Method.setup \<^binding>\standard\ (Scan.succeed (METHOD o standard_tac)) "standard proof step: Pure intro/elim rule or class introduction"); (** diagnostics **) fun pretty_specification thy class = if is_class thy class then let val class_ctxt = init class thy; val prt_class = Name_Space.pretty class_ctxt (Proof_Context.class_space class_ctxt); val super_classes = Sign.minimize_sort thy (Sign.super_classes thy class); val fix_args = #params (Axclass.get_info thy class) |> map (fn (c, T) => (Binding.name (Long_Name.base_name c), SOME T, NoSyn)); val fixes = if null fix_args then [] else [Element.Fixes fix_args]; val assumes = Locale.hyp_spec_of thy class; val header = [Pretty.keyword1 "class", Pretty.brk 1, prt_class class, Pretty.str " =", Pretty.brk 1] @ Pretty.separate " +" (map prt_class super_classes) @ (if null super_classes then [] else [Pretty.str " +"]); val body = if null fixes andalso null assumes then [] else maps (Element.pretty_ctxt_no_attribs class_ctxt) (fixes @ assumes) |> maps (fn prt => [Pretty.fbrk, prt]); in if null body then [] else [Pretty.block (header @ body)] end else []; end; diff --git a/src/Pure/Isar/class_declaration.ML b/src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML +++ b/src/Pure/Isar/class_declaration.ML @@ -1,395 +1,395 @@ (* Title: Pure/Isar/class_declaration.ML Author: Florian Haftmann, TU Muenchen Declaring classes and subclass relations. *) signature CLASS_DECLARATION = sig val class: binding -> Bundle.name list -> class list -> Element.context_i list -> theory -> string * local_theory val class_cmd: binding -> (xstring * Position.T) list -> 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 thy_ctxt = Proof_Context.init_global thy; val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy; val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy; (* instantiation of canonical interpretation *) val a_tfree = (Name.aT, base_sort); val a_type = TFree a_tfree; val param_map_const = (map o apsnd) Const param_map; val param_map_inst = param_map |> map (fn (x, (c, T)) => let val T' = map_atyps (K a_type) T in ((x, T'), cert (Const (c, T'))) end); val const_morph = Element.instantiate_normalize_morphism ([], param_map_inst); val typ_morph = Element.instantiate_normalize_morphism ([(a_tfree, certT (Term.aT [class]))], []) val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_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 some_prop = try the_single props; val some_witn = 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 (resolve_tac thy_ctxt [intro])); val tac = loc_intro_tac THEN ALLGOALS (Proof_Context.fact_tac thy_ctxt (sup_axioms @ the_list assm_axiom)); in Element.prove_witness thy_ctxt prop tac end) some_prop; val some_axiom = Option.map (Element.conclude_witness thy_ctxt) some_witn; (* canonical interpretation *) val base_morph = inst_morph $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class)) $> Element.satisfy_morphism (the_list some_witn); 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] thy_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'; in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm''])) end; val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class)); (* of_class *) val of_class_prop_concl = Logic.mk_of_class (a_type, class); val of_class_prop = (case some_prop of NONE => of_class_prop_concl | SOME prop => Logic.mk_implies (Morphism.term const_morph ((map_types o map_atyps) (K a_type) 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.global_ctyp_of thy a_type, base_sort); fun tac ctxt = REPEAT (SOMEGOAL (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) ORELSE' assume_tac ctxt)); val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context); in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end; (* reading and processing class specifications *) fun prep_class_elems prep_decl ctxt sups raw_elems = let (* user space type system: only permits 'a type variable, improves towards 'a *) val thy = Proof_Context.theory_of ctxt; 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 is_param = member (op =) (map fst (Class.these_params thy sups)); val base_constraints = (map o apsnd) (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd) (Class.these_operations thy sups); val singleton_fixate = burrow_types (fn Ts => let val tfrees = fold Term.add_tfreesT Ts []; val inferred_sort = (fold o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts []; val fixate_sort = (case tfrees of [] => inferred_sort | [(a, S)] => if a <> Name.aT then error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") else if Sorts.sort_le algebra (S, inferred_sort) then S 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 S) | _ => error "Multiple type variables in class specification"); val fixateT = Term.aT fixate_sort; in (map o map_atyps) (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts end); fun unify_params ts = let val param_Ts = (fold o fold_aterms) (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts []; val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts; val param_T = if null param_namesT then NONE else SOME (case get_first (try dest_TFree) param_Ts of SOME v_sort => TFree v_sort | NONE => TVar (hd param_namesT, proto_base_sort)); in case param_T of NONE => ts | SOME T => map (subst_TVars (map (rpair T) param_namesT)) ts end; (* preprocessing elements, retrieving base sort from type-checked elements *) val raw_supexpr = (map (fn sup => (sup, (("", false), (Expression.Positional [], [])))) sups, []); val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints #> Class.redeclare_operations thy sups #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate)); val ((raw_supparams, _, raw_inferred_elems, _), _) = ctxt |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params)) |> prep_decl raw_supexpr init_class_body raw_elems; fun filter_element (Element.Fixes []) = NONE | filter_element (e as Element.Fixes _) = SOME e | filter_element (Element.Constrains []) = NONE | filter_element (e as Element.Constrains _) = SOME e | filter_element (Element.Assumes []) = NONE | filter_element (e as Element.Assumes _) = SOME e | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.") | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.") | filter_element (Element.Lazy_Notes _) = error ("\"notes\" element not allowed in class specification."); val inferred_elems = map_filter filter_element raw_inferred_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; 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 (Term.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_include prep_class_elems ctxt raw_supclasses raw_includes raw_elems = let val thy = Proof_Context.theory_of ctxt; (* prepare import *) val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); val sups = Sign.minimize_sort thy (map (prep_class ctxt) raw_supclasses); val _ = (case filter_out (Class.is_class thy) sups of [] => () | no_classes => error ("No (proper) classes: " ^ commas_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_quote (duplicates (op =) raw_supparam_names))) else (); (* infer types and base sort *) val includes = map (prep_include ctxt) raw_includes; val includes_ctxt = Bundle.includes includes ctxt; val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems includes_ctxt sups raw_elems; val sup_sort = inter_sort base_sort sups; (* process elements as class specification *) val class_ctxt = Class.begin sups base_sort includes_ctxt; 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 (Pretty.chunks (Element.pretty_ctxt class_ctxt e))) else (); fun check_element (e as Element.Fixes fxs) = List.app (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs | check_element (e as Element.Assumes assms) = List.app (fn (_, ts_pss) => List.app (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms | check_element _ = (); val _ = List.app 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)), (includes, elems, global_syntax)) end; val cert_class_spec = prep_class_spec (K I) (K I) cert_class_elems; val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check 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) (K (Term.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 (Term.aT base_sort)) raw_ty; val ty0 = Type.strip_sorts ty; val ty' = map_atyps (K (Term.aT [class])) ty0; val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b; in thy |> Sign.declare_const_global ((b, ty0), syn) |> snd |> pair ((Variable.check_name 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 (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) [(Binding.empty_atts, 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_includes raw_supclasses raw_elems thy = let val class = Sign.full_name thy b; val prefix = Binding.qualify true "class"; val ctxt = Proof_Context.init_global thy; val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) = prep_class_spec ctxt raw_supclasses raw_includes raw_elems; in thy |> Expression.add_locale b (prefix b) includes supexpr elems |> snd |> Local_Theory.exit_global |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |-> (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, some_axiom, some_assm_intro, of_class) => - Locale.add_registration_theory' + Context.theory_map (Locale.add_registration {inst = (class, base_morph), mixin = Option.map (rpair true) eq_morph, - export = export_morph} + export = export_morph}) #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class))) |> snd |> Named_Target.init includes 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 = Proof_Context.theory_of lthy; val proto_sup = prep_class thy raw_sup; val proto_sub = (case Named_Target.class_of lthy of SOME class => class | NONE => error "Not in a class 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 = Class.register_subclass (sub, sup) some_dep_morph some_wit export; 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 fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); fun subclass x = gen_subclass (K I) user_proof x; fun subclass_cmd x = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof x; end; (*local*) end; diff --git a/src/Pure/Isar/generic_target.ML b/src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML +++ b/src/Pure/Isar/generic_target.ML @@ -1,436 +1,455 @@ (* Title: Pure/Isar/generic_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Common target infrastructure. *) signature GENERIC_TARGET = sig (*auxiliary*) val export_abbrev: Proof.context -> (term -> term) -> term -> term * ((string * sort) list * (term list * term list)) val check_mixfix: Proof.context -> binding * (string * sort) list -> mixfix -> mixfix val check_mixfix_global: binding * bool -> mixfix -> mixfix (*background primitives*) val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val background_declaration: declaration -> local_theory -> local_theory val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) -> theory -> theory (*nested local theories primitives*) val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list val standard_notes: (int * int -> bool) -> string -> Attrib.fact list -> local_theory -> local_theory val standard_declaration: (int * int -> bool) -> (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory + val local_interpretation: Locale.registration -> + local_theory -> local_theory (*lifting target primitives to local theory operations*) val define: (((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory) -> bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val notes: (string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory) -> string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory val abbrev: (Syntax.mode -> binding * mixfix -> term -> term list * term list -> local_theory -> local_theory) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory (*theory target primitives*) val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val theory_target_notes: string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory (*theory target operations*) val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val theory_declaration: declaration -> local_theory -> local_theory + val theory_registration: Locale.registration -> local_theory -> local_theory (*locale target primitives*) val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory (*locale operations*) val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory + val locale_dependency: string -> Locale.registration -> + local_theory -> local_theory end structure Generic_Target: GENERIC_TARGET = struct (** consts **) fun export_abbrev lthy preprocess rhs = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); val rhs' = rhs |> Assumption.export_term lthy (Local_Theory.target_of lthy) |> preprocess; val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); val u = fold_rev lambda term_params rhs'; val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; val extra_tfrees = subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); val type_params = map (Logic.mk_type o TFree) extra_tfrees; in (global_rhs, (extra_tfrees, (type_params, term_params))) end; fun check_mixfix ctxt (b, extra_tfrees) mx = if null extra_tfrees then mx else (if Context_Position.is_visible ctxt then warning ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^ (if Mixfix.is_empty mx then "" else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) else (); NoSyn); fun check_mixfix_global (b, no_params) mx = if no_params orelse Mixfix.is_empty mx then mx else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); fun same_const (Const (c, _), Const (c', _)) = c = c' | same_const (t $ _, t' $ _) = same_const (t, t') | same_const (_, _) = false; fun const_decl phi_pred prmode ((b, mx), rhs) phi context = if phi_pred phi then let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; val same_shape = Term.aconv_untyped (rhs, rhs'); val same_stem = same_shape orelse same_const (rhs, rhs'); val const_alias = if same_shape then (case rhs' of Const (c, T) => let val thy = Context.theory_of context; val ctxt = Context.proof_of context; in (case Type_Infer_Context.const_type ctxt c of SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE | NONE => NONE) end | _ => NONE) else NONE; in (case const_alias of SOME c => context |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c) |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)]) | NONE => context |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs') |-> (fn (const as Const (c, _), _) => same_stem ? (Proof_Context.generic_revert_abbrev (#1 prmode) c #> same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) end else context; (** background primitives **) structure Foundation_Interpretations = Theory_Data ( type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table; val empty = Inttab.empty; val extend = I; val merge = Inttab.merge (K true); ); fun add_foundation_interpretation f = Foundation_Interpretations.map (Inttab.update_new (serial (), f)); fun foundation_interpretation binding_const_params lthy = let val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy); val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps; in lthy |> Local_Theory.background_theory (Context.theory_map interp) |> Local_Theory.map_contexts (K (Context.proof_map interp)) end; fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let val params = type_params @ term_params; val target_params = type_params @ take_prefix is_Free (Variable.export_terms lthy (Local_Theory.target_of lthy) term_params); val mx' = check_mixfix_global (b, null params) mx; val (const, lthy2) = lthy |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); val lhs = Term.list_comb (const, params); val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result (Thm.add_def (Proof_Context.defs_context lthy2) false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))) ||> foundation_interpretation (b, (const, target_params)); in ((lhs, def), lthy3) end; fun background_declaration decl lthy = let fun theory_decl context = Local_Theory.standard_form lthy (Proof_Context.init_global (Context.theory_of context)) decl context; in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; fun background_abbrev (b, global_rhs) params = Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs)) #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params)) (** nested local theories primitives **) fun standard_facts lthy ctxt = Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt); fun standard_notes pred kind facts lthy = Local_Theory.map_contexts (fn level => fn ctxt => if pred (Local_Theory.level lthy, level) then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd else ctxt) lthy; fun standard_declaration pred decl lthy = Local_Theory.map_contexts (fn level => fn ctxt => if pred (Local_Theory.level lthy, level) then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt else ctxt) lthy; fun standard_const pred prmode ((b, mx), rhs) = standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs)); +fun local_interpretation registration lthy = + let val n = Local_Theory.level lthy in + lthy + |> Local_Theory.map_contexts (fn level => + level = n - 1 ? Context.proof_map (Locale.add_registration registration)) + end; + + (** lifting target primitives to local theory operations **) (* define *) fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (*term and type parameters*) val ((defs, _), rhs') = Thm.cterm_of lthy rhs |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; val xs = Variable.add_fixed lthy rhs' []; val T = Term.fastype_of rhs; val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs [])); val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs); val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; (*foundation*) val ((lhs', global_def), lthy2) = lthy |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); (*local definition*) val ([(lhs, (_, local_def))], lthy3) = lthy2 |> Context_Position.set_visible false |> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))] ||> Context_Position.restore_visible lthy2; (*result*) val def = Thm.transitive local_def global_def |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs))); val ([(res_name, [res])], lthy4) = lthy3 |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; in ((lhs, (res_name, res)), lthy4) end; (* notes *) local fun import_export_proof ctxt (name, raw_th) = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt); (*export assumes/defines*) val th = Goal.norm_result ctxt raw_th; val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms; (*export fixes*) val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); val frees = map Free (Thm.fold_terms Term.add_frees th' []); val (th'' :: vs) = (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |> Variable.export ctxt thy_ctxt |> Drule.zero_var_indexes_list; (*thm definition*) val result = Global_Theory.name_thm Global_Theory.official1 name th''; (*import fixes*) val (tvars, vars) = chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |>> map Logic.dest_type; val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); val inst = map_filter (fn (Var (xi, T), t) => SOME ((xi, Term_Subst.instantiateT instT T), Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) | _ => NONE) (vars ~~ frees); val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result; (*import assumes/defines*) val result'' = (fold (curry op COMP) asms' result' handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |> Local_Defs.contract ctxt defs (Thm.cprop_of th) |> Goal.norm_result ctxt |> Global_Theory.name_thm Global_Theory.unofficial2 name; in (result'', result) end; fun bind_name lthy b = (Local_Theory.full_name lthy b, Binding.default_pos_of b); fun map_facts f = map (apsnd (map (apfst (map f)))); in fun notes target_notes kind facts lthy = let val facts' = facts |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs)) |> map_facts (import_export_proof lthy); val local_facts = map_facts #1 facts'; val global_facts = map_facts #2 facts'; in lthy |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts) |> Attrib.local_notes kind local_facts end; end; (* abbrev *) fun abbrev target_abbrev prmode ((b, mx), rhs) lthy = let val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs; val mx' = check_mixfix lthy (b, extra_tfrees) mx; in lthy |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |> Context_Position.set_visible false |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) ||> Context_Position.restore_visible lthy end; (** theory target primitives **) fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun theory_target_notes kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> standard_notes (op <>) kind local_facts; fun theory_target_abbrev prmode (b, mx) global_rhs params = Local_Theory.background_theory_result (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) => (* FIXME type_params!? *) Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) #-> (fn lhs => standard_const (op <>) prmode ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params))); (** theory operations **) val theory_abbrev = abbrev theory_target_abbrev; fun theory_declaration decl = background_declaration decl #> standard_declaration (K true) decl; +val theory_registration = Local_Theory.raw_theory o Context.theory_map o Locale.add_registration; + (** locale target primitives **) fun locale_target_notes locale kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> (fn lthy => lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #> standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts; fun locale_target_declaration locale syntax decl lthy = lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_declaration locale syntax (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); fun locale_target_const locale phi_pred prmode ((b, mx), rhs) = locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs)) (** locale operations **) fun locale_declaration locale {syntax, pervasive} decl = pervasive ? background_declaration decl #> locale_target_declaration locale syntax decl #> standard_declaration (fn (_, other) => other <> 0) decl; fun locale_const locale prmode ((b, mx), rhs) = locale_target_const locale (K true) prmode ((b, mx), rhs) #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); +fun locale_dependency loc registration = + Local_Theory.raw_theory (Locale.add_dependency loc registration) + #> local_interpretation registration; + (** locale abbreviations **) fun locale_target_abbrev locale prmode (b, mx) global_rhs params = background_abbrev (b, global_rhs) (snd params) #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs)); fun locale_abbrev locale = abbrev (locale_target_abbrev locale); end; diff --git a/src/Pure/Isar/interpretation.ML b/src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML +++ b/src/Pure/Isar/interpretation.ML @@ -1,240 +1,245 @@ (* Title: Pure/Isar/interpretation.ML Author: Clemens Ballarin, TU Muenchen Author: Florian Haftmann, TU Muenchen Locale interpretation. *) signature INTERPRETATION = sig type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list (*interpretation in proofs*) val interpret: Expression.expression_i -> Proof.state -> Proof.state val interpret_cmd: Expression.expression -> Proof.state -> Proof.state (*interpretation in local theories*) val interpretation: Expression.expression_i -> local_theory -> Proof.state val interpretation_cmd: Expression.expression -> local_theory -> Proof.state (*interpretation into global theories*) val global_interpretation: Expression.expression_i -> term defines -> local_theory -> Proof.state val global_interpretation_cmd: Expression.expression -> string defines -> local_theory -> Proof.state (*interpretation between locales*) val sublocale: Expression.expression_i -> term defines -> local_theory -> Proof.state val sublocale_cmd: Expression.expression -> string defines -> local_theory -> Proof.state val global_sublocale: string -> Expression.expression_i -> term defines -> theory -> Proof.state val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> string defines -> theory -> Proof.state (*mixed Isar interface*) val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state end; structure Interpretation : INTERPRETATION = struct (** common interpretation machinery **) type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list (* reading of locale expressions with rewrite morphisms *) local fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy = let val rhs = prep_term lthy raw_rhs; val lthy' = Variable.declare_term rhs lthy; val ((_, (_, def)), lthy'') = Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy'; in (Thm.symmetric def, lthy'') end; fun augment_with_defs _ [] _ = pair [] (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) | augment_with_defs prep_term raw_defs deps = Local_Theory.begin_nested #> snd #> fold Locale.activate_declarations deps #> fold_map (augment_with_def prep_term) raw_defs #> Local_Theory.end_nested_result Morphism.fact; fun prep_interpretation prep_expr prep_term expression raw_defs initial_ctxt = let val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; val (def_eqns, def_ctxt) = augment_with_defs prep_term raw_defs deps expr_ctxt; val export' = Proof_Context.export_morphism def_ctxt expr_ctxt; in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; in fun cert_interpretation expression = prep_interpretation Expression.cert_goal_expression Syntax.check_term expression; fun read_interpretation expression = prep_interpretation Expression.read_goal_expression Syntax.read_term expression; end; (* interpretation machinery *) local fun abs_def_rule eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); fun note_eqns_register note add_registration deps eqnss witss def_eqns thms export export' ctxt = let val factss = thms |> unflat ((map o map) #1 eqnss) |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt; val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule; val deps' = (deps ~~ witss) |> map (fn ((dep, morph), wits) => (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))); fun register (dep, eqns) ctxt = ctxt |> add_registration {inst = dep, mixin = Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')), export = export}; in ctxt'' |> fold register (deps' ~~ eqnss') end; in fun generic_interpretation prep_interpretation setup_proof note add_registration expression raw_defs initial_ctxt = let val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = prep_interpretation expression raw_defs initial_ctxt; fun after_qed witss eqns = note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; end; (** interfaces **) (* interpretation in proofs *) local fun setup_proof state after_qed propss eqns goal_ctxt = Element.witness_local_proof_eqs (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) "interpret" propss eqns goal_ctxt state; +fun add_registration_proof registration ctxt = ctxt + |> Proof_Context.set_stmt false + |> Context.proof_map (Locale.add_registration registration) + |> Proof_Context.restore_stmt ctxt; + fun gen_interpret prep_interpretation expression state = Proof.assert_forward_or_chain state |> Proof.context_of |> generic_interpretation prep_interpretation (setup_proof state) - Attrib.local_notes Locale.add_registration_proof expression []; + Attrib.local_notes add_registration_proof expression []; in val interpret = gen_interpret cert_interpretation; val interpret_cmd = gen_interpret read_interpretation; end; (* interpretation in local theories *) val add_registration_local_theory = - Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory; + Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation; fun interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind add_registration_local_theory expression []; fun interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind add_registration_local_theory expression []; (* interpretation into global theories *) fun global_interpretation expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.theory_registration expression; fun global_interpretation_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.theory_registration expression; (* interpretation between locales *) fun sublocale expression = generic_interpretation cert_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.locale_dependency expression; fun sublocale_cmd expression = generic_interpretation read_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.locale_dependency expression; local fun gen_global_sublocale prep_loc prep_interpretation raw_locale expression raw_defs thy = let val lthy = Named_Target.init [] (prep_loc thy raw_locale) thy; fun setup_proof after_qed = Element.witness_proof_eqs (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); in lthy |> generic_interpretation prep_interpretation setup_proof Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs end; in fun global_sublocale expression = gen_global_sublocale (K I) cert_interpretation expression; fun global_sublocale_cmd raw_expression = gen_global_sublocale Locale.check read_interpretation raw_expression; end; (* mixed Isar interface *) local fun register_or_activate lthy = if Named_Target.is_theory lthy then Local_Theory.theory_registration else add_registration_local_theory; fun gen_isar_interpretation prep_interpretation expression lthy = generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy; in fun isar_interpretation expression = gen_isar_interpretation cert_interpretation expression; fun isar_interpretation_cmd raw_expression = gen_isar_interpretation read_interpretation raw_expression; end; end; diff --git a/src/Pure/Isar/locale.ML b/src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML +++ b/src/Pure/Isar/locale.ML @@ -1,807 +1,784 @@ (* Title: Pure/Isar/locale.ML Author: Clemens Ballarin, TU Muenchen Locales -- managed Isar proof contexts, based on Pure predicates. Draws basic ideas from Florian Kammueller's original version of locales, but uses the richer infrastructure of Isar instead of the raw meta-logic. Furthermore, structured composition of contexts (with merge and instantiation) is provided, as well as type-inference of the signature parts and predicate definitions of the specification text. Interpretation enables the transfer of declarations and theorems to other contexts, namely those defined by theories, structured proofs and locales themselves. A comprehensive account of locales is available: [1] Clemens Ballarin. Locales: a module system for mathematical theories. Journal of Automated Reasoning, 52(2):123-153, 2014. See also: [2] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. In Stefano Berardi et al., Types for Proofs and Programs: International Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004. [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing Dependencies between Locales. Technical Report TUM-I0607, Technische Universitaet Muenchen, 2006. [4] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, pages 31-43, 2006. *) signature LOCALE = sig (* Locale specification *) val register_locale: binding -> (string * sort) list * ((string * typ) * mixfix) list -> term option * term list -> thm option * thm option -> thm list -> Element.context_i list -> declaration list -> (string * Attrib.fact list) list -> (string * morphism) list -> theory -> theory val locale_space: theory -> Name_Space.T val intern: theory -> xstring -> string val check: theory -> xstring * Position.T -> string val extern: theory -> string -> xstring val markup_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val defined: theory -> string -> bool val parameters_of: theory -> string -> (string * sort) list * ((string * typ) * mixfix) list val params_of: theory -> string -> ((string * typ) * mixfix) list val intros_of: theory -> string -> thm option * thm option val axioms_of: theory -> string -> thm list val instance_of: theory -> string -> morphism -> term list val specification_of: theory -> string -> term option * term list val hyp_spec_of: theory -> string -> Element.context_i list (* Storing results *) val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context (* Activation *) val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic val activate_declarations: string * morphism -> Proof.context -> Proof.context val init: string -> theory -> Proof.context (* Reasoning about locales *) val get_witnesses: Proof.context -> thm list val get_intros: Proof.context -> thm list val get_unfolds: Proof.context -> thm list val witness_add: attribute val intro_add: attribute val unfold_add: attribute val intro_locales_tac: {strict: bool, eager: bool} -> Proof.context -> thm list -> tactic (* Registrations and dependencies *) type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism} val amend_registration: registration -> Context.generic -> Context.generic val add_registration: registration -> Context.generic -> Context.generic - val add_registration_theory': registration -> theory -> theory - val add_registration_theory: registration -> local_theory -> local_theory - val add_registration_local_theory: registration -> local_theory -> local_theory - val add_registration_proof: registration -> Proof.context -> Proof.context val registrations_of: Context.generic -> string -> (string * morphism) list - val add_dependency': string -> registration -> theory -> theory - val add_dependency: string -> registration -> local_theory -> local_theory + val add_dependency: string -> registration -> theory -> theory (* Diagnostic *) val get_locales: theory -> string list val pretty_locales: theory -> bool -> Pretty.T val pretty_locale: theory -> bool -> string -> Pretty.T val pretty_registrations: Proof.context -> string -> Pretty.T val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list type locale_dependency = {source: string, target: string, prefix: (string * bool) list, morphism: morphism, pos: Position.T, serial: serial} val dest_dependencies: theory list -> theory -> locale_dependency list val tracing : Proof.context -> string -> unit end; structure Locale: LOCALE = struct datatype ctxt = datatype Element.ctxt; (*** Locales ***) type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial}; fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2; fun make_dep (name, morphisms) : dep = {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()}; (*table of mixin lists, per list mixins in reverse order of declaration; lists indexed by registration/dependency serial, entries for empty lists may be omitted*) type mixin = (morphism * bool) * serial; type mixins = mixin list Inttab.table; fun lookup_mixins (mixins: mixins) serial' = Inttab.lookup_list mixins serial'; val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =); fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ())); fun rename_mixin (old, new) (mixins: mixins) = (case Inttab.lookup mixins old of NONE => mixins | SOME mixin => Inttab.delete old mixins |> Inttab.update_new (new, mixin)); fun compose_mixins (mixins: mixin list) = fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; datatype locale = Loc of { (* static part *) (*type and term parameters*) parameters: (string * sort) list * ((string * typ) * mixfix) list, (*assumptions (as a single predicate expression) and defines*) spec: term option * term list, intros: thm option * thm option, axioms: thm list, (*diagnostic device: theorem part of hypothetical body as specified by the user*) hyp_spec: Element.context_i list, (* dynamic part *) (*syntax declarations*) syntax_decls: (declaration * serial) list, (*theorem declarations*) notes: ((string * Attrib.fact list) * serial) list, (*locale dependencies (sublocale relation) in reverse order*) dependencies: dep list, (*mixin part of dependencies*) mixins: mixins }; fun mk_locale ((parameters, spec, intros, axioms, hyp_spec), ((syntax_decls, notes), (dependencies, mixins))) = Loc {parameters = parameters, spec = spec, intros = intros, axioms = axioms, hyp_spec = hyp_spec, syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins}; fun map_locale f (Loc {parameters, spec, intros, axioms, hyp_spec, syntax_decls, notes, dependencies, mixins}) = mk_locale (f ((parameters, spec, intros, axioms, hyp_spec), ((syntax_decls, notes), (dependencies, mixins)))); fun merge_locale (Loc {parameters, spec, intros, axioms, hyp_spec, syntax_decls, notes, dependencies, mixins}, Loc {syntax_decls = syntax_decls', notes = notes', dependencies = dependencies', mixins = mixins', ...}) = mk_locale ((parameters, spec, intros, axioms, hyp_spec), ((merge (eq_snd op =) (syntax_decls, syntax_decls'), merge (eq_snd op =) (notes, notes')), (merge eq_dep (dependencies, dependencies'), (merge_mixins (mixins, mixins'))))); structure Locales = Theory_Data ( type T = locale Name_Space.table; val empty : T = Name_Space.empty_table "locale"; val extend = I; val merge = Name_Space.join_tables (K merge_locale); ); val locale_space = Name_Space.space_of_table o Locales.get; val intern = Name_Space.intern o locale_space; fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); fun markup_extern ctxt = Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup; fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str; val get_locale = Name_Space.lookup o Locales.get; val defined = is_some oo get_locale; fun the_locale thy name = (case get_locale thy name of SOME (Loc loc) => loc | NONE => error ("Unknown locale " ^ quote name)); fun register_locale binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy = thy |> Locales.map (Name_Space.define (Context.Theory thy) true (binding, mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros, map Thm.trim_context axioms, hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes), (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, Inttab.empty)))) #> snd); (* FIXME Morphism.identity *) fun change_locale name = Locales.map o Name_Space.map_table_entry name o map_locale o apsnd; (** Primitive operations **) fun parameters_of thy = #parameters o the_locale thy; val params_of = #2 oo parameters_of; fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy; fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; fun instance_of thy name morph = params_of thy name |> map (Morphism.term morph o Free o #1); fun specification_of thy = #spec o the_locale thy; fun hyp_spec_of thy = #hyp_spec o the_locale thy; fun dependencies_of thy = #dependencies o the_locale thy; fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial; (* Print instance and qualifiers *) fun pretty_reg_inst ctxt qs (name, ts) = let fun print_qual (qual, mandatory) = qual ^ (if mandatory then "" else "?"); fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs)); val prt_term = Pretty.quote o Syntax.pretty_term ctxt; fun prt_term' t = if Config.get ctxt show_types then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] else prt_term t; fun prt_inst ts = Pretty.block (Pretty.breaks (pretty_name ctxt name :: map prt_term' ts)); in (case qs of [] => prt_inst ts | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts]) end; fun pretty_reg ctxt export (name, morph) = let val thy = Proof_Context.theory_of ctxt; val morph' = morph $> export; val qs = Morphism.binding_prefix morph'; val ts = instance_of thy name morph'; in pretty_reg_inst ctxt qs (name, ts) end; (*** Identifiers: activated locales in theory or proof context ***) type idents = term list list Symtab.table; (* name ~> instance (grouped by name) *) val empty_idents : idents = Symtab.empty; val insert_idents = Symtab.insert_list (eq_list (op aconv)); val merge_idents = Symtab.merge_list (eq_list (op aconv)); fun redundant_ident thy idents (name, instance) = exists (fn pat => Pattern.matchess thy (pat, instance)) (Symtab.lookup_list idents name); structure Idents = Generic_Data ( type T = idents; val empty = empty_idents; val extend = I; val merge = merge_idents; ); (** Resolve locale dependencies in a depth-first fashion **) local val roundup_bound = 120; fun add thy depth stem export (name, morph) (deps, marked) = if depth > roundup_bound then error "Roundup bound exceeded (sublocale relation probably not terminating)." else let val instance = instance_of thy name (morph $> stem $> export); in if redundant_ident thy marked (name, instance) then (deps, marked) else let (*no inheritance of mixins, regardless of requests by clients*) val dependencies = dependencies_of thy name |> map (fn dep as {morphisms = (morph', export'), ...} => (#name dep, morph' $> export' $> compose_mixins (mixins_of thy name (#serial dep)))); val marked' = insert_idents (name, instance) marked; val (deps', marked'') = fold_rev (add thy (depth + 1) (morph $> stem) export) dependencies ([], marked'); in ((name, morph $> stem) :: deps' @ deps, marked'') end end; in (* Note that while identifiers always have the external (exported) view, activate_dep is presented with the internal view. *) fun roundup thy activate_dep export (name, morph) (marked, input) = let (* Find all dependencies including new ones (which are dependencies enriching existing registrations). *) val (dependencies, marked') = add thy 0 Morphism.identity export (name, morph) ([], empty_idents); (* Filter out fragments from marked; these won't be activated. *) val dependencies' = filter_out (fn (name, morph) => redundant_ident thy marked (name, instance_of thy name (morph $> export))) dependencies; in (merge_idents (marked, marked'), input |> fold_rev activate_dep dependencies') end; end; (*** Registrations: interpretations in theories or proof contexts ***) val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord); structure Idtab = Table(type key = string * term list val ord = total_ident_ord); type reg = {morphisms: morphism * morphism, pos: Position.T, serial: serial}; type regs = reg Idtab.table; val join_regs : regs * regs -> regs = Idtab.join (fn id => fn (reg1, reg2) => if #serial reg1 = #serial reg2 then raise Idtab.SAME else raise Idtab.DUP id); (* FIXME consolidate with locale dependencies, consider one data slot only *) structure Global_Registrations = Theory_Data' ( (*registrations, indexed by locale name and instance; unique registration serial points to mixin list*) type T = regs * mixins; val empty: T = (Idtab.empty, Inttab.empty); val extend = I; fun merge old_thys = let fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T = (join_regs (regs1, regs2), merge_mixins (mixins1, mixins2)) handle Idtab.DUP id => (*distinct interpretations with same base: merge their mixins*) let val reg1 = Idtab.lookup regs1 id |> the; val reg2 = Idtab.lookup regs2 id |> the; val reg2' = {morphisms = #morphisms reg2, pos = Position.thread_data (), serial = #serial reg1}; val regs2' = Idtab.update (id, reg2') regs2; val mixins2' = rename_mixin (#serial reg2, #serial reg1) mixins2; val _ = warning ("Removed duplicate interpretation after retrieving its mixins" ^ Position.here_list [#pos reg1, #pos reg2] ^ ":\n " ^ Pretty.string_of (pretty_reg_inst (Syntax.init_pretty_global (#1 old_thys)) [] id)); in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end; in recursive_merge end; ); structure Local_Registrations = Proof_Data ( type T = Global_Registrations.T; val init = Global_Registrations.get; ); val get_registrations = Context.cases Global_Registrations.get Local_Registrations.get; fun map_registrations f (Context.Theory thy) = Context.Theory (Global_Registrations.map f thy) | map_registrations f (Context.Proof ctxt) = Context.Proof (Local_Registrations.map f ctxt); (* Primitive operations *) fun add_reg thy export (name, morph) = let val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()}; val id = (name, instance_of thy name (morph $> export)); in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end; fun add_mixin serial' mixin = (* registration to be amended identified by its serial id *) (map_registrations o apsnd) (insert_mixin serial' mixin); val get_regs = #1 o get_registrations; fun get_mixins context (name, morph) = let val thy = Context.theory_of context; val (regs, mixins) = get_registrations context; in (case Idtab.lookup regs (name, instance_of thy name morph) of NONE => [] | SOME {serial, ...} => lookup_mixins mixins serial) end; fun collect_mixins context (name, morph) = let val thy = Context.theory_of context; in roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep)) Morphism.identity (name, morph) (insert_idents (name, instance_of thy name morph) empty_idents, []) |> snd |> filter (snd o fst) (* only inheritable mixins *) |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph))) |> compose_mixins end; (*** Activate context elements of locale ***) fun activate_err msg kind (name, morph) context = cat_error msg ("The above error(s) occurred while activating " ^ kind ^ " of locale instance\n" ^ (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of)); fun init_element elem context = context |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really) |> Element.init elem |> Context.mapping I (fn ctxt => let val ctxt0 = Context.proof_of context in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end); (* Potentially lazy notes *) fun make_notes kind = map (fn ((b, atts), facts) => if null atts andalso forall (null o #2) facts then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts))) else Notes (kind, [((b, atts), facts)])); fun lazy_notes thy loc = rev (#notes (the_locale thy loc)) |> maps (fn ((kind, notes), _) => make_notes kind notes); fun consolidate_notes elems = elems |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE) |> Lazy.consolidate |> ignore; fun force_notes (Lazy_Notes (kind, (b, ths))) = Notes (kind, [((b, []), [(Lazy.force ths, [])])]) | force_notes elem = elem; (* Declarations, facts and entire locale content *) val trace_locales = Attrib.setup_config_bool (Binding.make ("trace_locales", \<^here>)) (K false); fun tracing context msg = if Config.get context trace_locales then Output.tracing msg else (); fun trace kind (name, morph) context = tracing (Context.proof_of context) ("Activating " ^ kind ^ " of " ^ (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of)); fun activate_syntax_decls (name, morph) context = let val _ = trace "syntax" (name, morph) context; val thy = Context.theory_of context; val {syntax_decls, ...} = the_locale thy name; in context |> fold_rev (fn (decl, _) => decl morph) syntax_decls handle ERROR msg => activate_err msg "syntax" (name, morph) context end; fun activate_notes activ_elem transfer context export' (name, morph) input = let val thy = Context.theory_of context; val mixin = (case export' of NONE => Morphism.identity | SOME export => collect_mixins context (name, morph $> export) $> export); val morph' = transfer input $> morph $> mixin; val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name); in (notes', input) |-> fold (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) end handle ERROR msg => activate_err msg "facts" (name, morph) context; fun activate_notes_trace activ_elem transfer context export' (name, morph) context' = let val _ = trace "facts" (name, morph) context'; in activate_notes activ_elem transfer context export' (name, morph) context' end; fun activate_all name thy activ_elem transfer (marked, input) = let val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name; val input' = input |> (not (null params) ? activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |> (* FIXME type parameters *) (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |> (not (null defs) ? activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs))); val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE; in roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input') end; (** Public activation functions **) fun activate_facts export dep context = context |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) (activate_notes_trace init_element Morphism.transfer_morphism'' context export) (the_default Morphism.identity export) dep |-> Idents.put |> Context_Position.restore_visible_generic context; fun activate_declarations dep = Context.proof_map (fn context => context |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep |-> Idents.put |> Context_Position.restore_visible_generic context); fun init name thy = let val context = Context.Proof (Proof_Context.init_global thy); val marked = Idents.get context; in context |> Context_Position.set_visible_generic false |> pair empty_idents |> activate_all name thy init_element Morphism.transfer_morphism'' |-> (fn marked' => Idents.put (merge_idents (marked, marked'))) |> Context_Position.restore_visible_generic context |> Context.proof_of end; (*** Add and extend registrations ***) type registration = Locale.registration; fun amend_registration {mixin = NONE, ...} context = context | amend_registration {inst = (name, morph), mixin = SOME mixin, export} context = let val thy = Context.theory_of context; val ctxt = Context.proof_of context; val regs = get_regs context; val base = instance_of thy name (morph $> export); val serial' = (case Idtab.lookup regs (name, base) of NONE => error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^ " with\nparameter instantiation " ^ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available") | SOME {serial = serial', ...} => serial'); in add_mixin serial' mixin context end; (* Note that a registration that would be subsumed by an existing one will not be generated, and it will not be possible to amend it. *) fun add_registration {inst = (name, base_morph), mixin, export} context = let val thy = Context.theory_of context; val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ())); val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix); val inst = instance_of thy name mix_morph; val idents = Idents.get context; in if redundant_ident thy idents (name, inst) then context (* FIXME amend mixins? *) else (idents, context) (* add new registrations with inherited mixins *) |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2 (* add mixin *) |> amend_registration {inst = (name, mix_morph), mixin = mixin, export = export} (* activate import hierarchy as far as not already active *) |> activate_facts (SOME export) (name, mix_morph $> pos_morph) end; -val add_registration_theory' = Context.theory_map o add_registration; - -val add_registration_theory = Local_Theory.raw_theory o add_registration_theory'; - -fun add_registration_local_theory registration lthy = - let val n = Local_Theory.level lthy in - lthy - |> Local_Theory.map_contexts (fn level => - level = n - 1 ? Context.proof_map (add_registration registration)) - end; - -fun add_registration_proof registration ctxt = ctxt - |> Proof_Context.set_stmt false - |> Context.proof_map (add_registration registration) - |> Proof_Context.restore_stmt ctxt; (*** Dependencies ***) fun registrations_of context loc = Idtab.fold_rev (fn ((name, _), {morphisms, ...}) => name = loc ? cons (name, morphisms)) (get_regs context) [] (*with inherited mixins*) |> map (fn (name, (base, export)) => (name, base $> (collect_mixins context (name, base $> export)) $> export)); -fun add_dependency' loc {inst = (name, morph), mixin, export} thy = +fun add_dependency loc {inst = (name, morph), mixin, export} thy = let val dep = make_dep (name, (morph, export)); val add_dep = apfst (cons dep) #> apsnd (case mixin of NONE => I | SOME mixin => insert_mixin (#serial dep) mixin); val thy' = change_locale loc (apsnd add_dep) thy; val context' = Context.Theory thy'; val (_, regs) = fold_rev (roundup thy' cons export) (registrations_of context' loc) (Idents.get context', []); in - fold_rev (fn inst => add_registration_theory' {inst = inst, mixin = NONE, export = export}) + fold_rev (fn inst => Context.theory_map (add_registration {inst = inst, mixin = NONE, export = export})) regs thy' end; -fun add_dependency loc registration = - Local_Theory.raw_theory (add_dependency' loc registration) - #> add_registration_local_theory registration; (*** Storing results ***) fun add_facts loc kind facts ctxt = if null facts then ctxt else let val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ()); val applied_notes = make_notes kind facts; fun apply_notes morph = applied_notes |> fold (fn elem => fn context => let val elem' = Element.transform_ctxt (Morphism.transfer_morphism'' context $> morph) elem in Element.init elem' context end); val apply_registrations = Context.theory_map (fn context => fold_rev (apply_notes o #2) (registrations_of context loc) context); in ctxt |> Attrib.local_notes kind facts |> #2 |> Proof_Context.background_theory ((change_locale loc o apfst o apsnd) (cons stored_notes) #> apply_registrations) end; fun add_declaration loc syntax decl = syntax ? Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ()))) #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)]; (*** Reasoning about locales ***) (* Storage for witnesses, intro and unfold rules *) structure Thms = Generic_Data ( type T = thm list * thm list * thm list; val empty = ([], [], []); val extend = I; fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) = (Thm.merge_thms (witnesses1, witnesses2), Thm.merge_thms (intros1, intros2), Thm.merge_thms (unfolds1, unfolds2)); ); fun get_thms which ctxt = map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt))); val get_witnesses = get_thms #1; val get_intros = get_thms #2; val get_unfolds = get_thms #3; val witness_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm (Thm.trim_context th) x, y, z))); val intro_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm (Thm.trim_context th) y, z))); val unfold_add = Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm (Thm.trim_context th) z))); (* Tactics *) fun intro_locales_tac {strict, eager} ctxt = (if strict then Method.intros_tac else Method.try_intros_tac) ctxt (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else [])); val _ = Theory.setup (Method.setup \<^binding>\intro_locales\ (Scan.succeed (METHOD o intro_locales_tac {strict = false, eager = false})) "back-chain introduction rules of locales without unfolding predicates" #> Method.setup \<^binding>\unfold_locales\ (Scan.succeed (METHOD o intro_locales_tac {strict = false, eager = true})) "back-chain all introduction rules of locales"); (*** diagnostic commands and interfaces ***) fun get_locales thy = map #1 (Name_Space.dest_table (Locales.get thy)); fun pretty_locales thy verbose = Pretty.block (Pretty.breaks (Pretty.str "locales:" :: map (Pretty.mark_str o #1) (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy)))); fun pretty_locale thy show_facts name = let val locale_ctxt = init name thy; fun cons_elem (elem as Notes _) = show_facts ? cons elem | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, []) |> snd |> rev |> tap consolidate_notes |> map force_notes; in Pretty.block (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name :: maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems) end; fun pretty_registrations ctxt name = (case registrations_of (Context.Proof ctxt) name of [] => Pretty.str "no interpretations" | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs))); fun pretty_locale_deps thy = let fun make_node name = {name = name, parents = map #name (dependencies_of thy name), body = pretty_locale thy false name}; val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); in map make_node names end; type locale_dependency = {source: string, target: string, prefix: (string * bool) list, morphism: morphism, pos: Position.T, serial: serial}; fun dest_dependencies prev_thys thy = let fun remove_prev loc prev_thy deps = (case get_locale prev_thy loc of NONE => deps | SOME (Loc {dependencies = prev_deps, ...}) => if eq_list eq_dep (prev_deps, deps) then [] else subtract eq_dep prev_deps deps); fun result loc (dep: dep) = let val morphism = op $> (#morphisms dep) in {source = #name dep, target = loc, prefix = Morphism.binding_prefix morphism, morphism = morphism, pos = #pos dep, serial = #serial dep} end; fun add (loc, Loc {dependencies = deps, ...}) = fold (cons o result loc) (fold (remove_prev loc) prev_thys deps); in Name_Space.fold_table add (Locales.get thy) [] |> sort (int_ord o apply2 #serial) end; end; diff --git a/src/Pure/Isar/named_target.ML b/src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML +++ b/src/Pure/Isar/named_target.ML @@ -1,152 +1,152 @@ (* Title: Pure/Isar/named_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Targets for theory, locale, class -- at the bottom of the nested structure. *) signature NAMED_TARGET = sig val is_theory: local_theory -> bool val locale_of: local_theory -> string option val bottom_locale_of: local_theory -> string option val class_of: local_theory -> string option val init: Bundle.name list -> string -> theory -> local_theory val theory_init: theory -> local_theory val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory val revoke_reinitializability: local_theory -> local_theory val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory end; structure Named_Target: NAMED_TARGET = struct (* context data *) datatype target = Theory | Locale of string | Class of string; fun target_of_ident _ "" = Theory | target_of_ident thy ident = if Locale.defined thy ident then (if Class.is_class thy ident then Class else Locale) ident else error ("No such locale: " ^ quote ident); fun ident_of_target Theory = "" | ident_of_target (Locale locale) = locale | ident_of_target (Class class) = class; fun target_is_theory (SOME Theory) = true | target_is_theory _ = false; fun locale_of_target (SOME (Locale locale)) = SOME locale | locale_of_target (SOME (Class locale)) = SOME locale | locale_of_target _ = NONE; fun class_of_target (SOME (Class class)) = SOME class | class_of_target _ = NONE; structure Data = Proof_Data ( type T = (target * bool) option; fun init _ = NONE; ); val get_bottom_target = Option.map fst o Data.get; fun get_target lthy = if Local_Theory.level lthy = 1 then get_bottom_target lthy else NONE; fun ident_of lthy = case get_target lthy of NONE => error "Not in a named target" | SOME target => ident_of_target target; val is_theory = target_is_theory o get_target; val locale_of = locale_of_target o get_target; val bottom_locale_of = locale_of_target o get_bottom_target; val class_of = class_of_target o get_target; fun is_reinitializable lthy = Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy; (* operations *) fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun class_foundation class (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params #> pair (lhs, def)); fun operations Theory = {define = Generic_Target.define Generic_Target.theory_target_foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.theory_abbrev, declaration = fn _ => Generic_Target.theory_declaration, - theory_registration = Locale.add_registration_theory, + theory_registration = Generic_Target.theory_registration, locale_dependency = fn _ => error "Not possible in theory target", pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} | operations (Locale locale) = {define = Generic_Target.define (locale_foundation locale), notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), abbrev = Generic_Target.locale_abbrev locale, declaration = Generic_Target.locale_declaration locale, theory_registration = fn _ => error "Not possible in locale target", - locale_dependency = Locale.add_dependency locale, + locale_dependency = Generic_Target.locale_dependency locale, pretty = fn ctxt => [Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale]} | operations (Class class) = {define = Generic_Target.define (class_foundation class), notes = Generic_Target.notes (Generic_Target.locale_target_notes class), abbrev = Class.abbrev class, declaration = Generic_Target.locale_declaration class, theory_registration = fn _ => error "Not possible in class target", - locale_dependency = Locale.add_dependency class, + locale_dependency = Generic_Target.locale_dependency class, pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class}; fun setup_context Theory = Proof_Context.init_global | setup_context (Locale locale) = Locale.init locale | setup_context (Class class) = Class.init class; fun setup target includes = setup_context target #> Data.put (SOME (target, null includes)) #> Bundle.includes includes; fun init includes ident thy = let val target = target_of_ident thy ident; in thy |> Local_Theory.init {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident), setup = setup target includes, conclude = I} (operations target) end; val theory_init = init [] ""; fun theory_map g = theory_init #> g #> Local_Theory.exit_global; fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); fun exit_global_reinitialize lthy = if is_reinitializable lthy then (init [] (ident_of lthy), Local_Theory.exit_global lthy) else error "Non-reinitializable local theory context"; end; diff --git a/src/Pure/Isar/overloading.ML b/src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML +++ b/src/Pure/Isar/overloading.ML @@ -1,226 +1,226 @@ (* Title: Pure/Isar/overloading.ML Author: Florian Haftmann, TU Muenchen Overloaded definitions without any discipline. *) signature OVERLOADING = sig type improvable_syntax val activate_improvable_syntax: Proof.context -> Proof.context val map_improvable_syntax: (improvable_syntax -> improvable_syntax) -> Proof.context -> Proof.context val set_primary_constraints: Proof.context -> Proof.context val show_reverted_improvements: bool Config.T; val overloading: (string * (string * typ) * bool) list -> theory -> local_theory val overloading_cmd: (string * string * bool) list -> theory -> local_theory val theory_map: (string * (string * typ) * bool) list -> (local_theory -> local_theory) -> theory -> theory val theory_map_result: (string * (string * typ) * bool) list -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory end; structure Overloading: OVERLOADING = struct (* generic check/uncheck combinators for improvable constants *) type improvable_syntax = { primary_constraints: (string * typ) list, secondary_constraints: (string * typ) list, improve: string * typ -> (typ * typ) option, subst: string * typ -> (typ * term) option, no_subst_in_abbrev_mode: bool, unchecks: (term * term) list } structure Improvable_Syntax = Proof_Data ( type T = {syntax: improvable_syntax, secondary_pass: bool} fun init _ = {syntax = { primary_constraints = [], secondary_constraints = [], improve = K NONE, subst = K NONE, no_subst_in_abbrev_mode = false, unchecks = [] }, secondary_pass = false}: T; ); fun map_improvable_syntax f = Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass}); val mark_passed = Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true}); fun improve_term_check ts ctxt = let val thy = Proof_Context.theory_of ctxt; val {syntax = {secondary_constraints, improve, subst, no_subst_in_abbrev_mode, ...}, secondary_pass} = Improvable_Syntax.get ctxt; val no_subst = Proof_Context.abbrev_mode ctxt andalso no_subst_in_abbrev_mode; fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty) of SOME ty_ty' => Sign.typ_match thy ty_ty' | _ => I) | accumulate_improvements _ = I; fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty) of SOME (ty', t') => if Sign.typ_instance thy (ty, ty') then SOME (ty', apply_subst t') else NONE | NONE => NONE) | _ => NONE) t; val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; val ts' = ts |> (map o map_types) (Envir.subst_type improvements) |> not no_subst ? map apply_subst; in if secondary_pass orelse no_subst then if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) else SOME (ts', ctxt |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints |> mark_passed) end; fun rewrite_liberal thy unchecks t = (case try (Pattern.rewrite_term_top thy unchecks []) t of NONE => NONE | SOME t' => if t aconv t' then NONE else SOME t'); val show_reverted_improvements = Attrib.setup_config_bool \<^binding>\show_reverted_improvements\ (K true); fun improve_term_uncheck ts ctxt = let val thy = Proof_Context.theory_of ctxt; val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt; val revert = Config.get ctxt show_reverted_improvements; val ts' = map (rewrite_liberal thy unchecks) ts; in if revert andalso exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; fun set_primary_constraints ctxt = let val {syntax = {primary_constraints, ...}, ...} = Improvable_Syntax.get ctxt; in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; val activate_improvable_syntax = Context.proof_map (Syntax_Phases.term_check' 0 "improvement" improve_term_check #> Syntax_Phases.term_uncheck' 0 "improvement" improve_term_uncheck) #> set_primary_constraints; (* overloading target *) structure Data = Proof_Data ( type T = ((string * typ) * (string * bool)) list; fun init _ = []; ); 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, (v, checked)) else NONE); fun synchronize_syntax ctxt = let 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); val unchecks = map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; in ctxt |> map_improvable_syntax (K {primary_constraints = [], secondary_constraints = [], improve = K NONE, subst = subst, no_subst_in_abbrev_mode = false, unchecks = unchecks}) end; fun define_overloaded (c, U) (v, checked) (b_def, rhs) = Local_Theory.background_theory_result (Thm.add_def_global (not checked) true (Thm.def_binding_optional (Binding.name v) b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) ##> Local_Theory.map_contexts (K synchronize_syntax) #-> (fn (_, def) => pair (Const (c, U), def)); fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case operation lthy b of SOME (c, (v, checked)) => if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) else error ("Illegal mixfix syntax for overloaded constant " ^ quote c) | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let val overloading = get_overloading lthy; fun pr_operation ((c, ty), (v, _)) = Pretty.block (Pretty.breaks [Pretty.str v, Pretty.str "\", Proof_Context.pretty_const lthy c, Pretty.str "::", Syntax.pretty_typ lthy ty]); in [Pretty.block (Pretty.fbreaks (Pretty.keyword1 "overloading" :: map pr_operation overloading))] end; fun conclude lthy = let val overloading = get_overloading lthy; val _ = if null overloading then () else error ("Missing definition(s) for parameter(s) " ^ commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading)); in lthy end; fun gen_overloading prep_const raw_overloading_spec thy = let val ctxt = Proof_Context.init_global thy; val _ = if null raw_overloading_spec then error "At least one parameter must be given" else (); val overloading_spec = raw_overloading_spec |> map (fn (v, const, checked) => (Term.dest_Const (prep_const ctxt const), (v, checked))); in thy |> Local_Theory.init {background_naming = Sign.naming_of thy, setup = Proof_Context.init_global #> Data.put overloading_spec #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading_spec #> activate_improvable_syntax #> synchronize_syntax, conclude = conclude} {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_target_notes, abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, declaration = K Generic_Target.theory_declaration, - theory_registration = Locale.add_registration_theory, + theory_registration = Generic_Target.theory_registration, locale_dependency = fn _ => error "Not possible in overloading target", pretty = pretty} end; val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); val overloading_cmd = gen_overloading Syntax.read_term; fun theory_map overloading_spec g = overloading overloading_spec #> g #> Local_Theory.exit_global; fun theory_map_result overloading_spec f g = overloading overloading_spec #> g #> Local_Theory.exit_result_global f; end;