--- a/NEWS Thu Aug 14 13:21:19 2014 +0200
+++ b/NEWS Thu Aug 14 19:55:00 2014 +0200
@@ -4,6 +4,12 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Commands 'method_setup' and 'attribute_setup' now work within a
+local theory context.
+
+
*** HOL ***
* Sledgehammer:
--- a/src/Doc/Isar_Ref/Proof.thy Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Thu Aug 14 19:55:00 2014 +0200
@@ -915,7 +915,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
@{rail \<open>
@@ -925,7 +925,7 @@
\begin{description}
\item @{command "method_setup"}~@{text "name = text description"}
- defines a proof method in the current theory. The given @{text
+ defines a proof method in the current context. The given @{text
"text"} has to be an ML expression of type
@{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
basic parsers defined in structure @{ML_structure Args} and @{ML_structure
--- a/src/Doc/Isar_Ref/Spec.thy Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Aug 14 19:55:00 2014 +0200
@@ -1031,7 +1031,7 @@
@{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
@{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{tabular}{rcll}
@{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
@@ -1093,7 +1093,7 @@
concrete outer syntax, for example.
\item @{command "attribute_setup"}~@{text "name = text description"}
- defines an attribute in the current theory. The given @{text
+ defines an attribute in the current context. The given @{text
"text"} has to be an ML expression of type
@{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
structure @{ML_structure Args} and @{ML_structure Attrib}.
--- a/src/Doc/Main/document/root.tex Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Doc/Main/document/root.tex Thu Aug 14 19:55:00 2014 +0200
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper]{article}
+\usepackage[T1]{fontenc}
\oddsidemargin=4.6mm
\evensidemargin=4.6mm
@@ -15,17 +16,15 @@
% this should be the last package used
\usepackage{pdfsetup}
-% urls in roman style, theory text in math-similar italics
+% urls in roman style, theory text in math-similar italics, with literal underscore
\urlstyle{rm}
-\isabellestyle{it}
+\isabellestyle{literal}
% for uniform font size
\renewcommand{\isastyle}{\isastyleminor}
\parindent 0pt\parskip 0.5ex
-\renewcommand{\isacharunderscore}{\_}
-
\usepackage{supertabular}
\begin{document}
--- a/src/Pure/Isar/args.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/args.ML Thu Aug 14 19:55:00 2014 +0200
@@ -51,7 +51,7 @@
val named_text: (string -> string) -> string parser
val named_typ: (string -> typ) -> typ parser
val named_term: (string -> term) -> term parser
- val named_fact: (string -> thm list) -> thm list parser
+ val named_fact: (string -> string option * thm list) -> thm list parser
val named_attribute:
(string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
val typ_abbrev: typ context_parser
@@ -106,7 +106,7 @@
| SOME (Token.Text s) => Pretty.str (quote s)
| SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
| SOME (Token.Term t) => Syntax.pretty_term ctxt t
- | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
+ | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
| _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
@@ -130,7 +130,7 @@
fun transform_values phi = map_args (Token.map_value
(fn Token.Typ T => Token.Typ (Morphism.typ phi T)
| Token.Term t => Token.Term (Morphism.term phi t)
- | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
+ | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
| Token.Attribute att => Token.Attribute (Morphism.transform phi att)
| tok => tok));
@@ -212,15 +212,17 @@
val internal_text = value (fn Token.Text s => s);
val internal_typ = value (fn Token.Typ T => T);
val internal_term = value (fn Token.Term t => t);
-val internal_fact = value (fn Token.Fact ths => ths);
+val internal_fact = value (fn Token.Fact (_, ths) => ths);
val internal_attribute = value (fn Token.Attribute att => att);
fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
-fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
- alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
+fun named_fact get =
+ internal_fact ||
+ named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
+ alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
fun named_attribute att =
internal_attribute ||
--- a/src/Pure/Isar/attrib.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Aug 14 19:55:00 2014 +0200
@@ -38,10 +38,12 @@
val generic_notes: string -> (binding * (thm list * src list) list) list ->
Context.generic -> (string * thm list) list * Context.generic
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
+ val attribute_syntax: attribute context_parser -> Args.src -> attribute
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val local_setup: Binding.binding -> attribute context_parser -> string ->
local_theory -> local_theory
- val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
+ val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+ local_theory -> local_theory
val internal: (morphism -> attribute) -> src
val add_del: attribute -> attribute -> attribute context_parser
val thm_sel: Facts.interval list parser
@@ -101,10 +103,10 @@
val get_attributes = Attributes.get o Context.Proof;
-fun transfer_attributes thy ctxt =
+fun transfer_attributes ctxt =
let
- val attribs' =
- Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
+ val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
+ val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
in Context.proof_map (Attributes.put attribs') ctxt end;
fun print_attributes ctxt =
@@ -131,24 +133,12 @@
Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
in (name, Context.the_theory (Attributes.put attribs' context)) end;
-fun define binding att comment lthy =
- let
- val standard_morphism =
- Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
- val att0 = att o Args.transform_values standard_morphism;
- in
- lthy
- |> Local_Theory.background_theory_result (define_global binding att0 comment)
- |-> (fn name =>
- Local_Theory.map_contexts
- (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
- #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
- let
- val naming = Name_Space.naming_of context;
- val binding' = Morphism.binding phi binding;
- in Attributes.map (Name_Space.alias_table naming binding' name) context end)
- #> pair name)
- end;
+fun define binding att comment =
+ Local_Theory.background_theory_result (define_global binding att comment)
+ #-> (fn name =>
+ Local_Theory.map_contexts (K transfer_attributes)
+ #> Local_Theory.generic_alias Attributes.map binding name
+ #> pair name);
(* check *)
@@ -215,12 +205,13 @@
fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
fun attribute_setup name source cmt =
- Context.theory_map (ML_Context.expression (#pos source)
+ (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+ ML_Lex.read_source false source @
+ ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+ |> ML_Context.expression (#pos source)
"val (name, scan, comment): binding * attribute context_parser * string"
- "Context.map_theory (Attrib.setup name scan comment)"
- (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
- ML_Lex.read_source false source @
- ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+ "Context.map_proof (Attrib.local_setup name scan comment)"
+ |> Context.proof_map;
(* internal attribute *)
@@ -254,7 +245,9 @@
let
val get = Proof_Context.get_fact_generic context;
val get_fact = get o Facts.Fact;
- fun get_named pos name = get (Facts.Named ((name, pos), NONE));
+ fun get_named is_sel pos name =
+ let val (a, ths) = get (Facts.Named ((name, pos), NONE))
+ in (if is_sel then NONE else a, ths) end;
in
Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
let
@@ -264,9 +257,9 @@
||
(Scan.ahead Args.alt_name -- Args.named_fact get_fact
>> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
- Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
- Args.named_fact (get_named pos) -- Scan.option thm_sel
- >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
+ Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) =>
+ Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel
+ >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
-- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
let
val ths = Facts.select thmref fact;
--- a/src/Pure/Isar/isar_cmd.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Aug 14 19:55:00 2014 +0200
@@ -39,9 +39,6 @@
val thy_deps: Toplevel.transition -> Toplevel.transition
val locale_deps: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
- val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
- val unused_thms: (string list * string list option) option ->
- Toplevel.transition -> Toplevel.transition
val print_stmts: string list * (Facts.ref * Attrib.src list) list
-> Toplevel.transition -> Toplevel.transition
val print_thms: string list * (Facts.ref * Attrib.src list) list
@@ -314,28 +311,6 @@
|> sort (int_ord o pairself #1) |> map #2;
in Graph_Display.display_graph gr end);
-fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Thm_Deps.thm_deps (Toplevel.theory_of state)
- (Attrib.eval_thms (Toplevel.context_of state) args));
-
-
-(* find unused theorems *)
-
-fun unused_thms opt_range = Toplevel.keep (fn state =>
- let
- val thy = Toplevel.theory_of state;
- val ctxt = Toplevel.context_of state;
- fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
- val get_theory = Context.get_theory thy;
- in
- Thm_Deps.unused_thms
- (case opt_range of
- NONE => (Theory.parents_of thy, [thy])
- | SOME (xs, NONE) => (map get_theory xs, [thy])
- | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
- |> map pretty_thm |> Pretty.writeln_chunks
- end);
-
(* print theorems, terms, types etc. *)
--- a/src/Pure/Isar/isar_syn.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Aug 14 19:55:00 2014 +0200
@@ -329,16 +329,16 @@
(Parse.ML_source >> Isar_Cmd.local_setup);
val _ =
- Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
+ Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
(Parse.position Parse.name --
Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
- >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+ >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
val _ =
- Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
+ Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
(Parse.position Parse.name --
Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
- >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
+ >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
val _ =
Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
@@ -894,10 +894,6 @@
(Scan.succeed Isar_Cmd.class_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
- (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
-
-val _ =
Outer_Syntax.improper_command @{command_spec "print_binds"}
"print term bindings of proof context -- Proof General legacy"
(Scan.succeed (Toplevel.unknown_context o
@@ -956,11 +952,6 @@
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
-val _ =
- Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
- (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
- Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
-
(** system commands (for interactive mode only) **)
--- a/src/Pure/Isar/local_theory.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML Thu Aug 14 19:55:00 2014 +0200
@@ -63,6 +63,9 @@
val set_defsort: sort -> local_theory -> local_theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+ val generic_alias:
+ (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
+ binding -> string -> local_theory -> local_theory
val class_alias: binding -> class -> local_theory -> local_theory
val type_alias: binding -> string -> local_theory -> local_theory
val const_alias: binding -> string -> local_theory -> local_theory
@@ -102,7 +105,8 @@
target: Proof.context};
fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
- {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
+ {naming = naming, operations = operations, after_close = after_close,
+ brittle = brittle, target = target};
(* context data *)
@@ -167,7 +171,7 @@
fun mark_brittle lthy =
if level lthy = 1 then
- map_top (fn (naming, operations, after_close, brittle, target) =>
+ map_top (fn (naming, operations, after_close, _, target) =>
(naming, operations, after_close, true, target)) lthy
else lthy;
@@ -254,12 +258,12 @@
val operations_of = #operations o top_of;
+fun operation f lthy = f (operations_of lthy) lthy;
+fun operation2 f x y = operation (fn ops => f ops x y);
+
(* primitives *)
-fun operation f lthy = f (operations_of lthy) lthy;
-fun operation2 f x y = operation (fn ops => f ops x y);
-
val pretty = operation #pretty;
val abbrev = operation2 #abbrev;
val define = operation2 #define false;
@@ -270,7 +274,7 @@
assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
-(* basic derived operations *)
+(* theorems *)
val notes = notes_kind "";
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
@@ -289,6 +293,9 @@
(Proof_Context.fact_alias binding' name)
end));
+
+(* default sort *)
+
fun set_defsort S =
declaration {syntax = true, pervasive = false}
(K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
@@ -315,14 +322,21 @@
(* name space aliases *)
-fun alias global_alias local_alias b name =
+fun generic_alias app b name =
+ declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+ let
+ val naming = Name_Space.naming_of context;
+ val b' = Morphism.binding phi b;
+ in app (Name_Space.alias_table naming b' name) context end);
+
+fun syntax_alias global_alias local_alias b name =
declaration {syntax = true, pervasive = false} (fn phi =>
let val b' = Morphism.binding phi b
in Context.mapping (global_alias b' name) (local_alias b' name) end);
-val class_alias = alias Sign.class_alias Proof_Context.class_alias;
-val type_alias = alias Sign.type_alias Proof_Context.type_alias;
-val const_alias = alias Sign.const_alias Proof_Context.const_alias;
+val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
+val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
+val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
--- a/src/Pure/Isar/method.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/method.ML Thu Aug 14 19:55:00 2014 +0200
@@ -66,8 +66,12 @@
val check_name: Proof.context -> xstring * Position.T -> string
val method: Proof.context -> src -> Proof.context -> method
val method_cmd: Proof.context -> src -> Proof.context -> method
+ val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
- val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
+ val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
+ local_theory -> local_theory
+ val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+ local_theory -> local_theory
type modifier = (Proof.context -> Proof.context) * attribute
val section: modifier parser list -> thm list context_parser
val sections: modifier parser list -> thm list list context_parser
@@ -309,7 +313,7 @@
(* method definitions *)
-structure Methods = Theory_Data
+structure Methods = Generic_Data
(
type T = ((src -> Proof.context -> method) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "method";
@@ -317,7 +321,13 @@
fun merge data : T = Name_Space.merge_tables data;
);
-val get_methods = Methods.get o Proof_Context.theory_of;
+val get_methods = Methods.get o Context.Proof;
+
+fun transfer_methods ctxt =
+ let
+ val meths0 = Methods.get (Context.Theory (Proof_Context.theory_of ctxt));
+ val meths' = Name_Space.merge_tables (meths0, get_methods ctxt);
+ in Context.proof_map (Methods.put meths') ctxt end;
fun print_methods ctxt =
let
@@ -331,8 +341,22 @@
|> Pretty.writeln_chunks
end;
-fun add_method name meth comment thy = thy
- |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
+
+(* define *)
+
+fun define_global binding meth comment thy =
+ let
+ val context = Context.Theory thy;
+ val (name, meths') =
+ Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
+ in (name, Context.the_theory (Methods.put meths' context)) end;
+
+fun define binding meth comment =
+ Local_Theory.background_theory_result (define_global binding meth comment)
+ #-> (fn name =>
+ Local_Theory.map_contexts (K transfer_methods)
+ #> Local_Theory.generic_alias Methods.map binding name
+ #> pair name);
(* check *)
@@ -360,17 +384,20 @@
(* method setup *)
-fun setup name scan =
- add_method name
- (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
+fun method_syntax scan src ctxt : method =
+ let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
+
+fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
+fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
fun method_setup name source cmt =
- Context.theory_map (ML_Context.expression (#pos source)
+ (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+ ML_Lex.read_source false source @
+ ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+ |> ML_Context.expression (#pos source)
"val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
- "Context.map_theory (Method.setup name scan comment)"
- (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
- ML_Lex.read_source false source @
- ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+ "Context.map_proof (Method.local_setup name scan comment)"
+ |> Context.proof_map;
--- a/src/Pure/Isar/proof_context.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Aug 14 19:55:00 2014 +0200
@@ -121,7 +121,7 @@
(term list list * (Proof.context -> Proof.context)) * Proof.context
val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
- val get_fact_generic: Context.generic -> Facts.ref -> thm list
+ val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
val get_fact: Proof.context -> Facts.ref -> thm list
val get_fact_single: Proof.context -> Facts.ref -> thm
val get_thms: Proof.context -> xstring -> thm list
@@ -948,22 +948,27 @@
[thm] => thm
| [] => err "Failed to retrieve literal fact"
| _ => err "Ambiguous specification of literal fact");
- in pick ("", Position.none) [thm] end
- | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
+ in pick true ("", Position.none) [thm] end
+ | retrieve pick context (Facts.Named ((xname, pos), sel)) =
let
val thy = Context.theory_of context;
- val (name, thms) =
+ fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
+ val {name, static, thms} =
(case xname of
- "" => (xname, [Thm.transfer thy Drule.dummy_thm])
- | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
+ "" => immediate Drule.dummy_thm
+ | "_" => immediate Drule.asm_rl
| _ => retrieve_generic context (xname, pos));
- in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
+ val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms;
+ in pick (static orelse is_some sel) (name, pos) thms' end;
in
-val get_fact_generic = retrieve (K I);
-val get_fact = retrieve (K I) o Context.Proof;
-val get_fact_single = retrieve Facts.the_single o Context.Proof;
+val get_fact_generic =
+ retrieve (fn static => fn (name, _) => fn thms =>
+ (if static then NONE else SOME name, thms));
+
+val get_fact = retrieve (K (K I)) o Context.Proof;
+val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
fun get_thms ctxt = get_fact ctxt o Facts.named;
fun get_thm ctxt = get_fact_single ctxt o Facts.named;
--- a/src/Pure/Isar/token.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Isar/token.ML Thu Aug 14 19:55:00 2014 +0200
@@ -12,7 +12,8 @@
Error of string | Sync | EOF
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
datatype value =
- Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
+ Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
+ Fact of string option * thm list |
Attribute of morphism -> attribute | Files of file Exn.result list
type T
val str_of_kind: kind -> string
@@ -57,7 +58,7 @@
val mk_text: string -> T
val mk_typ: typ -> T
val mk_term: term -> T
- val mk_fact: thm list -> T
+ val mk_fact: string option * thm list -> T
val mk_attribute: (morphism -> attribute) -> T
val init_assignable: T -> T
val assign: value option -> T -> unit
@@ -91,7 +92,7 @@
Text of string |
Typ of typ |
Term of term |
- Fact of thm list |
+ Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*)
Attribute of morphism -> attribute |
Files of file Exn.result list;
--- a/src/Pure/Pure.thy Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/Pure.thy Thu Aug 14 19:55:00 2014 +0200
@@ -112,6 +112,7 @@
ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
ML_file "Tools/rule_insts.ML";
+ML_file "Tools/thm_deps.ML";
ML_file "Tools/find_theorems.ML"
ML_file "Tools/find_consts.ML"
ML_file "Tools/proof_general_pure.ML"
--- a/src/Pure/ROOT Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/ROOT Thu Aug 14 19:55:00 2014 +0200
@@ -202,7 +202,6 @@
"Thy/latex.ML"
"Thy/present.ML"
"Thy/term_style.ML"
- "Thy/thm_deps.ML"
"Thy/thy_header.ML"
"Thy/thy_info.ML"
"Thy/thy_output.ML"
--- a/src/Pure/ROOT.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/ROOT.ML Thu Aug 14 19:55:00 2014 +0200
@@ -310,7 +310,6 @@
use "PIDE/document.ML";
(*theory and proof operations*)
-use "Thy/thm_deps.ML";
use "Isar/isar_cmd.ML";
use "subgoal.ML";
--- a/src/Pure/Thy/thm_deps.ML Thu Aug 14 13:21:19 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: Pure/Thy/thm_deps.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Visualize dependencies of theorems.
-*)
-
-signature THM_DEPS =
-sig
- val thm_deps: theory -> thm list -> unit
- val unused_thms: theory list * theory list -> (string * thm) list
-end;
-
-structure Thm_Deps: THM_DEPS =
-struct
-
-(* thm_deps *)
-
-fun thm_deps thy thms =
- let
- fun add_dep ("", _, _) = I
- | add_dep (name, _, PBody {thms = thms', ...}) =
- let
- val prefix = #1 (split_last (Long_Name.explode name));
- val session =
- (case prefix of
- a :: _ =>
- (case try (Context.get_theory thy) a of
- SOME thy =>
- (case Present.session_name thy of
- "" => []
- | session => [session])
- | NONE => [])
- | _ => ["global"]);
- val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
- val entry =
- {name = Long_Name.base_name name,
- ID = name,
- dir = space_implode "/" (session @ prefix),
- unfold = false,
- path = "",
- parents = parents,
- content = []};
- in cons entry end;
- val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
- in Graph_Display.display_graph (sort_wrt #ID deps) end;
-
-
-(* unused_thms *)
-
-fun unused_thms (base_thys, thys) =
- let
- fun add_fact space (name, ths) =
- if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
- else
- let val {concealed, group, ...} = Name_Space.the_entry space name in
- fold_rev (fn th =>
- (case Thm.derivation_name th of
- "" => I
- | a => cons (a, (th, concealed, group)))) ths
- end;
- fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
-
- val new_thms =
- fold (add_facts o Global_Theory.facts_of) thys []
- |> sort_distinct (string_ord o pairself #1);
-
- val used =
- Proofterm.fold_body_thms
- (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
- (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
- Symtab.empty;
-
- fun is_unused a = not (Symtab.defined used a);
-
- (* groups containing at least one used theorem *)
- val used_groups = fold (fn (a, (_, _, group)) =>
- if is_unused a then I
- else
- (case group of
- NONE => I
- | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
-
- val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
- if not concealed andalso
- (* FIXME replace by robust treatment of thm groups *)
- member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
- is_unused a
- then
- (case group of
- NONE => ((a, th) :: thms, seen_groups)
- | SOME grp =>
- if Inttab.defined used_groups grp orelse
- Inttab.defined seen_groups grp then q
- else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
- else q) new_thms ([], Inttab.empty);
- in rev thms' end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/thm_deps.ML Thu Aug 14 19:55:00 2014 +0200
@@ -0,0 +1,124 @@
+(* Title: Pure/Tools/thm_deps.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Visualize dependencies of theorems.
+*)
+
+signature THM_DEPS =
+sig
+ val thm_deps: theory -> thm list -> unit
+ val unused_thms: theory list * theory list -> (string * thm) list
+end;
+
+structure Thm_Deps: THM_DEPS =
+struct
+
+(* thm_deps *)
+
+fun thm_deps thy thms =
+ let
+ fun add_dep ("", _, _) = I
+ | add_dep (name, _, PBody {thms = thms', ...}) =
+ let
+ val prefix = #1 (split_last (Long_Name.explode name));
+ val session =
+ (case prefix of
+ a :: _ =>
+ (case try (Context.get_theory thy) a of
+ SOME thy =>
+ (case Present.session_name thy of
+ "" => []
+ | session => [session])
+ | NONE => [])
+ | _ => ["global"]);
+ val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
+ val entry =
+ {name = Long_Name.base_name name,
+ ID = name,
+ dir = space_implode "/" (session @ prefix),
+ unfold = false,
+ path = "",
+ parents = parents,
+ content = []};
+ in cons entry end;
+ val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
+ in Graph_Display.display_graph (sort_wrt #ID deps) end;
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
+ (Parse_Spec.xthms1 >> (fn args =>
+ Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
+
+
+(* unused_thms *)
+
+fun unused_thms (base_thys, thys) =
+ let
+ fun add_fact space (name, ths) =
+ if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
+ else
+ let val {concealed, group, ...} = Name_Space.the_entry space name in
+ fold_rev (fn th =>
+ (case Thm.derivation_name th of
+ "" => I
+ | a => cons (a, (th, concealed, group)))) ths
+ end;
+ fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
+
+ val new_thms =
+ fold (add_facts o Global_Theory.facts_of) thys []
+ |> sort_distinct (string_ord o pairself #1);
+
+ val used =
+ Proofterm.fold_body_thms
+ (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
+ (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+ Symtab.empty;
+
+ fun is_unused a = not (Symtab.defined used a);
+
+ (*groups containing at least one used theorem*)
+ val used_groups = fold (fn (a, (_, _, group)) =>
+ if is_unused a then I
+ else
+ (case group of
+ NONE => I
+ | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
+
+ val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
+ if not concealed andalso
+ (* FIXME replace by robust treatment of thm groups *)
+ member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso
+ is_unused a
+ then
+ (case group of
+ NONE => ((a, th) :: thms, seen_groups)
+ | SOME grp =>
+ if Inttab.defined used_groups grp orelse
+ Inttab.defined seen_groups grp then q
+ else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
+ else q) new_thms ([], Inttab.empty);
+ in rev thms' end;
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
+ (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
+ Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
+ Toplevel.keep (fn state =>
+ let
+ val thy = Toplevel.theory_of state;
+ val ctxt = Toplevel.context_of state;
+ fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
+ val get_theory = Context.get_theory thy;
+ in
+ unused_thms
+ (case opt_range of
+ NONE => (Theory.parents_of thy, [thy])
+ | SOME (xs, NONE) => (map get_theory xs, [thy])
+ | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
+ |> map pretty_thm |> Pretty.writeln_chunks
+ end)));
+
+end;
+
--- a/src/Pure/facts.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/facts.ML Thu Aug 14 19:55:00 2014 +0200
@@ -29,7 +29,8 @@
val extern: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val lookup: Context.generic -> T -> string -> (bool * thm list) option
- val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
+ val retrieve: Context.generic -> T -> xstring * Position.T ->
+ {name: string, static: bool, thms: thm list}
val defined: T -> string -> bool
val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
val dest_static: bool -> T list -> T -> (string * thm list) list
@@ -176,14 +177,18 @@
fun retrieve context facts (xname, pos) =
let
val name = check context facts (xname, pos);
- val thms =
+ val (static, thms) =
(case lookup context facts name of
SOME (static, thms) =>
(if static then ()
else Context_Position.report_generic context pos (Markup.dynamic_fact name);
- thms)
+ (static, thms))
| NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
- in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+ in
+ {name = name,
+ static = static,
+ thms = map (Thm.transfer (Context.theory_of context)) thms}
+ end;
(* static content *)
--- a/src/Pure/global_theory.ML Thu Aug 14 13:21:19 2014 +0200
+++ b/src/Pure/global_theory.ML Thu Aug 14 19:55:00 2014 +0200
@@ -72,7 +72,7 @@
(* retrieve theorems *)
fun get_thms thy xname =
- #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
+ #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
fun get_thm thy xname =
Facts.the_single (xname, Position.none) (get_thms thy xname);