Mirabelle tool script conforming to standard Isabelle tool interface,
tidied Perl script,
moved ML sources to Tools subdirectory
--- a/src/HOL/ex/Mirabelle/Mirabelle.thy Mon Aug 17 10:59:12 2009 +0200
+++ b/src/HOL/ex/Mirabelle/Mirabelle.thy Fri Aug 21 09:44:55 2009 +0200
@@ -3,12 +3,10 @@
*)
theory Mirabelle
-imports Main
-uses "mirabelle.ML"
+imports Plain
+uses "Tools/mirabelle.ML"
begin
-(* FIXME: use a logfile for each theory file *)
-
setup Mirabelle.setup
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Mirabelle/Tools/mirabelle.ML Fri Aug 21 09:44:55 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
--- a/src/HOL/ex/Mirabelle/etc/settings Mon Aug 17 10:59:12 2009 +0200
+++ b/src/HOL/ex/Mirabelle/etc/settings Fri Aug 21 09:44:55 2009 +0200
@@ -1,3 +1,8 @@
MIRABELLE_HOME="$COMPONENT"
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/mirabelle"
+MIRABELLE_LOGIC=HOL
+MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
+MIRABELLE_TIMEOUT=30
+MIRABELLE_VERBOSE=false
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Mirabelle/lib/Tools/mirabelle Fri Aug 21 09:44:55 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
+
--- a/src/HOL/ex/Mirabelle/lib/mirabelle Mon Aug 17 10:59:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-#!/usr/bin/perl -w
-
-use strict;
-use File::Basename;
-
-# Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html
-sub trim {
- my @out = @_;
- for (@out) {
- s/^\s+//;
- s/\s+$//;
- }
- return wantarray ? @out : $out[0];
-}
-
-sub quote {
- my $str = pop;
- return "\"" . $str . "\"";
-}
-
-sub print_usage_and_quit {
- print STDERR "Usage: mirabelle actions file1.thy...\n" .
- " actions: action1:...:actionN\n" .
- " action: name or name[key1=value1,...,keyM=valueM]\n";
- exit 1;
-}
-
-my $num_args = $#ARGV + 1;
-if ($num_args < 2) {
- print_usage_and_quit();
-}
-
-my @action_names;
-my @action_settings;
-
-foreach (split(/:/, $ARGV[0])) {
- my %settings;
-
- $_ =~ /([^[]*)(?:\[(.*)\])?/;
- my ($name, $settings_str) = ($1, $2 || "");
- my @setting_strs = split(/,/, $settings_str);
- foreach (@setting_strs) {
- $_ =~ /(.*)=(.*)/;
- my $key = $1;
- my $value = $2;
- $settings{trim($key)} = trim($value);
- }
-
- push @action_names, trim($name);
- push @action_settings, \%settings;
-}
-
-my $output_path = "/tmp/mirabelle"; # FIXME: generate path
-my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup";
-my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy";
-my $mirabelle_log_file = $output_path . "/mirabelle.log";
-
-mkdir $output_path, 0755;
-
-open(FILE, ">$mirabellesetup_file")
- || die "Could not create file '$mirabellesetup_file'";
-
-my $invoke_lines;
-
-for my $i (0 .. $#action_names) {
- my $settings_str = "";
- my $settings = $action_settings[$i];
- my $key;
- my $value;
-
- while (($key, $value) = each(%$settings)) {
- $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), ";
- }
- $settings_str =~ s/, $//;
-
- $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" ";
- $invoke_lines .= "[$settings_str] *}\n"
-}
-
-print FILE <<EOF;
-theory MirabelleSetup
-imports Mirabelle
-begin
-
-setup {* Mirabelle.set_logfile "$mirabelle_log_file" *}
-
-$invoke_lines
-
-end
-EOF
-
-my $root_text = "";
-my @new_thy_files;
-
-for my $i (1 .. $num_args - 1) {
- my $old_thy_file = $ARGV[$i];
- my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy");
- my $new_thy_name = $base . "Mirabelle";
- my $new_thy_file = $dir . $new_thy_name . $ext;
-
- open(OLD_FILE, "<$old_thy_file")
- || die "Cannot open file $old_thy_file";
- my @lines = <OLD_FILE>;
- 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 "$mirabellesetup_thy_name" /gm;
- die "No 'imports' found" if length($thy_text) == $old_len;
-
- open(NEW_FILE, ">$new_thy_file");
- print NEW_FILE $thy_text;
- close(NEW_FILE);
-
- $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n";
-
- push @new_thy_files, $new_thy_file;
-}
-
-my $root_file = "ROOT_mirabelle.ML";
-open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file";
-print ROOT_FILE $root_text;
-close(ROOT_FILE);
-
-system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL";
-
-# unlink $mirabellesetup_file;
-unlink $root_file;
-unlink @new_thy_files;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Mirabelle/lib/scripts/mirabelle.pl Fri Aug 21 09:44:55 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 <<END;
+theory "$setup_thy_name"
+imports "$mirabelle_thy"
+begin
+
+setup {*
+ Mirabelle.set_logfile "$log_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 = <OLD_FILE>;
+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;
+
--- a/src/HOL/ex/Mirabelle/mirabelle.ML Mon Aug 17 10:59:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,318 +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 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