wenzelm@20894: (* Title: Pure/Isar/theory_target.ML wenzelm@20894: ID: $Id$ haftmann@28861: ID: $Id$ wenzelm@20894: Author: Makarius wenzelm@20894: haftmann@25542: Common theory/locale/class/instantiation/overloading targets. wenzelm@20894: *) wenzelm@20894: wenzelm@20894: signature THEORY_TARGET = wenzelm@20894: sig haftmann@25462: val peek: local_theory -> {target: string, is_locale: bool, haftmann@25864: is_class: bool, instantiation: string list * (string * sort) list * sort, haftmann@25864: overloading: (string * (string * typ) * bool) list} haftmann@25269: val init: string option -> theory -> local_theory wenzelm@24935: val begin: string -> Proof.context -> local_theory wenzelm@25291: val context: xstring -> theory -> local_theory haftmann@25864: val instantiation: string list * (string * sort) list * sort -> theory -> local_theory haftmann@25864: val overloading: (string * (string * typ) * bool) list -> theory -> local_theory wenzelm@26049: val overloading_cmd: (string * string * bool) list -> theory -> local_theory wenzelm@20894: end; wenzelm@20894: wenzelm@20894: structure TheoryTarget: THEORY_TARGET = wenzelm@20894: struct wenzelm@20894: ballarin@28834: (* new locales *) ballarin@28834: ballarin@28849: fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x; ballarin@28849: fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x; ballarin@28849: fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x; ballarin@28849: fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x; ballarin@28849: fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x; ballarin@28849: fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x; ballarin@28849: fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x; ballarin@28834: wenzelm@21006: (* context data *) wenzelm@21006: haftmann@25462: datatype target = Target of {target: string, is_locale: bool, haftmann@25864: is_class: bool, instantiation: string list * (string * sort) list * sort, haftmann@25864: overloading: (string * (string * typ) * bool) list}; wenzelm@25012: haftmann@25519: fun make_target target is_locale is_class instantiation overloading = haftmann@25462: Target {target = target, is_locale = is_locale, haftmann@25519: is_class = is_class, instantiation = instantiation, overloading = overloading}; wenzelm@25291: haftmann@25542: val global_target = make_target "" false false ([], [], []) []; wenzelm@25012: wenzelm@21006: structure Data = ProofDataFun wenzelm@21006: ( wenzelm@25012: type T = target; wenzelm@25291: fun init _ = global_target; wenzelm@21006: ); wenzelm@21006: wenzelm@25012: val peek = (fn Target args => args) o Data.get; wenzelm@21006: wenzelm@21006: wenzelm@20894: (* pretty *) wenzelm@20894: haftmann@25607: fun pretty_thy ctxt target is_locale is_class = wenzelm@20894: let wenzelm@20894: val thy = ProofContext.theory_of ctxt; ballarin@28834: val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target; haftmann@28965: val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) wenzelm@28094: (#1 (ProofContext.inferred_fixes ctxt)); haftmann@28965: val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) wenzelm@28094: (Assumption.assms_of ctxt); wenzelm@20894: val elems = wenzelm@20894: (if null fixes then [] else [Element.Fixes fixes]) @ wenzelm@20894: (if null assumes then [] else [Element.Assumes assumes]); wenzelm@26049: in wenzelm@26049: if target = "" then [] haftmann@25607: else if null elems then [Pretty.str target_name] haftmann@25607: else [Pretty.big_list (target_name ^ " =") haftmann@25607: (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] wenzelm@20894: end; wenzelm@20894: haftmann@25607: fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt = haftmann@25607: Pretty.block [Pretty.str "theory", Pretty.brk 1, haftmann@25607: Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: haftmann@25607: (if not (null overloading) then [Overloading.pretty ctxt] wenzelm@26049: else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt] wenzelm@26049: else pretty_thy ctxt target is_locale is_class); haftmann@25607: wenzelm@20894: haftmann@24838: (* target declarations *) haftmann@24838: haftmann@27690: fun target_decl add (Target {target, is_class, ...}) d lthy = haftmann@24838: let wenzelm@24935: val d' = Morphism.transform (LocalTheory.target_morphism lthy) d; haftmann@24838: val d0 = Morphism.form d'; haftmann@24838: in wenzelm@25012: if target = "" then haftmann@24838: lthy haftmann@24838: |> LocalTheory.theory (Context.theory_map d0) haftmann@24838: |> LocalTheory.target (Context.proof_map d0) haftmann@24838: else haftmann@24838: lthy wenzelm@25012: |> LocalTheory.target (add target d') haftmann@24838: end; haftmann@24838: ballarin@28834: val type_syntax = target_decl locale_add_type_syntax; ballarin@28834: val term_syntax = target_decl locale_add_term_syntax; ballarin@28834: val declaration = target_decl locale_add_declaration; haftmann@24838: wenzelm@25105: fun class_target (Target {target, ...}) f = wenzelm@25105: LocalTheory.raw_theory f #> wenzelm@25105: LocalTheory.target (Class.refresh_syntax target); haftmann@24838: wenzelm@21611: wenzelm@20894: (* notes *) wenzelm@20894: wenzelm@21611: fun import_export_proof ctxt (name, raw_th) = wenzelm@21594: let wenzelm@21611: val thy = ProofContext.theory_of ctxt; wenzelm@21611: val thy_ctxt = ProofContext.init thy; wenzelm@21611: val certT = Thm.ctyp_of thy; wenzelm@21611: val cert = Thm.cterm_of thy; wenzelm@21594: wenzelm@21611: (*export assumes/defines*) wenzelm@21611: val th = Goal.norm_result raw_th; wenzelm@21611: val (defs, th') = LocalDefs.export ctxt thy_ctxt th; wenzelm@21708: val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th); wenzelm@21708: val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt); wenzelm@21611: val nprems = Thm.nprems_of th' - Thm.nprems_of th; wenzelm@21611: wenzelm@21611: (*export fixes*) wenzelm@22692: val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); wenzelm@22692: val frees = map Free (Thm.fold_terms Term.add_frees th' []); wenzelm@21611: val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) wenzelm@21611: |> Variable.export ctxt thy_ctxt wenzelm@21611: |> Drule.zero_var_indexes_list; wenzelm@21611: wenzelm@21611: (*thm definition*) wenzelm@28083: val result = PureThy.name_thm true true Position.none name th''; wenzelm@21611: wenzelm@21611: (*import fixes*) wenzelm@21611: val (tvars, vars) = wenzelm@21611: chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) wenzelm@21611: |>> map Logic.dest_type; wenzelm@21611: wenzelm@21611: val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); wenzelm@21611: val inst = filter (is_Var o fst) (vars ~~ frees); wenzelm@21611: val cinstT = map (pairself certT o apfst TVar) instT; wenzelm@21611: val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst; wenzelm@21611: val result' = Thm.instantiate (cinstT, cinst) result; wenzelm@21611: wenzelm@21611: (*import assumes/defines*) wenzelm@21594: val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms); wenzelm@21611: val result'' = wenzelm@21611: (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of wenzelm@21611: NONE => raise THM ("Failed to re-import result", 0, [result']) wenzelm@21845: | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv]) wenzelm@21644: |> Goal.norm_result wenzelm@28083: |> PureThy.name_thm false false Position.none name; wenzelm@21611: wenzelm@21611: in (result'', result) end; wenzelm@21611: haftmann@25684: fun note_local kind facts ctxt = haftmann@25684: ctxt haftmann@25684: |> ProofContext.qualified_names haftmann@25684: |> ProofContext.note_thmss_i kind facts haftmann@25684: ||> ProofContext.restore_naming ctxt; haftmann@25684: haftmann@27690: fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy = wenzelm@21585: let wenzelm@21594: val thy = ProofContext.theory_of lthy; wenzelm@21615: val full = LocalTheory.full_name lthy; wenzelm@21585: wenzelm@21594: val facts' = facts wenzelm@28083: |> map (fn (a, bs) => wenzelm@28083: (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs)) wenzelm@21615: |> PureThy.map_facts (import_export_proof lthy); wenzelm@21611: val local_facts = PureThy.map_facts #1 facts' wenzelm@21611: |> Attrib.map_facts (Attrib.attribute_i thy); wenzelm@21611: val target_facts = PureThy.map_facts #1 facts' wenzelm@25012: |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); wenzelm@21611: val global_facts = PureThy.map_facts #2 facts' wenzelm@25012: |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy); wenzelm@21594: in wenzelm@21611: lthy |> LocalTheory.theory wenzelm@21611: (Sign.qualified_names wenzelm@26132: #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd wenzelm@21611: #> Sign.restore_naming thy) haftmann@25684: |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) ballarin@28834: |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts) haftmann@25684: |> note_local kind local_facts wenzelm@20894: end; wenzelm@20894: wenzelm@20894: wenzelm@25105: (* declare_const *) wenzelm@24939: wenzelm@25105: fun fork_mixfix (Target {is_locale, is_class, ...}) mx = wenzelm@25105: if not is_locale then (NoSyn, NoSyn, mx) wenzelm@25105: else if not is_class then (NoSyn, mx, NoSyn) wenzelm@25105: else (mx, NoSyn, NoSyn); wenzelm@25068: haftmann@28861: fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi = wenzelm@24939: let haftmann@28965: val b' = Morphism.binding phi b; wenzelm@24939: val rhs' = Morphism.term phi rhs; haftmann@28861: val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs')); haftmann@28861: val arg = (b', Term.close_schematic_term rhs'); wenzelm@25372: val similar_body = Type.similar_types (rhs, rhs'); wenzelm@25212: (* FIXME workaround based on educated guess *) haftmann@28965: val (prefix', _) = Binding.dest b'; haftmann@28861: val class_global = Name.name_of b = Name.name_of b' haftmann@28861: andalso not (null prefix') haftmann@28861: andalso (fst o snd o split_last) prefix' = Class.class_prefix target; wenzelm@24939: in wenzelm@25372: not (is_class andalso (similar_body orelse class_global)) ? wenzelm@25212: (Context.mapping_result haftmann@28822: (fn thy => thy |> haftmann@28822: Sign.no_base_names haftmann@28822: |> Sign.add_abbrev PrintMode.internal tags legacy_arg haftmann@28822: ||> Sign.restore_naming thy) wenzelm@26132: (ProofContext.add_abbrev PrintMode.internal tags arg) wenzelm@25212: #-> (fn (lhs' as Const (d, _), _) => wenzelm@25372: similar_body ? wenzelm@25212: (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #> wenzelm@25212: Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) wenzelm@24939: end; wenzelm@24939: wenzelm@28083: fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy = wenzelm@24939: let wenzelm@28083: val c = Name.name_of b; wenzelm@26132: val tags = LocalTheory.group_position_of lthy; wenzelm@24939: val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); wenzelm@25105: val U = map #2 xs ---> T; wenzelm@25105: val (mx1, mx2, mx3) = fork_mixfix ta mx; haftmann@25519: fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); wenzelm@26049: val declare_const = wenzelm@26049: (case Class.instantiation_param lthy c of wenzelm@26049: SOME c' => wenzelm@26049: if mx3 <> NoSyn then syntax_error c' haftmann@25597: else LocalTheory.theory_result (AxClass.declare_overloaded (c', U)) haftmann@25485: ##> Class.confirm_declaration c wenzelm@26049: | NONE => wenzelm@26049: (case Overloading.operation lthy c of wenzelm@26049: SOME (c', _) => wenzelm@26049: if mx3 <> NoSyn then syntax_error c' wenzelm@26049: else LocalTheory.theory_result (Overloading.declare (c', U)) wenzelm@26049: ##> Overloading.confirm c wenzelm@28115: | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3)))); haftmann@25485: val (const, lthy') = lthy |> declare_const; wenzelm@25105: val t = Term.list_comb (const, map Free xs); wenzelm@24939: in wenzelm@24939: lthy' wenzelm@28083: |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t)) wenzelm@26132: |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t)) wenzelm@28083: |> LocalDefs.add_def ((b, NoSyn), t) wenzelm@24939: end; wenzelm@24939: wenzelm@24939: wenzelm@24939: (* abbrev *) wenzelm@24939: wenzelm@28083: fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy = wenzelm@24939: let wenzelm@28083: val c = Name.name_of b; wenzelm@26132: val tags = LocalTheory.group_position_of lthy; wenzelm@25053: val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy); wenzelm@25012: val target_ctxt = LocalTheory.target_of lthy; wenzelm@25105: wenzelm@25105: val (mx1, mx2, mx3) = fork_mixfix ta mx; wenzelm@25105: val t' = Assumption.export_term lthy target_ctxt t; wenzelm@25105: val xs = map Free (rev (Variable.add_fixed target_ctxt t' [])); wenzelm@25105: val u = fold_rev lambda xs t'; wenzelm@25105: val global_rhs = wenzelm@25105: singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u; wenzelm@25121: in wenzelm@25121: lthy |> wenzelm@25121: (if is_locale then haftmann@28861: LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (b, global_rhs)) wenzelm@25121: #-> (fn (lhs, _) => wenzelm@25105: let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in wenzelm@28083: term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #> wenzelm@26132: is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t')) wenzelm@25105: end) wenzelm@25105: else wenzelm@25121: LocalTheory.theory haftmann@28861: (Sign.add_abbrev (#1 prmode) tags (b, global_rhs) #-> (fn (lhs, _) => wenzelm@25121: Sign.notation true prmode [(lhs, mx3)]))) haftmann@28861: |> ProofContext.add_abbrev PrintMode.internal tags (b, t) |> snd wenzelm@28083: |> LocalDefs.fixed_abbrev ((b, NoSyn), t) wenzelm@24939: end; wenzelm@24939: wenzelm@24939: wenzelm@25022: (* define *) wenzelm@24939: haftmann@25485: fun define (ta as Target {target, is_locale, is_class, ...}) wenzelm@28083: kind ((b, mx), ((name, atts), rhs)) lthy = wenzelm@24939: let wenzelm@24987: val thy = ProofContext.theory_of lthy; wenzelm@24939: val thy_ctxt = ProofContext.init thy; wenzelm@24939: wenzelm@28083: val c = Name.name_of b; haftmann@28965: val name' = Binding.map_base (Thm.def_name_optional c) name; wenzelm@24987: val (rhs', rhs_conv) = wenzelm@24987: LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of; wenzelm@24987: val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' []; wenzelm@24939: val T = Term.fastype_of rhs; wenzelm@24939: wenzelm@25105: (*const*) wenzelm@28083: val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx); wenzelm@25022: val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def); wenzelm@24939: wenzelm@24939: (*def*) wenzelm@26049: val define_const = wenzelm@26049: (case Overloading.operation lthy c of wenzelm@26049: SOME (_, checked) => haftmann@25519: (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs)) wenzelm@26049: | NONE => wenzelm@26049: if is_none (Class.instantiation_param lthy c) haftmann@25519: then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq)) wenzelm@26049: else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs))); wenzelm@25022: val (global_def, lthy3) = lthy2 wenzelm@28083: |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs')); haftmann@25485: val def = LocalDefs.trans_terms lthy3 wenzelm@25022: [(*c == global.c xs*) local_def, wenzelm@25022: (*global.c xs == rhs'*) global_def, haftmann@25485: (*rhs' == rhs*) Thm.symmetric rhs_conv]; wenzelm@24939: wenzelm@25105: (*note*) wenzelm@24939: val ([(res_name, [res])], lthy4) = lthy3 wenzelm@26132: |> notes ta kind [((name', atts), [([def], [])])]; wenzelm@24939: in ((lhs, (res_name, res)), lthy4) end; wenzelm@24939: wenzelm@24939: wenzelm@25291: (* init *) wenzelm@25291: wenzelm@25291: local wenzelm@20894: wenzelm@25291: fun init_target _ NONE = global_target wenzelm@26049: | init_target thy (SOME target) = wenzelm@26049: make_target target true (Class.is_class thy target) ([], [], []) []; wenzelm@25291: haftmann@25519: fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) = wenzelm@26049: if not (null (#1 instantiation)) then Class.init_instantiation instantiation haftmann@25519: else if not (null overloading) then Overloading.init overloading haftmann@25485: else if not is_locale then ProofContext.init ballarin@28834: else if not is_class then locale_init target haftmann@25485: else Class.init target; haftmann@25269: haftmann@25542: fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = wenzelm@25291: Data.put ta #> wenzelm@25291: LocalTheory.init (NameSpace.base target) wenzelm@25291: {pretty = pretty ta, wenzelm@25291: abbrev = abbrev ta, wenzelm@25291: define = define ta, wenzelm@25291: notes = notes ta, wenzelm@25291: type_syntax = type_syntax ta, wenzelm@25291: term_syntax = term_syntax ta, wenzelm@25291: declaration = declaration ta, wenzelm@25291: reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy), wenzelm@26049: exit = LocalTheory.target_of o wenzelm@26049: (if not (null (#1 instantiation)) then Class.conclude_instantiation wenzelm@26049: else if not (null overloading) then Overloading.conclude wenzelm@26049: else I)} wenzelm@25291: and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta; wenzelm@20894: wenzelm@26049: fun gen_overloading prep_const raw_ops thy = wenzelm@26049: let wenzelm@26049: val ctxt = ProofContext.init thy; wenzelm@26049: val ops = raw_ops |> map (fn (name, const, checked) => wenzelm@26049: (name, Term.dest_Const (prep_const ctxt const), checked)); wenzelm@26049: in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end; wenzelm@26049: wenzelm@25291: in wenzelm@20894: wenzelm@25291: fun init target thy = init_lthy_ctxt (init_target thy target) thy; wenzelm@26049: fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; haftmann@25269: wenzelm@25291: fun context "-" thy = init NONE thy ballarin@28834: | context target thy = init (SOME (locale_intern thy target)) thy; wenzelm@20894: wenzelm@26049: fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); haftmann@25519: wenzelm@26049: val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); wenzelm@26049: val overloading_cmd = gen_overloading Syntax.read_term; haftmann@25462: wenzelm@20894: end; wenzelm@25291: wenzelm@25291: end; wenzelm@25291: