--- 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)
--- 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) =
--- 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;