--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 29 13:23:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jun 30 18:03:34 2010 +0200
@@ -12,8 +12,9 @@
type hol_clause = Metis_Clauses.hol_clause
type name_pool = string Symtab.table * string Symtab.table
+ val type_wrapper_name : string
val write_tptp_file :
- bool -> bool -> bool -> Path.T
+ 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
@@ -25,41 +26,57 @@
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 (`I Symtab.empty) else NONE
+ 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 []
-fun translate_first_char f s =
- String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+(* "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 =
- let
- val s = s |> Long_Name.base_name |> Name.desymbolize false
- val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
- val s' =
- (s' |> rev
- |> implode
- |> String.translate
- (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
- else ""))
- ^ replicate_string (String.size s - length s') "_"
- val s' =
- if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
- else s'
- (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
- ("op &", "op |", etc.). *)
- val s' = if s' = "equal" orelse s' = "op" then full_name else s'
- in
- case (Char.isLower (String.sub (full_name, 0)),
- Char.isLower (String.sub (s', 0))) of
- (true, false) => translate_first_char Char.toLower s'
- | (false, true) => translate_first_char Char.toUpper s'
- | _ => s'
- end
+ 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) =
@@ -84,237 +101,230 @@
end
in add 0 |> apsnd SOME end
-type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+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 paren_pack [] = ""
- | paren_pack strings = "(" ^ commas strings ^ ")"
+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 string_of_fol_type (TyVar sp) pool = nice_name sp pool
- | string_of_fol_type (TyFree sp) pool = nice_name sp pool
- | string_of_fol_type (TyConstr (sp, tys)) pool =
- let
- val (s, pool) = nice_name sp pool
- val (ss, pool) = pool_map string_of_fol_type tys pool
- in (s ^ paren_pack ss, pool) end
+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 needs_hBOOL NONE _ = true
- | needs_hBOOL (SOME the_const_tab) c =
- case Symtab.lookup the_const_tab c of
- SOME ({min_arity, max_arity, sub_level} : const_info) =>
- sub_level orelse min_arity < max_arity
+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 head_needs_hBOOL const_tab (CombConst ((c, _), _, _)) =
- needs_hBOOL const_tab c
- | head_needs_hBOOL _ _ = true
-
-fun wrap_type full_types (s, ty) pool =
- if full_types then
- let val (s', pool) = string_of_fol_type ty pool in
- (type_wrapper_name ^ paren_pack [s, s'], pool)
- end
+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
- (s, pool)
-
-fun wrap_type_if (full_types, const_tab) (head, s, tp) =
- if head_needs_hBOOL const_tab head then wrap_type full_types (s, tp)
- else pair s
-
-fun apply ss = "hAPP" ^ paren_pack ss;
-
-fun rev_apply (v, []) = v
- | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
-
-fun string_apply (v, args) = rev_apply (v, rev args)
-
-fun min_arity_of NONE _ = 0
- | min_arity_of (SOME the_const_tab) c =
- case Symtab.lookup the_const_tab c of
- SOME ({min_arity, ...} : const_info) => min_arity
- | NONE => 0
-
-(* Apply an operator to the argument strings, using either the "apply" operator
- or direct function application. *)
-fun string_of_application (full_types, const_tab)
- (CombConst ((s, s'), _, tvars), args) pool =
- let
- val s = if s = "equal" then "c_fequal" else s
- val nargs = min_arity_of const_tab s
- val args1 = List.take (args, nargs)
- handle Subscript =>
- raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
- " but is applied to " ^ commas (map quote args))
- val args2 = List.drop (args, nargs)
- val (targs, pool) = if full_types then ([], pool)
- else pool_map string_of_fol_type tvars pool
- val (s, pool) = nice_name (s, s') pool
- in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
- | string_of_application _ (CombVar (name, _), args) pool =
- nice_name name pool |>> (fn s => string_apply (s, args))
+ t |> not (is_predicate const_tab s) ? boolify
-fun string_of_combterm params t pool =
- let
- val (head, args) = strip_combterm_comb t
- val (ss, pool) = pool_map (string_of_combterm params) args pool
- val (s, pool) = string_of_application params (head, ss) pool
- in wrap_type_if params (head, s, type_of_combterm t) pool end
-
-(*Boolean-valued terms are here converted to literals.*)
-fun boolify params c =
- string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
-
-fun string_for_predicate (params as (_, const_tab)) t =
- case #1 (strip_combterm_comb t) of
- CombConst ((s, _), _, _) =>
- (if needs_hBOOL const_tab s then boolify else string_of_combterm) params t
- | _ => boolify params t
-
-fun string_for_equality params pos (t1, t2) =
- pool_map (string_of_combterm params) [t1, t2]
- #>> space_implode (if pos then " = " else " != ")
-
-fun string_for_sign true s = s
- | string_for_sign false s = "~ " ^ s
+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 string_for_literal params
- (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
- t2))) =
- string_for_equality params pos (t1, t2)
- | string_for_literal params (Literal (pos, pred)) =
- string_for_predicate params pred #>> string_for_sign pos
-
-fun string_for_type_literal pos (TyLitVar (s, name)) =
- nice_name name #>> (fn s' => string_for_sign pos (s ^ "(" ^ s' ^ ")"))
- | string_for_type_literal pos (TyLitFree (s, name)) =
- nice_name name #>> (fn s' => string_for_sign pos (s ^ "(" ^ s' ^ ")"))
-
-(* Given a clause, returns its literals paired with a list of literals
- concerning TFrees; the latter should only occur in conjecture clauses. *)
-fun string_for_type_literals params pos
- (HOLClause {literals, ctypes_sorts, ...}) pool =
- let
- (* ### FIXME: use combinator *)
- val (lits, pool) = pool_map (string_for_literal params) literals pool
- val (tylits, pool) = pool_map (string_for_type_literal pos)
- (type_literals_for_types ctypes_sorts) pool
- in ((lits, tylits), pool) end
-
-fun string_for_cnf_clause name kind formula =
- "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
-
-fun string_for_disjunction strings = "(" ^ space_implode " | " strings ^ ")"
+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
-val string_for_tfree_clause =
- string_for_cnf_clause "tfree_tcs" "negated_conjecture"
- o string_for_disjunction o single
-
-fun string_for_classrel_literals sub sup =
- let val tvar = "(T)" in
- string_for_disjunction [string_for_sign false (sub ^ tvar),
- string_for_sign true (sup ^ tvar)]
- end
-
-fun string_for_clause params
- (cls as HOLClause {axiom_name, clause_id, kind, ...}) pool =
+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 ((lits, tylits), pool) =
- string_for_type_literals params (kind = Conjecture) cls pool
- val name = clause_prefix ^ ascii_of axiom_name ^ "_" ^
- Int.toString clause_id
- val cnf =
- case kind of
- Axiom => string_for_cnf_clause name "axiom"
- (string_for_disjunction (tylits @ lits))
- | Conjecture => string_for_cnf_clause name "negated_conjecture"
- (string_for_disjunction lits)
- in ((cnf, tylits), pool) end
-
-fun string_for_classrel_clause (ClassrelClause {axiom_name, subclass,
- superclass, ...}) =
- string_for_cnf_clause axiom_name "axiom"
- (string_for_classrel_literals subclass superclass)
-
-fun string_for_arity_literal (TConsLit (c, t, args)) =
- string_for_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
- | string_for_arity_literal (TVarLit (c, str)) =
- string_for_sign false (make_type_class c ^ "(" ^ str ^ ")")
-
-fun string_for_arity_clause (ArityClause {axiom_name, conclLit, premLits,
- ...}) =
- string_for_cnf_clause (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
- (string_for_disjunction (map string_for_arity_literal
- (conclLit :: premLits)))
-
-(* Find the minimal arity of each function mentioned in the term. Also, note
- which uses are not at top level, to see if "hBOOL" is needed. *)
-fun count_constants_term top_level t =
- let val (head, args) = strip_combterm_comb t in
- (case head of
- CombConst ((a, _), _, _) =>
- let
- (* Predicate or function version of "equal"? *)
- val a = if a = "equal" andalso not top_level then "c_fequal" else a
- val n = length args
- in
- Symtab.map_default
- (a, {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
- | _ => I)
- #> fold (count_constants_term false) args
- end
-fun count_constants_literal (Literal (_, t)) = count_constants_term true t
-fun count_constants_clause (HOLClause {literals, ...}) =
- fold count_constants_literal literals
-fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
- fold (fold count_constants_clause)
- [conjectures, extra_clauses, helper_clauses]
-
-fun write_tptp_file readable_names full_types explicit_apply file clauses =
- let
- fun section _ [] = []
- | section name ss =
- "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
- ")\n" :: ss
- val pool = empty_name_pool readable_names
- val (conjectures, axclauses, _, helper_clauses,
- classrel_clauses, arity_clauses) = clauses
- val const_tab = if explicit_apply then NONE
- else SOME (Symtab.empty |> count_constants clauses)
- val params = (full_types, const_tab)
- val ((conjecture_clss, tfree_litss), pool) =
- pool_map (string_for_clause params) conjectures pool |>> ListPair.unzip
- val tfree_clss =
- map string_for_tfree_clause (fold (union (op =)) tfree_litss [])
- val (ax_clss, pool) =
- pool_map (apfst fst oo string_for_clause params) axclauses pool
- val classrel_clss = map string_for_classrel_clause classrel_clauses
- val arity_clss = map string_for_arity_clause arity_clauses
- val (helper_clss, pool) = pool_map (apfst fst oo string_for_clause params)
- helper_clauses pool
+ 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 ax_clss + length classrel_clss + length arity_clss
- + length helper_clss
- val _ =
- File.write_list file
- ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
- section "Relevant fact" ax_clss @
- section "Class relationship" classrel_clss @
- section "Arity declaration" arity_clss @
- section "Helper fact" helper_clss @
- section "Conjecture" conjecture_clss @
- section "Type variable" tfree_clss)
+ 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;