made Mirabelle a component
authorboehmes
Mon Aug 17 10:59:12 2009 +0200 (2009-08-17)
changeset 3238111542bebe4d4
parent 32365 9b74d0339c44
child 32382 98674ac811c4
made Mirabelle a component
etc/components
lib/scripts/mirabelle
src/HOL/ex/Mirabelle.thy
src/HOL/ex/Mirabelle/Mirabelle.thy
src/HOL/ex/Mirabelle/etc/settings
src/HOL/ex/Mirabelle/lib/mirabelle
src/HOL/ex/Mirabelle/mirabelle.ML
src/HOL/ex/mirabelle.ML
     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