9 signature ATP_RECONSTRUCT = |
9 signature ATP_RECONSTRUCT = |
10 sig |
10 sig |
11 type 'a fo_term = 'a ATP_Problem.fo_term |
11 type 'a fo_term = 'a ATP_Problem.fo_term |
12 type 'a proof = 'a ATP_Proof.proof |
12 type 'a proof = 'a ATP_Proof.proof |
13 type locality = ATP_Translate.locality |
13 type locality = ATP_Translate.locality |
14 type type_system = ATP_Translate.type_system |
14 type type_sys = ATP_Translate.type_sys |
15 |
15 |
16 datatype reconstructor = |
16 datatype reconstructor = |
17 Metis | |
17 Metis | |
18 MetisFT | |
18 MetisFT | |
19 SMT of string |
19 SMT of string |
25 |
25 |
26 type minimize_command = string list -> string |
26 type minimize_command = string list -> string |
27 type one_line_params = |
27 type one_line_params = |
28 play * string * (string * locality) list * minimize_command * int * int |
28 play * string * (string * locality) list * minimize_command * int * int |
29 type isar_params = |
29 type isar_params = |
30 bool * bool * int * type_system * string Symtab.table * int list list |
30 bool * bool * int * type_sys * string Symtab.table * int list list * int |
31 * int * (string * locality) list vector * int Symtab.table * string proof |
31 * (string * locality) list vector * int Symtab.table * string proof * thm |
32 * thm |
|
33 val repair_conjecture_shape_and_fact_names : |
32 val repair_conjecture_shape_and_fact_names : |
34 type_system -> string -> int list list -> int |
33 type_sys -> string -> int list list -> int |
35 -> (string * locality) list vector -> int list |
34 -> (string * locality) list vector -> int list |
36 -> int list list * int * (string * locality) list vector * int list |
35 -> int list list * int * (string * locality) list vector * int list |
37 val used_facts_in_atp_proof : |
36 val used_facts_in_atp_proof : |
38 Proof.context -> type_system -> int -> (string * locality) list vector |
37 Proof.context -> type_sys -> int -> (string * locality) list vector |
39 -> string proof -> (string * locality) list |
38 -> string proof -> (string * locality) list |
40 val used_facts_in_unsound_atp_proof : |
39 val used_facts_in_unsound_atp_proof : |
41 Proof.context -> type_system -> int list list -> int |
40 Proof.context -> type_sys -> int list list -> int |
42 -> (string * locality) list vector -> 'a proof -> string list option |
41 -> (string * locality) list vector -> 'a proof -> string list option |
43 val uses_typed_helpers : int list -> 'a proof -> bool |
42 val uses_typed_helpers : int list -> 'a proof -> bool |
44 val reconstructor_name : reconstructor -> string |
43 val reconstructor_name : reconstructor -> string |
45 val one_line_proof_text : one_line_params -> string |
44 val one_line_proof_text : one_line_params -> string |
46 val term_from_atp : |
45 val term_from_atp : |
72 |
71 |
73 type minimize_command = string list -> string |
72 type minimize_command = string list -> string |
74 type one_line_params = |
73 type one_line_params = |
75 play * string * (string * locality) list * minimize_command * int * int |
74 play * string * (string * locality) list * minimize_command * int * int |
76 type isar_params = |
75 type isar_params = |
77 bool * bool * int * type_system * string Symtab.table * int list list * int |
76 bool * bool * int * type_sys * string Symtab.table * int list list * int |
78 * (string * locality) list vector * int Symtab.table * string proof * thm |
77 * (string * locality) list vector * int Symtab.table * string proof * thm |
79 |
78 |
80 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
79 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
81 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
80 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) |
82 |
81 |