# HG changeset patch # User ballarin # Date 1111680217 -3600 # Node ID 484178635bd8022b907065c03da26e65bf31f680 # Parent 8b40f741597ccada8982bc197f54a1bba922f49a Further work on interpretation commands. New command `interpret' for interpretation in proof contexts. diff -r 8b40f741597c -r 484178635bd8 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Thu Mar 24 16:36:40 2005 +0100 +++ b/etc/isar-keywords-ZF.el Thu Mar 24 17:03:37 2005 +0100 @@ -74,6 +74,7 @@ "init_toplevel" "instance" "instantiate" + "interpret" "interpretation" "judgment" "kill" @@ -389,6 +390,7 @@ (defconst isar-keywords-proof-goal '("have" "hence" + "interpret" "show" "thus")) diff -r 8b40f741597c -r 484178635bd8 etc/isar-keywords.el --- a/etc/isar-keywords.el Thu Mar 24 16:36:40 2005 +0100 +++ b/etc/isar-keywords.el Thu Mar 24 17:03:37 2005 +0100 @@ -77,6 +77,7 @@ "init_toplevel" "instance" "instantiate" + "interpret" "interpretation" "judgment" "kill" @@ -423,6 +424,7 @@ (defconst isar-keywords-proof-goal '("have" "hence" + "interpret" "show" "thus")) diff -r 8b40f741597c -r 484178635bd8 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Thu Mar 24 16:36:40 2005 +0100 +++ b/src/FOL/ex/LocaleTest.thy Thu Mar 24 17:03:37 2005 +0100 @@ -20,7 +20,7 @@ print_interps L print_interps M -interpretation test [simp]: L . +interpretation test [simp]: L print_interps M . interpretation L . @@ -52,8 +52,19 @@ print_interps A -(* -thm asm_A a.asm_A p1.a.asm_A +(* possible accesses +thm p1.a.asm_A thm LocaleTest.p1.a.asm_A +thm LocaleTest.asm_A thm p1.asm_A +*) + +(* without prefix *) + +interpretation C ["W::'b" "Z::'b"] by (auto intro: A.intro C_axioms.intro) + +print_interps A + +(* possible accesses +thm a.asm_A thm asm_A thm LocaleTest.a.asm_A thm LocaleTest.asm_A *) interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute) @@ -64,7 +75,7 @@ thm p2.a.asm_A *) -interpretation p3: D [X Y] by (auto intro: A.intro) +interpretation p3: D [X Y] . (* duplicate: not registered *) (* @@ -87,4 +98,18 @@ interpretation A [Z] apply - apply (auto intro: A.intro) done *) +theorem True +proof - + fix alpha::i and beta::i and gamma::i + assume "A(alpha)" + then interpret p5: A [alpha] . + print_interps A + interpret p6: C [alpha beta] by (auto intro: C_axioms.intro) + print_interps A (* p6 not added! *) + print_interps C +qed rule + +(* lemma "bla.bla": True by rule *) + + end diff -r 8b40f741597c -r 484178635bd8 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/General/name_space.ML Thu Mar 24 17:03:37 2005 +0100 @@ -24,6 +24,7 @@ type T val empty: T val extend: T * string list -> T + val extend': (string -> string list) -> T * string list -> T val merge: T * T -> T val hide: bool -> T * string list -> T val intern: T -> string -> string @@ -97,12 +98,15 @@ (* extend *) (*later entries preferred*) -fun extend_aux (name, tab) = +fun gen_extend_aux acc (name, tab) = if is_hidden name then error ("Attempt to declare hidden name " ^ quote name) - else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name); + else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name); -fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux tab names); +fun extend' acc (NameSpace tab, names) = + NameSpace (foldr (gen_extend_aux acc) tab names); +fun extend (NameSpace tab, names) = + NameSpace (foldr (gen_extend_aux accesses) tab names); (* merge *) (*1st preferred over 2nd*) diff -r 8b40f741597c -r 484178635bd8 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Thu Mar 24 17:03:37 2005 +0100 @@ -222,10 +222,9 @@ Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body) end); -fun print_registrations name = Toplevel.unknown_theory o - Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in - Locale.print_global_registrations thy name - end); +fun print_registrations name = Toplevel.unknown_context o + Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name) + (Locale.print_local_registrations name o Proof.context_of)); val print_attributes = Toplevel.unknown_theory o Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); diff -r 8b40f741597c -r 484178635bd8 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/Isar/isar_syn.ML Thu Mar 24 17:03:37 2005 +0100 @@ -317,11 +317,17 @@ val interpretationP = OuterSyntax.command "interpretation" - "prove and register interpretation of locale expression" K.thy_goal + "prove and register interpretation of locale expression in theory" K.thy_goal ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val >> IsarThy.register_globally) >> (Toplevel.print oo Toplevel.theory_to_proof)); +val interpretP = + OuterSyntax.command "interpret" + "prove and register interpretation of locale expression in context" + K.prf_goal + (P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val >> + ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally)); (** proof commands **) @@ -800,7 +806,7 @@ default_proofP, immediate_proofP, done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP, - redoP, undos_proofP, undoP, killP, interpretationP, instantiateP, + redoP, undos_proofP, undoP, killP, interpretationP, interpretP, instantiateP, (*diagnostic commands*) pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, print_syntaxP, print_theoremsP, print_localesP, print_localeP, diff -r 8b40f741597c -r 484178635bd8 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/Isar/isar_thy.ML Thu Mar 24 17:03:37 2005 +0100 @@ -157,6 +157,9 @@ val register_globally: ((string * Args.src list) * Locale.expr) * string option list -> bool -> theory -> ProofHistory.T + val register_locally: + ((string * Args.src list) * Locale.expr) * string option list -> + ProofHistory.T -> ProofHistory.T end; @@ -625,16 +628,16 @@ val context = init_context (ThyInfo.quiet_update_thy true); -(* global registration of locale interpretation *) +(* registration of locale interpretation *) -fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy = +fun register_globally (((prfx, atts), expr), insts) b thy = let - val (thy', propss, activate) = Locale.prep_registration + val (thy', propss, activate) = Locale.prep_global_registration (prfx, map (Attrib.global_attribute thy) atts) expr insts thy; fun witness id (thy, thm) = let val thm' = Drule.freeze_all thm; in - (Locale.global_add_witness id thm' thy, thm') + (Locale.add_global_witness id thm' thy, thm') end; in multi_theorem_i Drule.internalK activate ("", []) [] @@ -642,5 +645,18 @@ map (fn prop => (prop, ([], []))) props)) propss) b thy' end; +fun register_locally (((prfx, atts), expr), insts) = + ProofHistory.apply (fn state => + let + val ctxt = Proof.context_of state; + val (ctxt', propss, activate) = Locale.prep_local_registration + (prfx, map (Attrib.local_attribute' ctxt) atts) expr insts ctxt; + fun witness id (ctxt, thm) = (Locale.add_local_witness id thm ctxt, thm); + in state + |> Proof.map_context (fn _ => ctxt') + |> Proof.interpret_i activate Seq.single true + (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), + map (fn prop => (prop, ([], []))) props)) propss) + end); end; diff -r 8b40f741597c -r 484178635bd8 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/Isar/locale.ML Thu Mar 24 17:03:37 2005 +0100 @@ -68,7 +68,8 @@ (* Diagnostic functions *) val print_locales: theory -> unit val print_locale: theory -> expr -> multi_attribute element list -> unit - val print_global_registrations: theory -> string -> unit + val print_global_registrations: string -> theory -> unit + val print_local_registrations: string -> context -> unit val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list @@ -85,14 +86,21 @@ val add_thmss: string -> ((string * thm list) * multi_attribute list) list -> theory * context -> (theory * context) * (string * thm list) list + (* Locale interpretation *) val instantiate: string -> string * context attribute list -> thm list option -> context -> context - val prep_registration: + val prep_global_registration: string * theory attribute list -> expr -> string option list -> theory -> theory * ((string * term list) * term list) list * (theory -> theory) - val global_add_witness: + val prep_local_registration: + string * context attribute list -> expr -> string option list -> context -> + context * ((string * term list) * term list) list * (context -> context) + val add_global_witness: string * term list -> thm -> theory -> theory + val add_local_witness: + string * term list -> thm -> context -> context + (* Theory setup for locales *) val setup: (theory -> theory) list end; @@ -138,7 +146,7 @@ (cf. [1], normalisation of locale expressions.) *) import: expr, (*dynamic import*) - elems: (multi_attribute element_i * stamp) list, (*static content*) + elems: (multi_attribute element_i * stamp) list, (*static content*) params: (string * typ option) list * string list} (*all/local params*) @@ -147,7 +155,7 @@ structure Termlisttab = TableFun(type key = term list val ord = Library.list_ord Term.term_ord); -structure LocalesArgs = +structure GlobalLocalesArgs = struct val name = "Isar/locales"; type T = NameSpace.T * locale Symtab.table * @@ -180,24 +188,41 @@ |> Pretty.writeln; end; -structure LocalesData = TheoryDataFun(LocalesArgs); -val print_locales = LocalesData.print; +structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs); + +(** context data **) -val intern = NameSpace.intern o #1 o LocalesData.get_sg; -val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; +structure LocalLocalesArgs = +struct + val name = "Isar/locales"; + type T = ((string * context attribute list) * thm list) Termlisttab.table + Symtab.table; + (* registrations: theorems instantiating locale assumptions, + with prefix and attributes, indexed by locale name and parameter + instantiation *) + fun init _ = Symtab.empty; + fun print _ _ = (); +end; + +structure LocalLocalesData = ProofDataFun(LocalLocalesArgs); (* access locales *) +val print_locales = GlobalLocalesData.print; + +val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg; +val cond_extern = NameSpace.cond_extern o #1 o GlobalLocalesData.get_sg; + fun declare_locale name = - LocalesData.map (fn (space, locs, regs) => + GlobalLocalesData.map (fn (space, locs, regs) => (NameSpace.extend (space, [name]), locs, regs)); fun put_locale name loc = - LocalesData.map (fn (space, locs, regs) => + GlobalLocalesData.map (fn (space, locs, regs) => (space, Symtab.update ((name, loc), locs), regs)); -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name); +fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name); fun the_locale thy name = (case get_locale thy name of @@ -207,34 +232,73 @@ (* access registrations *) -(* add registration to theory, ignored if already present *) +(* retrieve registration from theory or context *) + +fun gen_get_registration get thy_ctxt (name, ps) = + case Symtab.lookup (get thy_ctxt, name) of + NONE => NONE + | SOME tab => Termlisttab.lookup (tab, ps); + +val get_global_registration = + gen_get_registration (#3 o GlobalLocalesData.get); +val get_local_registration = + gen_get_registration LocalLocalesData.get; -fun global_put_registration (name, ps) attn = - LocalesData.map (fn (space, locs, regs) => - (space, locs, let +val test_global_registration = isSome oo get_global_registration; +val test_local_registration = isSome oo get_local_registration; +fun smart_test_registration ctxt id = + let + val thy = ProofContext.theory_of ctxt; + in + test_global_registration thy id orelse test_local_registration ctxt id + end; + + +(* add registration to theory or context, ignored if already present *) + +fun gen_put_registration map (name, ps) attn = + map (fn regs => + let val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty); in Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)), regs) - end handle Termlisttab.DUP _ => regs)); + end handle Termlisttab.DUP _ => regs); + +val put_global_registration = + gen_put_registration (fn f => + GlobalLocalesData.map (fn (space, locs, regs) => + (space, locs, f regs))); +val put_local_registration = gen_put_registration LocalLocalesData.map; -(* add witness theorem to registration in theory, +fun smart_put_registration id attn ctxt = + (* ignore registration if already present in theory *) + let + val thy = ProofContext.theory_of ctxt; + in case get_global_registration thy id of + NONE => put_local_registration id attn ctxt + | SOME _ => ctxt + end; + + +(* add witness theorem to registration in theory or context, ignored if registration not present *) -fun global_add_witness (name, ps) thm = - LocalesData.map (fn (space, locs, regs) => - (space, locs, let +fun gen_add_witness map (name, ps) thm = + map (fn regs => + let val tab = valOf (Symtab.lookup (regs, name)); val (x, thms) = valOf (Termlisttab.lookup (tab, ps)); in Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)), regs) - end handle Option => regs)) + end handle Option => regs); -fun global_get_registration thy (name, ps) = - case Symtab.lookup (#3 (LocalesData.get thy), name) of - NONE => NONE - | SOME tab => Termlisttab.lookup (tab, ps); +val add_global_witness = + gen_add_witness (fn f => + GlobalLocalesData.map (fn (space, locs, regs) => + (space, locs, f regs))); +val add_local_witness = gen_add_witness LocalLocalesData.map; (* import hierarchy @@ -255,28 +319,36 @@ end; -(* registrations *) +(* printing of registrations *) -fun print_global_registrations thy loc = +fun gen_print_registrations get_regs get_sign msg loc thy_ctxt = let - val sg = Theory.sign_of thy; + val sg = get_sign thy_ctxt; val loc_int = intern sg loc; - val (_, _, regs) = LocalesData.get thy; + val regs = get_regs thy_ctxt; val prt_term = Pretty.quote o Sign.pretty_term sg; - fun prt_inst (ts, ((prfx, _), thms)) = let -in + fun prt_inst (ts, ((prfx, _), thms)) = Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1, - Pretty.list "(" ")" (map prt_term ts)] -end; + Pretty.list "(" ")" (map prt_term ts)]; val loc_regs = Symtab.lookup (regs, loc_int); in (case loc_regs of - NONE => Pretty.str "No interpretations." - | SOME r => Pretty.big_list "interpretations:" + NONE => Pretty.str ("No interpretations in " ^ msg ^ ".") + | SOME r => Pretty.big_list ("Interpretations in " ^ msg ^ ":") (map prt_inst (Termlisttab.dest r))) |> Pretty.writeln end; +val print_global_registrations = + gen_print_registrations (#3 o GlobalLocalesData.get) + Theory.sign_of "theory"; +val print_local_registrations' = + gen_print_registrations LocalLocalesData.get + ProofContext.sign_of "context"; +fun print_local_registrations loc ctxt = + (print_global_registrations loc (ProofContext.theory_of ctxt); + print_local_registrations' loc ctxt); + (* diagnostics *) @@ -1747,53 +1819,83 @@ fun extract_asms_elemss elemss = map extract_asms_elems elemss; -(* add registration, without theorems, to theory *) - -fun prep_reg_global attn (thy, (id, _)) = - global_put_registration id attn thy; - -(* activate instantiated facts in theory *) +(* activate instantiated facts in theory or context *) -fun activate_facts_elem _ _ (thy, Fixes _) = thy - | activate_facts_elem _ _ (thy, Assumes _) = thy - | activate_facts_elem _ _ (thy, Defines _) = thy - | activate_facts_elem disch (prfx, atts) (thy, Notes facts) = +fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt + | activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt + | activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt + | activate_facts_elem note_thmss which + disch (prfx, atts) (thy_ctxt, Notes facts) = let - (* extract theory attributes *) - val (Notes facts) = map_attrib_element_i fst (Notes facts); + (* extract theory or context attributes *) + val (Notes facts) = map_attrib_element_i which (Notes facts); (* add attributs from registration *) val facts' = map (apfst (apsnd (fn a => a @ atts))) facts; (* discharge hyps and varify *) - val facts'' = map (apsnd (map (apfst (map (Drule.standard o disch))))) facts'; + val facts'' = map (apsnd (map (apfst (map disch)))) facts'; + (* prefix names *) + val facts''' = map (apfst (apfst (fn name => + if prfx = "" orelse name = "" then name + else NameSpace.pack [prfx, name]))) facts''; in - fst (note_thmss_qualified' "" prfx facts'' thy) + fst (note_thmss prfx facts''' thy_ctxt) end; -fun activate_facts_elems disch (thy, (id, elems)) = +fun activate_facts_elems get_reg note_thmss which + disch (thy_ctxt, (id, elems)) = let - val ((prfx, atts2), _) = valOf (global_get_registration thy id) + val ((prfx, atts2), _) = valOf (get_reg thy_ctxt id) handle Option => error ("(internal) unknown registration of " ^ quote (fst id) ^ " while activating facts."); in - Library.foldl (activate_facts_elem disch (prfx, atts2)) (thy, elems) + Library.foldl (activate_facts_elem note_thmss which + disch (prfx, atts2)) (thy_ctxt, elems) end; -fun activate_facts_elemss all_elemss new_elemss thy = +fun gen_activate_facts_elemss get_reg note_thmss which standard + all_elemss new_elemss thy_ctxt = let val prems = List.concat (List.mapPartial (fn (id, _) => - Option.map snd (global_get_registration thy id) + Option.map snd (get_reg thy_ctxt id) handle Option => error ("(internal) unknown registration of " ^ quote (fst id) ^ " while activating facts.")) all_elemss); - in Library.foldl (activate_facts_elems (Drule.satisfy_hyps prems)) - (thy, new_elemss) end; - -in + in Library.foldl (activate_facts_elems get_reg note_thmss which + (standard o Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end; -fun prep_registration attn expr insts thy = +fun loc_accesses prfx name = + (* full qualified name is T.p.r.n where + T: theory name, p: interpretation prefix, r: renaming prefix, n: name + *) + if prfx = "" then + case NameSpace.unpack name of + [] => [""] + | [T, n] => map NameSpace.pack [[T, n], [n]] + | [T, r, n] => map NameSpace.pack [[T, r, n], (*[T, n],*) [r, n], [n]] + | _ => error ("Locale accesses: illegal name " ^ quote name) + else case NameSpace.unpack name of + [] => [""] + | [T, p, n] => map NameSpace.pack [[T, p, n], [p, n]] + | [T, p, r, n] => map NameSpace.pack + [[T, p, r, n], [T, p, n], [p, r, n], [p, n]] + | _ => error ("Locale accesses: illegal name " ^ quote name); + +val global_activate_facts_elemss = gen_activate_facts_elemss + get_global_registration + (fn prfx => PureThy.note_thmss_qualified_i (loc_accesses prfx) + (Drule.kind "")) + fst Drule.standard; +val local_activate_facts_elemss = gen_activate_facts_elemss + get_local_registration (fn prfx => fn _ => fn ctxt => (ctxt, ctxt)) snd I; +(* +val local_activate_facts_elemss = gen_activate_facts_elemss + get_local_registration (fn prfx => ProofContext.note_thmss_i) snd I; +*) + +fun gen_prep_registration mk_ctxt read_terms test_reg put_reg activate + attn expr insts thy_ctxt = let - val ctxt = ProofContext.init thy; - val sign = Theory.sign_of thy; - val tsig = Sign.tsig_of sign; + val ctxt = mk_ctxt thy_ctxt; + val sign = ProofContext.sign_of ctxt; val (ids, raw_elemss) = flatten (ctxt, intern_expr sign) ([], Expr expr); @@ -1819,8 +1921,7 @@ val tvars = foldr Term.add_typ_tvars [] pvTs; val used = foldr Term.add_typ_varnames [] pvTs; fun sorts (a, i) = assoc (tvars, (a, i)); - val (vs, vinst) = Sign.read_def_terms (sign, K NONE, sorts) used true - given_insts; + val (vs, vinst) = read_terms thy_ctxt sorts used given_insts; (* replace new types (which are TFrees) by ones with new names *) val new_Tnames = foldr Term.add_term_tfree_names [] vs; val new_Tnames' = Term.invent_names used "'a" (length new_Tnames); @@ -1858,9 +1959,9 @@ map (fn Int e => e) elems)) (ids' ~~ all_elemss); - (* remove fragments already registered with theory *) + (* remove fragments already registered with theory or context *) val new_inst_elemss = List.filter (fn (id, _) => - is_none (global_get_registration thy id)) inst_elemss; + not (test_reg thy_ctxt id)) inst_elemss; val propss = extract_asms_elemss new_inst_elemss; @@ -1868,9 +1969,27 @@ (** add registrations to theory, without theorems, these are added after the proof **) - val thy' = Library.foldl (prep_reg_global attn) (thy, new_inst_elemss); + val thy_ctxt' = Library.foldl (fn (thy_ctxt, (id, _)) => + put_reg id attn thy_ctxt) (thy_ctxt, new_inst_elemss); + + in (thy_ctxt', propss, activate inst_elemss new_inst_elemss) end; + +in - in (thy', propss, activate_facts_elemss inst_elemss new_inst_elemss) end; +val prep_global_registration = gen_prep_registration + ProofContext.init + (fn thy => fn sorts => fn used => + Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true) + test_global_registration + put_global_registration + global_activate_facts_elemss; + +val prep_local_registration = gen_prep_registration + I + (fn ctxt => ProofContext.read_termTs ctxt (K false) (K NONE)) + smart_test_registration + put_local_registration + local_activate_facts_elemss; end; (* local *) @@ -1879,7 +1998,7 @@ (** locale theory setup **) val setup = - [LocalesData.init, + [GlobalLocalesData.init, LocalLocalesData.init, add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, SOME Syntax.NoSyn)]], add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]]; diff -r 8b40f741597c -r 484178635bd8 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/Isar/proof.ML Thu Mar 24 17:03:37 2005 +0100 @@ -115,6 +115,12 @@ val have_i: (state -> state Seq.seq) -> bool -> ((string * context attribute list) * (term * (term list * term list)) list) list -> state -> state + val interpret: (context -> context) -> (state -> state Seq.seq) -> bool + -> ((string * context attribute list) * (string * (string list * string list)) list) list + -> state -> state + val interpret_i: (context -> context) -> (state -> state Seq.seq) -> bool + -> ((string * context attribute list) * (term * (term list * term list)) list) list + -> state -> state val at_bottom: state -> bool val local_qed: (state -> state Seq.seq) -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit) @@ -143,11 +149,12 @@ (* type goal *) -(* CB: three kinds of Isar goals are distinguished: +(* CB: four kinds of Isar goals are distinguished: - Theorem: global goal in a theory, corresponds to Isar commands theorem, lemma and corollary, - Have: local goal in a proof, Isar command have - Show: local goal in a proof, Isar command show + - Interpret: local goal in a proof, Isar command interpret *) datatype kind = @@ -156,10 +163,14 @@ locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option, view: cterm list * cterm list, (* target view and includes view *) thy_mod: theory -> theory} | (* used in finish_global to modify final - theory, normally set to I; - used by registration command to activate registrations *) + theory, normally set to I; used by + registration command to activate + registrations *) Show of context attribute list list | - Have of context attribute list list; + Have of context attribute list list | + Interpret of {attss: context attribute list list, + ctxt_mod: context -> context}; (* used in finish_local to modify final + context *) (* CB: this function prints the goal kind (Isar command), name and target in the proof state *) @@ -170,7 +181,8 @@ locale_spec = SOME (name, _), ...}) = s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a) | kind_name _ (Show _) = "show" - | kind_name _ (Have _) = "have"; + | kind_name _ (Have _) = "have" + | kind_name _ (Interpret _) = "interpret"; type goal = (kind * (*result kind*) @@ -824,7 +836,10 @@ val show_i = local_goal' ProofContext.bind_propp_i Show; val have = local_goal ProofContext.bind_propp Have; val have_i = local_goal ProofContext.bind_propp_i Have; - +fun interpret ctxt_mod = local_goal ProofContext.bind_propp + (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod}); +fun interpret_i ctxt_mod = local_goal ProofContext.bind_propp_i + (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod}); (** conclusions **) @@ -872,19 +887,28 @@ results |> map (ProofContext.export false goal_ctxt outer_ctxt) |> Seq.commute |> Seq.map (Library.unflat tss); - val (attss, opt_solve) = + val (attss, opt_solve, ctxt_mod) = (case kind of Show attss => (attss, - export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results) - | Have attss => (attss, Seq.single) + export_goals goal_ctxt (if pr then print_rule else (K (K ()))) + results, I) + | Have attss => (attss, Seq.single, I) + | Interpret {attss, ctxt_mod} => (attss, Seq.single, ctxt_mod) | _ => err_malformed "finish_local" state); in conditional pr (fn () => print_result goal_ctxt (kind_name (sign_of state) kind, names ~~ Library.unflat tss results)); outer_state |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts) +(* original version |> (fn st => Seq.map (fn res => - note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq) + note_thmss_i ((names ~~ attss) ~~ + map (single o Thm.no_attributes) res) st) resultq) +*) + |> (fn st => Seq.map (fn res => + st |> note_thmss_i ((names ~~ attss) ~~ + map (single o Thm.no_attributes) res) + |> map_context ctxt_mod) resultq) |> (Seq.flat o Seq.map opt_solve) |> (Seq.flat o Seq.map after_qed) end; diff -r 8b40f741597c -r 484178635bd8 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 24 17:03:37 2005 +0100 @@ -199,8 +199,8 @@ sort Vartab.table * (*default sorts*) string list * (*used type variables*) term list Symtab.table, - delta: Object.T Symtab.table (* difference between local and global claset and simpset*), - delta_count: int ref (* number of local anonymous thms *) + delta: Object.T Symtab.table (* difference between local and global claset and simpset*), + delta_count: int ref (* number of local anonymous thms *) }; (*type variable occurrences*) exception CONTEXT of string * context; diff -r 8b40f741597c -r 484178635bd8 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/pure_thy.ML Thu Mar 24 17:03:37 2005 +0100 @@ -45,10 +45,24 @@ val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list - val note_thmss: theory attribute -> ((bstring * theory attribute list) * - (thmref * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list - val note_thmss_i: theory attribute -> ((bstring * theory attribute list) * - (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list + val note_thmss: + theory attribute -> ((bstring * theory attribute list) * + (thmref * theory attribute list) list) list -> theory -> + theory * (bstring * thm list) list + val note_thmss_i: + theory attribute -> ((bstring * theory attribute list) * + (thm list * theory attribute list) list) list -> theory -> + theory * (bstring * thm list) list + val note_thmss_qualified: + (string -> string list) -> + theory attribute -> ((bstring * theory attribute list) * + (thmref * theory attribute list) list) list -> theory -> + theory * (bstring * thm list) list + val note_thmss_qualified_i: + (string -> string list) -> + theory attribute -> ((bstring * theory attribute list) * + (thm list * theory attribute list) list) list -> theory -> + theory * (bstring * thm list) list val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory @@ -309,15 +323,15 @@ fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); -fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms) - | enter_thms sg pre_name post_name app_att thy (bname, thms) = +fun gen_enter_thms _ _ _ _ _ app_att thy ("", thms) = app_att (thy, thms) + | gen_enter_thms full acc sg pre_name post_name app_att thy (bname, thms) = let - val name = Sign.full_name sg bname; + val name = full sg bname; val (thy', thms') = app_att (thy, pre_name name thms); val named_thms = post_name name thms'; val r as ref {space, thms_tab, index} = get_theorems_sg sg; - val space' = NameSpace.extend (space, [name]); + val space' = NameSpace.extend' acc (space, [name]); val thms_tab' = Symtab.update ((name, named_thms), thms_tab); val index' = FactIndex.add (K false) (index, (name, named_thms)); in @@ -330,6 +344,7 @@ (thy', named_thms) end; +fun enter_thms sg = gen_enter_thms Sign.full_name NameSpace.accesses sg; (* add_thms(s) *) @@ -351,21 +366,31 @@ local -fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) = +fun gen_note_thss enter get kind_att (thy, ((bname, more_atts), ths_atts)) = let fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); - val (thy', thms) = enter_thms (Theory.sign_of thy) + val (thy', thms) = enter (Theory.sign_of thy) name_thmss (name_thms false) (apsnd List.concat o foldl_map app) thy (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts); in (thy', (bname, thms)) end; -fun gen_note_thmss get kind_att args thy = - foldl_map (gen_note_thss get kind_att) (thy, args); +fun gen_note_thmss enter get kind_att args thy = + foldl_map (gen_note_thss enter get kind_att) (thy, args); in -val note_thmss = gen_note_thmss get_thms; -val note_thmss_i = gen_note_thmss (K I); +(* if path is set, only permit unqualified names *) + +val note_thmss = gen_note_thmss enter_thms get_thms; +val note_thmss_i = gen_note_thmss enter_thms (K I); + +(* always permit qualified names, + clients may specify non-standard access policy *) + +fun note_thmss_qualified acc = + gen_note_thmss (gen_enter_thms Sign.full_name' acc) get_thms; +fun note_thmss_qualified_i acc = + gen_note_thmss (gen_enter_thms Sign.full_name' acc) (K I); end; diff -r 8b40f741597c -r 484178635bd8 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Mar 24 16:36:40 2005 +0100 +++ b/src/Pure/sign.ML Thu Mar 24 17:03:37 2005 +0100 @@ -54,6 +54,7 @@ val typeK: string val constK: string val full_name: sg -> bstring -> string + val full_name': sg -> bstring -> string val full_name_path: sg -> string -> bstring -> string val base_name: string -> bstring val intern: sg -> string -> xstring -> string @@ -491,7 +492,7 @@ fun add_names x = change_space NameSpace.extend x; fun hide_names b x = change_space (NameSpace.hide b) x; -(*make full names*) +(*make full names, standard version*) fun full _ "" = error "Attempt to declare empty name \"\"" | full NONE bname = bname | full (SOME path) bname = @@ -503,6 +504,18 @@ else warning ("Declared non-identifier " ^ quote name); name end; +(*make full names, variant permitting qualified names*) +fun full' _ "" = error "Attempt to declare empty name \"\"" + | full' NONE bname = bname + | full' (SOME path) bname = + let + val bnames = NameSpace.unpack bname; + val name = NameSpace.pack (path @ bnames) + in + if forall Syntax.is_identifier bnames then () + else warning ("Declared non-identifier " ^ quote name); name + end; + (*base name*) val base_name = NameSpace.base; @@ -566,6 +579,7 @@ val intern_tycons = intrn_tycons o spaces_of; val full_name = full o #path o rep_sg; + val full_name' = full' o #path o rep_sg; fun full_name_path sg elems = full (SOME (getOpt (#path (rep_sg sg), []) @ NameSpace.unpack elems));