Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
--- 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"))
--- 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"))
--- 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
--- 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*)
--- 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);
--- 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,
--- 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;
--- 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)]]];
--- 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;
--- 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;
--- 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;
--- 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));