# HG changeset patch # User boehmes # Date 1250840774 -7200 # Node ID 521065a499c64f54c73f5528ec36e84f70ab01a7 # Parent 98674ac811c4ff378950fc21d287788775fe4533 moved Mirabelle to HOL/Tools diff -r 98674ac811c4 -r 521065a499c6 src/HOL/Tools/Mirabelle/Mirabelle.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Mirabelle.thy Fri Aug 21 09:46:14 2009 +0200 @@ -0,0 +1,12 @@ +(* Title: Mirabelle.thy + Author: Jasmin Blanchette and Sascha Boehme +*) + +theory Mirabelle +imports Plain +uses "Tools/mirabelle.ML" +begin + +setup Mirabelle.setup + +end diff -r 98674ac811c4 -r 521065a499c6 src/HOL/Tools/Mirabelle/Tools/mirabelle.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Fri Aug 21 09:46:14 2009 +0200 @@ -0,0 +1,320 @@ +(* Title: mirabelle.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +signature MIRABELLE = +sig + type action + type settings + val register : string -> action -> theory -> theory + val invoke : string -> settings -> theory -> theory + + val timeout : int Config.T + val verbose : bool Config.T + val start_line : int Config.T + 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 +end + + + +structure Mirabelle (*: MIRABELLE*) = +struct + +(* Mirabelle core *) + +type settings = (string * string) list +type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option +type action = settings -> invoked + +structure Registered = TheoryDataFun +( + type T = action Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + 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 (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 +val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true +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 + +fun set_logfile name = + let val _ = File.write (Path.explode name) "" (* erase file content *) + in Config.put_thy logfile name end + +local + +fun log thy s = + let fun append_to n = if n = "" then K () else File.append (Path.explode n) + in append_to (Config.get_thy thy logfile) (s ^ "\n") end + (* FIXME: with multithreading and parallel proofs enabled, we might need to + encapsulate this inside a critical section *) + +fun verbose_msg verbose msg = if verbose then SOME msg else NONE + +fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x + handle TimeLimit.TimeOut => verbose_msg verb "time out" + | ERROR msg => verbose_msg verb ("error: " ^ msg) + +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 in_range _ _ NONE = true + | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) + +fun only_within_range thy pos f x = + let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line + in if in_range l r (Position.line_of pos) then f x else [] end + +fun pretty_print verbose pos name msgs = + let + val file = the_default "unknown file" (Position.file_of pos) + + val str0 = string_of_int o the_default 0 + val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) + + val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc + val head = full_loc ^ " (" ^ name ^ "):" + + fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg]) + in + Pretty.string_of (Pretty.big_list head (map pretty_msg msgs)) + end + +in + +fun basic_hook tr pre post = + let + val thy = Proof.theory_of pre + val pos = Toplevel.pos_of tr + val name = Toplevel.name_of tr + val verb = Config.get_thy thy verbose + val secs = Time.fromSeconds (Config.get_thy thy timeout) + val st = {pre=pre, post=post} + in + Invoked.get thy + |> only_within_range thy pos (map_filter (apply_action (verb, secs) st)) + |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs)) + end + +end + +fun step_hook tr pre post = + (* FIXME: might require wrapping into "interruptible" *) + if can (Proof.assert_backward o Toplevel.proof_of) pre andalso + not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr)) + then basic_hook tr (Toplevel.proof_of pre) (SOME post) + else () (* FIXME: add theory_hook here *) + + + +(* Mirabelle utility functions *) + +val goal_thm_of = snd o snd o Proof.get_goal + +fun can_apply tac st = + let val (ctxt, (facts, goal)) = Proof.get_goal st + in + (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of + SOME (thm, _) => true + | NONE => false) + end + +local + +fun fold_body_thms f = + let + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => + fn (x, seen) => + if Inttab.defined seen i then (x, seen) + else + let + val body' = Future.join body + val (x', seen') = app (n + (if name = "" then 0 else 1)) body' + (x, Inttab.update (i, ()) seen) + in (x' |> n = 0 ? f (name, prop, body'), seen') end) + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end + +in + +fun theorems_in_proof_term thm = + let + val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) + fun collect (s, _, _) = if s <> "" then insert (op =) s else I + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE + fun resolve_thms names = map_filter (member_of names) all_thms + in + resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) + end + +end + +fun theorems_of_sucessful_proof state = + (case state of + NONE => [] + | SOME st => + if not (Toplevel.is_proof st) then [] + else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) + +fun get_setting settings (key, default) = + the_default default (AList.lookup (op =) settings key) + +fun get_int_setting settings (key, default) = + (case Option.map Int.fromString (AList.lookup (op =) settings key) of + SOME (SOME i) => i + | 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 98674ac811c4 -r 521065a499c6 src/HOL/Tools/Mirabelle/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/etc/settings Fri Aug 21 09:46:14 2009 +0200 @@ -0,0 +1,8 @@ +MIRABELLE_HOME="$COMPONENT" + +MIRABELLE_LOGIC=HOL +MIRABELLE_OUTPUT_PATH=/tmp/mirabelle +MIRABELLE_TIMEOUT=30 +MIRABELLE_VERBOSE=false + +ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools" diff -r 98674ac811c4 -r 521065a499c6 src/HOL/Tools/Mirabelle/lib/Tools/mirabelle --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Fri Aug 21 09:46:14 2009 +0200 @@ -0,0 +1,79 @@ +#!/usr/bin/env bash +# +# Author: Sascha Boehme +# +# DESCRIPTION: testing tool for automated proof tools + + +PRG="$(basename "$0")" + +function usage() { + out="$MIRABELLE_OUTPUT_PATH" + timeout="$MIRABELLE_TIMEOUT" + echo + echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" + echo + echo " Options are:" + echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" + 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)" + echo + echo " Apply the given actions (i.e., automated proof tools)" + 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 + 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" + echo " indicating the range the given actions are to be applied." + echo + exit 1 +} + + +## process command line + +# options + +while getopts "L:O:vt:" OPT +do + case "$OPT" in + L) + MIRABELLE_LOGIC="$OPTARG" + ;; + O) + MIRABELLE_OUTPUT_PATH="$OPTARG" + ;; + v) + MIRABELLE_VERBOSE=true + ;; + t) + MIRABELLE_TIMEOUT="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + +ACTIONS="$1" + +shift + + +# setup + +mkdir -p $MIRABELLE_OUTPUT_PATH + + +## main + +for FILE in "$@" +do + perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE" +done + diff -r 98674ac811c4 -r 521065a499c6 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Fri Aug 21 09:46:14 2009 +0200 @@ -0,0 +1,114 @@ +# +# Author: Jasmin Blanchette and Sascha Boehme +# +# Testing tool for automated proof tools. +# + +use File::Basename; + +# environment + +my $isabelle_home = $ENV{'ISABELLE_HOME'}; +my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; +my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; +my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; +my $verbose = $ENV{'MIRABELLE_VERBOSE'}; +my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; + +my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; + + +# arguments + +my $actions = $ARGV[0]; + +my $thy_file = $ARGV[1]; +my $start_line = "0"; +my $end_line = "~1"; +if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME + my $thy_file = $1; + my $start_line = $2; + my $end_line = $3; +} +my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); +my $new_thy_name = $thy_name . "_Mirabelle"; +my $new_thy_file = $output_path . "/" . $new_thy_name . $ext; + + +# setup + +my $setup_thy_name = $thy_name . "_Setup"; +my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; +my $log_file = $output_path . "/" . $thy_name . ".log"; + +open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; + +print SETUP_FILE < + Config.put_thy Mirabelle.timeout $timeout #> + Config.put_thy Mirabelle.verbose $verbose #> + Config.put_thy Mirabelle.start_line $start_line #> + Config.put_thy Mirabelle.end_line $end_line +*} + +END + +foreach (split(/:/, $actions)) { + if (m/([^[]*)(?:\[(.*)\])?/) { + my ($name, $settings_str) = ($1, $2 || ""); + print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" ["; + my $sep = ""; + foreach (split(/,/, $settings_str)) { + if (m/\s*(.*)\s*=\s*(.*)\s*/) { + print SETUP_FILE "$sep(\"$1\", \"$2\")"; + $sep = ", "; + } + } + print SETUP_FILE "] *}\n"; + } +} + +print SETUP_FILE "\nend"; +close SETUP_FILE; + + +# modify target theory file + +open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; +my @lines = ; +close(OLD_FILE); + +my $thy_text = join("", @lines); +my $old_len = length($thy_text); +$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm; +die "No 'imports' found" if length($thy_text) == $old_len; + +open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; +print NEW_FILE $thy_text; +close(NEW_FILE); + +my $root_file = "$output_path/ROOT_$thy_name.ML"; +open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'"; +print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n"; +close(ROOT_FILE); + + +# run isabelle + +my $r = system "$isabelle_home/bin/isabelle-process " . + "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; + + +# cleanup + +unlink $root_file; +unlink $new_thy_file; +unlink $setup_file; + +exit $r; + diff -r 98674ac811c4 -r 521065a499c6 src/HOL/ex/Mirabelle/Mirabelle.thy --- a/src/HOL/ex/Mirabelle/Mirabelle.thy Fri Aug 21 09:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: Mirabelle.thy - Author: Jasmin Blanchette and Sascha Boehme -*) - -theory Mirabelle -imports Plain -uses "Tools/mirabelle.ML" -begin - -setup Mirabelle.setup - -end diff -r 98674ac811c4 -r 521065a499c6 src/HOL/ex/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/ex/Mirabelle/Tools/mirabelle.ML Fri Aug 21 09:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,320 +0,0 @@ -(* Title: mirabelle.ML - Author: Jasmin Blanchette and Sascha Boehme -*) - -signature MIRABELLE = -sig - type action - type settings - val register : string -> action -> theory -> theory - val invoke : string -> settings -> theory -> theory - - val timeout : int Config.T - val verbose : bool Config.T - val start_line : int Config.T - 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 -end - - - -structure Mirabelle (*: MIRABELLE*) = -struct - -(* Mirabelle core *) - -type settings = (string * string) list -type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option -type action = settings -> invoked - -structure Registered = TheoryDataFun -( - type T = action Symtab.table - val empty = Symtab.empty - val copy = I - val extend = I - 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 (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" -val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 -val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true -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 - -fun set_logfile name = - let val _ = File.write (Path.explode name) "" (* erase file content *) - in Config.put_thy logfile name end - -local - -fun log thy s = - let fun append_to n = if n = "" then K () else File.append (Path.explode n) - in append_to (Config.get_thy thy logfile) (s ^ "\n") end - (* FIXME: with multithreading and parallel proofs enabled, we might need to - encapsulate this inside a critical section *) - -fun verbose_msg verbose msg = if verbose then SOME msg else NONE - -fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x - handle TimeLimit.TimeOut => verbose_msg verb "time out" - | ERROR msg => verbose_msg verb ("error: " ^ msg) - -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 in_range _ _ NONE = true - | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) - -fun only_within_range thy pos f x = - let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line - in if in_range l r (Position.line_of pos) then f x else [] end - -fun pretty_print verbose pos name msgs = - let - val file = the_default "unknown file" (Position.file_of pos) - - val str0 = string_of_int o the_default 0 - val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) - - val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc - val head = full_loc ^ " (" ^ name ^ "):" - - fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg]) - in - Pretty.string_of (Pretty.big_list head (map pretty_msg msgs)) - end - -in - -fun basic_hook tr pre post = - let - val thy = Proof.theory_of pre - val pos = Toplevel.pos_of tr - val name = Toplevel.name_of tr - val verb = Config.get_thy thy verbose - val secs = Time.fromSeconds (Config.get_thy thy timeout) - val st = {pre=pre, post=post} - in - Invoked.get thy - |> only_within_range thy pos (map_filter (apply_action (verb, secs) st)) - |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs)) - end - -end - -fun step_hook tr pre post = - (* FIXME: might require wrapping into "interruptible" *) - if can (Proof.assert_backward o Toplevel.proof_of) pre andalso - not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr)) - then basic_hook tr (Toplevel.proof_of pre) (SOME post) - else () (* FIXME: add theory_hook here *) - - - -(* Mirabelle utility functions *) - -val goal_thm_of = snd o snd o Proof.get_goal - -fun can_apply tac st = - let val (ctxt, (facts, goal)) = Proof.get_goal st - in - (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of - SOME (thm, _) => true - | NONE => false) - end - -local - -fun fold_body_thms f = - let - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => - fn (x, seen) => - if Inttab.defined seen i then (x, seen) - else - let - val body' = Future.join body - val (x', seen') = app (n + (if name = "" then 0 else 1)) body' - (x, Inttab.update (i, ()) seen) - in (x' |> n = 0 ? f (name, prop, body'), seen') end) - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end - -in - -fun theorems_in_proof_term thm = - let - val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE - fun resolve_thms names = map_filter (member_of names) all_thms - in - resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) - end - -end - -fun theorems_of_sucessful_proof state = - (case state of - NONE => [] - | SOME st => - if not (Toplevel.is_proof st) then [] - else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) - -fun get_setting settings (key, default) = - the_default default (AList.lookup (op =) settings key) - -fun get_int_setting settings (key, default) = - (case Option.map Int.fromString (AList.lookup (op =) settings key) of - SOME (SOME i) => i - | 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 98674ac811c4 -r 521065a499c6 src/HOL/ex/Mirabelle/etc/settings --- a/src/HOL/ex/Mirabelle/etc/settings Fri Aug 21 09:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -MIRABELLE_HOME="$COMPONENT" - -MIRABELLE_LOGIC=HOL -MIRABELLE_OUTPUT_PATH=/tmp/mirabelle -MIRABELLE_TIMEOUT=30 -MIRABELLE_VERBOSE=false - -ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools" diff -r 98674ac811c4 -r 521065a499c6 src/HOL/ex/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/ex/Mirabelle/lib/Tools/mirabelle Fri Aug 21 09:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,79 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Sascha Boehme -# -# DESCRIPTION: testing tool for automated proof tools - - -PRG="$(basename "$0")" - -function usage() { - out="$MIRABELLE_OUTPUT_PATH" - timeout="$MIRABELLE_TIMEOUT" - echo - echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" - echo - echo " Options are:" - echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" - 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)" - echo - echo " Apply the given actions (i.e., automated proof tools)" - 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 - 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" - echo " indicating the range the given actions are to be applied." - echo - exit 1 -} - - -## process command line - -# options - -while getopts "L:O:vt:" OPT -do - case "$OPT" in - L) - MIRABELLE_LOGIC="$OPTARG" - ;; - O) - MIRABELLE_OUTPUT_PATH="$OPTARG" - ;; - v) - MIRABELLE_VERBOSE=true - ;; - t) - MIRABELLE_TIMEOUT="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - -ACTIONS="$1" - -shift - - -# setup - -mkdir -p $MIRABELLE_OUTPUT_PATH - - -## main - -for FILE in "$@" -do - perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE" -done - diff -r 98674ac811c4 -r 521065a499c6 src/HOL/ex/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/ex/Mirabelle/lib/scripts/mirabelle.pl Fri Aug 21 09:44:55 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,114 +0,0 @@ -# -# Author: Jasmin Blanchette and Sascha Boehme -# -# Testing tool for automated proof tools. -# - -use File::Basename; - -# environment - -my $isabelle_home = $ENV{'ISABELLE_HOME'}; -my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; -my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; -my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; -my $verbose = $ENV{'MIRABELLE_VERBOSE'}; -my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; - -my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; - - -# arguments - -my $actions = $ARGV[0]; - -my $thy_file = $ARGV[1]; -my $start_line = "0"; -my $end_line = "~1"; -if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME - my $thy_file = $1; - my $start_line = $2; - my $end_line = $3; -} -my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); -my $new_thy_name = $thy_name . "_Mirabelle"; -my $new_thy_file = $output_path . "/" . $new_thy_name . $ext; - - -# setup - -my $setup_thy_name = $thy_name . "_Setup"; -my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; -my $log_file = $output_path . "/" . $thy_name . ".log"; - -open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; - -print SETUP_FILE < - Config.put_thy Mirabelle.timeout $timeout #> - Config.put_thy Mirabelle.verbose $verbose #> - Config.put_thy Mirabelle.start_line $start_line #> - Config.put_thy Mirabelle.end_line $end_line -*} - -END - -foreach (split(/:/, $actions)) { - if (m/([^[]*)(?:\[(.*)\])?/) { - my ($name, $settings_str) = ($1, $2 || ""); - print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" ["; - my $sep = ""; - foreach (split(/,/, $settings_str)) { - if (m/\s*(.*)\s*=\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"$2\")"; - $sep = ", "; - } - } - print SETUP_FILE "] *}\n"; - } -} - -print SETUP_FILE "\nend"; -close SETUP_FILE; - - -# modify target theory file - -open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; -my @lines = ; -close(OLD_FILE); - -my $thy_text = join("", @lines); -my $old_len = length($thy_text); -$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm; -die "No 'imports' found" if length($thy_text) == $old_len; - -open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; -print NEW_FILE $thy_text; -close(NEW_FILE); - -my $root_file = "$output_path/ROOT_$thy_name.ML"; -open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'"; -print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n"; -close(ROOT_FILE); - - -# run isabelle - -my $r = system "$isabelle_home/bin/isabelle-process " . - "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; - - -# cleanup - -unlink $root_file; -unlink $new_thy_file; -unlink $setup_file; - -exit $r; -