added Mirabelle
authorboehmes
Fri Jul 31 23:31:11 2009 +0200 (2009-07-31)
changeset 322988ffc607c345d
parent 32297 3a4081abb3f7
child 32301 2b64fbc54a82
added Mirabelle
lib/scripts/mirabelle
src/HOL/IsaMakefile
src/HOL/ex/Mirabelle.thy
src/HOL/ex/mirabelle.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/mirabelle	Fri Jul 31 23:31:11 2009 +0200
     1.3 @@ -0,0 +1,129 @@
     1.4 +#!/usr/bin/perl -w
     1.5 +
     1.6 +use strict;
     1.7 +use File::Basename;
     1.8 +
     1.9 +# Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html
    1.10 +sub trim {
    1.11 +    my @out = @_;
    1.12 +    for (@out) {
    1.13 +        s/^\s+//;
    1.14 +        s/\s+$//;
    1.15 +    }
    1.16 +    return wantarray ? @out : $out[0];
    1.17 +}
    1.18 +
    1.19 +sub quote {
    1.20 +    my $str = pop;
    1.21 +    return "\"" . $str . "\"";
    1.22 +}
    1.23 +
    1.24 +sub print_usage_and_quit {
    1.25 +    print STDERR "Usage: mirabelle actions file1.thy...\n" .
    1.26 +                 "  actions: action1:...:actionN\n" .
    1.27 +                 "  action: name or name[key1=value1,...,keyM=valueM]\n";
    1.28 +    exit 1;
    1.29 +}
    1.30 +
    1.31 +my $num_args = $#ARGV + 1;
    1.32 +if ($num_args < 2) {
    1.33 +    print_usage_and_quit();
    1.34 +}
    1.35 +
    1.36 +my @action_names;
    1.37 +my @action_settings;
    1.38 +
    1.39 +foreach (split(/:/, $ARGV[0])) {
    1.40 +    my %settings;
    1.41 +
    1.42 +    $_ =~ /([^[]*)(?:\[(.*)\])?/;
    1.43 +    my ($name, $settings_str) = ($1, $2 || "");
    1.44 +    my @setting_strs = split(/,/, $settings_str);
    1.45 +    foreach (@setting_strs) {
    1.46 +        $_ =~ /(.*)=(.*)/;
    1.47 +	    my $key = $1;
    1.48 +	    my $value = $2;
    1.49 +	    $settings{trim($key)} = trim($value);
    1.50 +    }
    1.51 +
    1.52 +    push @action_names, trim($name);
    1.53 +    push @action_settings, \%settings;
    1.54 +}
    1.55 +
    1.56 +my $output_path = "/tmp/mirabelle"; # FIXME: generate path
    1.57 +my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup";
    1.58 +my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy";
    1.59 +my $mirabelle_log_file = $output_path . "/mirabelle.log";
    1.60 +
    1.61 +mkdir $output_path, 0755;
    1.62 +
    1.63 +open(FILE, ">$mirabellesetup_file")
    1.64 +    || die "Could not create file '$mirabellesetup_file'";
    1.65 +
    1.66 +my $invoke_lines;
    1.67 +
    1.68 +for my $i (0 .. $#action_names) { 
    1.69 +    my $settings_str = "";
    1.70 +    my $settings = $action_settings[$i];
    1.71 +    my $key;
    1.72 +    my $value;
    1.73 +
    1.74 +    while (($key, $value) = each(%$settings)) {
    1.75 +        $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), ";
    1.76 +    }
    1.77 +    $settings_str =~ s/, $//;
    1.78 +
    1.79 +    $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" ";
    1.80 +    $invoke_lines .= "[$settings_str] *}\n"
    1.81 +}
    1.82 +
    1.83 +print FILE <<EOF;
    1.84 +theory MirabelleSetup
    1.85 +imports Mirabelle
    1.86 +begin
    1.87 +
    1.88 +setup {* Mirabelle.set_logfile "$mirabelle_log_file" *}
    1.89 +
    1.90 +$invoke_lines
    1.91 +
    1.92 +end
    1.93 +EOF
    1.94 +
    1.95 +my $root_text = "";
    1.96 +my @new_thy_files;
    1.97 +
    1.98 +for my $i (1 .. $num_args - 1) {
    1.99 +    my $old_thy_file = $ARGV[$i];
   1.100 +    my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy");
   1.101 +    my $new_thy_name = $base . "Mirabelle";
   1.102 +    my $new_thy_file = $dir . $new_thy_name . $ext;
   1.103 +
   1.104 +    open(OLD_FILE, "<$old_thy_file")
   1.105 +        || die "Cannot open file $old_thy_file";
   1.106 +    my @lines = <OLD_FILE>;
   1.107 +    close(OLD_FILE);
   1.108 +
   1.109 +    my $thy_text = join("", @lines);
   1.110 +    my $old_len = length($thy_text);
   1.111 +    $thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$mirabellesetup_thy_name" /gm;
   1.112 +    die "No 'imports' found" if length($thy_text) == $old_len;
   1.113 +
   1.114 +    open(NEW_FILE, ">$new_thy_file");
   1.115 +    print NEW_FILE $thy_text;
   1.116 +    close(NEW_FILE);
   1.117 +
   1.118 +    $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n";
   1.119 +
   1.120 +    push @new_thy_files, $new_thy_file;
   1.121 +}
   1.122 +
   1.123 +my $root_file = "ROOT_mirabelle.ML";
   1.124 +open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file";
   1.125 +print ROOT_FILE $root_text;
   1.126 +close(ROOT_FILE);
   1.127 +
   1.128 +system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL";
   1.129 +
   1.130 +# unlink $mirabellesetup_file;
   1.131 +unlink $root_file;
   1.132 +unlink @new_thy_files;
     2.1 --- a/src/HOL/IsaMakefile	Fri Jul 31 23:30:21 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Jul 31 23:31:11 2009 +0200
     2.3 @@ -903,7 +903,8 @@
     2.4    ex/Sudoku.thy ex/Tarski.thy \
     2.5    ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
     2.6    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
     2.7 -  ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
     2.8 +  ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy \
     2.9 +  ex/Mirabelle.thy ex/mirabelle.ML
    2.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    2.11  
    2.12  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Mirabelle.thy	Fri Jul 31 23:31:11 2009 +0200
     3.3 @@ -0,0 +1,14 @@
     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.ML	Fri Jul 31 23:31:11 2009 +0200
     4.3 @@ -0,0 +1,318 @@
     4.4 +(* Title:  mirabelle.ML
     4.5 +   Author: Jasmin Blanchette and Sascha Boehme
     4.6 +*)
     4.7 +
     4.8 +signature MIRABELLE =
     4.9 +sig
    4.10 +  type action
    4.11 +  type settings
    4.12 +  val register : string -> action -> theory -> theory
    4.13 +  val invoke : string -> settings -> theory -> theory
    4.14 +
    4.15 +  val timeout : int Config.T
    4.16 +  val verbose : bool Config.T
    4.17 +  val set_logfile : string -> theory -> theory
    4.18 +
    4.19 +  val setup : theory -> theory
    4.20 +
    4.21 +  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    4.22 +    unit
    4.23 +
    4.24 +  val goal_thm_of : Proof.state -> thm
    4.25 +  val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
    4.26 +  val theorems_in_proof_term : Thm.thm -> Thm.thm list
    4.27 +  val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
    4.28 +  val get_setting : settings -> string * string -> string
    4.29 +  val get_int_setting : settings -> string * int -> int
    4.30 +
    4.31 +(* FIXME  val refute_action : action *)
    4.32 +  val quickcheck_action : action
    4.33 +  val arith_action : action
    4.34 +  val sledgehammer_action : action
    4.35 +  val metis_action : action
    4.36 +end
    4.37 +
    4.38 +
    4.39 +
    4.40 +structure Mirabelle (*: MIRABELLE*) =
    4.41 +struct
    4.42 +
    4.43 +(* Mirabelle core *)
    4.44 +
    4.45 +type settings = (string * string) list
    4.46 +type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
    4.47 +type action = settings -> invoked
    4.48 +
    4.49 +structure Registered = TheoryDataFun
    4.50 +(
    4.51 +  type T = action Symtab.table
    4.52 +  val empty = Symtab.empty
    4.53 +  val copy = I
    4.54 +  val extend = I
    4.55 +  fun merge _ = Symtab.merge (K true)
    4.56 +)
    4.57 +
    4.58 +fun register name act = Registered.map (Symtab.update_new (name, act))
    4.59 +
    4.60 +
    4.61 +structure Invoked = TheoryDataFun
    4.62 +(
    4.63 +  type T = (string * invoked) list
    4.64 +  val empty = []
    4.65 +  val copy = I
    4.66 +  val extend = I
    4.67 +  fun merge _ = Library.merge (K true)
    4.68 +)
    4.69 +
    4.70 +fun invoke name sts thy = 
    4.71 +  let 
    4.72 +    val act = 
    4.73 +      (case Symtab.lookup (Registered.get thy) name of
    4.74 +        SOME act => act
    4.75 +      | NONE => error ("The invoked action " ^ quote name ^ 
    4.76 +          " is not registered."))
    4.77 +  in Invoked.map (cons (name, act sts)) thy end
    4.78 +
    4.79 +val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
    4.80 +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
    4.81 +val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
    4.82 +val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
    4.83 +val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
    4.84 +
    4.85 +val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
    4.86 +
    4.87 +fun set_logfile name =
    4.88 +  let val _ = File.write (Path.explode name) ""   (* erase file content *)
    4.89 +  in Config.put_thy logfile name end
    4.90 +
    4.91 +local
    4.92 +
    4.93 +fun log thy s =
    4.94 +  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
    4.95 +  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
    4.96 +  (* FIXME: with multithreading and parallel proofs enabled, we might need to
    4.97 +     encapsulate this inside a critical section *)
    4.98 +
    4.99 +fun verbose_msg verbose msg = if verbose then SOME msg else NONE
   4.100 +
   4.101 +fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
   4.102 +  handle TimeLimit.TimeOut => verbose_msg verb "time out"
   4.103 +       | ERROR msg => verbose_msg verb ("error: " ^ msg)
   4.104 +
   4.105 +fun capture_exns verb f x =
   4.106 +  (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
   4.107 +
   4.108 +fun apply_action (c as (verb, _)) st (name, invoked) =
   4.109 +  Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
   4.110 +
   4.111 +fun in_range _ _ NONE = true
   4.112 +  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
   4.113 +
   4.114 +fun only_within_range thy pos f x =
   4.115 +  let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
   4.116 +  in if in_range l r (Position.line_of pos) then f x else [] end
   4.117 +
   4.118 +fun pretty_print verbose pos name msgs =
   4.119 +  let
   4.120 +    val file = the_default "unknown file" (Position.file_of pos)
   4.121 +
   4.122 +    val str0 = string_of_int o the_default 0
   4.123 +    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
   4.124 +
   4.125 +    val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
   4.126 +    val head = full_loc ^ " (" ^ name ^ "):"
   4.127 +
   4.128 +    fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
   4.129 +  in
   4.130 +    Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
   4.131 +  end
   4.132 +
   4.133 +in
   4.134 +
   4.135 +fun basic_hook tr pre post =
   4.136 +  let
   4.137 +    val thy = Proof.theory_of pre
   4.138 +    val pos = Toplevel.pos_of tr
   4.139 +    val name = Toplevel.name_of tr
   4.140 +    val verb = Config.get_thy thy verbose
   4.141 +    val secs = Time.fromSeconds (Config.get_thy thy timeout)
   4.142 +    val st = {pre=pre, post=post}
   4.143 +  in
   4.144 +    Invoked.get thy
   4.145 +    |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
   4.146 +    |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
   4.147 +  end
   4.148 +
   4.149 +end
   4.150 +
   4.151 +fun step_hook tr pre post =
   4.152 + (* FIXME: might require wrapping into "interruptible" *)
   4.153 +  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
   4.154 +     not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
   4.155 +  then basic_hook tr (Toplevel.proof_of pre) (SOME post)
   4.156 +  else ()   (* FIXME: add theory_hook here *)
   4.157 +
   4.158 +
   4.159 +
   4.160 +(* Mirabelle utility functions *)
   4.161 +
   4.162 +val goal_thm_of = snd o snd o Proof.get_goal
   4.163 +
   4.164 +fun can_apply tac st =
   4.165 +  let val (ctxt, (facts, goal)) = Proof.get_goal st
   4.166 +  in
   4.167 +    (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
   4.168 +      SOME (thm, _) => true
   4.169 +    | NONE => false)
   4.170 +  end
   4.171 +
   4.172 +local
   4.173 +
   4.174 +fun fold_body_thms f =
   4.175 +  let
   4.176 +    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
   4.177 +      fn (x, seen) =>
   4.178 +        if Inttab.defined seen i then (x, seen)
   4.179 +        else
   4.180 +          let
   4.181 +            val body' = Future.join body
   4.182 +            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
   4.183 +              (x, Inttab.update (i, ()) seen)
   4.184 +        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
   4.185 +  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
   4.186 +
   4.187 +in
   4.188 +
   4.189 +fun theorems_in_proof_term thm =
   4.190 +  let
   4.191 +    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
   4.192 +    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
   4.193 +    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
   4.194 +    fun resolve_thms names = map_filter (member_of names) all_thms
   4.195 +  in
   4.196 +    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
   4.197 +  end
   4.198 +
   4.199 +end
   4.200 +
   4.201 +fun theorems_of_sucessful_proof state =
   4.202 +  (case state of
   4.203 +    NONE => []
   4.204 +  | SOME st =>
   4.205 +      if not (Toplevel.is_proof st) then []
   4.206 +      else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
   4.207 +
   4.208 +fun get_setting settings (key, default) =
   4.209 +  the_default default (AList.lookup (op =) settings key)
   4.210 +
   4.211 +fun get_int_setting settings (key, default) =
   4.212 +  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
   4.213 +    SOME (SOME i) => i
   4.214 +  | SOME NONE => error ("bad option: " ^ key)
   4.215 +  | NONE => default)
   4.216 +
   4.217 +
   4.218 +
   4.219 +(* Mirabelle actions *)
   4.220 +
   4.221 +(* FIXME
   4.222 +fun refute_action settings {pre=st, ...} = 
   4.223 +  let
   4.224 +    val params   = [("minsize", "2") (*"maxsize", "2"*)]
   4.225 +    val subgoal = 0
   4.226 +    val thy     = Proof.theory_of st
   4.227 +    val thm = goal_thm_of st
   4.228 +
   4.229 +    val _ = Refute.refute_subgoal thy parms thm subgoal
   4.230 +  in
   4.231 +    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
   4.232 +    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
   4.233 +
   4.234 +    val r =
   4.235 +      if Substring.isSubstring "model found" writ_log
   4.236 +      then
   4.237 +        if Substring.isSubstring "spurious" warn_log
   4.238 +        then SOME "potential counterexample"
   4.239 +        else SOME "real counterexample (bug?)"
   4.240 +      else
   4.241 +        if Substring.isSubstring "time limit" writ_log
   4.242 +        then SOME "no counterexample (time out)"
   4.243 +        else if Substring.isSubstring "Search terminated" writ_log
   4.244 +        then SOME "no counterexample (normal termination)"
   4.245 +        else SOME "no counterexample (unknown)"
   4.246 +  in r end
   4.247 +*)
   4.248 +
   4.249 +fun quickcheck_action settings {pre=st, ...} =
   4.250 +  let
   4.251 +    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
   4.252 +    val args = filter has_valid_key settings
   4.253 +  in
   4.254 +    (case Quickcheck.quickcheck args 1 st of
   4.255 +      NONE => SOME "no counterexample"
   4.256 +    | SOME _ => SOME "counterexample found")
   4.257 +  end
   4.258 +
   4.259 +
   4.260 +fun arith_action _ {pre=st, ...} = 
   4.261 +  if can_apply Arith_Data.arith_tac st
   4.262 +  then SOME "succeeded"
   4.263 +  else NONE
   4.264 +
   4.265 +
   4.266 +fun sledgehammer_action settings {pre=st, ...} =
   4.267 +  let
   4.268 +    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
   4.269 +    val thy = Proof.theory_of st
   4.270 + 
   4.271 +    val prover = the (AtpManager.get_prover prover_name thy)
   4.272 +    val timeout = AtpManager.get_timeout () 
   4.273 +
   4.274 +    val (success, message) =
   4.275 +      let
   4.276 +        val (success, message, _, _, _) =
   4.277 +          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
   4.278 +      in (success, message) end
   4.279 +      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
   4.280 +           | ERROR msg => (false, "error: " ^ msg)
   4.281 +  in
   4.282 +    if success
   4.283 +    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
   4.284 +    else NONE
   4.285 +  end
   4.286 +
   4.287 +
   4.288 +fun metis_action settings {pre, post} =
   4.289 +  let
   4.290 +    val thms = theorems_of_sucessful_proof post
   4.291 +    val names = map Thm.get_name thms
   4.292 +
   4.293 +    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
   4.294 +
   4.295 +    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
   4.296 +  in
   4.297 +    (if can_apply metis pre then "succeeded" else "failed")
   4.298 +    |> suffix (" (" ^ commas names ^ ")")
   4.299 +    |> SOME
   4.300 +  end
   4.301 +
   4.302 +
   4.303 +
   4.304 +(* Mirabelle setup *)
   4.305 +
   4.306 +val setup =
   4.307 +  setup_config #>
   4.308 +(* FIXME  register "refute" refute_action #> *)
   4.309 +  register "quickcheck" quickcheck_action #>
   4.310 +  register "arith" arith_action #>
   4.311 +  register "sledgehammer" sledgehammer_action #>
   4.312 +  register "metis" metis_action (* #> FIXME:
   4.313 +  Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
   4.314 +
   4.315 +end
   4.316 +
   4.317 +val _ = Toplevel.add_hook Mirabelle.step_hook
   4.318 +
   4.319 +(* no multithreading, no parallel proofs *)
   4.320 +val _ = Multithreading.max_threads := 1
   4.321 +val _ = Goal.parallel_proofs := 0