moved Mirabelle from HOL/Tools to HOL,
authorboehmes
Wed Sep 02 16:23:53 2009 +0200 (2009-09-02)
changeset 324964ab00a2642c3
parent 32495 6decc1ffdbed
child 32497 922718ac81e4
moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle
etc/components
src/HOL/IsaMakefile
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/Mirabelle/MirabelleTest.thy
src/HOL/Mirabelle/ROOT.ML
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mirabelle/Tools/mirabelle_arith.ML
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
src/HOL/Mirabelle/Tools/mirabelle_refute.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/doc/options.txt
src/HOL/Mirabelle/etc/settings
src/HOL/Mirabelle/lib/Tools/mirabelle
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
src/HOL/Tools/Mirabelle/Mirabelle.thy
src/HOL/Tools/Mirabelle/Tools/mirabelle.ML
src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML
src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML
src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML
src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Mirabelle/doc/options.txt
src/HOL/Tools/Mirabelle/etc/settings
src/HOL/Tools/Mirabelle/lib/Tools/mirabelle
src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
     1.1 --- a/etc/components	Wed Sep 02 16:02:37 2009 +0200
     1.2 +++ b/etc/components	Wed Sep 02 16:23:53 2009 +0200
     1.3 @@ -13,5 +13,5 @@
     1.4  #misc components
     1.5  src/Tools/Code
     1.6  src/HOL/Tools/ATP_Manager
     1.7 -src/HOL/Tools/Mirabelle
     1.8 +src/HOL/Mirabelle
     1.9  src/HOL/Library/Sum_Of_Squares
     2.1 --- a/src/HOL/IsaMakefile	Wed Sep 02 16:02:37 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Wed Sep 02 16:23:53 2009 +0200
     2.3 @@ -31,6 +31,7 @@
     2.4    HOL-Matrix \
     2.5    HOL-MetisExamples \
     2.6    HOL-MicroJava \
     2.7 +  HOL-Mirabelle \
     2.8    HOL-Modelcheck \
     2.9    HOL-NanoJava \
    2.10    HOL-Nominal-Examples \
    2.11 @@ -1119,6 +1120,20 @@
    2.12  	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
    2.13  
    2.14  
    2.15 +## HOL-Mirabelle
    2.16 +
    2.17 +HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
    2.18 +
    2.19 +$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
    2.20 +  Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
    2.21 +  Mirabelle/Tools/mirabelle_arith.ML \
    2.22 +  Mirabelle/Tools/mirabelle_metis.ML \
    2.23 +  Mirabelle/Tools/mirabelle_quickcheck.ML \
    2.24 +  Mirabelle/Tools/mirabelle_refute.ML \
    2.25 +  Mirabelle/Tools/mirabelle_sledgehammer.ML
    2.26 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    2.27 +
    2.28 +
    2.29  ## clean
    2.30  
    2.31  clean:
    2.32 @@ -1140,4 +1155,5 @@
    2.33  		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
    2.34  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
    2.35  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
    2.36 -		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
    2.37 +		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
    2.38 +                $(LOG)/HOL-Mirabelle.gz
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Wed Sep 02 16:23:53 2009 +0200
     3.3 @@ -0,0 +1,25 @@
     3.4 +(* Title: Mirabelle.thy
     3.5 +   Author: Jasmin Blanchette and Sascha Boehme
     3.6 +*)
     3.7 +
     3.8 +theory Mirabelle
     3.9 +imports Pure
    3.10 +uses "Tools/mirabelle.ML"
    3.11 +begin
    3.12 +
    3.13 +(* no multithreading, no parallel proofs *)
    3.14 +ML {* Multithreading.max_threads := 1 *}
    3.15 +ML {* Goal.parallel_proofs := 0 *}
    3.16 +
    3.17 +ML {* Toplevel.add_hook Mirabelle.step_hook *}
    3.18 +
    3.19 +setup Mirabelle.setup
    3.20 +
    3.21 +ML {*
    3.22 +signature MIRABELLE_ACTION =
    3.23 +sig
    3.24 +  val invoke : (string * string) list -> theory -> theory
    3.25 +end
    3.26 +*}
    3.27 +
    3.28 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Mirabelle/MirabelleTest.thy	Wed Sep 02 16:23:53 2009 +0200
     4.3 @@ -0,0 +1,22 @@
     4.4 +(* Title: MirabelleTest.thy
     4.5 +   Author: Sascha Boehme
     4.6 +*)
     4.7 +
     4.8 +header {* Simple test theory for Mirabelle actions *}
     4.9 +
    4.10 +theory MirabelleTest
    4.11 +imports Main Mirabelle
    4.12 +uses
    4.13 +  "Tools/mirabelle_arith.ML"
    4.14 +  "Tools/mirabelle_metis.ML"
    4.15 +  "Tools/mirabelle_quickcheck.ML"
    4.16 +  "Tools/mirabelle_refute.ML"
    4.17 +  "Tools/mirabelle_sledgehammer.ML"
    4.18 +begin
    4.19 +
    4.20 +(*
    4.21 +  only perform type-checking of the actions,
    4.22 +  any reasonable test would be too complicated
    4.23 +*)
    4.24 +
    4.25 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Mirabelle/ROOT.ML	Wed Sep 02 16:23:53 2009 +0200
     5.3 @@ -0,0 +1,1 @@
     5.4 +use_thy "MirabelleTest";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 16:23:53 2009 +0200
     6.3 @@ -0,0 +1,185 @@
     6.4 +(* Title:  mirabelle.ML
     6.5 +   Author: Jasmin Blanchette and Sascha Boehme
     6.6 +*)
     6.7 +
     6.8 +signature MIRABELLE =
     6.9 +sig
    6.10 +  (* configuration *)
    6.11 +  val logfile : string Config.T
    6.12 +  val timeout : int Config.T
    6.13 +  val start_line : int Config.T
    6.14 +  val end_line : int Config.T
    6.15 +  val setup : theory -> theory
    6.16 +
    6.17 +  (* core *)
    6.18 +  type action
    6.19 +  val register : string * action -> theory -> theory
    6.20 +  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    6.21 +    unit
    6.22 +
    6.23 +  (* utility functions *)
    6.24 +  val goal_thm_of : Proof.state -> thm
    6.25 +  val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
    6.26 +    Proof.state -> bool
    6.27 +  val theorems_in_proof_term : Thm.thm -> Thm.thm list
    6.28 +  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
    6.29 +  val get_setting : (string * string) list -> string * string -> string
    6.30 +  val get_int_setting : (string * string) list -> string * int -> int
    6.31 +end
    6.32 +
    6.33 +
    6.34 +
    6.35 +structure Mirabelle : MIRABELLE_EXT =
    6.36 +struct
    6.37 +
    6.38 +(* Mirabelle configuration *)
    6.39 +
    6.40 +val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
    6.41 +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
    6.42 +val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
    6.43 +val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
    6.44 +
    6.45 +val setup = setup1 #> setup2 #> setup3 #> setup4
    6.46 +
    6.47 +
    6.48 +
    6.49 +(* Mirabelle core *)
    6.50 +
    6.51 +type action = {pre: Proof.state, post: Toplevel.state option,
    6.52 +  timeout: Time.time, log: string -> unit} -> unit
    6.53 +
    6.54 +structure Actions = TheoryDataFun
    6.55 +(
    6.56 +  type T = action Symtab.table
    6.57 +  val empty = Symtab.empty
    6.58 +  val copy = I
    6.59 +  val extend = I
    6.60 +  fun merge _ = Symtab.merge (K true)
    6.61 +)
    6.62 +
    6.63 +val register = Actions.map o Symtab.update_new
    6.64 +
    6.65 +local
    6.66 +
    6.67 +fun log thy s =
    6.68 +  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
    6.69 +  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
    6.70 +  (* FIXME: with multithreading and parallel proofs enabled, we might need to
    6.71 +     encapsulate this inside a critical section *)
    6.72 +
    6.73 +fun log_block thy msg = log thy (msg ^ "\n------------------")
    6.74 +fun log_action thy name msg = log_block thy (name ^ ": " ^ msg)
    6.75 +
    6.76 +fun capture_exns logf f x =
    6.77 +  let
    6.78 +    fun f' x = f x
    6.79 +      handle TimeLimit.TimeOut => logf "time out"
    6.80 +           | ERROR msg => logf ("error: " ^ msg)
    6.81 +  in (case try f' x of NONE => logf "exception" | _ => ()) end
    6.82 +
    6.83 +fun apply_actions thy info (pre, post, time) actions =
    6.84 +  let
    6.85 +    val _ = log_block thy info
    6.86 +    fun apply (name, action) =
    6.87 +      let val st = {pre=pre, post=post, timeout=time, log=log_action thy name}
    6.88 +      in capture_exns (log_action thy name) action st end
    6.89 +  in List.app apply actions end
    6.90 +
    6.91 +fun in_range _ _ NONE = true
    6.92 +  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
    6.93 +
    6.94 +fun only_within_range thy pos f x =
    6.95 +  let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
    6.96 +  in if in_range l r (Position.line_of pos) then f x else () end
    6.97 +
    6.98 +in
    6.99 +
   6.100 +fun basic_hook tr pre post =
   6.101 +  let
   6.102 +    val thy = Proof.theory_of pre
   6.103 +    val pos = Toplevel.pos_of tr
   6.104 +    val name = Toplevel.name_of tr
   6.105 +    val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
   6.106 +
   6.107 +    val str0 = string_of_int o the_default 0
   6.108 +    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
   6.109 +    val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
   6.110 +  in
   6.111 +    Actions.get thy
   6.112 +    |> Symtab.dest
   6.113 +    |> only_within_range thy pos (apply_actions thy info st)
   6.114 +  end
   6.115 +
   6.116 +end
   6.117 +
   6.118 +val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
   6.119 +
   6.120 +fun step_hook tr pre post =
   6.121 + (* FIXME: might require wrapping into "interruptible" *)
   6.122 +  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
   6.123 +     not (member (op =) blacklist (Toplevel.name_of tr))
   6.124 +  then basic_hook tr (Toplevel.proof_of pre) (SOME post)
   6.125 +  else ()   (* FIXME: add theory_hook here *)
   6.126 +
   6.127 +
   6.128 +
   6.129 +(* Mirabelle utility functions *)
   6.130 +
   6.131 +val goal_thm_of = snd o snd o Proof.get_goal
   6.132 +
   6.133 +fun can_apply time tac st =
   6.134 +  let
   6.135 +    val (ctxt, (facts, goal)) = Proof.get_goal st
   6.136 +    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   6.137 +  in
   6.138 +    (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
   6.139 +      SOME (thm, _) => true
   6.140 +    | NONE => false)
   6.141 +  end
   6.142 +
   6.143 +local
   6.144 +
   6.145 +fun fold_body_thms f =
   6.146 +  let
   6.147 +    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
   6.148 +      fn (x, seen) =>
   6.149 +        if Inttab.defined seen i then (x, seen)
   6.150 +        else
   6.151 +          let
   6.152 +            val body' = Future.join body
   6.153 +            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
   6.154 +              (x, Inttab.update (i, ()) seen)
   6.155 +        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
   6.156 +  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
   6.157 +
   6.158 +in
   6.159 +
   6.160 +fun theorems_in_proof_term thm =
   6.161 +  let
   6.162 +    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
   6.163 +    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
   6.164 +    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
   6.165 +    fun resolve_thms names = map_filter (member_of names) all_thms
   6.166 +  in
   6.167 +    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
   6.168 +  end
   6.169 +
   6.170 +end
   6.171 +
   6.172 +fun theorems_of_sucessful_proof state =
   6.173 +  (case state of
   6.174 +    NONE => []
   6.175 +  | SOME st =>
   6.176 +      if not (Toplevel.is_proof st) then []
   6.177 +      else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
   6.178 +
   6.179 +fun get_setting settings (key, default) =
   6.180 +  the_default default (AList.lookup (op =) settings key)
   6.181 +
   6.182 +fun get_int_setting settings (key, default) =
   6.183 +  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
   6.184 +    SOME (SOME i) => i
   6.185 +  | SOME NONE => error ("bad option: " ^ key)
   6.186 +  | NONE => default)
   6.187 +
   6.188 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Wed Sep 02 16:23:53 2009 +0200
     7.3 @@ -0,0 +1,15 @@
     7.4 +(* Title:  mirabelle_arith.ML
     7.5 +   Author: Jasmin Blanchette and Sascha Boehme
     7.6 +*)
     7.7 +
     7.8 +structure Mirabelle_Arith : MIRABELLE_ACTION =
     7.9 +struct
    7.10 +
    7.11 +fun arith_action {pre, timeout, log, ...} =
    7.12 +  if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
    7.13 +  then log "succeeded"
    7.14 +  else ()
    7.15 +
    7.16 +fun invoke _ = Mirabelle.register ("arith", arith_action)
    7.17 +
    7.18 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Wed Sep 02 16:23:53 2009 +0200
     8.3 @@ -0,0 +1,25 @@
     8.4 +(* Title:  mirabelle_metis.ML
     8.5 +   Author: Jasmin Blanchette and Sascha Boehme
     8.6 +*)
     8.7 +
     8.8 +structure Mirabelle_Metis : MIRABELLE_ACTION =
     8.9 +struct
    8.10 +
    8.11 +fun metis_action {pre, post, timeout, log} =
    8.12 +  let
    8.13 +    val thms = Mirabelle.theorems_of_sucessful_proof post
    8.14 +    val names = map Thm.get_name thms
    8.15 +    val add_info = if null names then I else suffix (":\n" ^ commas names)
    8.16 +
    8.17 +    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
    8.18 +
    8.19 +    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
    8.20 +  in
    8.21 +    (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    8.22 +    |> add_info
    8.23 +    |> log
    8.24 +  end
    8.25 +
    8.26 +fun invoke _ = Mirabelle.register ("metis", metis_action)
    8.27 +
    8.28 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Sep 02 16:23:53 2009 +0200
     9.3 @@ -0,0 +1,20 @@
     9.4 +(* Title:  mirabelle_quickcheck.ML
     9.5 +   Author: Jasmin Blanchette and Sascha Boehme
     9.6 +*)
     9.7 +
     9.8 +structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
     9.9 +struct
    9.10 +
    9.11 +fun quickcheck_action limit args {pre=st, ...} =
    9.12 +  let
    9.13 +    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    9.14 +    val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
    9.15 +  in
    9.16 +    (case TimeLimit.timeLimit limit quickcheck st of
    9.17 +      NONE => SOME "no counterexample"
    9.18 +    | SOME _ => SOME "counterexample found")
    9.19 +  end
    9.20 +
    9.21 +fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
    9.22 +
    9.23 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Wed Sep 02 16:23:53 2009 +0200
    10.3 @@ -0,0 +1,39 @@
    10.4 +(* Title:  mirabelle_refute.ML
    10.5 +   Author: Jasmin Blanchette and Sascha Boehme
    10.6 +*)
    10.7 +
    10.8 +structure Mirabelle_Refute : MIRABELLE_ACTION =
    10.9 +struct
   10.10 +
   10.11 +
   10.12 +(* FIXME:
   10.13 +fun refute_action args timeout {pre=st, ...} = 
   10.14 +  let
   10.15 +    val subgoal = 0
   10.16 +    val thy     = Proof.theory_of st
   10.17 +    val thm = goal_thm_of st
   10.18 +
   10.19 +    val refute = Refute.refute_subgoal thy args thm
   10.20 +    val _ = TimeLimit.timeLimit timeout refute subgoal
   10.21 +  in
   10.22 +    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
   10.23 +    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
   10.24 +
   10.25 +    val r =
   10.26 +      if Substring.isSubstring "model found" writ_log
   10.27 +      then
   10.28 +        if Substring.isSubstring "spurious" warn_log
   10.29 +        then SOME "potential counterexample"
   10.30 +        else SOME "real counterexample (bug?)"
   10.31 +      else
   10.32 +        if Substring.isSubstring "time limit" writ_log
   10.33 +        then SOME "no counterexample (time out)"
   10.34 +        else if Substring.isSubstring "Search terminated" writ_log
   10.35 +        then SOME "no counterexample (normal termination)"
   10.36 +        else SOME "no counterexample (unknown)"
   10.37 +  in r end
   10.38 +*)
   10.39 +
   10.40 +fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
   10.41 +
   10.42 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 02 16:23:53 2009 +0200
    11.3 @@ -0,0 +1,84 @@
    11.4 +(* Title:  mirabelle_sledgehammer.ML
    11.5 +   Author: Jasmin Blanchette and Sascha Boehme
    11.6 +*)
    11.7 +
    11.8 +structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
    11.9 +struct
   11.10 +
   11.11 +fun thms_of_name ctxt name =
   11.12 +  let
   11.13 +    val lex = OuterKeyword.get_lexicons
   11.14 +    val get = maps (ProofContext.get_fact ctxt o fst)
   11.15 +  in
   11.16 +    Source.of_string name
   11.17 +    |> Symbol.source {do_recover=false}
   11.18 +    |> OuterLex.source {do_recover=SOME false} lex Position.start
   11.19 +    |> OuterLex.source_proper
   11.20 +    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
   11.21 +    |> Source.exhaust
   11.22 +  end
   11.23 +
   11.24 +fun safe init done f x =
   11.25 +  let
   11.26 +    val y = init x
   11.27 +    val z = Exn.capture f y
   11.28 +    val _ = done y
   11.29 +  in Exn.release z end
   11.30 +
   11.31 +val proverK = "prover"
   11.32 +val keepK = "keep"
   11.33 +val metisK = "metis"
   11.34 +
   11.35 +fun sledgehammer_action args {pre=st, timeout, log, ...} =
   11.36 +  let
   11.37 +    val prover_name =
   11.38 +      AList.lookup (op =) args proverK
   11.39 +      |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
   11.40 +
   11.41 +    val thy = Proof.theory_of st
   11.42 + 
   11.43 +    val prover = the (AtpManager.get_prover prover_name thy)
   11.44 +    val atp_timeout = AtpManager.get_timeout () 
   11.45 +
   11.46 +    (* run sledgehammer *)
   11.47 +    fun init NONE = !AtpWrapper.destdir
   11.48 +      | init (SOME path) =
   11.49 +          let
   11.50 +            (* Warning: we implicitly assume single-threaded execution here! *)
   11.51 +            val old = !AtpWrapper.destdir
   11.52 +            val _ = AtpWrapper.destdir := path
   11.53 +          in old end
   11.54 +    fun done path = AtpWrapper.destdir := path
   11.55 +    fun sh _ =
   11.56 +      let
   11.57 +        val atp = prover atp_timeout NONE NONE prover_name 1
   11.58 +        val (success, (message, thm_names), _, _, _) =
   11.59 +          TimeLimit.timeLimit timeout atp (Proof.get_goal st)
   11.60 +      in (success, message, SOME thm_names) end
   11.61 +      handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
   11.62 +    val (success, message, thm_names) = safe init done sh
   11.63 +      (AList.lookup (op =) args keepK)
   11.64 +    val _ =
   11.65 +      if success then log (quote prover_name ^ " succeeded:\n" ^ message)
   11.66 +      else log (prover_name ^ " failed")
   11.67 +
   11.68 +    (* try metis *)
   11.69 +    fun get_thms ctxt = maps (thms_of_name ctxt)
   11.70 +    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
   11.71 +    fun log_metis s =
   11.72 +      log ("applying metis: " ^ s)
   11.73 +    fun apply_metis thms =
   11.74 +      if Mirabelle.can_apply timeout (metis thms) st
   11.75 +      then "succeeded" else "failed"
   11.76 +    val _ =
   11.77 +      if not (AList.defined (op =) args metisK) then ()
   11.78 +      else
   11.79 +        these thm_names
   11.80 +        |> get_thms (Proof.context_of st)
   11.81 +        |> apply_metis
   11.82 +        |> log_metis
   11.83 +  in () end
   11.84 +
   11.85 +fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
   11.86 +
   11.87 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Mirabelle/doc/options.txt	Wed Sep 02 16:23:53 2009 +0200
    12.3 @@ -0,0 +1,6 @@
    12.4 +Options for sledgehammer:
    12.5 +
    12.6 +  * prover=NAME: name of the external prover to call
    12.7 +  * keep=PATH: path where to keep temporary files created by sledgehammer 
    12.8 +  * metis=X: apply metis with the theorems found by sledgehammer (X may be any
    12.9 +      non-empty string)
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Mirabelle/etc/settings	Wed Sep 02 16:23:53 2009 +0200
    13.3 @@ -0,0 +1,8 @@
    13.4 +MIRABELLE_HOME="$COMPONENT"
    13.5 +
    13.6 +MIRABELLE_LOGIC=HOL
    13.7 +MIRABELLE_THEORY=Main
    13.8 +MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
    13.9 +MIRABELLE_TIMEOUT=30
   13.10 +
   13.11 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed Sep 02 16:23:53 2009 +0200
    14.3 @@ -0,0 +1,88 @@
    14.4 +#!/usr/bin/env bash
    14.5 +#
    14.6 +# Author: Sascha Boehme
    14.7 +#
    14.8 +# DESCRIPTION: testing tool for automated proof tools
    14.9 +
   14.10 +
   14.11 +PRG="$(basename "$0")"
   14.12 +
   14.13 +function print_action_names() {
   14.14 +  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
   14.15 +  for NAME in $TOOLS
   14.16 +  do
   14.17 +    echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
   14.18 +  done
   14.19 +}
   14.20 +
   14.21 +function usage() {
   14.22 +  out="$MIRABELLE_OUTPUT_PATH"
   14.23 +  timeout="$MIRABELLE_TIMEOUT"
   14.24 +  echo
   14.25 +  echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
   14.26 +  echo
   14.27 +  echo "  Options are:"
   14.28 +  echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
   14.29 +  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
   14.30 +  echo "    -O DIR       output directory for test data (default $out)"
   14.31 +  echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
   14.32 +  echo
   14.33 +  echo "  Apply the given actions (i.e., automated proof tools)"
   14.34 +  echo "  at all proof steps in the given theory files."
   14.35 +  echo
   14.36 +  echo "  ACTIONS is a colon-separated list of actions, where each action is"
   14.37 +  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
   14.38 +  print_action_names
   14.39 +  echo
   14.40 +  echo "  FILES is a list of theory files, where each file is either NAME.thy"
   14.41 +  echo "  or NAME.thy[START:END] and START and END are numbers indicating the"
   14.42 +  echo "  range the given actions are to be applied."
   14.43 +  echo
   14.44 +  exit 1
   14.45 +}
   14.46 +
   14.47 +
   14.48 +## process command line
   14.49 +
   14.50 +# options
   14.51 +
   14.52 +while getopts "L:T:O:t:?" OPT
   14.53 +do
   14.54 +  case "$OPT" in
   14.55 +    L)
   14.56 +      MIRABELLE_LOGIC="$OPTARG"
   14.57 +      ;;
   14.58 +    T)
   14.59 +      MIRABELLE_THEORY="$OPTARG"
   14.60 +      ;;
   14.61 +    O)
   14.62 +      MIRABELLE_OUTPUT_PATH="$OPTARG"
   14.63 +      ;;
   14.64 +    t)
   14.65 +      MIRABELLE_TIMEOUT="$OPTARG"
   14.66 +      ;;
   14.67 +    \?)
   14.68 +      usage
   14.69 +      ;;
   14.70 +  esac
   14.71 +done
   14.72 +
   14.73 +shift $(($OPTIND - 1))
   14.74 +
   14.75 +ACTIONS="$1"
   14.76 +
   14.77 +shift
   14.78 +
   14.79 +
   14.80 +# setup
   14.81 +
   14.82 +mkdir -p "$MIRABELLE_OUTPUT_PATH"
   14.83 +
   14.84 +
   14.85 +## main
   14.86 +
   14.87 +for FILE in "$@"
   14.88 +do
   14.89 +  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
   14.90 +done
   14.91 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Sep 02 16:23:53 2009 +0200
    15.3 @@ -0,0 +1,135 @@
    15.4 +#
    15.5 +# Author: Jasmin Blanchette and Sascha Boehme
    15.6 +#
    15.7 +# Testing tool for automated proof tools.
    15.8 +#
    15.9 +
   15.10 +use File::Basename;
   15.11 +
   15.12 +# environment
   15.13 +
   15.14 +my $isabelle_home = $ENV{'ISABELLE_HOME'};
   15.15 +my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
   15.16 +my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
   15.17 +my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
   15.18 +my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
   15.19 +my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
   15.20 +
   15.21 +my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
   15.22 +
   15.23 +
   15.24 +# arguments
   15.25 +
   15.26 +my $actions = $ARGV[0];
   15.27 +
   15.28 +my $thy_file = $ARGV[1];
   15.29 +my $start_line = "0";
   15.30 +my $end_line = "~1";
   15.31 +if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
   15.32 +  $thy_file = $1;
   15.33 +  $start_line = $2;
   15.34 +  $end_line = $3;
   15.35 +}
   15.36 +my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
   15.37 +my $new_thy_name = $thy_name . "_Mirabelle";
   15.38 +my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
   15.39 +
   15.40 +
   15.41 +# setup
   15.42 +
   15.43 +my $setup_thy_name = $thy_name . "_Setup";
   15.44 +my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
   15.45 +my $log_file = $output_path . "/" . $thy_name . ".log";
   15.46 +
   15.47 +my @action_files;
   15.48 +my @action_names;
   15.49 +foreach (split(/:/, $actions)) {
   15.50 +  if (m/([^[]*)/) {
   15.51 +    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
   15.52 +    push @action_names, $1;
   15.53 +  }
   15.54 +}
   15.55 +my $tools = "";
   15.56 +if ($#action_files >= 0) {
   15.57 +  $tools = "uses " . join(" ", @action_files);
   15.58 +}
   15.59 +
   15.60 +open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
   15.61 +
   15.62 +print SETUP_FILE <<END;
   15.63 +theory "$setup_thy_name"
   15.64 +imports "$mirabelle_thy" "$mirabelle_theory"
   15.65 +$tools
   15.66 +begin
   15.67 +
   15.68 +setup {* 
   15.69 +  Config.put_thy Mirabelle.logfile "$log_file" #>
   15.70 +  Config.put_thy Mirabelle.timeout $timeout #>
   15.71 +  Config.put_thy Mirabelle.start_line $start_line #>
   15.72 +  Config.put_thy Mirabelle.end_line $end_line
   15.73 +*}
   15.74 +
   15.75 +END
   15.76 +
   15.77 +foreach (split(/:/, $actions)) {
   15.78 +  if (m/([^[]*)(?:\[(.*)\])?/) {
   15.79 +    my ($name, $settings_str) = ($1, $2 || "");
   15.80 +    $name =~ s/^([a-z])/\U$1/;
   15.81 +    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
   15.82 +    my $sep = "";
   15.83 +    foreach (split(/,/, $settings_str)) {
   15.84 +      if (m/\s*(.*)\s*=\s*(.*)\s*/) {
   15.85 +        print SETUP_FILE "$sep(\"$1\", \"$2\")";
   15.86 +        $sep = ", ";
   15.87 +      }
   15.88 +    }
   15.89 +    print SETUP_FILE "] *}\n";
   15.90 +  }
   15.91 +}
   15.92 +
   15.93 +print SETUP_FILE "\nend";
   15.94 +close SETUP_FILE;
   15.95 +
   15.96 +
   15.97 +# modify target theory file
   15.98 +
   15.99 +open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
  15.100 +my @lines = <OLD_FILE>;
  15.101 +close(OLD_FILE);
  15.102 +
  15.103 +my $thy_text = join("", @lines);
  15.104 +my $old_len = length($thy_text);
  15.105 +$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
  15.106 +$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
  15.107 +die "No 'imports' found" if length($thy_text) == $old_len;
  15.108 +
  15.109 +open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
  15.110 +print NEW_FILE $thy_text;
  15.111 +close(NEW_FILE);
  15.112 +
  15.113 +my $root_file = "$output_path/ROOT_$thy_name.ML";
  15.114 +open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
  15.115 +print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
  15.116 +close(ROOT_FILE);
  15.117 +
  15.118 +
  15.119 +# run isabelle
  15.120 +
  15.121 +open(LOG_FILE, ">$log_file");
  15.122 +print LOG_FILE "Run of $new_thy_file with:\n";
  15.123 +foreach $name (@action_names) {
  15.124 +  print LOG_FILE "  $name\n";
  15.125 +}
  15.126 +close(LOG_FILE);
  15.127 +
  15.128 +my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
  15.129 +  "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
  15.130 +
  15.131 +
  15.132 +# cleanup
  15.133 +
  15.134 +unlink $root_file;
  15.135 +unlink $setup_file;
  15.136 +
  15.137 +exit $r;
  15.138 +
    16.1 --- a/src/HOL/Tools/Mirabelle/Mirabelle.thy	Wed Sep 02 16:02:37 2009 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,25 +0,0 @@
    16.4 -(* Title: Mirabelle.thy
    16.5 -   Author: Jasmin Blanchette and Sascha Boehme
    16.6 -*)
    16.7 -
    16.8 -theory Mirabelle
    16.9 -imports Pure
   16.10 -uses "Tools/mirabelle.ML"
   16.11 -begin
   16.12 -
   16.13 -(* no multithreading, no parallel proofs *)
   16.14 -ML {* Multithreading.max_threads := 1 *}
   16.15 -ML {* Goal.parallel_proofs := 0 *}
   16.16 -
   16.17 -ML {* Toplevel.add_hook Mirabelle.step_hook *}
   16.18 -
   16.19 -setup Mirabelle.setup
   16.20 -
   16.21 -ML {*
   16.22 -signature MIRABELLE_ACTION =
   16.23 -sig
   16.24 -  val invoke : (string * string) list -> theory -> theory
   16.25 -end
   16.26 -*}
   16.27 -
   16.28 -end
    17.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 16:02:37 2009 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,185 +0,0 @@
    17.4 -(* Title:  mirabelle.ML
    17.5 -   Author: Jasmin Blanchette and Sascha Boehme
    17.6 -*)
    17.7 -
    17.8 -signature MIRABELLE =
    17.9 -sig
   17.10 -  (* configuration *)
   17.11 -  val logfile : string Config.T
   17.12 -  val timeout : int Config.T
   17.13 -  val start_line : int Config.T
   17.14 -  val end_line : int Config.T
   17.15 -  val setup : theory -> theory
   17.16 -
   17.17 -  (* core *)
   17.18 -  type action
   17.19 -  val register : string * action -> theory -> theory
   17.20 -  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
   17.21 -    unit
   17.22 -
   17.23 -  (* utility functions *)
   17.24 -  val goal_thm_of : Proof.state -> thm
   17.25 -  val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
   17.26 -    Proof.state -> bool
   17.27 -  val theorems_in_proof_term : Thm.thm -> Thm.thm list
   17.28 -  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
   17.29 -  val get_setting : (string * string) list -> string * string -> string
   17.30 -  val get_int_setting : (string * string) list -> string * int -> int
   17.31 -end
   17.32 -
   17.33 -
   17.34 -
   17.35 -structure Mirabelle : MIRABELLE_EXT =
   17.36 -struct
   17.37 -
   17.38 -(* Mirabelle configuration *)
   17.39 -
   17.40 -val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
   17.41 -val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
   17.42 -val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
   17.43 -val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
   17.44 -
   17.45 -val setup = setup1 #> setup2 #> setup3 #> setup4
   17.46 -
   17.47 -
   17.48 -
   17.49 -(* Mirabelle core *)
   17.50 -
   17.51 -type action = {pre: Proof.state, post: Toplevel.state option,
   17.52 -  timeout: Time.time, log: string -> unit} -> unit
   17.53 -
   17.54 -structure Actions = TheoryDataFun
   17.55 -(
   17.56 -  type T = action Symtab.table
   17.57 -  val empty = Symtab.empty
   17.58 -  val copy = I
   17.59 -  val extend = I
   17.60 -  fun merge _ = Symtab.merge (K true)
   17.61 -)
   17.62 -
   17.63 -val register = Actions.map o Symtab.update_new
   17.64 -
   17.65 -local
   17.66 -
   17.67 -fun log thy s =
   17.68 -  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
   17.69 -  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
   17.70 -  (* FIXME: with multithreading and parallel proofs enabled, we might need to
   17.71 -     encapsulate this inside a critical section *)
   17.72 -
   17.73 -fun log_block thy msg = log thy (msg ^ "\n------------------")
   17.74 -fun log_action thy name msg = log_block thy (name ^ ": " ^ msg)
   17.75 -
   17.76 -fun capture_exns logf f x =
   17.77 -  let
   17.78 -    fun f' x = f x
   17.79 -      handle TimeLimit.TimeOut => logf "time out"
   17.80 -           | ERROR msg => logf ("error: " ^ msg)
   17.81 -  in (case try f' x of NONE => logf "exception" | _ => ()) end
   17.82 -
   17.83 -fun apply_actions thy info (pre, post, time) actions =
   17.84 -  let
   17.85 -    val _ = log_block thy info
   17.86 -    fun apply (name, action) =
   17.87 -      let val st = {pre=pre, post=post, timeout=time, log=log_action thy name}
   17.88 -      in capture_exns (log_action thy name) action st end
   17.89 -  in List.app apply actions end
   17.90 -
   17.91 -fun in_range _ _ NONE = true
   17.92 -  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
   17.93 -
   17.94 -fun only_within_range thy pos f x =
   17.95 -  let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
   17.96 -  in if in_range l r (Position.line_of pos) then f x else () end
   17.97 -
   17.98 -in
   17.99 -
  17.100 -fun basic_hook tr pre post =
  17.101 -  let
  17.102 -    val thy = Proof.theory_of pre
  17.103 -    val pos = Toplevel.pos_of tr
  17.104 -    val name = Toplevel.name_of tr
  17.105 -    val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
  17.106 -
  17.107 -    val str0 = string_of_int o the_default 0
  17.108 -    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
  17.109 -    val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
  17.110 -  in
  17.111 -    Actions.get thy
  17.112 -    |> Symtab.dest
  17.113 -    |> only_within_range thy pos (apply_actions thy info st)
  17.114 -  end
  17.115 -
  17.116 -end
  17.117 -
  17.118 -val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
  17.119 -
  17.120 -fun step_hook tr pre post =
  17.121 - (* FIXME: might require wrapping into "interruptible" *)
  17.122 -  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
  17.123 -     not (member (op =) blacklist (Toplevel.name_of tr))
  17.124 -  then basic_hook tr (Toplevel.proof_of pre) (SOME post)
  17.125 -  else ()   (* FIXME: add theory_hook here *)
  17.126 -
  17.127 -
  17.128 -
  17.129 -(* Mirabelle utility functions *)
  17.130 -
  17.131 -val goal_thm_of = snd o snd o Proof.get_goal
  17.132 -
  17.133 -fun can_apply time tac st =
  17.134 -  let
  17.135 -    val (ctxt, (facts, goal)) = Proof.get_goal st
  17.136 -    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
  17.137 -  in
  17.138 -    (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
  17.139 -      SOME (thm, _) => true
  17.140 -    | NONE => false)
  17.141 -  end
  17.142 -
  17.143 -local
  17.144 -
  17.145 -fun fold_body_thms f =
  17.146 -  let
  17.147 -    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
  17.148 -      fn (x, seen) =>
  17.149 -        if Inttab.defined seen i then (x, seen)
  17.150 -        else
  17.151 -          let
  17.152 -            val body' = Future.join body
  17.153 -            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
  17.154 -              (x, Inttab.update (i, ()) seen)
  17.155 -        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
  17.156 -  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
  17.157 -
  17.158 -in
  17.159 -
  17.160 -fun theorems_in_proof_term thm =
  17.161 -  let
  17.162 -    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
  17.163 -    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
  17.164 -    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
  17.165 -    fun resolve_thms names = map_filter (member_of names) all_thms
  17.166 -  in
  17.167 -    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
  17.168 -  end
  17.169 -
  17.170 -end
  17.171 -
  17.172 -fun theorems_of_sucessful_proof state =
  17.173 -  (case state of
  17.174 -    NONE => []
  17.175 -  | SOME st =>
  17.176 -      if not (Toplevel.is_proof st) then []
  17.177 -      else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
  17.178 -
  17.179 -fun get_setting settings (key, default) =
  17.180 -  the_default default (AList.lookup (op =) settings key)
  17.181 -
  17.182 -fun get_int_setting settings (key, default) =
  17.183 -  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
  17.184 -    SOME (SOME i) => i
  17.185 -  | SOME NONE => error ("bad option: " ^ key)
  17.186 -  | NONE => default)
  17.187 -
  17.188 -end
    18.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Wed Sep 02 16:02:37 2009 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,15 +0,0 @@
    18.4 -(* Title:  mirabelle_arith.ML
    18.5 -   Author: Jasmin Blanchette and Sascha Boehme
    18.6 -*)
    18.7 -
    18.8 -structure Mirabelle_Arith : MIRABELLE_ACTION =
    18.9 -struct
   18.10 -
   18.11 -fun arith_action {pre, timeout, log, ...} =
   18.12 -  if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
   18.13 -  then log "succeeded"
   18.14 -  else ()
   18.15 -
   18.16 -fun invoke _ = Mirabelle.register ("arith", arith_action)
   18.17 -
   18.18 -end
    19.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Wed Sep 02 16:02:37 2009 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,25 +0,0 @@
    19.4 -(* Title:  mirabelle_metis.ML
    19.5 -   Author: Jasmin Blanchette and Sascha Boehme
    19.6 -*)
    19.7 -
    19.8 -structure Mirabelle_Metis : MIRABELLE_ACTION =
    19.9 -struct
   19.10 -
   19.11 -fun metis_action {pre, post, timeout, log} =
   19.12 -  let
   19.13 -    val thms = Mirabelle.theorems_of_sucessful_proof post
   19.14 -    val names = map Thm.get_name thms
   19.15 -    val add_info = if null names then I else suffix (":\n" ^ commas names)
   19.16 -
   19.17 -    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
   19.18 -
   19.19 -    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
   19.20 -  in
   19.21 -    (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
   19.22 -    |> add_info
   19.23 -    |> log
   19.24 -  end
   19.25 -
   19.26 -fun invoke _ = Mirabelle.register ("metis", metis_action)
   19.27 -
   19.28 -end
    20.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Sep 02 16:02:37 2009 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,20 +0,0 @@
    20.4 -(* Title:  mirabelle_quickcheck.ML
    20.5 -   Author: Jasmin Blanchette and Sascha Boehme
    20.6 -*)
    20.7 -
    20.8 -structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
    20.9 -struct
   20.10 -
   20.11 -fun quickcheck_action limit args {pre=st, ...} =
   20.12 -  let
   20.13 -    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
   20.14 -    val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
   20.15 -  in
   20.16 -    (case TimeLimit.timeLimit limit quickcheck st of
   20.17 -      NONE => SOME "no counterexample"
   20.18 -    | SOME _ => SOME "counterexample found")
   20.19 -  end
   20.20 -
   20.21 -fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
   20.22 -
   20.23 -end
    21.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Wed Sep 02 16:02:37 2009 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,39 +0,0 @@
    21.4 -(* Title:  mirabelle_refute.ML
    21.5 -   Author: Jasmin Blanchette and Sascha Boehme
    21.6 -*)
    21.7 -
    21.8 -structure Mirabelle_Refute : MIRABELLE_ACTION =
    21.9 -struct
   21.10 -
   21.11 -
   21.12 -(* FIXME:
   21.13 -fun refute_action args timeout {pre=st, ...} = 
   21.14 -  let
   21.15 -    val subgoal = 0
   21.16 -    val thy     = Proof.theory_of st
   21.17 -    val thm = goal_thm_of st
   21.18 -
   21.19 -    val refute = Refute.refute_subgoal thy args thm
   21.20 -    val _ = TimeLimit.timeLimit timeout refute subgoal
   21.21 -  in
   21.22 -    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
   21.23 -    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
   21.24 -
   21.25 -    val r =
   21.26 -      if Substring.isSubstring "model found" writ_log
   21.27 -      then
   21.28 -        if Substring.isSubstring "spurious" warn_log
   21.29 -        then SOME "potential counterexample"
   21.30 -        else SOME "real counterexample (bug?)"
   21.31 -      else
   21.32 -        if Substring.isSubstring "time limit" writ_log
   21.33 -        then SOME "no counterexample (time out)"
   21.34 -        else if Substring.isSubstring "Search terminated" writ_log
   21.35 -        then SOME "no counterexample (normal termination)"
   21.36 -        else SOME "no counterexample (unknown)"
   21.37 -  in r end
   21.38 -*)
   21.39 -
   21.40 -fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
   21.41 -
   21.42 -end
    22.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 02 16:02:37 2009 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,84 +0,0 @@
    22.4 -(* Title:  mirabelle_sledgehammer.ML
    22.5 -   Author: Jasmin Blanchette and Sascha Boehme
    22.6 -*)
    22.7 -
    22.8 -structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
    22.9 -struct
   22.10 -
   22.11 -fun thms_of_name ctxt name =
   22.12 -  let
   22.13 -    val lex = OuterKeyword.get_lexicons
   22.14 -    val get = maps (ProofContext.get_fact ctxt o fst)
   22.15 -  in
   22.16 -    Source.of_string name
   22.17 -    |> Symbol.source {do_recover=false}
   22.18 -    |> OuterLex.source {do_recover=SOME false} lex Position.start
   22.19 -    |> OuterLex.source_proper
   22.20 -    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
   22.21 -    |> Source.exhaust
   22.22 -  end
   22.23 -
   22.24 -fun safe init done f x =
   22.25 -  let
   22.26 -    val y = init x
   22.27 -    val z = Exn.capture f y
   22.28 -    val _ = done y
   22.29 -  in Exn.release z end
   22.30 -
   22.31 -val proverK = "prover"
   22.32 -val keepK = "keep"
   22.33 -val metisK = "metis"
   22.34 -
   22.35 -fun sledgehammer_action args {pre=st, timeout, log, ...} =
   22.36 -  let
   22.37 -    val prover_name =
   22.38 -      AList.lookup (op =) args proverK
   22.39 -      |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
   22.40 -
   22.41 -    val thy = Proof.theory_of st
   22.42 - 
   22.43 -    val prover = the (AtpManager.get_prover prover_name thy)
   22.44 -    val atp_timeout = AtpManager.get_timeout () 
   22.45 -
   22.46 -    (* run sledgehammer *)
   22.47 -    fun init NONE = !AtpWrapper.destdir
   22.48 -      | init (SOME path) =
   22.49 -          let
   22.50 -            (* Warning: we implicitly assume single-threaded execution here! *)
   22.51 -            val old = !AtpWrapper.destdir
   22.52 -            val _ = AtpWrapper.destdir := path
   22.53 -          in old end
   22.54 -    fun done path = AtpWrapper.destdir := path
   22.55 -    fun sh _ =
   22.56 -      let
   22.57 -        val atp = prover atp_timeout NONE NONE prover_name 1
   22.58 -        val (success, (message, thm_names), _, _, _) =
   22.59 -          TimeLimit.timeLimit timeout atp (Proof.get_goal st)
   22.60 -      in (success, message, SOME thm_names) end
   22.61 -      handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
   22.62 -    val (success, message, thm_names) = safe init done sh
   22.63 -      (AList.lookup (op =) args keepK)
   22.64 -    val _ =
   22.65 -      if success then log (quote prover_name ^ " succeeded:\n" ^ message)
   22.66 -      else log (prover_name ^ " failed")
   22.67 -
   22.68 -    (* try metis *)
   22.69 -    fun get_thms ctxt = maps (thms_of_name ctxt)
   22.70 -    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
   22.71 -    fun log_metis s =
   22.72 -      log ("applying metis: " ^ s)
   22.73 -    fun apply_metis thms =
   22.74 -      if Mirabelle.can_apply timeout (metis thms) st
   22.75 -      then "succeeded" else "failed"
   22.76 -    val _ =
   22.77 -      if not (AList.defined (op =) args metisK) then ()
   22.78 -      else
   22.79 -        these thm_names
   22.80 -        |> get_thms (Proof.context_of st)
   22.81 -        |> apply_metis
   22.82 -        |> log_metis
   22.83 -  in () end
   22.84 -
   22.85 -fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
   22.86 -
   22.87 -end
    23.1 --- a/src/HOL/Tools/Mirabelle/doc/options.txt	Wed Sep 02 16:02:37 2009 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,6 +0,0 @@
    23.4 -Options for sledgehammer:
    23.5 -
    23.6 -  * prover=NAME: name of the external prover to call
    23.7 -  * keep=PATH: path where to keep temporary files created by sledgehammer 
    23.8 -  * metis=X: apply metis with the theorems found by sledgehammer (X may be any
    23.9 -      non-empty string)
    24.1 --- a/src/HOL/Tools/Mirabelle/etc/settings	Wed Sep 02 16:02:37 2009 +0200
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,8 +0,0 @@
    24.4 -MIRABELLE_HOME="$COMPONENT"
    24.5 -
    24.6 -MIRABELLE_LOGIC=HOL
    24.7 -MIRABELLE_THEORY=Main
    24.8 -MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
    24.9 -MIRABELLE_TIMEOUT=30
   24.10 -
   24.11 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    25.1 --- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Wed Sep 02 16:02:37 2009 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,88 +0,0 @@
    25.4 -#!/usr/bin/env bash
    25.5 -#
    25.6 -# Author: Sascha Boehme
    25.7 -#
    25.8 -# DESCRIPTION: testing tool for automated proof tools
    25.9 -
   25.10 -
   25.11 -PRG="$(basename "$0")"
   25.12 -
   25.13 -function print_action_names() {
   25.14 -  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
   25.15 -  for NAME in $TOOLS
   25.16 -  do
   25.17 -    echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
   25.18 -  done
   25.19 -}
   25.20 -
   25.21 -function usage() {
   25.22 -  out="$MIRABELLE_OUTPUT_PATH"
   25.23 -  timeout="$MIRABELLE_TIMEOUT"
   25.24 -  echo
   25.25 -  echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
   25.26 -  echo
   25.27 -  echo "  Options are:"
   25.28 -  echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
   25.29 -  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
   25.30 -  echo "    -O DIR       output directory for test data (default $out)"
   25.31 -  echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
   25.32 -  echo
   25.33 -  echo "  Apply the given actions (i.e., automated proof tools)"
   25.34 -  echo "  at all proof steps in the given theory files."
   25.35 -  echo
   25.36 -  echo "  ACTIONS is a colon-separated list of actions, where each action is"
   25.37 -  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
   25.38 -  print_action_names
   25.39 -  echo
   25.40 -  echo "  FILES is a list of theory files, where each file is either NAME.thy"
   25.41 -  echo "  or NAME.thy[START:END] and START and END are numbers indicating the"
   25.42 -  echo "  range the given actions are to be applied."
   25.43 -  echo
   25.44 -  exit 1
   25.45 -}
   25.46 -
   25.47 -
   25.48 -## process command line
   25.49 -
   25.50 -# options
   25.51 -
   25.52 -while getopts "L:T:O:t:?" OPT
   25.53 -do
   25.54 -  case "$OPT" in
   25.55 -    L)
   25.56 -      MIRABELLE_LOGIC="$OPTARG"
   25.57 -      ;;
   25.58 -    T)
   25.59 -      MIRABELLE_THEORY="$OPTARG"
   25.60 -      ;;
   25.61 -    O)
   25.62 -      MIRABELLE_OUTPUT_PATH="$OPTARG"
   25.63 -      ;;
   25.64 -    t)
   25.65 -      MIRABELLE_TIMEOUT="$OPTARG"
   25.66 -      ;;
   25.67 -    \?)
   25.68 -      usage
   25.69 -      ;;
   25.70 -  esac
   25.71 -done
   25.72 -
   25.73 -shift $(($OPTIND - 1))
   25.74 -
   25.75 -ACTIONS="$1"
   25.76 -
   25.77 -shift
   25.78 -
   25.79 -
   25.80 -# setup
   25.81 -
   25.82 -mkdir -p "$MIRABELLE_OUTPUT_PATH"
   25.83 -
   25.84 -
   25.85 -## main
   25.86 -
   25.87 -for FILE in "$@"
   25.88 -do
   25.89 -  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
   25.90 -done
   25.91 -
    26.1 --- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Wed Sep 02 16:02:37 2009 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,135 +0,0 @@
    26.4 -#
    26.5 -# Author: Jasmin Blanchette and Sascha Boehme
    26.6 -#
    26.7 -# Testing tool for automated proof tools.
    26.8 -#
    26.9 -
   26.10 -use File::Basename;
   26.11 -
   26.12 -# environment
   26.13 -
   26.14 -my $isabelle_home = $ENV{'ISABELLE_HOME'};
   26.15 -my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
   26.16 -my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
   26.17 -my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
   26.18 -my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
   26.19 -my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
   26.20 -
   26.21 -my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
   26.22 -
   26.23 -
   26.24 -# arguments
   26.25 -
   26.26 -my $actions = $ARGV[0];
   26.27 -
   26.28 -my $thy_file = $ARGV[1];
   26.29 -my $start_line = "0";
   26.30 -my $end_line = "~1";
   26.31 -if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
   26.32 -  $thy_file = $1;
   26.33 -  $start_line = $2;
   26.34 -  $end_line = $3;
   26.35 -}
   26.36 -my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
   26.37 -my $new_thy_name = $thy_name . "_Mirabelle";
   26.38 -my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
   26.39 -
   26.40 -
   26.41 -# setup
   26.42 -
   26.43 -my $setup_thy_name = $thy_name . "_Setup";
   26.44 -my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
   26.45 -my $log_file = $output_path . "/" . $thy_name . ".log";
   26.46 -
   26.47 -my @action_files;
   26.48 -my @action_names;
   26.49 -foreach (split(/:/, $actions)) {
   26.50 -  if (m/([^[]*)/) {
   26.51 -    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
   26.52 -    push @action_names, $1;
   26.53 -  }
   26.54 -}
   26.55 -my $tools = "";
   26.56 -if ($#action_files >= 0) {
   26.57 -  $tools = "uses " . join(" ", @action_files);
   26.58 -}
   26.59 -
   26.60 -open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
   26.61 -
   26.62 -print SETUP_FILE <<END;
   26.63 -theory "$setup_thy_name"
   26.64 -imports "$mirabelle_thy" "$mirabelle_theory"
   26.65 -$tools
   26.66 -begin
   26.67 -
   26.68 -setup {* 
   26.69 -  Config.put_thy Mirabelle.logfile "$log_file" #>
   26.70 -  Config.put_thy Mirabelle.timeout $timeout #>
   26.71 -  Config.put_thy Mirabelle.start_line $start_line #>
   26.72 -  Config.put_thy Mirabelle.end_line $end_line
   26.73 -*}
   26.74 -
   26.75 -END
   26.76 -
   26.77 -foreach (split(/:/, $actions)) {
   26.78 -  if (m/([^[]*)(?:\[(.*)\])?/) {
   26.79 -    my ($name, $settings_str) = ($1, $2 || "");
   26.80 -    $name =~ s/^([a-z])/\U$1/;
   26.81 -    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
   26.82 -    my $sep = "";
   26.83 -    foreach (split(/,/, $settings_str)) {
   26.84 -      if (m/\s*(.*)\s*=\s*(.*)\s*/) {
   26.85 -        print SETUP_FILE "$sep(\"$1\", \"$2\")";
   26.86 -        $sep = ", ";
   26.87 -      }
   26.88 -    }
   26.89 -    print SETUP_FILE "] *}\n";
   26.90 -  }
   26.91 -}
   26.92 -
   26.93 -print SETUP_FILE "\nend";
   26.94 -close SETUP_FILE;
   26.95 -
   26.96 -
   26.97 -# modify target theory file
   26.98 -
   26.99 -open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
  26.100 -my @lines = <OLD_FILE>;
  26.101 -close(OLD_FILE);
  26.102 -
  26.103 -my $thy_text = join("", @lines);
  26.104 -my $old_len = length($thy_text);
  26.105 -$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
  26.106 -$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
  26.107 -die "No 'imports' found" if length($thy_text) == $old_len;
  26.108 -
  26.109 -open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
  26.110 -print NEW_FILE $thy_text;
  26.111 -close(NEW_FILE);
  26.112 -
  26.113 -my $root_file = "$output_path/ROOT_$thy_name.ML";
  26.114 -open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
  26.115 -print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
  26.116 -close(ROOT_FILE);
  26.117 -
  26.118 -
  26.119 -# run isabelle
  26.120 -
  26.121 -open(LOG_FILE, ">$log_file");
  26.122 -print LOG_FILE "Run of $new_thy_file with:\n";
  26.123 -foreach $name (@action_names) {
  26.124 -  print LOG_FILE "  $name\n";
  26.125 -}
  26.126 -close(LOG_FILE);
  26.127 -
  26.128 -my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
  26.129 -  "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
  26.130 -
  26.131 -
  26.132 -# cleanup
  26.133 -
  26.134 -unlink $root_file;
  26.135 -unlink $setup_file;
  26.136 -
  26.137 -exit $r;
  26.138 -