author | boehmes |
Tue, 01 Sep 2009 14:09:59 +0200 | |
changeset 32469 | 1ad7d4fc0954 |
parent 32468 | 3e6f5365971e |
child 32472 | 7b92a8b8daaf |
permissions | -rw-r--r-- |
32381 | 1 |
(* Title: mirabelle.ML |
2 |
Author: Jasmin Blanchette and Sascha Boehme |
|
3 |
*) |
|
4 |
||
5 |
signature MIRABELLE = |
|
6 |
sig |
|
7 |
type action |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
8 |
val register : string * action -> theory -> theory |
32381 | 9 |
|
32396 | 10 |
val logfile : string Config.T |
32381 | 11 |
val timeout : int Config.T |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
12 |
val start_line : int Config.T |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
13 |
val end_line : int Config.T |
32381 | 14 |
|
15 |
val goal_thm_of : Proof.state -> thm |
|
32469 | 16 |
val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
17 |
Proof.state -> bool |
|
32381 | 18 |
val theorems_in_proof_term : Thm.thm -> Thm.thm list |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
19 |
val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
20 |
val get_setting : (string * string) list -> string * string -> string |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
21 |
val get_int_setting : (string * string) list -> string * int -> int |
32381 | 22 |
end |
23 |
||
24 |
||
25 |
||
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
26 |
signature MIRABELLE_EXT = |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
27 |
sig |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
28 |
include MIRABELLE |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
29 |
val setup : theory -> theory |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
30 |
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
31 |
unit |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
32 |
end |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
33 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
34 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
35 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
36 |
structure Mirabelle : MIRABELLE_EXT = |
32381 | 37 |
struct |
38 |
||
39 |
(* Mirabelle core *) |
|
40 |
||
32469 | 41 |
type action = Time.time -> {pre: Proof.state, post: Toplevel.state option} -> |
42 |
string option |
|
32381 | 43 |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
44 |
structure Actions = TheoryDataFun |
32381 | 45 |
( |
46 |
type T = action Symtab.table |
|
47 |
val empty = Symtab.empty |
|
48 |
val copy = I |
|
49 |
val extend = I |
|
50 |
fun merge _ = Symtab.merge (K true) |
|
51 |
) |
|
52 |
||
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
53 |
val register = Actions.map o Symtab.update_new |
32381 | 54 |
|
55 |
val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" |
|
56 |
val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 |
|
32469 | 57 |
val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0 |
58 |
val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1 |
|
32381 | 59 |
|
32469 | 60 |
val setup = setup1 #> setup2 #> setup3 #> setup4 |
32381 | 61 |
|
62 |
local |
|
63 |
||
64 |
fun log thy s = |
|
65 |
let fun append_to n = if n = "" then K () else File.append (Path.explode n) |
|
66 |
in append_to (Config.get_thy thy logfile) (s ^ "\n") end |
|
67 |
(* FIXME: with multithreading and parallel proofs enabled, we might need to |
|
68 |
encapsulate this inside a critical section *) |
|
69 |
||
32469 | 70 |
fun capture_exns f x = |
71 |
let |
|
72 |
fun f' x = f x |
|
73 |
handle TimeLimit.TimeOut => SOME "time out" |
|
74 |
| ERROR msg => SOME ("error: " ^ msg) |
|
75 |
in (case try f' x of NONE => SOME "exception" | SOME msg => msg) end |
|
32381 | 76 |
|
32469 | 77 |
fun apply_action timeout st (name, action) = |
78 |
Option.map (pair name) (capture_exns (action timeout) st) |
|
32381 | 79 |
|
80 |
fun in_range _ _ NONE = true |
|
81 |
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) |
|
82 |
||
83 |
fun only_within_range thy pos f x = |
|
84 |
let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line |
|
85 |
in if in_range l r (Position.line_of pos) then f x else [] end |
|
86 |
||
32396 | 87 |
fun pretty_print pos name msgs = |
32381 | 88 |
let |
89 |
val str0 = string_of_int o the_default 0 |
|
90 |
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) |
|
32396 | 91 |
val head = "at " ^ loc ^ " (" ^ name ^ "):" |
32381 | 92 |
|
93 |
fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg]) |
|
94 |
in |
|
95 |
Pretty.string_of (Pretty.big_list head (map pretty_msg msgs)) |
|
96 |
end |
|
97 |
||
98 |
in |
|
99 |
||
100 |
fun basic_hook tr pre post = |
|
101 |
let |
|
102 |
val thy = Proof.theory_of pre |
|
103 |
val pos = Toplevel.pos_of tr |
|
104 |
val name = Toplevel.name_of tr |
|
32469 | 105 |
val timeout = Time.fromSeconds (Config.get_thy thy timeout) |
32381 | 106 |
val st = {pre=pre, post=post} |
107 |
in |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
108 |
Actions.get thy |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
109 |
|> Symtab.dest |
32469 | 110 |
|> only_within_range thy pos (map_filter (apply_action timeout st)) |
32396 | 111 |
|> (fn [] => () | msgs => log thy (pretty_print pos name msgs)) |
32381 | 112 |
end |
113 |
||
114 |
end |
|
115 |
||
32468
3e6f5365971e
Mirabelle: explicit command blacklist, preliminary documentation
boehmes
parents:
32396
diff
changeset
|
116 |
val blacklist = ["disable_pr", "enable_pr", "done", "."] |
3e6f5365971e
Mirabelle: explicit command blacklist, preliminary documentation
boehmes
parents:
32396
diff
changeset
|
117 |
|
32381 | 118 |
fun step_hook tr pre post = |
119 |
(* FIXME: might require wrapping into "interruptible" *) |
|
120 |
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso |
|
32468
3e6f5365971e
Mirabelle: explicit command blacklist, preliminary documentation
boehmes
parents:
32396
diff
changeset
|
121 |
not (member (op =) blacklist (Toplevel.name_of tr)) |
32381 | 122 |
then basic_hook tr (Toplevel.proof_of pre) (SOME post) |
123 |
else () (* FIXME: add theory_hook here *) |
|
124 |
||
125 |
||
126 |
||
127 |
(* Mirabelle utility functions *) |
|
128 |
||
129 |
val goal_thm_of = snd o snd o Proof.get_goal |
|
130 |
||
32469 | 131 |
fun can_apply timeout tac st = |
132 |
let |
|
133 |
val (ctxt, (facts, goal)) = Proof.get_goal st |
|
134 |
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) |
|
32381 | 135 |
in |
32469 | 136 |
(case TimeLimit.timeLimit timeout (Seq.pull o full_tac) goal of |
32381 | 137 |
SOME (thm, _) => true |
138 |
| NONE => false) |
|
139 |
end |
|
140 |
||
141 |
local |
|
142 |
||
143 |
fun fold_body_thms f = |
|
144 |
let |
|
145 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => |
|
146 |
fn (x, seen) => |
|
147 |
if Inttab.defined seen i then (x, seen) |
|
148 |
else |
|
149 |
let |
|
150 |
val body' = Future.join body |
|
151 |
val (x', seen') = app (n + (if name = "" then 0 else 1)) body' |
|
152 |
(x, Inttab.update (i, ()) seen) |
|
153 |
in (x' |> n = 0 ? f (name, prop, body'), seen') end) |
|
154 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end |
|
155 |
||
156 |
in |
|
157 |
||
158 |
fun theorems_in_proof_term thm = |
|
159 |
let |
|
160 |
val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) |
|
161 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
|
162 |
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE |
|
163 |
fun resolve_thms names = map_filter (member_of names) all_thms |
|
164 |
in |
|
165 |
resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) |
|
166 |
end |
|
167 |
||
168 |
end |
|
169 |
||
170 |
fun theorems_of_sucessful_proof state = |
|
171 |
(case state of |
|
172 |
NONE => [] |
|
173 |
| SOME st => |
|
174 |
if not (Toplevel.is_proof st) then [] |
|
175 |
else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) |
|
176 |
||
177 |
fun get_setting settings (key, default) = |
|
178 |
the_default default (AList.lookup (op =) settings key) |
|
179 |
||
180 |
fun get_int_setting settings (key, default) = |
|
181 |
(case Option.map Int.fromString (AList.lookup (op =) settings key) of |
|
182 |
SOME (SOME i) => i |
|
183 |
| SOME NONE => error ("bad option: " ^ key) |
|
184 |
| NONE => default) |
|
185 |
||
186 |
end |