--- a/src/HOL/IMP/Compiler.thy Thu Aug 08 16:38:28 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Thu Aug 08 16:38:50 2013 +0200
@@ -34,14 +34,11 @@
subsection "Instructions and Stack Machine"
+text_raw{*\snip{instrdef}{0}{1}{% *}
datatype instr =
- LOADI int |
- LOAD vname |
- ADD |
- STORE vname |
- JMP int |
- JMPLESS int |
- JMPGE int
+ LOADI int | LOAD vname | ADD | STORE vname |
+ JMP int | JMPLESS int | JMPGE int
+text_raw{*}%endsnip*}
type_synonym stack = "val list"
type_synonym config = "int \<times> state \<times> stack"
--- a/src/HOL/String.thy Thu Aug 08 16:38:28 2013 +0200
+++ b/src/HOL/String.thy Thu Aug 08 16:38:50 2013 +0200
@@ -420,6 +420,19 @@
and (Haskell) infix 4 "=="
and (Scala) infixl 5 "=="
+setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
+
+definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
+where [simp, code del]: "abort _ f = f ()"
+
+setup {* Sign.map_naming Name_Space.parent_path *}
+
+code_printing constant Code.abort \<rightharpoonup>
+ (SML) "!(raise/ Fail/ _)"
+ and (OCaml) "failwith"
+ and (Haskell) "error"
+ and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
+
hide_type (open) literal
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 08 16:38:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 08 16:38:50 2013 +0200
@@ -495,4 +495,43 @@
val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ =
+ Query_Operation.register_parallel sledgehammerN
+ (fn st => fn [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] =>
+ (case try Toplevel.proof_of st of
+ SOME state =>
+ let
+ val ctxt = Proof.context_of state
+
+ val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
+ val override_params =
+ ([("timeout", [timeout_arg]),
+ ("blocking", ["true"])] @
+ (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
+ then [("isar_proofs", [isar_proofs_arg])] else []) @
+ (if debug then [("debug", ["false"])] else []) @
+ (if verbose then [("verbose", ["false"])] else []) @
+ (if overlord then [("overlord", ["false"])] else []))
+ |> map (normalize_raw_param ctxt)
+
+ val i = the_default 1 (Int.fromString subgoal_arg)
+
+ val {provers, ...} =
+ get_params Normal ctxt
+ (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
+
+ fun run prover =
+ let
+ val prover_params = ("provers", [prover]) :: override_params
+ val sledgehammer_params = get_params Normal ctxt prover_params
+ val minimize = minimize_command prover_params i
+ val (_, (_, state')) =
+ state
+ |> Proof.map_context (Config.put sledgehammer_result_request true)
+ |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
+ in Config.get (Proof.context_of state') sledgehammer_result end
+
+ in map (fn prover => fn () => run prover) provers end
+ | NONE => error "Unknown proof context"));
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Aug 08 16:38:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Aug 08 16:38:50 2013 +0200
@@ -19,6 +19,8 @@
val timeoutN : string
val unknownN : string
val string_of_factss : (string * fact list) list -> string
+ val sledgehammer_result_request : bool Config.T
+ val sledgehammer_result : string Config.T
val run_sledgehammer :
params -> mode -> int -> fact_override
-> ((string * string list) list -> string -> minimize_command)
@@ -64,6 +66,11 @@
(if blocking then "."
else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
+val sledgehammer_result_request =
+ Config.bool (Config.declare "sledgehammer_result_request" (fn _ => Config.Bool false));
+val sledgehammer_result =
+ Config.string (Config.declare "sledgehammer_result" (fn _ => Config.String ""));
+
fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
timeout, expect, ...})
mode minimize_command only learn
@@ -145,15 +152,19 @@
else if blocking then
let
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
- in
- (if outcome_code = someN orelse mode = Normal then
- quote name ^ ": " ^ message ()
- else
- "")
- |> Async_Manager.break_into_chunks
- |> List.app Output.urgent_message;
- (outcome_code, state)
- end
+ val state' =
+ if Config.get ctxt sledgehammer_result_request then
+ state |> Proof.map_context
+ (Config.put sledgehammer_result (quote name ^ ": " ^ message ()))
+ else
+ ((if outcome_code = someN orelse mode = Normal then
+ quote name ^ ": " ^ message ()
+ else
+ "")
+ |> Async_Manager.break_into_chunks
+ |> List.app Output.urgent_message;
+ state)
+ in (outcome_code, state') end
else
(Async_Manager.thread SledgehammerN birth_time death_time (desc ())
((fn (outcome_code, message) =>
@@ -187,7 +198,8 @@
if null provers then
error "No prover is set."
else case subgoal_count state of
- 0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
+ 0 =>
+ ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
| n =>
let
val _ = Proof.assert_backward state
@@ -245,7 +257,9 @@
mash_learn_proof ctxt params prover (prop_of goal) all_facts
val launch = launch_prover params mode minimize_command only learn
in
- if mode = Auto_Try then
+ if mode = Auto_Try orelse
+ Config.get (Proof.context_of state) sledgehammer_result_request
+ then
(unknownN, state)
|> fold (fn prover => fn accum as (outcome_code, _) =>
if outcome_code = someN then accum
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Aug 08 16:38:28 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Aug 08 16:38:50 2013 +0200
@@ -41,6 +41,7 @@
"src/rendering.scala"
"src/rich_text_area.scala"
"src/scala_console.scala"
+ "src/sledgehammer_dockable.scala"
"src/symbols_dockable.scala"
"src/syslog_dockable.scala"
"src/text_overview.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Thu Aug 08 16:38:28 2013 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Thu Aug 08 16:38:50 2013 +0200
@@ -37,6 +37,7 @@
isabelle.protocol-panel \
isabelle.raw-output-panel \
isabelle.readme-panel \
+ isabelle.sledgehammer-panel \
isabelle.symbols-panel \
isabelle.syslog-panel \
isabelle.theories-panel \
@@ -48,6 +49,7 @@
isabelle.protocol-panel.label=Protocol panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.readme-panel.label=README panel
+isabelle.sledgehammer-panel.label=Sledgehammer panel
isabelle.symbols-panel.label=Symbols panel
isabelle.syslog-panel.label=Syslog panel
isabelle.theories-panel.label=Theories panel
@@ -63,6 +65,7 @@
isabelle-raw-output.title=Raw Output
isabelle-documentation.title=Documentation
isabelle-readme.title=README
+isabelle-sledgehammer.title=Sledgehammer
isabelle-symbols.title=Symbols
isabelle-syslog.title=Syslog
isabelle-theories.title=Theories
--- a/src/Tools/jEdit/src/actions.xml Thu Aug 08 16:38:28 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Thu Aug 08 16:38:50 2013 +0200
@@ -32,6 +32,11 @@
wm.addDockableWindow("isabelle-find");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.sledgehammer-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-sledgehammer");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.output-panel">
<CODE>
wm.addDockableWindow("isabelle-output");
--- a/src/Tools/jEdit/src/dockables.xml Thu Aug 08 16:38:28 2013 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Thu Aug 08 16:38:50 2013 +0200
@@ -23,6 +23,9 @@
<DOCKABLE NAME="isabelle-find" MOVABLE="TRUE">
new isabelle.jedit.Find_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
+ new isabelle.jedit.Sledgehammer_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
new isabelle.jedit.Info_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Aug 08 16:38:28 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Thu Aug 08 16:38:50 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, CheckBox}
+import scala.swing.{FlowPanel, Button}
import scala.swing.event.ButtonClicked
import java.lang.System
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Aug 08 16:38:50 2013 +0200
@@ -0,0 +1,144 @@
+/* Title: Tools/jEdit/src/sledgehammer_dockable.scala
+ Author: Makarius
+
+Dockable window for Sledgehammer.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import scala.swing.{FlowPanel, Button, Component, Label, TextField, CheckBox}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.HistoryTextField
+
+
+class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ Swing_Thread.require()
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+
+ /* query operation */
+
+ private val sledgehammer =
+ Query_Operation(view, "sledgehammer",
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+
+ /* resize */
+
+ private var zoom_factor = 100
+
+ private def handle_resize()
+ {
+ Swing_Thread.require()
+
+ pretty_text_area.resize(Rendering.font_family(),
+ (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ }
+
+ private val delay_resize =
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case _: Session.Global_Options =>
+ Swing_Thread.later { handle_resize() }
+ case bad =>
+ java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ PIDE.session.global_options += main_actor
+ handle_resize()
+ sledgehammer.activate()
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ sledgehammer.deactivate()
+ PIDE.session.global_options -= main_actor
+ delay_resize.revoke()
+ }
+
+
+ /* controls */
+
+ private def clicked {
+ sledgehammer.apply_query(
+ List(provers.getText, timeout.text, subgoal.text, isar_proofs.selected.toString))
+ }
+
+ private val provers_label = new Label("Provers: ") {
+ tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")"
+ }
+
+ private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
+ setToolTipText(provers_label.tooltip)
+ setColumns(20)
+ }
+
+ private val timeout = new TextField("30.0", 5) {
+ tooltip = "Soft time limit for each automatic prover (seconds > 0)"
+ verifier = (s: String) =>
+ s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false }
+ }
+
+ private val subgoal = new TextField("1", 5) {
+ tooltip = "Subgoal number"
+ verifier = (s: String) =>
+ s match { case Properties.Value.Int(x) => x > 0 case _ => false }
+ }
+
+ private val isar_proofs = new CheckBox("Isar proofs") {
+ tooltip = "Specify whether Isar proofs should be output in addition to metis line"
+ selected = false
+ }
+
+ private val apply_query = new Button("Apply") {
+ tooltip = "Search for first-order proof using automatic theorem provers"
+ reactions += { case ButtonClicked(_) => clicked }
+ }
+
+ private val locate_query = new Button("Locate") {
+ tooltip = "Locate context of current query within source text"
+ reactions += { case ButtonClicked(_) => sledgehammer.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)(
+ provers_label, Component.wrap(provers), timeout, subgoal, isar_proofs,
+ sledgehammer.animation, apply_query, locate_query, zoom)
+ add(controls.peer, BorderLayout.NORTH)
+}