1.1 --- a/etc/components Wed Aug 12 00:26:01 2009 +0200
1.2 +++ b/etc/components Mon Aug 17 10:59:12 2009 +0200
1.3 @@ -13,4 +13,4 @@
1.4 #misc components
1.5 src/HOL/Tools/ATP_Manager
1.6 src/HOL/Library/Sum_Of_Squares
1.7 -
1.8 +src/HOL/ex/Mirabelle
2.1 --- a/lib/scripts/mirabelle Wed Aug 12 00:26:01 2009 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,129 +0,0 @@
2.4 -#!/usr/bin/perl -w
2.5 -
2.6 -use strict;
2.7 -use File::Basename;
2.8 -
2.9 -# Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html
2.10 -sub trim {
2.11 - my @out = @_;
2.12 - for (@out) {
2.13 - s/^\s+//;
2.14 - s/\s+$//;
2.15 - }
2.16 - return wantarray ? @out : $out[0];
2.17 -}
2.18 -
2.19 -sub quote {
2.20 - my $str = pop;
2.21 - return "\"" . $str . "\"";
2.22 -}
2.23 -
2.24 -sub print_usage_and_quit {
2.25 - print STDERR "Usage: mirabelle actions file1.thy...\n" .
2.26 - " actions: action1:...:actionN\n" .
2.27 - " action: name or name[key1=value1,...,keyM=valueM]\n";
2.28 - exit 1;
2.29 -}
2.30 -
2.31 -my $num_args = $#ARGV + 1;
2.32 -if ($num_args < 2) {
2.33 - print_usage_and_quit();
2.34 -}
2.35 -
2.36 -my @action_names;
2.37 -my @action_settings;
2.38 -
2.39 -foreach (split(/:/, $ARGV[0])) {
2.40 - my %settings;
2.41 -
2.42 - $_ =~ /([^[]*)(?:\[(.*)\])?/;
2.43 - my ($name, $settings_str) = ($1, $2 || "");
2.44 - my @setting_strs = split(/,/, $settings_str);
2.45 - foreach (@setting_strs) {
2.46 - $_ =~ /(.*)=(.*)/;
2.47 - my $key = $1;
2.48 - my $value = $2;
2.49 - $settings{trim($key)} = trim($value);
2.50 - }
2.51 -
2.52 - push @action_names, trim($name);
2.53 - push @action_settings, \%settings;
2.54 -}
2.55 -
2.56 -my $output_path = "/tmp/mirabelle"; # FIXME: generate path
2.57 -my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup";
2.58 -my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy";
2.59 -my $mirabelle_log_file = $output_path . "/mirabelle.log";
2.60 -
2.61 -mkdir $output_path, 0755;
2.62 -
2.63 -open(FILE, ">$mirabellesetup_file")
2.64 - || die "Could not create file '$mirabellesetup_file'";
2.65 -
2.66 -my $invoke_lines;
2.67 -
2.68 -for my $i (0 .. $#action_names) {
2.69 - my $settings_str = "";
2.70 - my $settings = $action_settings[$i];
2.71 - my $key;
2.72 - my $value;
2.73 -
2.74 - while (($key, $value) = each(%$settings)) {
2.75 - $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), ";
2.76 - }
2.77 - $settings_str =~ s/, $//;
2.78 -
2.79 - $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" ";
2.80 - $invoke_lines .= "[$settings_str] *}\n"
2.81 -}
2.82 -
2.83 -print FILE <<EOF;
2.84 -theory MirabelleSetup
2.85 -imports Mirabelle
2.86 -begin
2.87 -
2.88 -setup {* Mirabelle.set_logfile "$mirabelle_log_file" *}
2.89 -
2.90 -$invoke_lines
2.91 -
2.92 -end
2.93 -EOF
2.94 -
2.95 -my $root_text = "";
2.96 -my @new_thy_files;
2.97 -
2.98 -for my $i (1 .. $num_args - 1) {
2.99 - my $old_thy_file = $ARGV[$i];
2.100 - my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy");
2.101 - my $new_thy_name = $base . "Mirabelle";
2.102 - my $new_thy_file = $dir . $new_thy_name . $ext;
2.103 -
2.104 - open(OLD_FILE, "<$old_thy_file")
2.105 - || die "Cannot open file $old_thy_file";
2.106 - my @lines = <OLD_FILE>;
2.107 - close(OLD_FILE);
2.108 -
2.109 - my $thy_text = join("", @lines);
2.110 - my $old_len = length($thy_text);
2.111 - $thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$mirabellesetup_thy_name" /gm;
2.112 - die "No 'imports' found" if length($thy_text) == $old_len;
2.113 -
2.114 - open(NEW_FILE, ">$new_thy_file");
2.115 - print NEW_FILE $thy_text;
2.116 - close(NEW_FILE);
2.117 -
2.118 - $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n";
2.119 -
2.120 - push @new_thy_files, $new_thy_file;
2.121 -}
2.122 -
2.123 -my $root_file = "ROOT_mirabelle.ML";
2.124 -open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file";
2.125 -print ROOT_FILE $root_text;
2.126 -close(ROOT_FILE);
2.127 -
2.128 -system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL";
2.129 -
2.130 -# unlink $mirabellesetup_file;
2.131 -unlink $root_file;
2.132 -unlink @new_thy_files;
3.1 --- a/src/HOL/ex/Mirabelle.thy Wed Aug 12 00:26:01 2009 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,14 +0,0 @@
3.4 -(* Title: Mirabelle.thy
3.5 - Author: Jasmin Blanchette and Sascha Boehme
3.6 -*)
3.7 -
3.8 -theory Mirabelle
3.9 -imports Main
3.10 -uses "mirabelle.ML"
3.11 -begin
3.12 -
3.13 -(* FIXME: use a logfile for each theory file *)
3.14 -
3.15 -setup Mirabelle.setup
3.16 -
3.17 -end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/ex/Mirabelle/Mirabelle.thy Mon Aug 17 10:59:12 2009 +0200
4.3 @@ -0,0 +1,14 @@
4.4 +(* Title: Mirabelle.thy
4.5 + Author: Jasmin Blanchette and Sascha Boehme
4.6 +*)
4.7 +
4.8 +theory Mirabelle
4.9 +imports Main
4.10 +uses "mirabelle.ML"
4.11 +begin
4.12 +
4.13 +(* FIXME: use a logfile for each theory file *)
4.14 +
4.15 +setup Mirabelle.setup
4.16 +
4.17 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/ex/Mirabelle/etc/settings Mon Aug 17 10:59:12 2009 +0200
5.3 @@ -0,0 +1,3 @@
5.4 +MIRABELLE_HOME="$COMPONENT"
5.5 +
5.6 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/mirabelle"
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/ex/Mirabelle/lib/mirabelle Mon Aug 17 10:59:12 2009 +0200
6.3 @@ -0,0 +1,129 @@
6.4 +#!/usr/bin/perl -w
6.5 +
6.6 +use strict;
6.7 +use File::Basename;
6.8 +
6.9 +# Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html
6.10 +sub trim {
6.11 + my @out = @_;
6.12 + for (@out) {
6.13 + s/^\s+//;
6.14 + s/\s+$//;
6.15 + }
6.16 + return wantarray ? @out : $out[0];
6.17 +}
6.18 +
6.19 +sub quote {
6.20 + my $str = pop;
6.21 + return "\"" . $str . "\"";
6.22 +}
6.23 +
6.24 +sub print_usage_and_quit {
6.25 + print STDERR "Usage: mirabelle actions file1.thy...\n" .
6.26 + " actions: action1:...:actionN\n" .
6.27 + " action: name or name[key1=value1,...,keyM=valueM]\n";
6.28 + exit 1;
6.29 +}
6.30 +
6.31 +my $num_args = $#ARGV + 1;
6.32 +if ($num_args < 2) {
6.33 + print_usage_and_quit();
6.34 +}
6.35 +
6.36 +my @action_names;
6.37 +my @action_settings;
6.38 +
6.39 +foreach (split(/:/, $ARGV[0])) {
6.40 + my %settings;
6.41 +
6.42 + $_ =~ /([^[]*)(?:\[(.*)\])?/;
6.43 + my ($name, $settings_str) = ($1, $2 || "");
6.44 + my @setting_strs = split(/,/, $settings_str);
6.45 + foreach (@setting_strs) {
6.46 + $_ =~ /(.*)=(.*)/;
6.47 + my $key = $1;
6.48 + my $value = $2;
6.49 + $settings{trim($key)} = trim($value);
6.50 + }
6.51 +
6.52 + push @action_names, trim($name);
6.53 + push @action_settings, \%settings;
6.54 +}
6.55 +
6.56 +my $output_path = "/tmp/mirabelle"; # FIXME: generate path
6.57 +my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup";
6.58 +my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy";
6.59 +my $mirabelle_log_file = $output_path . "/mirabelle.log";
6.60 +
6.61 +mkdir $output_path, 0755;
6.62 +
6.63 +open(FILE, ">$mirabellesetup_file")
6.64 + || die "Could not create file '$mirabellesetup_file'";
6.65 +
6.66 +my $invoke_lines;
6.67 +
6.68 +for my $i (0 .. $#action_names) {
6.69 + my $settings_str = "";
6.70 + my $settings = $action_settings[$i];
6.71 + my $key;
6.72 + my $value;
6.73 +
6.74 + while (($key, $value) = each(%$settings)) {
6.75 + $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), ";
6.76 + }
6.77 + $settings_str =~ s/, $//;
6.78 +
6.79 + $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" ";
6.80 + $invoke_lines .= "[$settings_str] *}\n"
6.81 +}
6.82 +
6.83 +print FILE <<EOF;
6.84 +theory MirabelleSetup
6.85 +imports Mirabelle
6.86 +begin
6.87 +
6.88 +setup {* Mirabelle.set_logfile "$mirabelle_log_file" *}
6.89 +
6.90 +$invoke_lines
6.91 +
6.92 +end
6.93 +EOF
6.94 +
6.95 +my $root_text = "";
6.96 +my @new_thy_files;
6.97 +
6.98 +for my $i (1 .. $num_args - 1) {
6.99 + my $old_thy_file = $ARGV[$i];
6.100 + my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy");
6.101 + my $new_thy_name = $base . "Mirabelle";
6.102 + my $new_thy_file = $dir . $new_thy_name . $ext;
6.103 +
6.104 + open(OLD_FILE, "<$old_thy_file")
6.105 + || die "Cannot open file $old_thy_file";
6.106 + my @lines = <OLD_FILE>;
6.107 + close(OLD_FILE);
6.108 +
6.109 + my $thy_text = join("", @lines);
6.110 + my $old_len = length($thy_text);
6.111 + $thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$mirabellesetup_thy_name" /gm;
6.112 + die "No 'imports' found" if length($thy_text) == $old_len;
6.113 +
6.114 + open(NEW_FILE, ">$new_thy_file");
6.115 + print NEW_FILE $thy_text;
6.116 + close(NEW_FILE);
6.117 +
6.118 + $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n";
6.119 +
6.120 + push @new_thy_files, $new_thy_file;
6.121 +}
6.122 +
6.123 +my $root_file = "ROOT_mirabelle.ML";
6.124 +open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file";
6.125 +print ROOT_FILE $root_text;
6.126 +close(ROOT_FILE);
6.127 +
6.128 +system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL";
6.129 +
6.130 +# unlink $mirabellesetup_file;
6.131 +unlink $root_file;
6.132 +unlink @new_thy_files;
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/ex/Mirabelle/mirabelle.ML Mon Aug 17 10:59:12 2009 +0200
7.3 @@ -0,0 +1,318 @@
7.4 +(* Title: mirabelle.ML
7.5 + Author: Jasmin Blanchette and Sascha Boehme
7.6 +*)
7.7 +
7.8 +signature MIRABELLE =
7.9 +sig
7.10 + type action
7.11 + type settings
7.12 + val register : string -> action -> theory -> theory
7.13 + val invoke : string -> settings -> theory -> theory
7.14 +
7.15 + val timeout : int Config.T
7.16 + val verbose : bool Config.T
7.17 + val set_logfile : string -> theory -> theory
7.18 +
7.19 + val setup : theory -> theory
7.20 +
7.21 + val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
7.22 + unit
7.23 +
7.24 + val goal_thm_of : Proof.state -> thm
7.25 + val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
7.26 + val theorems_in_proof_term : Thm.thm -> Thm.thm list
7.27 + val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
7.28 + val get_setting : settings -> string * string -> string
7.29 + val get_int_setting : settings -> string * int -> int
7.30 +
7.31 +(* FIXME val refute_action : action *)
7.32 + val quickcheck_action : action
7.33 + val arith_action : action
7.34 + val sledgehammer_action : action
7.35 + val metis_action : action
7.36 +end
7.37 +
7.38 +
7.39 +
7.40 +structure Mirabelle (*: MIRABELLE*) =
7.41 +struct
7.42 +
7.43 +(* Mirabelle core *)
7.44 +
7.45 +type settings = (string * string) list
7.46 +type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
7.47 +type action = settings -> invoked
7.48 +
7.49 +structure Registered = TheoryDataFun
7.50 +(
7.51 + type T = action Symtab.table
7.52 + val empty = Symtab.empty
7.53 + val copy = I
7.54 + val extend = I
7.55 + fun merge _ = Symtab.merge (K true)
7.56 +)
7.57 +
7.58 +fun register name act = Registered.map (Symtab.update_new (name, act))
7.59 +
7.60 +
7.61 +structure Invoked = TheoryDataFun
7.62 +(
7.63 + type T = (string * invoked) list
7.64 + val empty = []
7.65 + val copy = I
7.66 + val extend = I
7.67 + fun merge _ = Library.merge (K true)
7.68 +)
7.69 +
7.70 +fun invoke name sts thy =
7.71 + let
7.72 + val act =
7.73 + (case Symtab.lookup (Registered.get thy) name of
7.74 + SOME act => act
7.75 + | NONE => error ("The invoked action " ^ quote name ^
7.76 + " is not registered."))
7.77 + in Invoked.map (cons (name, act sts)) thy end
7.78 +
7.79 +val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
7.80 +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
7.81 +val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
7.82 +val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
7.83 +val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
7.84 +
7.85 +val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
7.86 +
7.87 +fun set_logfile name =
7.88 + let val _ = File.write (Path.explode name) "" (* erase file content *)
7.89 + in Config.put_thy logfile name end
7.90 +
7.91 +local
7.92 +
7.93 +fun log thy s =
7.94 + let fun append_to n = if n = "" then K () else File.append (Path.explode n)
7.95 + in append_to (Config.get_thy thy logfile) (s ^ "\n") end
7.96 + (* FIXME: with multithreading and parallel proofs enabled, we might need to
7.97 + encapsulate this inside a critical section *)
7.98 +
7.99 +fun verbose_msg verbose msg = if verbose then SOME msg else NONE
7.100 +
7.101 +fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
7.102 + handle TimeLimit.TimeOut => verbose_msg verb "time out"
7.103 + | ERROR msg => verbose_msg verb ("error: " ^ msg)
7.104 +
7.105 +fun capture_exns verb f x =
7.106 + (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
7.107 +
7.108 +fun apply_action (c as (verb, _)) st (name, invoked) =
7.109 + Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
7.110 +
7.111 +fun in_range _ _ NONE = true
7.112 + | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
7.113 +
7.114 +fun only_within_range thy pos f x =
7.115 + let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
7.116 + in if in_range l r (Position.line_of pos) then f x else [] end
7.117 +
7.118 +fun pretty_print verbose pos name msgs =
7.119 + let
7.120 + val file = the_default "unknown file" (Position.file_of pos)
7.121 +
7.122 + val str0 = string_of_int o the_default 0
7.123 + val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
7.124 +
7.125 + val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
7.126 + val head = full_loc ^ " (" ^ name ^ "):"
7.127 +
7.128 + fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
7.129 + in
7.130 + Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
7.131 + end
7.132 +
7.133 +in
7.134 +
7.135 +fun basic_hook tr pre post =
7.136 + let
7.137 + val thy = Proof.theory_of pre
7.138 + val pos = Toplevel.pos_of tr
7.139 + val name = Toplevel.name_of tr
7.140 + val verb = Config.get_thy thy verbose
7.141 + val secs = Time.fromSeconds (Config.get_thy thy timeout)
7.142 + val st = {pre=pre, post=post}
7.143 + in
7.144 + Invoked.get thy
7.145 + |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
7.146 + |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
7.147 + end
7.148 +
7.149 +end
7.150 +
7.151 +fun step_hook tr pre post =
7.152 + (* FIXME: might require wrapping into "interruptible" *)
7.153 + if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
7.154 + not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
7.155 + then basic_hook tr (Toplevel.proof_of pre) (SOME post)
7.156 + else () (* FIXME: add theory_hook here *)
7.157 +
7.158 +
7.159 +
7.160 +(* Mirabelle utility functions *)
7.161 +
7.162 +val goal_thm_of = snd o snd o Proof.get_goal
7.163 +
7.164 +fun can_apply tac st =
7.165 + let val (ctxt, (facts, goal)) = Proof.get_goal st
7.166 + in
7.167 + (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
7.168 + SOME (thm, _) => true
7.169 + | NONE => false)
7.170 + end
7.171 +
7.172 +local
7.173 +
7.174 +fun fold_body_thms f =
7.175 + let
7.176 + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
7.177 + fn (x, seen) =>
7.178 + if Inttab.defined seen i then (x, seen)
7.179 + else
7.180 + let
7.181 + val body' = Future.join body
7.182 + val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
7.183 + (x, Inttab.update (i, ()) seen)
7.184 + in (x' |> n = 0 ? f (name, prop, body'), seen') end)
7.185 + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
7.186 +
7.187 +in
7.188 +
7.189 +fun theorems_in_proof_term thm =
7.190 + let
7.191 + val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
7.192 + fun collect (s, _, _) = if s <> "" then insert (op =) s else I
7.193 + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
7.194 + fun resolve_thms names = map_filter (member_of names) all_thms
7.195 + in
7.196 + resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
7.197 + end
7.198 +
7.199 +end
7.200 +
7.201 +fun theorems_of_sucessful_proof state =
7.202 + (case state of
7.203 + NONE => []
7.204 + | SOME st =>
7.205 + if not (Toplevel.is_proof st) then []
7.206 + else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
7.207 +
7.208 +fun get_setting settings (key, default) =
7.209 + the_default default (AList.lookup (op =) settings key)
7.210 +
7.211 +fun get_int_setting settings (key, default) =
7.212 + (case Option.map Int.fromString (AList.lookup (op =) settings key) of
7.213 + SOME (SOME i) => i
7.214 + | SOME NONE => error ("bad option: " ^ key)
7.215 + | NONE => default)
7.216 +
7.217 +
7.218 +
7.219 +(* Mirabelle actions *)
7.220 +
7.221 +(* FIXME
7.222 +fun refute_action settings {pre=st, ...} =
7.223 + let
7.224 + val params = [("minsize", "2") (*"maxsize", "2"*)]
7.225 + val subgoal = 0
7.226 + val thy = Proof.theory_of st
7.227 + val thm = goal_thm_of st
7.228 +
7.229 + val _ = Refute.refute_subgoal thy parms thm subgoal
7.230 + in
7.231 + val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
7.232 + val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
7.233 +
7.234 + val r =
7.235 + if Substring.isSubstring "model found" writ_log
7.236 + then
7.237 + if Substring.isSubstring "spurious" warn_log
7.238 + then SOME "potential counterexample"
7.239 + else SOME "real counterexample (bug?)"
7.240 + else
7.241 + if Substring.isSubstring "time limit" writ_log
7.242 + then SOME "no counterexample (time out)"
7.243 + else if Substring.isSubstring "Search terminated" writ_log
7.244 + then SOME "no counterexample (normal termination)"
7.245 + else SOME "no counterexample (unknown)"
7.246 + in r end
7.247 +*)
7.248 +
7.249 +fun quickcheck_action settings {pre=st, ...} =
7.250 + let
7.251 + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
7.252 + val args = filter has_valid_key settings
7.253 + in
7.254 + (case Quickcheck.quickcheck args 1 st of
7.255 + NONE => SOME "no counterexample"
7.256 + | SOME _ => SOME "counterexample found")
7.257 + end
7.258 +
7.259 +
7.260 +fun arith_action _ {pre=st, ...} =
7.261 + if can_apply Arith_Data.arith_tac st
7.262 + then SOME "succeeded"
7.263 + else NONE
7.264 +
7.265 +
7.266 +fun sledgehammer_action settings {pre=st, ...} =
7.267 + let
7.268 + val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
7.269 + val thy = Proof.theory_of st
7.270 +
7.271 + val prover = the (AtpManager.get_prover prover_name thy)
7.272 + val timeout = AtpManager.get_timeout ()
7.273 +
7.274 + val (success, message) =
7.275 + let
7.276 + val (success, message, _, _, _) =
7.277 + prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
7.278 + in (success, message) end
7.279 + handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
7.280 + | ERROR msg => (false, "error: " ^ msg)
7.281 + in
7.282 + if success
7.283 + then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
7.284 + else NONE
7.285 + end
7.286 +
7.287 +
7.288 +fun metis_action settings {pre, post} =
7.289 + let
7.290 + val thms = theorems_of_sucessful_proof post
7.291 + val names = map Thm.get_name thms
7.292 +
7.293 + val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
7.294 +
7.295 + fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
7.296 + in
7.297 + (if can_apply metis pre then "succeeded" else "failed")
7.298 + |> suffix (" (" ^ commas names ^ ")")
7.299 + |> SOME
7.300 + end
7.301 +
7.302 +
7.303 +
7.304 +(* Mirabelle setup *)
7.305 +
7.306 +val setup =
7.307 + setup_config #>
7.308 +(* FIXME register "refute" refute_action #> *)
7.309 + register "quickcheck" quickcheck_action #>
7.310 + register "arith" arith_action #>
7.311 + register "sledgehammer" sledgehammer_action #>
7.312 + register "metis" metis_action (* #> FIXME:
7.313 + Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
7.314 +
7.315 +end
7.316 +
7.317 +val _ = Toplevel.add_hook Mirabelle.step_hook
7.318 +
7.319 +(* no multithreading, no parallel proofs *)
7.320 +val _ = Multithreading.max_threads := 1
7.321 +val _ = Goal.parallel_proofs := 0
8.1 --- a/src/HOL/ex/mirabelle.ML Wed Aug 12 00:26:01 2009 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,318 +0,0 @@
8.4 -(* Title: mirabelle.ML
8.5 - Author: Jasmin Blanchette and Sascha Boehme
8.6 -*)
8.7 -
8.8 -signature MIRABELLE =
8.9 -sig
8.10 - type action
8.11 - type settings
8.12 - val register : string -> action -> theory -> theory
8.13 - val invoke : string -> settings -> theory -> theory
8.14 -
8.15 - val timeout : int Config.T
8.16 - val verbose : bool Config.T
8.17 - val set_logfile : string -> theory -> theory
8.18 -
8.19 - val setup : theory -> theory
8.20 -
8.21 - val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
8.22 - unit
8.23 -
8.24 - val goal_thm_of : Proof.state -> thm
8.25 - val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
8.26 - val theorems_in_proof_term : Thm.thm -> Thm.thm list
8.27 - val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
8.28 - val get_setting : settings -> string * string -> string
8.29 - val get_int_setting : settings -> string * int -> int
8.30 -
8.31 -(* FIXME val refute_action : action *)
8.32 - val quickcheck_action : action
8.33 - val arith_action : action
8.34 - val sledgehammer_action : action
8.35 - val metis_action : action
8.36 -end
8.37 -
8.38 -
8.39 -
8.40 -structure Mirabelle (*: MIRABELLE*) =
8.41 -struct
8.42 -
8.43 -(* Mirabelle core *)
8.44 -
8.45 -type settings = (string * string) list
8.46 -type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
8.47 -type action = settings -> invoked
8.48 -
8.49 -structure Registered = TheoryDataFun
8.50 -(
8.51 - type T = action Symtab.table
8.52 - val empty = Symtab.empty
8.53 - val copy = I
8.54 - val extend = I
8.55 - fun merge _ = Symtab.merge (K true)
8.56 -)
8.57 -
8.58 -fun register name act = Registered.map (Symtab.update_new (name, act))
8.59 -
8.60 -
8.61 -structure Invoked = TheoryDataFun
8.62 -(
8.63 - type T = (string * invoked) list
8.64 - val empty = []
8.65 - val copy = I
8.66 - val extend = I
8.67 - fun merge _ = Library.merge (K true)
8.68 -)
8.69 -
8.70 -fun invoke name sts thy =
8.71 - let
8.72 - val act =
8.73 - (case Symtab.lookup (Registered.get thy) name of
8.74 - SOME act => act
8.75 - | NONE => error ("The invoked action " ^ quote name ^
8.76 - " is not registered."))
8.77 - in Invoked.map (cons (name, act sts)) thy end
8.78 -
8.79 -val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
8.80 -val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
8.81 -val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
8.82 -val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
8.83 -val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
8.84 -
8.85 -val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
8.86 -
8.87 -fun set_logfile name =
8.88 - let val _ = File.write (Path.explode name) "" (* erase file content *)
8.89 - in Config.put_thy logfile name end
8.90 -
8.91 -local
8.92 -
8.93 -fun log thy s =
8.94 - let fun append_to n = if n = "" then K () else File.append (Path.explode n)
8.95 - in append_to (Config.get_thy thy logfile) (s ^ "\n") end
8.96 - (* FIXME: with multithreading and parallel proofs enabled, we might need to
8.97 - encapsulate this inside a critical section *)
8.98 -
8.99 -fun verbose_msg verbose msg = if verbose then SOME msg else NONE
8.100 -
8.101 -fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
8.102 - handle TimeLimit.TimeOut => verbose_msg verb "time out"
8.103 - | ERROR msg => verbose_msg verb ("error: " ^ msg)
8.104 -
8.105 -fun capture_exns verb f x =
8.106 - (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
8.107 -
8.108 -fun apply_action (c as (verb, _)) st (name, invoked) =
8.109 - Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
8.110 -
8.111 -fun in_range _ _ NONE = true
8.112 - | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
8.113 -
8.114 -fun only_within_range thy pos f x =
8.115 - let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
8.116 - in if in_range l r (Position.line_of pos) then f x else [] end
8.117 -
8.118 -fun pretty_print verbose pos name msgs =
8.119 - let
8.120 - val file = the_default "unknown file" (Position.file_of pos)
8.121 -
8.122 - val str0 = string_of_int o the_default 0
8.123 - val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
8.124 -
8.125 - val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
8.126 - val head = full_loc ^ " (" ^ name ^ "):"
8.127 -
8.128 - fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
8.129 - in
8.130 - Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
8.131 - end
8.132 -
8.133 -in
8.134 -
8.135 -fun basic_hook tr pre post =
8.136 - let
8.137 - val thy = Proof.theory_of pre
8.138 - val pos = Toplevel.pos_of tr
8.139 - val name = Toplevel.name_of tr
8.140 - val verb = Config.get_thy thy verbose
8.141 - val secs = Time.fromSeconds (Config.get_thy thy timeout)
8.142 - val st = {pre=pre, post=post}
8.143 - in
8.144 - Invoked.get thy
8.145 - |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
8.146 - |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
8.147 - end
8.148 -
8.149 -end
8.150 -
8.151 -fun step_hook tr pre post =
8.152 - (* FIXME: might require wrapping into "interruptible" *)
8.153 - if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
8.154 - not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
8.155 - then basic_hook tr (Toplevel.proof_of pre) (SOME post)
8.156 - else () (* FIXME: add theory_hook here *)
8.157 -
8.158 -
8.159 -
8.160 -(* Mirabelle utility functions *)
8.161 -
8.162 -val goal_thm_of = snd o snd o Proof.get_goal
8.163 -
8.164 -fun can_apply tac st =
8.165 - let val (ctxt, (facts, goal)) = Proof.get_goal st
8.166 - in
8.167 - (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
8.168 - SOME (thm, _) => true
8.169 - | NONE => false)
8.170 - end
8.171 -
8.172 -local
8.173 -
8.174 -fun fold_body_thms f =
8.175 - let
8.176 - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
8.177 - fn (x, seen) =>
8.178 - if Inttab.defined seen i then (x, seen)
8.179 - else
8.180 - let
8.181 - val body' = Future.join body
8.182 - val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
8.183 - (x, Inttab.update (i, ()) seen)
8.184 - in (x' |> n = 0 ? f (name, prop, body'), seen') end)
8.185 - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
8.186 -
8.187 -in
8.188 -
8.189 -fun theorems_in_proof_term thm =
8.190 - let
8.191 - val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
8.192 - fun collect (s, _, _) = if s <> "" then insert (op =) s else I
8.193 - fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
8.194 - fun resolve_thms names = map_filter (member_of names) all_thms
8.195 - in
8.196 - resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
8.197 - end
8.198 -
8.199 -end
8.200 -
8.201 -fun theorems_of_sucessful_proof state =
8.202 - (case state of
8.203 - NONE => []
8.204 - | SOME st =>
8.205 - if not (Toplevel.is_proof st) then []
8.206 - else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
8.207 -
8.208 -fun get_setting settings (key, default) =
8.209 - the_default default (AList.lookup (op =) settings key)
8.210 -
8.211 -fun get_int_setting settings (key, default) =
8.212 - (case Option.map Int.fromString (AList.lookup (op =) settings key) of
8.213 - SOME (SOME i) => i
8.214 - | SOME NONE => error ("bad option: " ^ key)
8.215 - | NONE => default)
8.216 -
8.217 -
8.218 -
8.219 -(* Mirabelle actions *)
8.220 -
8.221 -(* FIXME
8.222 -fun refute_action settings {pre=st, ...} =
8.223 - let
8.224 - val params = [("minsize", "2") (*"maxsize", "2"*)]
8.225 - val subgoal = 0
8.226 - val thy = Proof.theory_of st
8.227 - val thm = goal_thm_of st
8.228 -
8.229 - val _ = Refute.refute_subgoal thy parms thm subgoal
8.230 - in
8.231 - val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
8.232 - val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
8.233 -
8.234 - val r =
8.235 - if Substring.isSubstring "model found" writ_log
8.236 - then
8.237 - if Substring.isSubstring "spurious" warn_log
8.238 - then SOME "potential counterexample"
8.239 - else SOME "real counterexample (bug?)"
8.240 - else
8.241 - if Substring.isSubstring "time limit" writ_log
8.242 - then SOME "no counterexample (time out)"
8.243 - else if Substring.isSubstring "Search terminated" writ_log
8.244 - then SOME "no counterexample (normal termination)"
8.245 - else SOME "no counterexample (unknown)"
8.246 - in r end
8.247 -*)
8.248 -
8.249 -fun quickcheck_action settings {pre=st, ...} =
8.250 - let
8.251 - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
8.252 - val args = filter has_valid_key settings
8.253 - in
8.254 - (case Quickcheck.quickcheck args 1 st of
8.255 - NONE => SOME "no counterexample"
8.256 - | SOME _ => SOME "counterexample found")
8.257 - end
8.258 -
8.259 -
8.260 -fun arith_action _ {pre=st, ...} =
8.261 - if can_apply Arith_Data.arith_tac st
8.262 - then SOME "succeeded"
8.263 - else NONE
8.264 -
8.265 -
8.266 -fun sledgehammer_action settings {pre=st, ...} =
8.267 - let
8.268 - val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
8.269 - val thy = Proof.theory_of st
8.270 -
8.271 - val prover = the (AtpManager.get_prover prover_name thy)
8.272 - val timeout = AtpManager.get_timeout ()
8.273 -
8.274 - val (success, message) =
8.275 - let
8.276 - val (success, message, _, _, _) =
8.277 - prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
8.278 - in (success, message) end
8.279 - handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
8.280 - | ERROR msg => (false, "error: " ^ msg)
8.281 - in
8.282 - if success
8.283 - then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
8.284 - else NONE
8.285 - end
8.286 -
8.287 -
8.288 -fun metis_action settings {pre, post} =
8.289 - let
8.290 - val thms = theorems_of_sucessful_proof post
8.291 - val names = map Thm.get_name thms
8.292 -
8.293 - val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
8.294 -
8.295 - fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
8.296 - in
8.297 - (if can_apply metis pre then "succeeded" else "failed")
8.298 - |> suffix (" (" ^ commas names ^ ")")
8.299 - |> SOME
8.300 - end
8.301 -
8.302 -
8.303 -
8.304 -(* Mirabelle setup *)
8.305 -
8.306 -val setup =
8.307 - setup_config #>
8.308 -(* FIXME register "refute" refute_action #> *)
8.309 - register "quickcheck" quickcheck_action #>
8.310 - register "arith" arith_action #>
8.311 - register "sledgehammer" sledgehammer_action #>
8.312 - register "metis" metis_action (* #> FIXME:
8.313 - Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
8.314 -
8.315 -end
8.316 -
8.317 -val _ = Toplevel.add_hook Mirabelle.step_hook
8.318 -
8.319 -(* no multithreading, no parallel proofs *)
8.320 -val _ = Multithreading.max_threads := 1
8.321 -val _ = Goal.parallel_proofs := 0