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