5 TPTP syntax. |
5 TPTP syntax. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_TPTP_FORMAT = |
8 signature SLEDGEHAMMER_TPTP_FORMAT = |
9 sig |
9 sig |
10 type name_pool = Metis_Clauses.name_pool |
|
11 type type_literal = Metis_Clauses.type_literal |
|
12 type classrel_clause = Metis_Clauses.classrel_clause |
10 type classrel_clause = Metis_Clauses.classrel_clause |
13 type arity_clause = Metis_Clauses.arity_clause |
11 type arity_clause = Metis_Clauses.arity_clause |
14 type hol_clause = Metis_Clauses.hol_clause |
12 type hol_clause = Metis_Clauses.hol_clause |
15 |
13 type name_pool = string Symtab.table * string Symtab.table |
16 val tptp_of_type_literal : |
14 |
17 bool -> type_literal -> name_pool option -> string * name_pool option |
|
18 val write_tptp_file : |
15 val write_tptp_file : |
19 bool -> bool -> bool -> Path.T |
16 bool -> bool -> bool -> Path.T |
20 -> hol_clause list * hol_clause list * hol_clause list * hol_clause list |
17 -> hol_clause list * hol_clause list * hol_clause list * hol_clause list |
21 * classrel_clause list * arity_clause list |
18 * classrel_clause list * arity_clause list |
22 -> name_pool option * int |
19 -> name_pool option * int |
25 structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = |
22 structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = |
26 struct |
23 struct |
27 |
24 |
28 open Metis_Clauses |
25 open Metis_Clauses |
29 open Sledgehammer_Util |
26 open Sledgehammer_Util |
|
27 |
|
28 type name_pool = string Symtab.table * string Symtab.table |
|
29 |
|
30 fun empty_name_pool readable_names = |
|
31 if readable_names then SOME (`I Symtab.empty) else NONE |
|
32 |
|
33 fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs |
|
34 fun pool_map f xs = |
|
35 pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] |
|
36 |
|
37 fun translate_first_char f s = |
|
38 String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE) |
|
39 fun readable_name full_name s = |
|
40 let |
|
41 val s = s |> Long_Name.base_name |> Name.desymbolize false |
|
42 val s' = s |> explode |> rev |> dropwhile (curry (op =) "'") |
|
43 val s' = |
|
44 (s' |> rev |
|
45 |> implode |
|
46 |> String.translate |
|
47 (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c |
|
48 else "")) |
|
49 ^ replicate_string (String.size s - length s') "_" |
|
50 val s' = |
|
51 if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s' |
|
52 else s' |
|
53 (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous |
|
54 ("op &", "op |", etc.). *) |
|
55 val s' = if s' = "equal" orelse s' = "op" then full_name else s' |
|
56 in |
|
57 case (Char.isLower (String.sub (full_name, 0)), |
|
58 Char.isLower (String.sub (s', 0))) of |
|
59 (true, false) => translate_first_char Char.toLower s' |
|
60 | (false, true) => translate_first_char Char.toUpper s' |
|
61 | _ => s' |
|
62 end |
|
63 |
|
64 fun nice_name (full_name, _) NONE = (full_name, NONE) |
|
65 | nice_name (full_name, desired_name) (SOME the_pool) = |
|
66 case Symtab.lookup (fst the_pool) full_name of |
|
67 SOME nice_name => (nice_name, SOME the_pool) |
|
68 | NONE => |
|
69 let |
|
70 val nice_prefix = readable_name full_name desired_name |
|
71 fun add j = |
|
72 let |
|
73 val nice_name = nice_prefix ^ |
|
74 (if j = 0 then "" else "_" ^ Int.toString j) |
|
75 in |
|
76 case Symtab.lookup (snd the_pool) nice_name of |
|
77 SOME full_name' => |
|
78 if full_name = full_name' then (nice_name, the_pool) |
|
79 else add (j + 1) |
|
80 | NONE => |
|
81 (nice_name, |
|
82 (Symtab.update_new (full_name, nice_name) (fst the_pool), |
|
83 Symtab.update_new (nice_name, full_name) (snd the_pool))) |
|
84 end |
|
85 in add 0 |> apsnd SOME end |
30 |
86 |
31 type const_info = {min_arity: int, max_arity: int, sub_level: bool} |
87 type const_info = {min_arity: int, max_arity: int, sub_level: bool} |
32 |
88 |
33 val clause_prefix = "cls_" |
89 val clause_prefix = "cls_" |
34 val arity_clause_prefix = "clsarity_" |
90 val arity_clause_prefix = "clsarity_" |