# HG changeset patch # User paulson # Date 1164371070 -3600 # Node ID 6c5755ad9caeaac042d34453455e4064a8460b31 # Parent 3029fb2d56507be56bdf91c1f1cb30cc4deb26ef ATP linkup now generates "new TPTP" rather than "old TPTP" diff -r 3029fb2d5650 -r 6c5755ad9cae src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Nov 23 23:05:28 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Fri Nov 24 13:24:30 2006 +0100 @@ -817,7 +817,7 @@ let val Eprover = helper_path "E_HOME" "eproof" in ("E", Eprover, - "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) :: + "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) :: make_atp_list xs (n+1) end else error ("Invalid prover name: " ^ !prover) diff -r 3029fb2d5650 -r 6c5755ad9cae src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Nov 23 23:05:28 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Fri Nov 24 13:24:30 2006 +0100 @@ -17,12 +17,14 @@ datatype fol_term = UVar of string * fol_type | Fun of string * fol_type list * fol_term list; datatype predicate = Predicate of string * fol_type list * fol_term list; + datatype kind = Axiom | Conjecture; + val name_of_kind : kind -> string type typ_var and type_literal and literal val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list val arity_clause_thy: theory -> arityClause list val ascii_of : string -> string - val bracket_pack : string list -> string + val tptp_pack : string list -> string val make_classrel_clauses: theory -> class list -> class list -> classrelClause list val clause_prefix : string val clause2tptp : clause -> string * string list @@ -30,8 +32,7 @@ val dfg_write_file: thm list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list val fixed_var_prefix : string - val gen_tptp_cls : int * string * string * string -> string - val gen_tptp_type_cls : int * string * string * string * int -> string + val gen_tptp_cls : int * string * string * string list -> string val get_axiomName : clause -> string val get_literals : clause -> literal list val init : theory -> unit @@ -52,7 +53,6 @@ val mk_typ_var_sort : Term.typ -> typ_var * sort val paren_pack : string list -> string val schematic_var_prefix : string - val special_equal : bool ref val string_of_fol_type : fol_type -> string val tconst_prefix : string val tfree_prefix : string @@ -86,11 +86,6 @@ structure ResClause = struct -(* Added for typed equality *) -val special_equal = ref false; (* by default,equality does not carry type information *) -val eq_typ_wrapper = "typeinfo"; (* default string *) - - val schematic_var_prefix = "V_"; val fixed_var_prefix = "v_"; @@ -167,7 +162,8 @@ fun paren_pack [] = "" (*empty argument list*) | paren_pack strings = "(" ^ commas strings ^ ")"; -fun bracket_pack strings = "[" ^ commas strings ^ "]"; +(*TSTP format uses (...) rather than the old [...]*) +fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")"; (*Remove the initial ' character from a type variable, if it is present*) @@ -207,10 +203,9 @@ val keep_types = ref true; -datatype kind = Axiom | Hypothesis | Conjecture; +datatype kind = Axiom | Conjecture; fun name_of_kind Axiom = "axiom" - | name_of_kind Hypothesis = "hypothesis" - | name_of_kind Conjecture = "conjecture"; + | name_of_kind Conjecture = "negated_conjecture"; type clause_id = int; type axiom_name = string; @@ -640,33 +635,24 @@ (**** String-oriented operations ****) -fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; - -(*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed - and if we specifically ask for types to be included. *) -fun string_of_equality (typ,terms) = - let val [tstr1,tstr2] = map string_of_term terms - val typ' = string_of_fol_type typ - in - if !keep_types andalso !special_equal - then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ - (wrap_eq_type typ' tstr2) ^ ")" - else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" - end -and string_of_term (UVar(x,_)) = x - | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) +fun string_of_term (UVar(x,_)) = x | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs)) | string_of_term (Fun (name,typs,terms)) = - let val terms_as_strings = map string_of_term terms - val typs' = if !keep_types then map string_of_fol_type typs else [] - in name ^ (paren_pack (terms_as_strings @ typs')) end; + let val typs' = if !keep_types then map string_of_fol_type typs else [] + in name ^ (paren_pack (map string_of_term terms @ typs')) end; + +fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2) + | string_of_pair _ = raise ERROR ("equality predicate requires two arguments"); + +fun string_of_equality ts = + let val (s1,s2) = string_of_pair ts + in "equal(" ^ s1 ^ "," ^ s2 ^ ")" end; (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) -fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) - | string_of_predicate (Predicate(name,typs,terms)) = - let val terms_as_strings = map string_of_term terms - val typs' = if !keep_types then map string_of_fol_type typs else [] - in name ^ (paren_pack (terms_as_strings @ typs')) end; +fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts + | string_of_predicate (Predicate(name,typs,ts)) = + let val typs' = if !keep_types then map string_of_fol_type typs else [] + in name ^ (paren_pack (map string_of_term ts @ typs')) end; fun string_of_clausename (cls_id,ax_name) = clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; @@ -746,7 +732,7 @@ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" fun dfg_tfree_clause tfree_lit = - "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" + "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" fun string_of_arClauseID (ArityClause {axiom_name,...}) = arclause_prefix ^ ascii_of axiom_name; @@ -807,22 +793,23 @@ (**** Produce TPTP files ****) (*Attach sign in TPTP syntax: false means negate.*) -fun tptp_sign true s = "++" ^ s - | tptp_sign false s = "--" ^ s +fun tptp_sign true s = s + | tptp_sign false s = "~ " ^ s -fun tptp_literal (Literal(pol,pred)) = - (if pol then "++" else "--") ^ string_of_predicate pred; +fun tptp_of_equality pol ts = + let val (s1,s2) = string_of_pair ts + val eqop = if pol then " = " else " != " + in s1 ^ eqop ^ s2 end; -fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")" - | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; +fun tptp_literal (Literal(pol,Predicate("equal",_,ts))) = tptp_of_equality pol ts + | tptp_literal (Literal(pol,pred)) = tptp_sign pol (string_of_predicate pred); + +fun tptp_of_typeLit (LTVar (s,ty)) = tptp_sign false (s ^ "(" ^ ty ^ ")") + | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true (s ^ "(" ^ ty ^ ")"); fun gen_tptp_cls (cls_id,ax_name,knd,lits) = - "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ - knd ^ "," ^ lits ^ ").\n"; - -fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = - "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ - knd ^ ",[" ^ tfree_lit ^ "]).\n"; + "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ + name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n"; fun tptp_type_lits (Clause {literals, types_sorts, ...}) = let val lits = map tptp_literal literals @@ -838,15 +825,14 @@ fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) = let val (lits,tfree_lits) = tptp_type_lits cls (*"lits" includes the typing assumptions (TVars)*) - val knd = name_of_kind kind - val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) + val cls_str = gen_tptp_cls(clause_id, axiom_name, kind, lits) in (cls_str,tfree_lits) end; fun tptp_tfree_clause tfree_lit = - "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n"; - + "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n"; + fun tptp_of_arLit (TConsLit(b,(c,t,args))) = tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")") | tptp_of_arLit (TVarLit(b,(c,str))) = @@ -857,17 +843,15 @@ val knd = name_of_kind kind val lits = map tptp_of_arLit (conclLit :: premLits) in - "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ bracket_pack lits ^ ").\n" + "cnf(" ^ arcls_id ^ "," ^ knd ^ "," ^ tptp_pack lits ^ ").\n" end; fun tptp_classrelLits sub sup = - let val tvar = "(T)" - in - "[--" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" - end; + let val tvar = "(T)" + in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = - "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" + "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" (* write out a subgoal as tptp clauses to the file "xxxx_N"*) fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) = diff -r 3029fb2d5650 -r 6c5755ad9cae src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Thu Nov 23 23:05:28 2006 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Fri Nov 24 13:24:30 2006 +0100 @@ -250,10 +250,6 @@ type axiom_name = string; -datatype kind = Axiom | Conjecture; - -fun name_of_kind Axiom = "axiom" - | name_of_kind Conjecture = "conjecture"; type polarity = bool; type indexname = Term.indexname; @@ -280,20 +276,13 @@ Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, - kind: kind, + kind: ResClause.kind, literals: literal list, ctypes_sorts: (ctyp_var * csort) list, ctvar_type_literals: ctype_literal list, ctfree_type_literals: ctype_literal list}; -fun string_of_kind (Clause cls) = name_of_kind (#kind cls); -fun get_axiomName (Clause cls) = #axiom_name cls; -fun get_clause_id (Clause cls) = #clause_id cls; - -fun get_literals (c as Clause(cls)) = #literals cls; - - (*********************************************************************) (* convert a clause with type Term.term to a clause with type clause *) (*********************************************************************) @@ -404,47 +393,37 @@ fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P | literals_of_term1 args (Const("op |",_) $ P $ Q) = - let val args' = literals_of_term1 args P - in - literals_of_term1 args' Q - end + literals_of_term1 (literals_of_term1 args P) Q | literals_of_term1 (lits,ts) P = - let val ((pred,ts'),pol) = predicate_of (P,true) - val lits' = Literal(pol,pred)::lits - in - (lits',ts union ts') - end; - + let val ((pred,ts'),pol) = predicate_of (P,true) + in + (Literal(pol,pred)::lits, ts union ts') + end; fun literals_of_term P = literals_of_term1 ([],[]) P; (* making axiom and conjecture clauses *) exception MAKE_CLAUSE -fun make_clause(clause_id,axiom_name,kind,thm,is_user) = - let val term = prop_of thm - val term' = comb_of term is_user - val (lits,ctypes_sorts) = literals_of_term term' +fun make_clause(clause_id,axiom_name,kind,th,is_user) = + let val (lits,ctypes_sorts) = literals_of_term (comb_of (prop_of th) is_user) val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts in if forall isFalse lits then error "Problem too trivial for resolution (empty clause)" else - Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind, + Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, literals = lits, ctypes_sorts = ctypes_sorts, ctvar_type_literals = ctvar_lits, ctfree_type_literals = ctfree_lits} end; -fun make_axiom_clause thm (ax_name,cls_id,is_user) = - make_clause(cls_id,ax_name,Axiom,thm,is_user); - fun make_axiom_clauses [] user_lemmas = [] - | make_axiom_clauses ((thm,(name,id))::thms) user_lemmas = + | make_axiom_clauses ((th,(name,id))::ths) user_lemmas = let val is_user = name mem user_lemmas - val cls = SOME (make_axiom_clause thm (name,id,is_user)) + val cls = SOME (make_clause(id, name, ResClause.Axiom, th, is_user)) handle MAKE_CLAUSE => NONE - val clss = make_axiom_clauses thms user_lemmas + val clss = make_axiom_clauses ths user_lemmas in case cls of NONE => clss | SOME(cls') => if isTaut cls' then clss @@ -454,7 +433,7 @@ fun make_conjecture_clauses_aux _ [] = [] | make_conjecture_clauses_aux n (th::ths) = - make_clause(n,"conjecture",Conjecture,th,true) :: + make_clause(n,"conjecture", ResClause.Conjecture, th, true) :: make_conjecture_clauses_aux (n+1) ths; val make_conjecture_clauses = make_conjecture_clauses_aux 0; @@ -574,13 +553,7 @@ (* tptp format *) -fun tptp_literal (Literal(pol,pred)) = - let val pred_string = string_of_combterm true pred - val pol_str = if pol then "++" else "--" - in - pol_str ^ pred_string - end; - +fun tptp_literal (Literal(pol,pred)) = ResClause.tptp_sign pol (string_of_combterm true pred); fun tptp_type_lits (Clause cls) = let val lits = map tptp_literal (#literals cls) @@ -595,13 +568,9 @@ end; -fun clause2tptp cls = +fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = let val (lits,ctfree_lits) = tptp_type_lits cls - val cls_id = get_clause_id cls - val ax_name = get_axiomName cls - val knd = string_of_kind cls - val lits_str = ResClause.bracket_pack lits - val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str) + val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits) in (cls_str,ctfree_lits) end; @@ -638,7 +607,7 @@ let val (lits,tfree_lits) = dfg_clause_aux cls val vars = dfg_vars cls val tvars = ResClause.get_tvar_strs ctypes_sorts - val knd = name_of_kind kind + val knd = ResClause.name_of_kind kind val lits_str = commas lits val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) in (cls_str, tfree_lits) end;