18 type text_result = string * (string * locality) list |
18 type text_result = string * (string * locality) list |
19 |
19 |
20 val repair_conjecture_shape_and_axiom_names : |
20 val repair_conjecture_shape_and_axiom_names : |
21 string -> int list list -> (string * locality) list vector |
21 string -> int list list -> (string * locality) list vector |
22 -> int list list * (string * locality) list vector |
22 -> int list list * (string * locality) list vector |
|
23 val apply_on_subgoal : int -> int -> string |
|
24 val command_call : string -> string list -> string |
|
25 val sendback_line : string -> string -> string |
23 val metis_proof_text : metis_params -> text_result |
26 val metis_proof_text : metis_params -> text_result |
24 val isar_proof_text : isar_params -> metis_params -> text_result |
27 val isar_proof_text : isar_params -> metis_params -> text_result |
25 val proof_text : bool -> isar_params -> metis_params -> text_result |
28 val proof_text : bool -> isar_params -> metis_params -> text_result |
26 end; |
29 end; |
27 |
30 |
109 |
112 |
110 (** Soft-core proof reconstruction: Metis one-liner **) |
113 (** Soft-core proof reconstruction: Metis one-liner **) |
111 |
114 |
112 fun string_for_label (s, num) = s ^ string_of_int num |
115 fun string_for_label (s, num) = s ^ string_of_int num |
113 |
116 |
114 fun metis_using [] = "" |
117 fun apply_on_subgoal _ 1 = "by " |
115 | metis_using ls = |
118 | apply_on_subgoal 1 _ = "apply " |
|
119 | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply " |
|
120 fun command_call name [] = name |
|
121 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" |
|
122 fun sendback_line banner command = |
|
123 banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." |
|
124 fun using_labels [] = "" |
|
125 | using_labels ls = |
116 "using " ^ space_implode " " (map string_for_label ls) ^ " " |
126 "using " ^ space_implode " " (map string_for_label ls) ^ " " |
117 fun metis_apply _ 1 = "by " |
|
118 | metis_apply 1 _ = "apply " |
|
119 | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " |
|
120 fun metis_name full_types = if full_types then "metisFT" else "metis" |
127 fun metis_name full_types = if full_types then "metisFT" else "metis" |
121 fun metis_call full_types [] = metis_name full_types |
128 fun metis_call full_types ss = command_call (metis_name full_types) ss |
122 | metis_call full_types ss = |
|
123 "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" |
|
124 fun metis_command full_types i n (ls, ss) = |
129 fun metis_command full_types i n (ls, ss) = |
125 metis_using ls ^ metis_apply i n ^ metis_call full_types ss |
130 using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss |
126 fun metis_line banner full_types i n ss = |
131 fun metis_line banner full_types i n ss = |
127 banner ^ ": " ^ |
132 sendback_line banner (metis_command full_types i n ([], ss)) |
128 Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." |
|
129 fun minimize_line _ [] = "" |
133 fun minimize_line _ [] = "" |
130 | minimize_line minimize_command ss = |
134 | minimize_line minimize_command ss = |
131 case minimize_command ss of |
135 case minimize_command ss of |
132 "" => "" |
136 "" => "" |
133 | command => |
137 | command => |