# HG changeset patch # User blanchet # Date 1277243642 -7200 # Node ID f39464d971c44fb33b1b7866e7f9e5d6f5a6fa4a # Parent f9af8a863bd3bd7eff6e75f24dd6075351a0dbe9 factor out TPTP format output into file of its own, to facilitate further changes diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/IsaMakefile --- 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 \ diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Sledgehammer.thy --- 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 diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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 = diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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 (); diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 = diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- 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; diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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; diff -r f9af8a863bd3 -r f39464d971c4 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- /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;