author | wenzelm |
Sun, 24 Oct 2021 16:43:54 +0200 | |
changeset 74567 | 40910c47d7a1 |
parent 74564 | 0a66a61e740c |
child 74745 | f54c81fe84f2 |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle.ML |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Munich |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
3 |
Author: Sascha Boehme, TU Munich |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
4 |
Author: Makarius |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
5 |
Author: Martin Desharnais, UniBw Munich |
32381 | 6 |
*) |
7 |
||
8 |
signature MIRABELLE = |
|
9 |
sig |
|
32564 | 10 |
(*core*) |
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
74077
diff
changeset
|
11 |
type action_context = |
74125 | 12 |
{index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time, |
13 |
output_dir: Path.T} |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
14 |
type command = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
15 |
{theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
16 |
type action = {run_action: command -> string, finalize: unit -> string} |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
17 |
val register_action: string -> (action_context -> action) -> unit |
32495 | 18 |
|
32564 | 19 |
(*utility functions*) |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
20 |
val print_exn: exn -> string |
32469 | 21 |
val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
22 |
Proof.state -> bool |
|
60361 | 23 |
val theorems_in_proof_term : theory -> thm -> thm list |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
24 |
val theorems_of_sucessful_proof: Toplevel.state -> thm list |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
25 |
val get_argument : (string * string) list -> string * string -> string |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
26 |
val get_int_argument : (string * string) list -> string * int -> int |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
27 |
val get_bool_argument : (string * string) list -> string * bool -> bool |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
28 |
val cpu_time : ('a -> 'b) -> 'a -> 'b * int |
32381 | 29 |
end |
30 |
||
32497 | 31 |
structure Mirabelle : MIRABELLE = |
32495 | 32 |
struct |
33 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
34 |
(** Mirabelle core **) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
35 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
36 |
(* concrete syntax *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
37 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
38 |
fun read_actions str = |
74125 | 39 |
let |
74558 | 40 |
val thy = \<^theory>; |
41 |
val ctxt = Proof_Context.init_global thy |
|
74567 | 42 |
val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords thy) |
74558 | 43 |
|
74564 | 44 |
fun read_actions () = Parse.read_embedded ctxt keywords |
74125 | 45 |
(Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) |
74558 | 46 |
(Input.string str) |
74125 | 47 |
fun split_name_label (name, args) labels = |
48 |
(case String.tokens (fn c => c = #".") name of |
|
49 |
[name] => (("", name, args), labels) |
|
50 |
| [label, name] => |
|
51 |
(if Symtab.defined labels label then |
|
52 |
error ("Action label '" ^ label ^ "' already defined.") |
|
53 |
else |
|
54 |
(); |
|
55 |
((label, name, args), Symtab.insert_set label labels)) |
|
56 |
| _ => error "Cannot parse action") |
|
57 |
in |
|
74558 | 58 |
try read_actions () |
59 |
|> Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty)) |
|
74125 | 60 |
end |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
61 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
62 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
63 |
(* actions *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
64 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
65 |
type command = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
66 |
{theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; |
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
74077
diff
changeset
|
67 |
type action_context = |
74125 | 68 |
{index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time, |
69 |
output_dir: Path.T}; |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
70 |
type action = {run_action: command -> string, finalize: unit -> string}; |
32381 | 71 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
72 |
local |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
73 |
val actions = Synchronized.var "Mirabelle.actions" |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
74 |
(Symtab.empty : (action_context -> action) Symtab.table); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
75 |
in |
73694 | 76 |
|
73851
bb277f37c34a
added warnings when defining unamed or redefining Mirabelle action
desharna
parents:
73850
diff
changeset
|
77 |
fun register_action name make_action = |
bb277f37c34a
added warnings when defining unamed or redefining Mirabelle action
desharna
parents:
73850
diff
changeset
|
78 |
(if name = "" then error "Registering unnamed Mirabelle action" else (); |
bb277f37c34a
added warnings when defining unamed or redefining Mirabelle action
desharna
parents:
73850
diff
changeset
|
79 |
Synchronized.change actions (Symtab.map_default (name, make_action) |
bb277f37c34a
added warnings when defining unamed or redefining Mirabelle action
desharna
parents:
73850
diff
changeset
|
80 |
(fn f => (warning ("Redefining Mirabelle action: " ^ quote name); f)))); |
73694 | 81 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
82 |
fun get_action name = Symtab.lookup (Synchronized.value actions) name; |
73694 | 83 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
84 |
end |
73694 | 85 |
|
86 |
||
87 |
(* apply actions *) |
|
88 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
89 |
fun print_exn exn = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
90 |
(case exn of |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
91 |
Timeout.TIMEOUT _ => "timeout" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
92 |
| ERROR msg => "error: " ^ msg |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
93 |
| exn => "exception: " ^ General.exnMessage exn); |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
94 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
95 |
fun run_action_function f = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
96 |
f () handle exn => |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
97 |
if Exn.is_interrupt exn then Exn.reraise exn |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
98 |
else print_exn exn; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
99 |
|
74511
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
100 |
fun make_action_string ({index, label, name, ...} : action_context) = |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
101 |
if label = "" then string_of_int index ^ "." ^ name else label; |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
102 |
|
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
103 |
val make_action_path = Path.basic o make_action_string; |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
104 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
105 |
fun finalize_action ({finalize, ...} : action) context = |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
106 |
let |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
107 |
val s = run_action_function finalize; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
108 |
val action_path = make_action_path context; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
109 |
val export_name = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
110 |
Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); |
74511
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
111 |
val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log") |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
112 |
(prefix_lines (make_action_string context ^ " finalize ") (YXML.content_of s) ^ "\n") |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
113 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
114 |
if s <> "" then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
115 |
Export.export \<^theory> export_name [XML.Text s] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
116 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
117 |
() |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
118 |
end |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
119 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
120 |
fun apply_action ({run_action, ...} : action) context (command as {pos, pre, ...} : command) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
121 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
122 |
val thy = Proof.theory_of pre; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
123 |
val action_path = make_action_path context; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
124 |
val goal_name_path = Path.basic (#name command) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
125 |
val line_path = Path.basic (string_of_int (the (Position.line_of pos))); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
126 |
val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
127 |
val export_name = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
128 |
Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
129 |
line_path + offset_path); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
130 |
val s = run_action_function (fn () => run_action command); |
74511
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
131 |
val prefix = make_action_string context ^ " goal." ^ StringCvt.padRight #" " 6 (#name command) ^ |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
132 |
Context.theory_long_name thy ^ " " ^ |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
133 |
string_of_int (the (Position.line_of pos)) ^ ":" ^ |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
134 |
string_of_int (the (Position.offset_of pos)) ^ " " |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
135 |
val _ = Substring.triml |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
136 |
val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log") |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
137 |
(prefix_lines prefix (YXML.content_of s) ^ "\n") |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
138 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
139 |
if s <> "" then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
140 |
Export.export thy export_name [XML.Text s] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
141 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
142 |
() |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
143 |
end; |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
144 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
145 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
146 |
(* theory line range *) |
32381 | 147 |
|
148 |
local |
|
149 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
150 |
val theory_name = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
151 |
Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
152 |
>> Symbol_Pos.content; |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
153 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
154 |
val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
155 |
val end_line = Symbol_Pos.$$ ":" |-- line; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
156 |
val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; |
32381 | 157 |
|
158 |
in |
|
159 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
160 |
fun read_theory_range str = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
161 |
(case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
162 |
SOME res => res |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
163 |
| NONE => error ("Malformed specification of theory line range: " ^ quote str)); |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
164 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
165 |
end; |
32381 | 166 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
167 |
fun check_theories strs = |
32521 | 168 |
let |
74069 | 169 |
fun theory_import_name s = |
170 |
#theory_name (Resources.import_name (Session.get_name ()) Path.current s); |
|
171 |
val theories = map read_theory_range strs |
|
172 |
|> map (apfst theory_import_name); |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
173 |
fun get_theory name = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
174 |
if null theories then SOME NONE |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
175 |
else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
176 |
fun check_line NONE _ = false |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
177 |
| check_line _ NONE = true |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
178 |
| check_line (SOME NONE) _ = true |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
179 |
| check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
180 |
| check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
181 |
fun check_pos range = check_line range o Position.line_of; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
182 |
in check_pos o get_theory end; |
32521 | 183 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
184 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
185 |
(* presentation hook *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
186 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
187 |
val whitelist = ["apply", "by", "proof"]; |
32381 | 188 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
189 |
val _ = |
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
190 |
Build.add_hook (fn qualifier => fn loaded_theories => |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
191 |
let |
73820
745e2cd1f5f5
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
wenzelm
parents:
73808
diff
changeset
|
192 |
val mirabelle_actions = Options.default_string \<^system_option>\<open>mirabelle_actions\<close>; |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
193 |
val actions = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
194 |
(case read_actions mirabelle_actions of |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
195 |
SOME actions => actions |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
196 |
| NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
197 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
198 |
if null actions then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
199 |
() |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
200 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
201 |
let |
73849 | 202 |
val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>; |
203 |
val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>; |
|
204 |
val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>; |
|
205 |
val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>; |
|
74511
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
206 |
val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close> |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
207 |
|> Path.explode |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
208 |
|> Isabelle_System.make_directory; |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
209 |
val check_theory = check_theories (space_explode "," mirabelle_theories); |
32381 | 210 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
211 |
fun make_commands (thy_index, (thy, segments)) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
212 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
213 |
val thy_long_name = Context.theory_long_name thy; |
74069 | 214 |
val check_thy = check_theory thy_long_name; |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
215 |
fun make_command {command = tr, prev_state = st, state = st', ...} = |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
216 |
let |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
217 |
val name = Toplevel.name_of tr; |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
218 |
val pos = Toplevel.pos_of tr; |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
219 |
in |
73824 | 220 |
if Context.proper_subthy (\<^theory>, thy) andalso |
221 |
can (Proof.assert_backward o Toplevel.proof_of) st andalso |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
222 |
member (op =) whitelist name andalso check_thy pos |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
223 |
then SOME {theory_index = thy_index, name = name, pos = pos, |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
224 |
pre = Toplevel.proof_of st, post = st'} |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
225 |
else NONE |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
226 |
end; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
227 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
228 |
if Resources.theory_qualifier thy_long_name = qualifier then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
229 |
map_filter make_command segments |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
230 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
231 |
[] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
232 |
end; |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
233 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
234 |
(* initialize actions *) |
74125 | 235 |
val contexts = actions |> map_index (fn (n, (label, name, args)) => |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
236 |
let |
74514 | 237 |
val make_action = |
238 |
(case get_action name of |
|
239 |
SOME f => f |
|
240 |
| NONE => error "Unknown action"); |
|
74511
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
241 |
val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label; |
6d111935299c
produced Mirabelle output directly in ML until Scala output gets fixed
desharna
parents:
74125
diff
changeset
|
242 |
val output_dir = Path.append mirabelle_output_dir (Path.basic action_subdir); |
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
74077
diff
changeset
|
243 |
val context = |
74125 | 244 |
{index = n, label = label, name = name, arguments = args, |
245 |
timeout = mirabelle_timeout, output_dir = output_dir}; |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
246 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
247 |
(make_action context, context) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
248 |
end); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
249 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
250 |
(* run actions on all relevant goals *) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
251 |
loaded_theories |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
252 |
|> map_index I |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
253 |
|> maps make_commands |
74077
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
254 |
|> (fn xs => fold_map (fn x => fn i => ((i, x), i + 1)) xs 0) |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
255 |
|> (fn (indexed_commands, commands_length) => |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
256 |
let |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
257 |
val stride = |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
258 |
if mirabelle_stride <= 0 then |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
259 |
Integer.max 1 (commands_length div mirabelle_max_calls) |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
260 |
else |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
261 |
mirabelle_stride |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
262 |
in |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
263 |
maps (fn (n, command) => |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
264 |
let val (m, k) = Integer.div_mod (n + 1) stride in |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
265 |
if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
266 |
map (fn context => (context, command)) contexts |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
267 |
else |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
268 |
[] |
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
74069
diff
changeset
|
269 |
end) indexed_commands |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
270 |
end) |
73849 | 271 |
|> Par_List.map (fn ((action, context), command) => apply_action action context command); |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
272 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
273 |
(* finalize actions *) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
274 |
List.app (uncurry finalize_action) contexts |
73850 | 275 |
end |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73820
diff
changeset
|
276 |
end); |
32381 | 277 |
|
278 |
||
279 |
(* Mirabelle utility functions *) |
|
280 |
||
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
281 |
fun can_apply time tac st = |
32469 | 282 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
283 |
val {context = ctxt, facts, goal} = Proof.goal st; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
284 |
val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); |
32381 | 285 |
in |
62519 | 286 |
(case try (Timeout.apply time (Seq.pull o full_tac)) goal of |
39451
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
287 |
SOME (SOME _) => true |
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
288 |
| _ => false) |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
289 |
end; |
32381 | 290 |
|
291 |
local |
|
292 |
||
293 |
fun fold_body_thms f = |
|
294 |
let |
|
64573 | 295 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => |
32381 | 296 |
fn (x, seen) => |
297 |
if Inttab.defined seen i then (x, seen) |
|
298 |
else |
|
299 |
let |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
300 |
val name = Proofterm.thm_node_name thm_node; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
301 |
val prop = Proofterm.thm_node_prop thm_node; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
302 |
val body = Future.join (Proofterm.thm_node_body thm_node); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
303 |
val (x', seen') = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
304 |
app (n + (if name = "" then 0 else 1)) body |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
305 |
(x, Inttab.update (i, ()) seen); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
306 |
in (x' |> n = 0 ? f (name, prop, body), seen') end); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
307 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; |
32381 | 308 |
|
309 |
in |
|
310 |
||
60361 | 311 |
fun theorems_in_proof_term thy thm = |
32381 | 312 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
313 |
val all_thms = Global_Theory.all_thms_of thy true; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
314 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
315 |
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
316 |
fun resolve_thms names = map_filter (member_of names) all_thms; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
317 |
in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; |
32381 | 318 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
319 |
end; |
32381 | 320 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
321 |
fun theorems_of_sucessful_proof st = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
322 |
(case try Toplevel.proof_of st of |
32381 | 323 |
NONE => [] |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
324 |
| SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); |
32381 | 325 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
326 |
fun get_argument arguments (key, default) = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
327 |
the_default default (AList.lookup (op =) arguments key); |
32381 | 328 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
329 |
fun get_int_argument arguments (key, default) = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
330 |
(case Option.map Int.fromString (AList.lookup (op =) arguments key) of |
32381 | 331 |
SOME (SOME i) => i |
332 |
| SOME NONE => error ("bad option: " ^ key) |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
333 |
| NONE => default); |
32381 | 334 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
335 |
fun get_bool_argument arguments (key, default) = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
336 |
(case Option.map Bool.fromString (AList.lookup (op =) arguments key) of |
73292
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
337 |
SOME (SOME i) => i |
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
338 |
| SOME NONE => error ("bad option: " ^ key) |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
339 |
| NONE => default); |
73292
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
340 |
|
42014
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
341 |
fun cpu_time f x = |
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
342 |
let val ({cpu, ...}, y) = Timing.timing f x |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
343 |
in (y, Time.toMilliseconds cpu) end; |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
344 |
|
32381 | 345 |
end |