--- a/NEWS Fri Aug 09 15:40:38 2013 +0200
+++ b/NEWS Fri Aug 09 20:44:46 2013 +0200
@@ -59,6 +59,9 @@
* Support for automatic tools in HOL, which try to prove or disprove
toplevel theorem statements.
+* Dockable window "Find" provides query operations for formal entities
+(GUI front-end to 'find_theorems' command).
+
* Dockable window "Documentation" provides access to Isabelle
documentation.
--- a/src/Pure/Concurrent/par_list.ML Fri Aug 09 15:40:38 2013 +0200
+++ b/src/Pure/Concurrent/par_list.ML Fri Aug 09 20:44:46 2013 +0200
@@ -35,9 +35,13 @@
else
uninterruptible (fn restore_attributes => fn () =>
let
- val group = Future.new_group (Future.worker_group ());
+ val (group, pri) =
+ (case Future.worker_task () of
+ SOME task =>
+ (Future.new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
+ | NONE => (Future.new_group NONE, 0));
val futures =
- Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
+ Future.forks {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
(map (fn x => fn () => f x) xs);
val results =
restore_attributes Future.join_results futures
--- a/src/Pure/Tools/find_theorems.ML Fri Aug 09 15:40:38 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Aug 09 20:44:46 2013 +0200
@@ -9,31 +9,17 @@
sig
datatype 'term criterion =
Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
-
- datatype theorem =
- Internal of Facts.ref * thm | External of Facts.ref * term
-
type 'term query = {
goal: thm option,
limit: int option,
rem_dups: bool,
criteria: (bool * 'term criterion) list
}
-
- val read_criterion: Proof.context -> string criterion -> term criterion
val read_query: Position.T -> string -> (bool * string criterion) list
-
val find_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * term criterion) list -> int option * (Facts.ref * thm) list
val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> int option * (Facts.ref * thm) list
-
- val filter_theorems: Proof.context -> theorem list -> term query ->
- int option * theorem list
- val filter_theorems_cmd: Proof.context -> theorem list -> string query ->
- int option * theorem list
-
- val pretty_theorem: Proof.context -> theorem -> Pretty.T
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
end;
@@ -164,18 +150,18 @@
is_nontrivial thy pat andalso
Pattern.matches thy (if po then (pat, obj) else (obj, pat));
- fun substsize pat =
+ fun subst_size pat =
let val (_, subst) =
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
- fun bestmatch [] = NONE
- | bestmatch xs = SOME (foldl1 Int.min xs);
+ fun best_match [] = NONE
+ | best_match xs = SOME (foldl1 Int.min xs);
val match_thm = matches o refine_term;
in
- map (substsize o refine_term) (filter match_thm (extract_terms term_src))
- |> bestmatch
+ map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
+ |> best_match
end;
@@ -222,7 +208,7 @@
val goal_concl = Logic.concl_of_goal goal 1;
val rule_mp = hd (Logic.strip_imp_prems rule);
val rule_concl = Logic.strip_imp_concl rule;
- fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);
+ fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); (* FIXME ?? *)
val rule_tree = combine rule_mp rule_concl;
fun goal_tree prem = combine prem goal_concl;
fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
@@ -244,11 +230,11 @@
val ctxt' = Proof_Context.transfer thy' ctxt;
val goal' = Thm.transfer thy' goal;
- fun etacn thm i =
+ fun limited_etac thm i =
Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
fun try_thm thm =
if Thm.no_prems thm then rtac thm 1 goal'
- else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
+ else (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt')) 1 goal';
in
fn Internal (_, thm) =>
if is_some (Seq.pull (try_thm thm))
@@ -275,16 +261,13 @@
fun get_names t = Term.add_const_names t (Term.add_free_names t []);
-(*Including all constants and frees is only sound because
- matching uses higher-order patterns. If full matching
- were used, then constants that may be subject to
- beta-reduction after substitution of frees should
- not be included for LHS set because they could be
- thrown away by the substituted function.
- e.g. for (?F 1 2) do not include 1 or 2, if it were
- possible for ?F to be (% x y. 3)
- The largest possible set should always be included on
- the RHS.*)
+(*Including all constants and frees is only sound because matching
+ uses higher-order patterns. If full matching were used, then
+ constants that may be subject to beta-reduction after substitution
+ of frees should not be included for LHS set because they could be
+ thrown away by the substituted function. E.g. for (?F 1 2) do not
+ include 1 or 2, if it were possible for ?F to be (%x y. 3). The
+ largest possible set should always be included on the RHS.*)
fun filter_pattern ctxt pat =
let
@@ -305,16 +288,14 @@
fun err_no_goal c =
error ("Current goal required for " ^ c ^ " search criterion");
-val fix_goal = Thm.prop_of;
-
fun filter_crit _ _ (Name name) = apfst (filter_name name)
| filter_crit _ NONE Intro = err_no_goal "intro"
| filter_crit _ NONE Elim = err_no_goal "elim"
| filter_crit _ NONE Dest = err_no_goal "dest"
| filter_crit _ NONE Solves = err_no_goal "solves"
- | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
- | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
- | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
+ | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
+ | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
@@ -365,7 +346,7 @@
end;
-(* removing duplicates, preferring nicer names, roughly n log n *)
+(* removing duplicates, preferring nicer names, roughly O(n log n) *)
local
@@ -412,7 +393,7 @@
in nicer end;
fun rem_thm_dups nicer xs =
- xs ~~ (1 upto length xs)
+ (xs ~~ (1 upto length xs))
|> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
|> rem_cdups nicer
|> sort (int_ord o pairself #2)
@@ -421,7 +402,10 @@
end;
-(* pretty_theorems *)
+
+(** main operations **)
+
+(* filter_theorems *)
fun all_facts_of ctxt =
let
@@ -460,8 +444,12 @@
in find theorems end;
fun filter_theorems_cmd ctxt theorems raw_query =
- filter_theorems ctxt theorems (map_criteria
- (map (apsnd (read_criterion ctxt))) raw_query);
+ filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query);
+
+
+(* find_theorems *)
+
+local
fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
let
@@ -476,9 +464,18 @@
|> apsnd (map (fn Internal f => f))
end;
+in
+
val find_theorems = gen_find_theorems filter_theorems;
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
+end;
+
+
+(* pretty_theorems *)
+
+local
+
fun pretty_ref ctxt thmref =
let
val (name, sel) =
@@ -495,18 +492,23 @@
| pretty_theorem ctxt (External (thmref, prop)) =
Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
+in
+
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
-fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun pretty_theorems state opt_limit rem_dups raw_criteria =
let
+ val ctxt = Proof.context_of state;
+ val opt_goal = try Proof.simple_goal state |> Option.map #goal;
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val (foundo, theorems) =
+
+ val (opt_found, theorems) =
filter_theorems ctxt (map Internal (all_facts_of ctxt))
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
val returned = length theorems;
val tally_msg =
- (case foundo of
+ (case opt_found of
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
| SOME found =>
"found " ^ string_of_int found ^ " theorem(s)" ^
@@ -522,16 +524,17 @@
grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems)
end |> Pretty.fbreaks |> curry Pretty.blk 0;
-fun pretty_theorems_cmd state opt_lim rem_dups spec =
- let
- val ctxt = Toplevel.context_of state;
- val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
- in pretty_theorems ctxt opt_goal opt_lim rem_dups spec end;
+end;
(** Isar command syntax **)
+fun proof_state st =
+ (case try Toplevel.proof_of st of
+ SOME state => state
+ | NONE => Proof.init (Toplevel.context_of st));
+
local
val criterion =
@@ -563,8 +566,8 @@
Outer_Syntax.improper_command @{command_spec "find_theorems"}
"find theorems meeting specified criteria"
(options -- query >> (fn ((opt_lim, rem_dups), spec) =>
- Toplevel.keep (fn state =>
- Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec))));
+ Toplevel.keep (fn st =>
+ Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
end;
@@ -573,9 +576,17 @@
(** PIDE query operation **)
val _ =
- Query_Operation.register "find_theorems" (fn st => fn args =>
- if can Toplevel.theory_of st then
- Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args))
- else error "Unknown theory context");
+ Query_Operation.register "find_theorems"
+ (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
+ if can Toplevel.context_of st then
+ let
+ val state =
+ if context_arg = "" then proof_state st
+ else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
+ val opt_limit = Int.fromString limit_arg;
+ val rem_dups = allow_dups_arg = "false";
+ val criteria = read_query Position.none query_arg;
+ in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
+ else error "Unknown context");
end;
--- a/src/Tools/jEdit/src/find_dockable.scala Fri Aug 09 15:40:38 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Fri Aug 09 20:44:46 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, Component}
+import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -105,7 +105,14 @@
/* controls */
- private def clicked { find_theorems.apply_query(List(query.getText)) }
+ private def clicked {
+ find_theorems.apply_query(
+ List(limit.text, allow_dups.selected.toString, context.selection.item.name, query.getText))
+ }
+
+ private val query_label = new Label("Search criteria:") {
+ tooltip = "Search criteria for find operation"
+ }
private val query = new HistoryTextField("isabelle-find-theorems") {
override def processKeyEvent(evt: KeyEvent)
@@ -115,26 +122,45 @@
}
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
+ setToolTipText(query_label.tooltip)
+ }
+
+ private case class Context_Entry(val name: String, val description: String)
+ {
+ override def toString = description
}
- private val query_wrapped = Component.wrap(query)
+ private val context_entries =
+ new Context_Entry("", "current context") ::
+ PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
+
+ private val context = new ComboBox[Context_Entry](context_entries) {
+ tooltip = "Search in pre-loaded theory (default: context of current command)"
+ }
+
+ private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
+ tooltip = "Limit of displayed results"
+ verifier = (s: String) =>
+ s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+ }
+
+ private val allow_dups = new CheckBox("Duplicates") {
+ tooltip = "Allow duplicates in result (faster for large theories)"
+ selected = false
+ }
private val apply_query = new Button("Apply") {
tooltip = "Find theorems meeting specified criteria"
reactions += { case ButtonClicked(_) => clicked }
}
- private val locate_query = new Button("Locate") {
- tooltip = "Locate context of current query within source text"
- reactions += { case ButtonClicked(_) => find_theorems.locate_query() }
- }
-
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
tooltip = "Zoom factor for output font size"
}
private val controls =
new FlowPanel(FlowPanel.Alignment.Right)(
- query_wrapped, process_indicator.component, apply_query, locate_query, zoom)
+ query_label, Component.wrap(query), context, limit, allow_dups,
+ process_indicator.component, apply_query, zoom)
add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/jEdit.props Fri Aug 09 15:40:38 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Fri Aug 09 20:44:46 2013 +0200
@@ -178,29 +178,22 @@
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
+isabelle-documentation.dock-position=right
+isabelle-find.dock-position=bottom
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
-isabelle-documentation.dock-position=right
isabelle-readme.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
-isabelle.set-continuous-checking.label=Set continuous checking
-isabelle.reset-continuous-checking.label=Reset continuous checking
-isabelle.toggle-continuous-checking.label=Toggle continuous checking
-isabelle.toggle-continuous-checking.shortcut=C+e ENTER
-isabelle.set-node-required.label=Set node required
-isabelle.reset-node-required.label=Reset node required
-isabelle.toggle-node-required.label=Toggle node required
-isabelle.toggle-node-required.shortcut=C+e SPACE
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-isub.label=Control subscript
isabelle.control-isub.shortcut=C+e DOWN
+isabelle.control-reset.label=Control reset
+isabelle.control-reset.shortcut=C+e LEFT
isabelle.control-sup.label=Control superscript
isabelle.control-sup.shortcut=C+e UP
-isabelle.control-reset.label=Control reset
-isabelle.control-reset.shortcut=C+e LEFT
isabelle.decrease-font-size.label=Decrease font size
isabelle.decrease-font-size.shortcut2=C+SUBTRACT
isabelle.decrease-font-size.shortcut=C+MINUS
@@ -211,8 +204,16 @@
isabelle.increase-font-size.shortcut2=C+ADD
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
+isabelle.increase-font-size2.shortcut=C+EQUALS
#isabelle.increase-font-size2.shortcut2=C+ADD
-isabelle.increase-font-size2.shortcut=C+EQUALS
+isabelle.reset-continuous-checking.label=Reset continuous checking
+isabelle.reset-node-required.label=Reset node required
+isabelle.set-continuous-checking.label=Set continuous checking
+isabelle.set-node-required.label=Set node required
+isabelle.toggle-continuous-checking.label=Toggle continuous checking
+isabelle.toggle-continuous-checking.shortcut=C+e ENTER
+isabelle.toggle-node-required.label=Toggle node required
+isabelle.toggle-node-required.shortcut=C+e SPACE
lang.usedefaultlocale=false
largefilemode=full
line-end.shortcut=END
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Aug 09 15:40:38 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Aug 09 20:44:46 2013 +0200
@@ -110,7 +110,7 @@
List(provers.getText, timeout.text, subgoal.text, isar_proofs.selected.toString))
}
- private val provers_label = new Label("Provers: ") {
+ private val provers_label = new Label("Provers:") {
tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")"
}
@@ -147,7 +147,7 @@
}
private val cancel_query = new Button("Cancel") {
- tooltip = "Interrupt unfinished query process"
+ tooltip = "Interrupt unfinished sledgehammering"
reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
}