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 -