author | wenzelm |
Sat, 15 May 2021 13:25:52 +0200 | |
changeset 73694 | 60519a7bfc53 |
parent 73691 | 2f9877db82a1 |
child 73697 | 0e7a5c7a14c8 |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle.ML |
32564 | 2 |
Author: Jasmin Blanchette and 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
|
3 |
Author: Makarius |
32381 | 4 |
*) |
5 |
||
6 |
signature MIRABELLE = |
|
7 |
sig |
|
32564 | 8 |
(*core*) |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
9 |
val print_name: string -> string |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
10 |
val print_properties: Properties.T -> string |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
11 |
type context = {tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
12 |
type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} |
73694 | 13 |
val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory |
14 |
val log_command: command -> XML.body -> XML.tree |
|
15 |
val log_report: Properties.T -> XML.body -> XML.tree |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
16 |
val print_exn: exn -> string |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
17 |
val command_action: binding -> (context -> command -> string) -> theory -> theory |
32495 | 18 |
|
32564 | 19 |
(*utility functions*) |
32469 | 20 |
val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
21 |
Proof.state -> bool |
|
60361 | 22 |
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
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
val get_bool_argument : (string * string) list -> string * bool -> bool |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
27 |
val cpu_time : ('a -> 'b) -> 'a -> 'b * int |
32381 | 28 |
end |
29 |
||
32497 | 30 |
structure Mirabelle : MIRABELLE = |
32495 | 31 |
struct |
32 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
33 |
(** Mirabelle core **) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
34 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
35 |
(* concrete syntax *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
36 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
37 |
val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); |
32495 | 38 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
39 |
val print_name = Token.print_name keywords; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
40 |
val print_properties = Token.print_properties keywords; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
41 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
(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
|
45 |
(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
|
46 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
47 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
48 |
(* actions *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
49 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
50 |
type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
51 |
type context = {tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
52 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
53 |
structure Data = Theory_Data |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
54 |
( |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
55 |
type T = (context -> command list -> XML.body) Name_Space.table; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
56 |
val empty = Name_Space.empty_table "mirabelle_action"; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
57 |
val extend = I; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
58 |
val merge = Name_Space.merge_tables; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
59 |
); |
32381 | 60 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
61 |
fun theory_action binding action thy = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
62 |
let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
63 |
in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; |
32381 | 64 |
|
73694 | 65 |
|
66 |
(* log content *) |
|
67 |
||
68 |
fun log_action name arguments = |
|
69 |
XML.Elem (("action", (Markup.nameN, name) :: arguments), |
|
70 |
[XML.Text (print_name name ^ (if null arguments then "" else " " ^ print_properties arguments))]); |
|
71 |
||
72 |
fun log_command ({name, pos, ...}: command) body = |
|
73 |
XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); |
|
74 |
||
75 |
fun log_report props body = |
|
76 |
XML.Elem (("report", props), body); |
|
77 |
||
78 |
||
79 |
(* apply actions *) |
|
80 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
81 |
fun apply_action index name arguments timeout commands thy = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
82 |
let |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
83 |
val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
84 |
val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
85 |
val context = {tag = tag, arguments = arguments, timeout = timeout, theory = thy}; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
86 |
val export_body = action context commands; |
73694 | 87 |
val export_head = log_action name arguments; |
88 |
val export_name = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); |
|
89 |
in |
|
90 |
if null export_body then () |
|
91 |
else Export.export thy export_name (export_head :: export_body) |
|
92 |
end; |
|
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
93 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
94 |
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
|
95 |
(case exn of |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
96 |
Timeout.TIMEOUT _ => "timeout" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
97 |
| ERROR msg => "error: " ^ msg |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
98 |
| exn => "exception:\n" ^ General.exnMessage exn); |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
99 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
100 |
fun command_action binding action = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
101 |
let |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
102 |
fun apply context command = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
103 |
let val s = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
104 |
action context command handle exn => |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
105 |
if Exn.is_interrupt exn then Exn.reraise exn |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
106 |
else #tag context ^ print_exn exn; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
107 |
in |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
108 |
if s = "" then NONE |
73694 | 109 |
else SOME (log_command command [XML.Text s]) end; |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
110 |
in theory_action binding (map_filter o apply) end; |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
111 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
112 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
113 |
(* theory line range *) |
32381 | 114 |
|
115 |
local |
|
116 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
117 |
val theory_name = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
118 |
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
|
119 |
>> Symbol_Pos.content; |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
120 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
121 |
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
|
122 |
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
|
123 |
val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; |
32381 | 124 |
|
125 |
in |
|
126 |
||
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
127 |
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
|
128 |
(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
|
129 |
SOME res => res |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
130 |
| 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
|
131 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
132 |
end; |
32381 | 133 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
134 |
fun check_theories strs = |
32521 | 135 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
| 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
|
142 |
| 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
|
143 |
| 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
|
144 |
| 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
|
145 |
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
|
146 |
in check_pos o get_theory end; |
32521 | 147 |
|
73691
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 |
(* presentation hook *) |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
150 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
151 |
val whitelist = ["apply", "by", "proof"]; |
32381 | 152 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
153 |
val _ = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
154 |
Theory.setup (Thy_Info.add_presentation (fn context => fn thy => |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
155 |
let |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
156 |
val {options, adjust_pos, segments, ...} = context; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
157 |
val mirabelle_timeout = Options.seconds options \<^system_option>\<open>mirabelle_timeout\<close>; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
158 |
val mirabelle_actions = Options.string options \<^system_option>\<open>mirabelle_actions\<close>; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
159 |
val mirabelle_theories = Options.string options \<^system_option>\<open>mirabelle_theories\<close>; |
32468
3e6f5365971e
Mirabelle: explicit command blacklist, preliminary documentation
boehmes
parents:
32396
diff
changeset
|
160 |
|
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)); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
165 |
val check = check_theories (space_explode "," mirabelle_theories); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
166 |
val commands = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
167 |
segments |> map_filter (fn {command = tr, prev_state = st, state = st', ...} => |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
168 |
let |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
169 |
val name = Toplevel.name_of tr; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
170 |
val pos = adjust_pos (Toplevel.pos_of tr); |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
171 |
in |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
172 |
if can (Proof.assert_backward o Toplevel.proof_of) st andalso |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
173 |
member (op =) whitelist name andalso |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
174 |
check (Context.theory_long_name thy) pos |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
175 |
then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
176 |
else NONE |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
177 |
end); |
32381 | 178 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
179 |
fun apply (i, (name, arguments)) () = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
180 |
apply_action (i + 1) name arguments mirabelle_timeout commands thy; |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
181 |
in if null commands then () else fold_index apply actions () end)); |
32381 | 182 |
|
183 |
||
184 |
(* Mirabelle utility functions *) |
|
185 |
||
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
186 |
fun can_apply time tac st = |
32469 | 187 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
188 |
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
|
189 |
val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); |
32381 | 190 |
in |
62519 | 191 |
(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
|
192 |
SOME (SOME _) => true |
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
193 |
| _ => false) |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
194 |
end; |
32381 | 195 |
|
196 |
local |
|
197 |
||
198 |
fun fold_body_thms f = |
|
199 |
let |
|
64573 | 200 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => |
32381 | 201 |
fn (x, seen) => |
202 |
if Inttab.defined seen i then (x, seen) |
|
203 |
else |
|
204 |
let |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
val (x', seen') = |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
209 |
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
|
210 |
(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
|
211 |
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
|
212 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; |
32381 | 213 |
|
214 |
in |
|
215 |
||
60361 | 216 |
fun theorems_in_proof_term thy thm = |
32381 | 217 |
let |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
218 |
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
|
219 |
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
|
220 |
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
|
221 |
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
|
222 |
in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; |
32381 | 223 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
224 |
end; |
32381 | 225 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
226 |
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
|
227 |
(case try Toplevel.proof_of st of |
32381 | 228 |
NONE => [] |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
229 |
| SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); |
32381 | 230 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
231 |
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
|
232 |
the_default default (AList.lookup (op =) arguments key); |
32381 | 233 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
234 |
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
|
235 |
(case Option.map Int.fromString (AList.lookup (op =) arguments key) of |
32381 | 236 |
SOME (SOME i) => i |
237 |
| 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
|
238 |
| NONE => default); |
32381 | 239 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73685
diff
changeset
|
240 |
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
|
241 |
(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
|
242 |
SOME (SOME i) => i |
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
243 |
| 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
|
244 |
| NONE => default); |
73292
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
69597
diff
changeset
|
245 |
|
42014
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
246 |
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
|
247 |
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
|
248 |
in (y, Time.toMilliseconds cpu) end; |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
249 |
|
32381 | 250 |
end |