factor out TPTP format output into file of its own, to facilitate further changes
--- a/src/HOL/IsaMakefile Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 22 23:54:02 2010 +0200
@@ -322,6 +322,7 @@
Tools/Sledgehammer/sledgehammer_hol_clause.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
+ Tools/Sledgehammer/sledgehammer_tptp_format.ML \
Tools/Sledgehammer/sledgehammer_util.ML \
Tools/SMT/cvc3_solver.ML \
Tools/SMT/smtlib_interface.ML \
--- a/src/HOL/Sledgehammer.thy Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jun 22 23:54:02 2010 +0200
@@ -17,6 +17,7 @@
("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+ ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_systems.ML")
("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
@@ -103,6 +104,7 @@
use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_systems.ML"
setup ATP_Systems.setup
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 23:54:02 2010 +0200
@@ -27,6 +27,7 @@
open Sledgehammer_HOL_Clause
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_TPTP_Format
open ATP_Manager
(** generic ATP **)
@@ -191,8 +192,8 @@
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
in (output, as_time t) end;
- fun split_time' s =
- if Config.get ctxt measure_runtime then split_time s else (s, 0)
+ val split_time' =
+ if Config.get ctxt measure_runtime then split_time else rpair 0
fun run_on probfile =
if File.exists command then
write_tptp_file (debug andalso overlord) full_types explicit_apply
@@ -244,35 +245,8 @@
fun tptp_prover name p = (name, generic_tptp_prover (name, p));
-
-(** common provers **)
-
fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
-(* Vampire *)
-
-(* Vampire requires an explicit time limit. *)
-
-val vampire_config : prover_config =
- {home_var = "VAMPIRE_HOME",
- executable = "vampire",
- arguments = fn timeout =>
- "--output_syntax tptp --mode casc -t " ^
- string_of_int (to_generous_secs timeout),
- proof_delims =
- [("=========== Refutation ==========",
- "======= End of refutation ======="),
- ("% SZS output start Refutation", "% SZS output end Refutation")],
- known_failures =
- [(Unprovable, "UNPROVABLE"),
- (IncompleteUnprovable, "CANNOT PROVE"),
- (Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found")],
- max_axiom_clauses = 60,
- prefers_theory_relevant = false}
-val vampire = tptp_prover "vampire" vampire_config
-
-
(* E prover *)
val tstp_proof_delims =
@@ -299,8 +273,6 @@
val e = tptp_prover "e" e_config
-(* SPASS *)
-
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
@@ -322,7 +294,28 @@
prefers_theory_relevant = true}
val spass = tptp_prover "spass" spass_config
-(* remote prover invocation via SystemOnTPTP *)
+(* Vampire *)
+
+val vampire_config : prover_config =
+ {home_var = "VAMPIRE_HOME",
+ executable = "vampire",
+ arguments = fn timeout =>
+ "--output_syntax tptp --mode casc -t " ^
+ string_of_int (to_generous_secs timeout),
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation ======="),
+ ("% SZS output start Refutation", "% SZS output end Refutation")],
+ known_failures =
+ [(Unprovable, "UNPROVABLE"),
+ (IncompleteUnprovable, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
+ (OutOfResources, "Refutation not found")],
+ max_axiom_clauses = 60,
+ prefers_theory_relevant = false}
+val vampire = tptp_prover "vampire" vampire_config
+
+(* Remote prover invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([]: string list);
@@ -333,7 +326,7 @@
error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
fun refresh_systems_on_tptp () =
- Synchronized.change systems (fn _ => get_systems ());
+ Synchronized.change systems (fn _ => get_systems ())
fun get_system prefix = Synchronized.change_result systems (fn systems =>
(if null systems then get_systems () else systems)
@@ -341,15 +334,14 @@
fun the_system prefix =
(case get_system prefix of
- NONE => error ("System " ^ quote prefix ^
- " not available at SystemOnTPTP.")
+ NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
| SOME sys => sys);
val remote_known_failures =
[(TimedOut, "says Timeout"),
(MalformedOutput, "Remote script could not extract proof")]
-fun remote_prover_config atp_prefix args
+fun remote_config atp_prefix args
({proof_delims, known_failures, max_axiom_clauses,
prefers_theory_relevant, ...} : prover_config) : prover_config =
{home_var = "ISABELLE_ATP_MANAGER",
@@ -362,17 +354,12 @@
max_axiom_clauses = max_axiom_clauses,
prefers_theory_relevant = prefers_theory_relevant}
-val remote_vampire =
- tptp_prover (remotify (fst vampire))
- (remote_prover_config "Vampire---9" "" vampire_config)
+fun remote_tptp_prover prover atp_prefix args config =
+ tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
-val remote_e =
- tptp_prover (remotify (fst e))
- (remote_prover_config "EP---" "" e_config)
-
-val remote_spass =
- tptp_prover (remotify (fst spass))
- (remote_prover_config "SPASS---" "-x" spass_config)
+val remote_e = remote_tptp_prover e "EP---" "" e_config
+val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config
+val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config
fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
name |> getenv home_var = "" ? remotify
@@ -381,7 +368,7 @@
space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
remotify (fst vampire)]
-val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
+val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
val prover_setup = fold add_prover provers
val setup =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 22 23:54:02 2010 +0200
@@ -24,6 +24,7 @@
open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 23:54:02 2010 +0200
@@ -576,6 +576,47 @@
|> has_override ? make_unique
end
+(** Helper clauses **)
+
+fun count_combterm (CombConst ((c, _), _, _)) =
+ Symtab.map_entry c (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
+fun count_literal (Literal (_, t)) = count_combterm t
+fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+
+val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
+fun cnf_helper_thms thy raw =
+ map (`Thm.get_name_hint)
+ #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
+
+val optional_helpers =
+ [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
+ (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
+ (["c_COMBS"], (false, @{thms COMBS_def}))]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], (true, @{thms True_or_False})),
+ (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+
+val init_counters =
+ Symtab.make (maps (maps (map (rpair 0) o fst))
+ [optional_helpers, optional_typed_helpers])
+
+fun get_helper_clauses thy is_FO full_types conjectures axcls =
+ let
+ val axclauses = map snd (make_axiom_clauses thy axcls)
+ val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ val cnfs =
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, (raw, ths)) =>
+ if exists is_needed ss then cnf_helper_thms thy raw ths
+ else []))
+ @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
+ in map snd (make_axiom_clauses thy cnfs) end
+
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
fun prepare_clauses full_types goal_cls axcls extra_cls thy =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 22 23:54:02 2010 +0200
@@ -10,11 +10,11 @@
signature SLEDGEHAMMER_FOL_CLAUSE =
sig
+ val type_wrapper_name : string
val schematic_var_prefix: string
val fixed_var_prefix: string
val tvar_prefix: string
val tfree_prefix: string
- val clause_prefix: string
val const_prefix: string
val tconst_prefix: string
val class_prefix: string
@@ -23,7 +23,6 @@
val type_const_trans_table: string Symtab.table
val ascii_of: string -> string
val undo_ascii_of: string -> string
- val paren_pack : string list -> string
val make_schematic_var : string * int -> string
val make_fixed_var : string -> string
val make_schematic_type_var : string * int -> string
@@ -37,12 +36,6 @@
val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
val nice_name : name -> name_pool option -> string * name_pool option
datatype kind = Axiom | Conjecture
- datatype fol_type =
- TyVar of name |
- TyFree of name |
- TyConstr of name * fol_type list
- val string_of_fol_type :
- fol_type -> name_pool option -> string * name_pool option
datatype type_literal =
TyLitVar of string * name |
TyLitFree of string * name
@@ -57,13 +50,6 @@
{axiom_name: string, subclass: class, superclass: class}
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
- val tptp_sign: bool -> string -> string
- val tptp_of_type_literal :
- bool -> type_literal -> name_pool option -> string * name_pool option
- val gen_tptp_cls : int * string * kind * string list * string list -> string
- val tptp_tfree_clause : string -> string
- val tptp_arity_clause : arity_clause -> string
- val tptp_classrel_clause : classrel_clause -> string
end
structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
@@ -71,15 +57,15 @@
open Sledgehammer_Util
+val type_wrapper_name = "ti"
+
val schematic_var_prefix = "V_";
val fixed_var_prefix = "v_";
val tvar_prefix = "T_";
val tfree_prefix = "t_";
-val clause_prefix = "cls_";
-val arclause_prefix = "clsarity_"
-val clrelclause_prefix = "clsrel_";
+val classrel_clause_prefix = "clsrel_";
val const_prefix = "c_";
val tconst_prefix = "tc_";
@@ -152,12 +138,6 @@
val undo_ascii_of = undo_ascii_aux [] o String.explode;
-(* convert a list of strings into one single string; surrounded by brackets *)
-fun paren_pack [] = "" (*empty argument list*)
- | paren_pack strings = "(" ^ commas strings ^ ")";
-
-fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
-
(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
@@ -260,19 +240,6 @@
(**** Isabelle FOL clauses ****)
-datatype fol_type =
- TyVar of name |
- TyFree of name |
- TyConstr of name * fol_type list
-
-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
-
(* The first component is the type class; the second is a TVar or TFree. *)
datatype type_literal =
TyLitVar of string * name |
@@ -341,7 +308,8 @@
in fold add_supers subs [] end
fun make_classrel_clause (sub,super) =
- ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
+ ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+ ascii_of super,
subclass = make_type_class sub,
superclass = make_type_class super};
@@ -390,48 +358,4 @@
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
in (classes', multi_arity_clause cpairs) end;
-
-(**** Produce TPTP files ****)
-
-fun string_of_clausename (cls_id, ax_name) =
- clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id
-
-fun tptp_sign true s = s
- | tptp_sign false s = "~ " ^ s
-
-fun tptp_of_type_literal pos (TyLitVar (s, name)) =
- nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
- | tptp_of_type_literal pos (TyLitFree (s, name)) =
- nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
-
-fun tptp_cnf name kind formula =
- "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
-
-fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
- tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
- (tptp_clause (tylits @ lits))
- | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
- tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
- (tptp_clause lits)
-
-fun tptp_tfree_clause tfree_lit =
- tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
-
-fun tptp_of_arLit (TConsLit (c,t,args)) =
- tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
- | tptp_of_arLit (TVarLit (c,str)) =
- tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
-
-fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
- tptp_cnf (arclause_prefix ^ ascii_of axiom_name) "axiom"
- (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
-
-fun tptp_classrelLits sub sup =
- let val tvar = "(T)"
- in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
-
-fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
- ...}) =
- tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 19:10:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 23:54:02 2010 +0200
@@ -2,7 +2,7 @@
Author: Jia Meng, NICTA
Author: Jasmin Blanchette, TU Muenchen
-FOL clauses translated from HOL formulae.
+FOL clauses translated from HOL formulas.
*)
signature SLEDGEHAMMER_HOL_CLAUSE =
@@ -11,21 +11,24 @@
type name = Sledgehammer_FOL_Clause.name
type name_pool = Sledgehammer_FOL_Clause.name_pool
type kind = Sledgehammer_FOL_Clause.kind
- type fol_type = Sledgehammer_FOL_Clause.fol_type
type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
type arity_clause = Sledgehammer_FOL_Clause.arity_clause
type polarity = bool
+ datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
datatype combterm =
- CombConst of name * fol_type * fol_type list (* Const and Free *) |
- CombVar of name * fol_type |
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
datatype hol_clause =
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
literals: literal list, ctypes_sorts: typ list}
- val type_of_combterm : combterm -> fol_type
+ val type_of_combterm : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
val conceal_skolem_somes :
@@ -33,12 +36,6 @@
exception TRIVIAL of unit
val make_conjecture_clauses : theory -> thm list -> hol_clause list
val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
- val type_wrapper_name : string
- val get_helper_clauses :
- theory -> bool -> bool -> hol_clause list -> cnf_thm list -> hol_clause list
- val write_tptp_file : 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_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
@@ -48,24 +45,20 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
-fun min_arity_of const_min_arity c =
- the_default 0 (Symtab.lookup const_min_arity c)
-
-(*True if the constant ever appears outside of the top-level position in literals.
- If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL explicit_apply const_needs_hBOOL c =
- explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
-
-
(******************************************************)
(* data types for typed combinator expressions *)
(******************************************************)
type polarity = bool
+datatype combtyp =
+ TyVar of name |
+ TyFree of name |
+ TyConstr of name * combtyp list
+
datatype combterm =
- CombConst of name * fol_type * fol_type list (* Const and Free *) |
- CombVar of name * fol_type |
+ CombConst of name * combtyp * combtyp list (* Const and Free *) |
+ CombVar of name * combtyp |
CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm;
@@ -74,11 +67,24 @@
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
literals: literal list, ctypes_sorts: typ list}
-
(*********************************************************************)
(* convert a clause with type Term.term to a clause with type clause *)
(*********************************************************************)
+(*Result of a function type; no need to check that the argument type matches.*)
+fun result_type (TyConstr (_, [_, tp2])) = tp2
+ | result_type _ = raise Fail "non-function type"
+
+fun type_of_combterm (CombConst (_, tp, _)) = tp
+ | type_of_combterm (CombVar (_, tp)) = tp
+ | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
+
+(*gets the head of a combinator application, along with the list of arguments*)
+fun strip_combterm_comb u =
+ let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
+ | stripc x = x
+ in stripc(u,[]) end
+
fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
(pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
| isFalse _ = false;
@@ -109,7 +115,6 @@
| simp_type_of (TVar (x, _)) =
TyVar (make_schematic_type_var x, string_of_indexname x)
-
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
fun combterm_of thy (Const (c, T)) =
let
@@ -224,254 +229,4 @@
in cls :: aux (n + 1) skolem_somes ths end
in aux 0 [] end
-(**********************************************************************)
-(* convert clause into TPTP format *)
-(**********************************************************************)
-
-(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
- | result_type _ = raise Fail "non-function type"
-
-fun type_of_combterm (CombConst (_, tp, _)) = tp
- | type_of_combterm (CombVar (_, tp)) = tp
- | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
-
-(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
- let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
- | stripc x = x
- in stripc(u,[]) end;
-
-val type_wrapper_name = "ti"
-
-fun head_needs_hBOOL explicit_apply const_needs_hBOOL
- (CombConst ((c, _), _, _)) =
- needs_hBOOL explicit_apply const_needs_hBOOL 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
- else
- (s, pool)
-
-fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
- if head_needs_hBOOL explicit_apply cnh 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);
-
-(* Apply an operator to the argument strings, using either the "apply" operator
- or direct function application. *)
-fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
- pool =
- let
- val s = if s = "equal" then "c_fequal" else s
- val nargs = min_arity_of cma 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))
-
-fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) 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 full_types cma (head, ss) pool
- in
- wrap_type_if full_types explicit_apply cnh (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_of_predicate (params as (_, explicit_apply, _, cnh)) t =
- case #1 (strip_combterm_comb t) of
- CombConst ((s, _), _, _) =>
- (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
- params t
- | _ => boolify params t
-
-
-(*** TPTP format ***)
-
-fun tptp_of_equality params pos (t1, t2) =
- pool_map (string_of_combterm params) [t1, t2]
- #>> space_implode (if pos then " = " else " != ")
-
-fun tptp_literal params
- (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
- t2))) =
- tptp_of_equality params pos (t1, t2)
- | tptp_literal params (Literal (pos, pred)) =
- string_of_predicate params pred #>> tptp_sign pos
-
-(* Given a clause, returns its literals paired with a list of literals
- concerning TFrees; the latter should only occur in conjecture clauses. *)
-fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
- pool =
- let
- val (lits, pool) = pool_map (tptp_literal params) literals pool
- val (tylits, pool) = pool_map (tptp_of_type_literal pos)
- (type_literals_for_types ctypes_sorts) pool
- in ((lits, tylits), pool) end
-
-fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
- pool =
- let
- val ((lits, tylits), pool) =
- tptp_type_literals params (kind = Conjecture) cls pool
- in
- ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
- end
-
-
-(**********************************************************************)
-(* write clauses to files *)
-(**********************************************************************)
-
-fun count_combterm (CombConst ((c, _), _, _)) =
- Symtab.map_entry c (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-
-fun count_literal (Literal (_, t)) = count_combterm t
-
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
-
-val optional_helpers =
- [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
- (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
- (["c_COMBS"], (false, @{thms COMBS_def}))]
-val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{thms if_True if_False True_or_False}))]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
-
-val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
-
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
- let
- val axclauses = map snd (make_axiom_clauses thy axcls)
- val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- val cnfs =
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, (raw, ths)) =>
- if exists is_needed ss then cnf_helper_thms thy raw ths
- else []))
- @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
- in map snd (make_axiom_clauses thy cnfs) end
-
-(*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 toplev t (const_min_arity, const_needs_hBOOL) =
- let val (head, args) = strip_combterm_comb t
- val n = length args
- val (const_min_arity, const_needs_hBOOL) =
- (const_min_arity, const_needs_hBOOL)
- |> fold (count_constants_term false) args
- in
- case head of
- CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
- let val a = if a="equal" andalso not toplev then "c_fequal" else a
- in
- (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
- const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
- end
- | _ => (const_min_arity, const_needs_hBOOL)
- end;
-
-(*A literal is a top-level term*)
-fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
- count_constants_term true t (const_min_arity, const_needs_hBOOL);
-
-fun count_constants_clause (HOLClause {literals, ...})
- (const_min_arity, const_needs_hBOOL) =
- fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
-
-fun display_arity explicit_apply const_needs_hBOOL (c, n) =
- trace_msg (fn () => "Constant: " ^ c ^
- " arity:\t" ^ Int.toString n ^
- (if needs_hBOOL explicit_apply const_needs_hBOOL c then
- " needs hBOOL"
- else
- ""))
-
-fun count_constants explicit_apply
- (conjectures, _, extra_clauses, helper_clauses, _, _) =
- if not explicit_apply then
- let val (const_min_arity, const_needs_hBOOL) =
- fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
- |> fold count_constants_clause extra_clauses
- |> fold count_constants_clause helper_clauses
- val _ = app (display_arity explicit_apply const_needs_hBOOL)
- (Symtab.dest (const_min_arity))
- in (const_min_arity, const_needs_hBOOL) end
- else (Symtab.empty, Symtab.empty);
-
-(* TPTP format *)
-
-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 (cma, cnh) = count_constants explicit_apply clauses
- val params = (full_types, explicit_apply, cma, cnh)
- val ((conjecture_clss, tfree_litss), pool) =
- pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
- val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
- val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
- pool
- val classrel_clss = map tptp_classrel_clause classrel_clauses
- val arity_clss = map tptp_arity_clause arity_clauses
- val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
- helper_clauses pool
- 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)
- in (pool, conjecture_offset) end
-
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 22 23:54:02 2010 +0200
@@ -0,0 +1,255 @@
+(* 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 name_pool = Sledgehammer_FOL_Clause.name_pool
+ type type_literal = Sledgehammer_FOL_Clause.type_literal
+ type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
+ type arity_clause = Sledgehammer_FOL_Clause.arity_clause
+ type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+
+ val tptp_of_type_literal :
+ bool -> type_literal -> name_pool option -> string * name_pool option
+ val write_tptp_file :
+ 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 Sledgehammer_Util
+open Sledgehammer_FOL_Clause
+open Sledgehammer_HOL_Clause
+
+val clause_prefix = "cls_"
+val arity_clause_prefix = "clsarity_"
+
+fun paren_pack [] = ""
+ | paren_pack strings = "(" ^ commas strings ^ ")"
+
+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
+
+(* True if the constant ever appears outside of the top-level position in
+ literals. If false, the constant always receives all of its arguments and is
+ used as a predicate. *)
+fun needs_hBOOL explicit_apply const_needs_hBOOL c =
+ explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
+
+fun head_needs_hBOOL explicit_apply const_needs_hBOOL
+ (CombConst ((c, _), _, _)) =
+ needs_hBOOL explicit_apply const_needs_hBOOL 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
+ else
+ (s, pool)
+
+fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
+ if head_needs_hBOOL explicit_apply cnh 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 const_min_arity = the_default 0 o Symtab.lookup const_min_arity
+
+(* Apply an operator to the argument strings, using either the "apply" operator
+ or direct function application. *)
+fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
+ pool =
+ let
+ val s = if s = "equal" then "c_fequal" else s
+ val nargs = min_arity_of cma 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))
+
+fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) 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 full_types cma (head, ss) pool
+ in
+ wrap_type_if full_types explicit_apply cnh (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_of_predicate (params as (_, explicit_apply, _, cnh)) t =
+ case #1 (strip_combterm_comb t) of
+ CombConst ((s, _), _, _) =>
+ (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
+ params t
+ | _ => boolify params t
+
+fun tptp_of_equality params pos (t1, t2) =
+ pool_map (string_of_combterm params) [t1, t2]
+ #>> space_implode (if pos then " = " else " != ")
+
+fun tptp_sign true s = s
+ | tptp_sign false s = "~ " ^ s
+
+fun tptp_literal params
+ (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
+ t2))) =
+ tptp_of_equality params pos (t1, t2)
+ | tptp_literal params (Literal (pos, pred)) =
+ string_of_predicate params pred #>> tptp_sign pos
+
+fun tptp_of_type_literal pos (TyLitVar (s, name)) =
+ nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
+ | tptp_of_type_literal pos (TyLitFree (s, name)) =
+ nice_name name #>> (fn s' => tptp_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 tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
+ pool =
+ let
+ val (lits, pool) = pool_map (tptp_literal params) literals pool
+ val (tylits, pool) = pool_map (tptp_of_type_literal pos)
+ (type_literals_for_types ctypes_sorts) pool
+ in ((lits, tylits), pool) end
+
+fun tptp_cnf name kind formula =
+ "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
+
+fun tptp_raw_clause strings = "(" ^ space_implode " | " strings ^ ")"
+
+val tptp_tfree_clause =
+ tptp_cnf "tfree_tcs" "negated_conjecture" o tptp_raw_clause o single
+
+fun tptp_classrel_literals sub sup =
+ let val tvar = "(T)" in
+ tptp_raw_clause [tptp_sign false (sub ^ tvar), tptp_sign true (sup ^ tvar)]
+ end
+
+fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
+ pool =
+ let
+ val ((lits, tylits), pool) =
+ tptp_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 => tptp_cnf name "axiom" (tptp_raw_clause (tylits @ lits))
+ | Conjecture => tptp_cnf name "negated_conjecture" (tptp_raw_clause lits)
+ in ((cnf, tylits), pool) end
+
+fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
+ ...}) =
+ tptp_cnf axiom_name "axiom" (tptp_classrel_literals subclass superclass)
+
+fun tptp_of_arity_literal (TConsLit (c, t, args)) =
+ tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
+ | tptp_of_arity_literal (TVarLit (c, str)) =
+ tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
+
+fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
+ tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
+ (tptp_raw_clause (map tptp_of_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 toplev t (const_min_arity, const_needs_hBOOL) =
+ let
+ val (head, args) = strip_combterm_comb t
+ val n = length args
+ val (const_min_arity, const_needs_hBOOL) =
+ (const_min_arity, const_needs_hBOOL)
+ |> fold (count_constants_term false) args
+ in
+ case head of
+ CombConst ((a, _), _, _) => (*predicate or function version of "equal"?*)
+ let val a = if a="equal" andalso not toplev then "c_fequal" else a
+ in
+ (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
+ const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
+ end
+ | _ => (const_min_arity, const_needs_hBOOL)
+ end
+fun count_constants_lit (Literal (_, t)) = count_constants_term true t
+fun count_constants_clause (HOLClause {literals, ...}) =
+ fold count_constants_lit literals
+fun count_constants explicit_apply
+ (conjectures, _, extra_clauses, helper_clauses, _, _) =
+ (Symtab.empty, Symtab.empty)
+ |> (if explicit_apply then
+ I
+ else
+ 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 (cma, cnh) = count_constants explicit_apply clauses
+ val params = (full_types, explicit_apply, cma, cnh)
+ val ((conjecture_clss, tfree_litss), pool) =
+ pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
+ val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
+ val (ax_clss, pool) =
+ pool_map (apfst fst oo tptp_clause params) axclauses pool
+ val classrel_clss = map tptp_classrel_clause classrel_clauses
+ val arity_clss = map tptp_arity_clause arity_clauses
+ val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
+ helper_clauses pool
+ 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)
+ in (pool, conjecture_offset) end
+
+end;