# HG changeset patch # User boehmes # Date 1250853679 -7200 # Node ID 594890623c466d946d1b1946ca98f27c7e5b369b # Parent 8629581acc0bbf457ae85eaeedd3c07dcab69103 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Mirabelle.thy --- a/src/HOL/Tools/Mirabelle/Mirabelle.thy Fri Aug 21 09:49:10 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Mirabelle.thy Fri Aug 21 13:21:19 2009 +0200 @@ -3,10 +3,23 @@ *) theory Mirabelle -imports Plain +imports Pure uses "Tools/mirabelle.ML" begin +(* no multithreading, no parallel proofs *) +ML {* Multithreading.max_threads := 1 *} +ML {* Goal.parallel_proofs := 0 *} + +ML {* Toplevel.add_hook Mirabelle.step_hook *} + setup Mirabelle.setup +ML {* +signature MIRABELLE_ACTION = +sig + val invoke : (string * string) list -> theory -> theory end +*} + +end diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Fri Aug 21 09:49:10 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Fri Aug 21 13:21:19 2009 +0200 @@ -5,9 +5,7 @@ signature MIRABELLE = sig type action - type settings - val register : string -> action -> theory -> theory - val invoke : string -> settings -> theory -> theory + val register : string * action -> theory -> theory val timeout : int Config.T val verbose : bool Config.T @@ -15,37 +13,34 @@ val end_line : int Config.T val set_logfile : string -> theory -> theory - val setup : theory -> theory - - val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> - unit - val goal_thm_of : Proof.state -> thm val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : Thm.thm -> Thm.thm list - val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list - val get_setting : settings -> string * string -> string - val get_int_setting : settings -> string * int -> int - -(* FIXME val refute_action : action *) - val quickcheck_action : action - val arith_action : action - val sledgehammer_action : action - val metis_action : action + val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list + val get_setting : (string * string) list -> string * string -> string + val get_int_setting : (string * string) list -> string * int -> int end -structure Mirabelle (*: MIRABELLE*) = +signature MIRABELLE_EXT = +sig + include MIRABELLE + val setup : theory -> theory + val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> + unit +end + + + +structure Mirabelle : MIRABELLE_EXT = struct (* Mirabelle core *) -type settings = (string * string) list -type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option -type action = settings -> invoked +type action = {pre: Proof.state, post: Toplevel.state option} -> string option -structure Registered = TheoryDataFun +structure Actions = TheoryDataFun ( type T = action Symtab.table val empty = Symtab.empty @@ -54,26 +49,7 @@ fun merge _ = Symtab.merge (K true) ) -fun register name act = Registered.map (Symtab.update_new (name, act)) - - -structure Invoked = TheoryDataFun -( - type T = (string * invoked) list - val empty = [] - val copy = I - val extend = I - fun merge _ = Library.merge (K true) -) - -fun invoke name sts thy = - let - val act = - (case Symtab.lookup (Registered.get thy) name of - SOME act => act - | NONE => error ("The invoked action " ^ quote name ^ - " is not registered.")) - in Invoked.map (cons (name, act sts)) thy end +val register = Actions.map o Symtab.update_new val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 @@ -81,7 +57,7 @@ val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0 val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1 -val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5 +val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5 fun set_logfile name = let val _ = File.write (Path.explode name) "" (* erase file content *) @@ -104,8 +80,8 @@ fun capture_exns verb f x = (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg) -fun apply_action (c as (verb, _)) st (name, invoked) = - Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st) +fun apply_action (c as (verb, _)) st (name, action) = + Option.map (pair name) (capture_exns verb (with_time_limit c action) st) fun in_range _ _ NONE = true | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) @@ -140,7 +116,8 @@ val secs = Time.fromSeconds (Config.get_thy thy timeout) val st = {pre=pre, post=post} in - Invoked.get thy + Actions.get thy + |> Symtab.dest |> only_within_range thy pos (map_filter (apply_action (verb, secs) st)) |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs)) end @@ -213,108 +190,4 @@ | SOME NONE => error ("bad option: " ^ key) | NONE => default) - - -(* Mirabelle actions *) - -(* FIXME -fun refute_action settings {pre=st, ...} = - let - val params = [("minsize", "2") (*"maxsize", "2"*)] - val subgoal = 0 - val thy = Proof.theory_of st - val thm = goal_thm_of st - - val _ = Refute.refute_subgoal thy parms thm subgoal - in - val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) - val warn_log = Substring.full (the (Symtab.lookup tab "warning")) - - val r = - if Substring.isSubstring "model found" writ_log - then - if Substring.isSubstring "spurious" warn_log - then SOME "potential counterexample" - else SOME "real counterexample (bug?)" - else - if Substring.isSubstring "time limit" writ_log - then SOME "no counterexample (time out)" - else if Substring.isSubstring "Search terminated" writ_log - then SOME "no counterexample (normal termination)" - else SOME "no counterexample (unknown)" - in r end -*) - -fun quickcheck_action settings {pre=st, ...} = - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst - val args = filter has_valid_key settings - in - (case Quickcheck.quickcheck args 1 st of - NONE => SOME "no counterexample" - | SOME _ => SOME "counterexample found") - end - - -fun arith_action _ {pre=st, ...} = - if can_apply Arith_Data.arith_tac st - then SOME "succeeded" - else NONE - - -fun sledgehammer_action settings {pre=st, ...} = - let - val prover_name = hd (space_explode " " (AtpManager.get_atps ())) - val thy = Proof.theory_of st - - val prover = the (AtpManager.get_prover prover_name thy) - val timeout = AtpManager.get_timeout () - - val (success, message) = - let - val (success, message, _, _, _) = - prover timeout NONE NONE prover_name 1 (Proof.get_goal st) - in (success, message) end - handle ResHolClause.TOO_TRIVIAL => (true, "trivial") - | ERROR msg => (false, "error: " ^ msg) - in - if success - then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")") - else NONE - end - - -fun metis_action settings {pre, post} = - let - val thms = theorems_of_sucessful_proof post - val names = map Thm.get_name thms - - val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) - - fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) - in - (if can_apply metis pre then "succeeded" else "failed") - |> suffix (" (" ^ commas names ^ ")") - |> SOME - end - - - -(* Mirabelle setup *) - -val setup = - setup_config #> -(* FIXME register "refute" refute_action #> *) - register "quickcheck" quickcheck_action #> - register "arith" arith_action #> - register "sledgehammer" sledgehammer_action #> - register "metis" metis_action (* #> FIXME: - Context.theory_map (Specification.add_theorem_hook theorem_hook) *) - end - -val _ = Toplevel.add_hook Mirabelle.step_hook - -(* no multithreading, no parallel proofs *) -val _ = Multithreading.max_threads := 1 -val _ = Goal.parallel_proofs := 0 diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Fri Aug 21 13:21:19 2009 +0200 @@ -0,0 +1,15 @@ +(* Title: mirabelle_arith.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Arith : MIRABELLE_ACTION = +struct + +fun arith_action {pre=st, ...} = + if Mirabelle.can_apply Arith_Data.arith_tac st + then SOME "succeeded" + else NONE + +fun invoke _ = Mirabelle.register ("arith", arith_action) + +end diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Fri Aug 21 13:21:19 2009 +0200 @@ -0,0 +1,24 @@ +(* Title: mirabelle_metis.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Metis : MIRABELLE_ACTION = +struct + +fun metis_action {pre, post} = + let + val thms = Mirabelle.theorems_of_sucessful_proof post + val names = map Thm.get_name thms + + val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) + + fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) + in + (if Mirabelle.can_apply metis pre then "succeeded" else "failed") + |> suffix (" (" ^ commas names ^ ")") + |> SOME + end + +fun invoke _ = Mirabelle.register ("metis", metis_action) + +end diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Fri Aug 21 13:21:19 2009 +0200 @@ -0,0 +1,19 @@ +(* Title: mirabelle_quickcheck.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Quickcheck : MIRABELLE_ACTION = +struct + +fun quickcheck_action args {pre=st, ...} = + let + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst + in + (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of + NONE => SOME "no counterexample" + | SOME _ => SOME "counterexample found") + end + +fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args) + +end diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Fri Aug 21 13:21:19 2009 +0200 @@ -0,0 +1,36 @@ +(* Title: mirabelle_refute.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Refute : MIRABELLE_ACTION = +struct + + +fun refute_action args {pre=st, ...} = + let + val subgoal = 0 + val thy = Proof.theory_of st + val thm = goal_thm_of st + + val _ = Refute.refute_subgoal thy args thm subgoal + in + val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) + val warn_log = Substring.full (the (Symtab.lookup tab "warning")) + + val r = + if Substring.isSubstring "model found" writ_log + then + if Substring.isSubstring "spurious" warn_log + then SOME "potential counterexample" + else SOME "real counterexample (bug?)" + else + if Substring.isSubstring "time limit" writ_log + then SOME "no counterexample (time out)" + else if Substring.isSubstring "Search terminated" writ_log + then SOME "no counterexample (normal termination)" + else SOME "no counterexample (unknown)" + in r end + +fun invoke args = Mirabelle.register ("refute", refute_action args) + +end diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 21 13:21:19 2009 +0200 @@ -0,0 +1,31 @@ +(* Title: mirabelle_sledgehammer.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = +struct + +fun sledgehammer_action {pre=st, ...} = + let + val prover_name = hd (space_explode " " (AtpManager.get_atps ())) + val thy = Proof.theory_of st + + val prover = the (AtpManager.get_prover prover_name thy) + val timeout = AtpManager.get_timeout () + + val (success, message) = + let + val (success, message, _, _, _) = + prover timeout NONE NONE prover_name 1 (Proof.get_goal st) + in (success, message) end + handle ResHolClause.TOO_TRIVIAL => (true, "trivial") + | ERROR msg => (false, "error: " ^ msg) + in + if success + then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")") + else NONE + end + +fun invoke _ = Mirabelle.register ("sledgehammer", sledgehammer_action) + +end diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/etc/settings --- a/src/HOL/Tools/Mirabelle/etc/settings Fri Aug 21 09:49:10 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/etc/settings Fri Aug 21 13:21:19 2009 +0200 @@ -1,6 +1,7 @@ MIRABELLE_HOME="$COMPONENT" MIRABELLE_LOGIC=HOL +MIRABELLE_THEORY=Main MIRABELLE_OUTPUT_PATH=/tmp/mirabelle MIRABELLE_TIMEOUT=30 MIRABELLE_VERBOSE=false diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Fri Aug 21 09:49:10 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Fri Aug 21 13:21:19 2009 +0200 @@ -7,14 +7,21 @@ PRG="$(basename "$0")" +function action_names() { + TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML" + ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'` +} + function usage() { out="$MIRABELLE_OUTPUT_PATH" timeout="$MIRABELLE_TIMEOUT" + action_names echo echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" echo echo " Options are:" echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" + echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" echo " -O DIR output directory for test data (default $out)" echo " -v be verbose" echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" @@ -23,7 +30,11 @@ echo " at all proof steps in the given theory files." echo echo " ACTIONS is a colon-separated list of actions, where each action is" - echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]." + echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:" + for NAME in $ACTION_NAMES + do + echo " $NAME" + done echo echo " FILES is a space-separated list of theory files, where each file is" echo " either NAME.thy or NAME.thy[START:END] and START and END are numbers" @@ -37,12 +48,15 @@ # options -while getopts "L:O:vt:" OPT +while getopts "L:T:O:vt:" OPT do case "$OPT" in L) MIRABELLE_LOGIC="$OPTARG" ;; + T) + MIRABELLE_THEORY="$OPTARG" + ;; O) MIRABELLE_OUTPUT_PATH="$OPTARG" ;; diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Fri Aug 21 09:49:10 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Fri Aug 21 13:21:19 2009 +0200 @@ -11,6 +11,7 @@ my $isabelle_home = $ENV{'ISABELLE_HOME'}; my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; +my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; my $verbose = $ENV{'MIRABELLE_VERBOSE'}; my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; @@ -41,11 +42,23 @@ my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; my $log_file = $output_path . "/" . $thy_name . ".log"; +my @action_files; +foreach (split(/:/, $actions)) { + if (m/([^[]*)/) { + push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; + } +} +my $tools = ""; +if ($#action_files >= 0) { + $tools = "uses " . join(" ", @action_files); +} + open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; print SETUP_FILE <