(* Title: HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
Author: Jia Meng, NICTA
Author: Jasmin Blanchette, TU Muenchen
TPTP syntax.
*)
signature SLEDGEHAMMER_TPTP_FORMAT =
sig
type classrel_clause = Metis_Clauses.classrel_clause
type arity_clause = Metis_Clauses.arity_clause
type hol_clause = Metis_Clauses.hol_clause
type name_pool = string Symtab.table * string Symtab.table
val write_tptp_file :
theory -> bool -> bool -> bool -> Path.T
-> hol_clause list * hol_clause list * hol_clause list * hol_clause list
* classrel_clause list * arity_clause list
-> name_pool option * int
end;
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
struct
open Metis_Clauses
open Sledgehammer_Util
(** ATP problem **)
datatype 'a atp_term = ATerm of 'a * 'a atp_term list
type 'a atp_literal = bool * 'a atp_term
datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list
type 'a problem = (string * 'a problem_line list) list
fun string_for_atp_term (ATerm (s, [])) = s
| string_for_atp_term (ATerm (s, ts)) =
s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")"
fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) =
string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^
string_for_atp_term t2
| string_for_atp_literal (pos, t) =
(if pos then "" else "~ ") ^ string_for_atp_term t
fun string_for_problem_line (Cnf (ident, kind, lits)) =
"cnf(" ^ ident ^ ", " ^
(case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^
" (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n"
fun strings_for_problem problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
map string_for_problem_line lines) problem
(** Nice names **)
type name_pool = string Symtab.table * string Symtab.table
fun empty_name_pool readable_names =
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
fun pool_map f xs =
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
unreadable "op_1", "op_2", etc., in the problem files. *)
val reserved_nice_names = ["equal", "op"]
fun readable_name full_name s =
if s = full_name then
s
else
let
val s = s |> Long_Name.base_name
|> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
in if member (op =) reserved_nice_names s then full_name else s end
fun nice_name (full_name, _) NONE = (full_name, NONE)
| nice_name (full_name, desired_name) (SOME the_pool) =
case Symtab.lookup (fst the_pool) full_name of
SOME nice_name => (nice_name, SOME the_pool)
| NONE =>
let
val nice_prefix = readable_name full_name desired_name
fun add j =
let
val nice_name = nice_prefix ^
(if j = 0 then "" else "_" ^ Int.toString j)
in
case Symtab.lookup (snd the_pool) nice_name of
SOME full_name' =>
if full_name = full_name' then (nice_name, the_pool)
else add (j + 1)
| NONE =>
(nice_name,
(Symtab.update_new (full_name, nice_name) (fst the_pool),
Symtab.update_new (nice_name, full_name) (snd the_pool)))
end
in add 0 |> apsnd SOME end
fun nice_atp_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_atp_term ts #>> ATerm
fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
fun nice_problem_line (Cnf (ident, kind, lits)) =
pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
val nice_problem =
pool_map (fn (heading, lines) =>
pool_map nice_problem_line lines #>> pair heading)
(** Sledgehammer stuff **)
val clause_prefix = "cls_"
val arity_clause_prefix = "clsarity_"
fun hol_ident axiom_name clause_id =
clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
fun atp_term_for_combtyp (TyVar name) = ATerm (name, [])
| atp_term_for_combtyp (TyFree name) = ATerm (name, [])
| atp_term_for_combtyp (TyConstr (name, tys)) =
ATerm (name, map atp_term_for_combtyp tys)
fun atp_term_for_combterm full_types top_level u =
let
val (head, args) = strip_combterm_comb u
val (x, ty_args) =
case head of
CombConst (name, _, ty_args) =>
if fst name = "equal" then
(if top_level andalso length args = 2 then name
else ("c_fequal", @{const_name fequal}), [])
else
(name, if full_types then [] else ty_args)
| CombVar (name, _) => (name, [])
| CombApp _ => raise Fail "impossible \"CombApp\""
val t = ATerm (x, map atp_term_for_combtyp ty_args @
map (atp_term_for_combterm full_types false) args)
in
if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t
else t
end
fun atp_literal_for_literal full_types (Literal (pos, t)) =
(pos, atp_term_for_combterm full_types true t)
fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
(pos, ATerm (class, [ATerm (name, [])]))
| atp_literal_for_type_literal pos (TyLitFree (class, name)) =
(pos, ATerm (class, [ATerm (name, [])]))
fun atp_literals_for_axiom full_types
(HOLClause {literals, ctypes_sorts, ...}) =
map (atp_literal_for_literal full_types) literals @
map (atp_literal_for_type_literal false)
(type_literals_for_types ctypes_sorts)
fun problem_line_for_axiom full_types
(clause as HOLClause {axiom_name, clause_id, kind, ...}) =
Cnf (hol_ident axiom_name clause_id, kind,
atp_literals_for_axiom full_types clause)
fun problem_line_for_classrel
(ClassrelClause {axiom_name, subclass, superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
(true, ATerm (superclass, [ty_arg]))])
end
fun atp_literal_for_arity_literal (TConsLit (c, t, args)) =
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
| atp_literal_for_arity_literal (TVarLit (c, sort)) =
(false, ATerm (c, [ATerm (sort, [])]))
fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) =
Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
map atp_literal_for_arity_literal (conclLit :: premLits))
fun problem_line_for_conjecture full_types
(clause as HOLClause {axiom_name, clause_id, kind, literals, ...}) =
Cnf (hol_ident axiom_name clause_id, kind,
map (atp_literal_for_literal full_types) literals)
fun atp_free_type_literals_for_conjecture (HOLClause {ctypes_sorts, ...}) =
map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
fun problem_lines_for_free_types conjectures =
let
val litss = map atp_free_type_literals_for_conjecture conjectures
val lits = fold (union (op =)) litss []
in map problem_line_for_free_type lits end
(** "hBOOL" and "hAPP" **)
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
fun consider_term top_level (ATerm ((s, _), ts)) =
(if is_atp_variable s then
I
else
let val n = length ts in
Symtab.map_default
(s, {min_arity = n, max_arity = 0, sub_level = false})
(fn {min_arity, max_arity, sub_level} =>
{min_arity = Int.min (n, min_arity),
max_arity = Int.max (n, max_arity),
sub_level = sub_level orelse not top_level})
end)
#> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
fun consider_literal (_, t) = consider_term true t
fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
val consider_problem = fold (fold consider_problem_line o snd)
fun const_table_for_problem explicit_apply problem =
if explicit_apply then NONE
else SOME (Symtab.empty |> consider_problem problem)
val tc_fun = make_fixed_type_const @{type_name fun}
fun min_arity_of thy full_types NONE s =
(if s = "equal" orelse s = type_wrapper_name orelse
String.isPrefix type_const_prefix s orelse
String.isPrefix class_prefix s then
16383 (* large number *)
else if full_types then
0
else case strip_prefix const_prefix s of
SOME s' => num_type_args thy (invert_const s')
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =
case Symtab.lookup the_const_tab s of
SOME ({min_arity, ...} : const_info) => min_arity
| NONE => 0
fun full_type_of (ATerm ((s, _), [ty, _])) =
if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
| full_type_of _ = raise Fail "expected type wrapper"
fun list_hAPP_rev _ t1 [] = t1
| list_hAPP_rev NONE t1 (t2 :: ts2) =
ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
| list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
[full_type_of t2, ty]) in
ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
end
fun repair_applications_in_term thy full_types const_tab =
let
fun aux opt_ty (ATerm (name as (s, _), ts)) =
if s = type_wrapper_name then
case ts of
[t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
| _ => raise Fail "malformed type wrapper"
else
let
val ts = map (aux NONE) ts
val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
in aux NONE end
fun boolify t = ATerm (`I "hBOOL", [t])
(* True if the constant ever appears outside of the top-level position in
literals, or if it appears with different arities (e.g., because of different
type instantiations). If false, the constant always receives all of its
arguments and is used as a predicate. *)
fun is_predicate NONE s =
s = "equal" orelse String.isPrefix type_const_prefix s orelse
String.isPrefix class_prefix s
| is_predicate (SOME the_const_tab) s =
case Symtab.lookup the_const_tab s of
SOME {min_arity, max_arity, sub_level} =>
not sub_level andalso min_arity = max_arity
| NONE => false
fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
if s = type_wrapper_name then
case ts of
[_, t' as ATerm ((s', _), _)] =>
if is_predicate const_tab s' then t' else boolify t
| _ => raise Fail "malformed type wrapper"
else
t |> not (is_predicate const_tab s) ? boolify
fun repair_literal thy full_types const_tab (pos, t) =
(pos, t |> repair_applications_in_term thy full_types const_tab
|> repair_predicates_in_term const_tab)
fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
val repair_problem_with_const_table = map o apsnd o map ooo repair_problem_line
fun repair_problem thy full_types explicit_apply problem =
repair_problem_with_const_table thy full_types
(const_table_for_problem explicit_apply problem) problem
fun write_tptp_file thy readable_names full_types explicit_apply file
(conjectures, axiom_clauses, extra_clauses, helper_clauses,
classrel_clauses, arity_clauses) =
let
val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
val classrel_lines = map problem_line_for_classrel classrel_clauses
val arity_lines = map problem_line_for_arity arity_clauses
val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
val conjecture_lines =
map (problem_line_for_conjecture full_types) conjectures
val tfree_lines = problem_lines_for_free_types conjectures
val problem = [("Relevant facts", axiom_lines),
("Class relationships", classrel_lines),
("Arity declarations", arity_lines),
("Helper facts", helper_lines),
("Conjectures", conjecture_lines),
("Type variables", tfree_lines)]
|> repair_problem thy full_types explicit_apply
val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
val conjecture_offset =
length axiom_lines + length classrel_lines + length arity_lines
+ length helper_lines
val _ = File.write_list file (strings_for_problem problem)
in (pool, conjecture_offset) end
end;