author | desharna |
Fri, 11 Jun 2021 09:33:43 +0200 | |
changeset 73849 | 4eac16052a94 |
parent 73848 | 77306bf4e1ee |
child 73850 | 93228ff7aa67 |
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*) |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
11 |
type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time} |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
12 |
type command = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
13 |
{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
|
14 |
type action = {run_action: command -> string, finalize: unit -> string} |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
15 |
val register_action: string -> (action_context -> action) -> unit |
32495 | 16 |
|
32564 | 17 |
(*utility functions*) |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
18 |
val print_exn: exn -> string |
32469 | 19 |
val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
20 |
Proof.state -> bool |
|
60361 | 21 |
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
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
val get_bool_argument : (string * string) list -> string * bool -> bool |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
26 |
val cpu_time : ('a -> 'b) -> 'a -> 'b * int |
32381 | 27 |
end |
28 |
||
32497 | 29 |
structure Mirabelle : MIRABELLE = |
32495 | 30 |
struct |
31 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
32 |
(** Mirabelle core **) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
33 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
34 |
(* concrete syntax *) |
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 |
val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); |
32495 | 37 |
|
73691
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 = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
39 |
Token.read_body keywords |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
40 |
(Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
41 |
(Symbol_Pos.explode0 str); |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
42 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
43 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
44 |
(* actions *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
45 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
46 |
type command = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
47 |
{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
|
48 |
type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time}; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
49 |
type action = {run_action: command -> string, finalize: unit -> string}; |
32381 | 50 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
51 |
local |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
52 |
val actions = Synchronized.var "Mirabelle.actions" |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
53 |
(Symtab.empty : (action_context -> action) Symtab.table); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
54 |
in |
73694 | 55 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
56 |
val register_action = Synchronized.change actions oo curry Symtab.update; |
73694 | 57 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
58 |
fun get_action name = Symtab.lookup (Synchronized.value actions) name; |
73694 | 59 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
60 |
end |
73694 | 61 |
|
62 |
||
63 |
(* apply actions *) |
|
64 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
65 |
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
|
66 |
(case exn of |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
67 |
Timeout.TIMEOUT _ => "timeout" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
68 |
| ERROR msg => "error: " ^ msg |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
69 |
| exn => "exception: " ^ General.exnMessage exn); |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
70 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
71 |
fun run_action_function f = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
72 |
f () handle exn => |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
73 |
if Exn.is_interrupt exn then Exn.reraise exn |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
74 |
else print_exn exn; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
75 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
76 |
fun make_action_path (context as {index, name, ...} : action_context) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
77 |
Path.basic (string_of_int index ^ "." ^ name); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
78 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
79 |
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
|
80 |
let |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
81 |
val s = run_action_function finalize; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
82 |
val action_path = make_action_path context; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
83 |
val export_name = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
84 |
Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
85 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
86 |
if s <> "" then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
87 |
Export.export \<^theory> export_name [XML.Text s] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
88 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
89 |
() |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
90 |
end |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
91 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
92 |
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
|
93 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
94 |
val thy = Proof.theory_of pre; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
95 |
val action_path = make_action_path context; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
96 |
val goal_name_path = Path.basic (#name command) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
97 |
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
|
98 |
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
|
99 |
val export_name = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
100 |
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
|
101 |
line_path + offset_path); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
102 |
val s = run_action_function (fn () => run_action command); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
103 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
104 |
if s <> "" then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
105 |
Export.export thy export_name [XML.Text s] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
106 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
107 |
() |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
108 |
end; |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
109 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
110 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
111 |
(* theory line range *) |
32381 | 112 |
|
113 |
local |
|
114 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
115 |
val theory_name = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
116 |
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
|
117 |
>> Symbol_Pos.content; |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
118 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; |
32381 | 122 |
|
123 |
in |
|
124 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
125 |
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
|
126 |
(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
|
127 |
SOME res => res |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
128 |
| 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
|
129 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
130 |
end; |
32381 | 131 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
132 |
fun check_theories strs = |
32521 | 133 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
134 |
val theories = map read_theory_range strs; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
| 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
|
140 |
| 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
|
141 |
| 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
|
142 |
| 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
|
143 |
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
|
144 |
in check_pos o get_theory end; |
32521 | 145 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
146 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
147 |
(* presentation hook *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
148 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
149 |
val whitelist = ["apply", "by", "proof"]; |
32381 | 150 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
151 |
val _ = |
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
152 |
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
|
153 |
let |
73820
745e2cd1f5f5
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
wenzelm
parents:
73808
diff
changeset
|
154 |
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
|
155 |
val actions = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
156 |
(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
|
157 |
SOME actions => actions |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
158 |
| 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
|
159 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
160 |
if null actions then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
161 |
() |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
162 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
163 |
let |
73849 | 164 |
val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>; |
165 |
val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>; |
|
166 |
val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>; |
|
167 |
val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>; |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
168 |
val check_theory = check_theories (space_explode "," mirabelle_theories); |
32381 | 169 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
170 |
fun make_commands (thy_index, (thy, segments)) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
171 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
172 |
val thy_long_name = Context.theory_long_name thy; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
173 |
val check_thy = check_theory thy_long_name; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
in |
73824 | 179 |
if Context.proper_subthy (\<^theory>, thy) andalso |
180 |
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
|
181 |
member (op =) whitelist name andalso check_thy pos |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
182 |
then SOME {theory_index = thy_index, name = name, pos = pos, |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
183 |
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
|
184 |
else NONE |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
185 |
end; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
186 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
187 |
if Resources.theory_qualifier thy_long_name = qualifier then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
188 |
map_filter make_command segments |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
189 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
190 |
[] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
191 |
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
|
192 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
193 |
(* initialize actions *) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
194 |
val contexts = actions |> map_index (fn (n, (name, args)) => |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
195 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
196 |
val make_action = the (get_action name); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
197 |
val context = {index = n, name = name, arguments = args, timeout = mirabelle_timeout}; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
198 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
199 |
(make_action context, context) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
200 |
end); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
201 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
202 |
(* run actions on all relevant goals *) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
203 |
loaded_theories |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
204 |
|> map_index I |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
205 |
|> maps make_commands |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
206 |
|> map_index I |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
207 |
|> maps (fn (n, command) => |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
208 |
let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
209 |
if k = 0 andalso m <= mirabelle_max_calls then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
210 |
map (fn context => (context, command)) contexts |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
211 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
212 |
[] |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
213 |
end) |
73849 | 214 |
|> 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
|
215 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
216 |
(* finalize actions *) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
217 |
List.app (uncurry finalize_action) contexts |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73822
diff
changeset
|
218 |
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
|
219 |
end); |
32381 | 220 |
|
221 |
||
222 |
(* Mirabelle utility functions *) |
|
223 |
||
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
224 |
fun can_apply time tac st = |
32469 | 225 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
226 |
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
|
227 |
val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); |
32381 | 228 |
in |
62519 | 229 |
(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
|
230 |
SOME (SOME _) => true |
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
231 |
| _ => false) |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
232 |
end; |
32381 | 233 |
|
234 |
local |
|
235 |
||
236 |
fun fold_body_thms f = |
|
237 |
let |
|
64573 | 238 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => |
32381 | 239 |
fn (x, seen) => |
240 |
if Inttab.defined seen i then (x, seen) |
|
241 |
else |
|
242 |
let |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
243 |
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
|
244 |
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
|
245 |
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
|
246 |
val (x', seen') = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
247 |
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
|
248 |
(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
|
249 |
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
|
250 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; |
32381 | 251 |
|
252 |
in |
|
253 |
||
60361 | 254 |
fun theorems_in_proof_term thy thm = |
32381 | 255 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
256 |
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
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; |
32381 | 261 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
262 |
end; |
32381 | 263 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
264 |
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
|
265 |
(case try Toplevel.proof_of st of |
32381 | 266 |
NONE => [] |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
267 |
| SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); |
32381 | 268 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
269 |
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
|
270 |
the_default default (AList.lookup (op =) arguments key); |
32381 | 271 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
272 |
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
|
273 |
(case Option.map Int.fromString (AList.lookup (op =) arguments key) of |
32381 | 274 |
SOME (SOME i) => i |
275 |
| 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
|
276 |
| NONE => default); |
32381 | 277 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
278 |
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
|
279 |
(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
|
280 |
SOME (SOME i) => i |
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
281 |
| 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
|
282 |
| NONE => default); |
73292
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
283 |
|
42014
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
284 |
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
|
285 |
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
|
286 |
in (y, Time.toMilliseconds cpu) end; |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
287 |
|
32381 | 288 |
end |