ATP linkup now generates "new TPTP" rather than "old TPTP"
authorpaulson
Fri Nov 24 13:24:30 2006 +0100 (2006-11-24)
changeset 215096c5755ad9cae
parent 21508 3029fb2d5650
child 21510 7e72185e4b24
ATP linkup now generates "new TPTP" rather than "old TPTP"
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Nov 23 23:05:28 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Nov 24 13:24:30 2006 +0100
     1.3 @@ -817,7 +817,7 @@
     1.4  	       let val Eprover = helper_path "E_HOME" "eproof"
     1.5  	       in
     1.6  		  ("E", Eprover, 
     1.7 -		     "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
     1.8 +		     "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
     1.9  		   make_atp_list xs (n+1)
    1.10  	       end
    1.11  	     else error ("Invalid prover name: " ^ !prover)
     2.1 --- a/src/HOL/Tools/res_clause.ML	Thu Nov 23 23:05:28 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Nov 24 13:24:30 2006 +0100
     2.3 @@ -17,12 +17,14 @@
     2.4    datatype fol_term = UVar of string * fol_type
     2.5                      | Fun of string * fol_type list * fol_term list;
     2.6    datatype predicate = Predicate of string * fol_type list * fol_term list;
     2.7 +  datatype kind = Axiom | Conjecture;
     2.8 +  val name_of_kind : kind -> string
     2.9    type typ_var and type_literal and literal
    2.10    val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list
    2.11    val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    2.12    val arity_clause_thy: theory -> arityClause list 
    2.13    val ascii_of : string -> string
    2.14 -  val bracket_pack : string list -> string
    2.15 +  val tptp_pack : string list -> string
    2.16    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
    2.17    val clause_prefix : string 
    2.18    val clause2tptp : clause -> string * string list
    2.19 @@ -30,8 +32,7 @@
    2.20    val dfg_write_file:  thm list -> string -> 
    2.21         ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
    2.22    val fixed_var_prefix : string
    2.23 -  val gen_tptp_cls : int * string * string * string -> string
    2.24 -  val gen_tptp_type_cls : int * string * string * string * int -> string
    2.25 +  val gen_tptp_cls : int * string * string * string list -> string
    2.26    val get_axiomName : clause ->  string
    2.27    val get_literals : clause -> literal list
    2.28    val init : theory -> unit
    2.29 @@ -52,7 +53,6 @@
    2.30    val mk_typ_var_sort : Term.typ -> typ_var * sort
    2.31    val paren_pack : string list -> string
    2.32    val schematic_var_prefix : string
    2.33 -  val special_equal : bool ref
    2.34    val string_of_fol_type : fol_type -> string
    2.35    val tconst_prefix : string 
    2.36    val tfree_prefix : string
    2.37 @@ -86,11 +86,6 @@
    2.38  structure ResClause =
    2.39  struct
    2.40  
    2.41 -(* Added for typed equality *)
    2.42 -val special_equal = ref false; (* by default,equality does not carry type information *)
    2.43 -val eq_typ_wrapper = "typeinfo"; (* default string *)
    2.44 -
    2.45 -
    2.46  val schematic_var_prefix = "V_";
    2.47  val fixed_var_prefix = "v_";
    2.48  
    2.49 @@ -167,7 +162,8 @@
    2.50  fun paren_pack [] = ""   (*empty argument list*)
    2.51    | paren_pack strings = "(" ^ commas strings ^ ")";
    2.52  
    2.53 -fun bracket_pack strings = "[" ^ commas strings ^ "]";
    2.54 +(*TSTP format uses (...) rather than the old [...]*)
    2.55 +fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
    2.56  
    2.57  
    2.58  (*Remove the initial ' character from a type variable, if it is present*)
    2.59 @@ -207,10 +203,9 @@
    2.60  
    2.61  val keep_types = ref true;
    2.62  
    2.63 -datatype kind = Axiom | Hypothesis | Conjecture;
    2.64 +datatype kind = Axiom | Conjecture;
    2.65  fun name_of_kind Axiom = "axiom"
    2.66 -  | name_of_kind Hypothesis = "hypothesis"
    2.67 -  | name_of_kind Conjecture = "conjecture";
    2.68 +  | name_of_kind Conjecture = "negated_conjecture";
    2.69  
    2.70  type clause_id = int;
    2.71  type axiom_name = string;
    2.72 @@ -640,33 +635,24 @@
    2.73  
    2.74  (**** String-oriented operations ****)
    2.75  
    2.76 -fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
    2.77 -
    2.78 -(*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed 
    2.79 - and if we specifically ask for types to be included.   *)
    2.80 -fun string_of_equality (typ,terms) =
    2.81 -      let val [tstr1,tstr2] = map string_of_term terms
    2.82 -	  val typ' = string_of_fol_type typ
    2.83 -      in
    2.84 -	  if !keep_types andalso !special_equal 
    2.85 -	  then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ 
    2.86 -		 	  (wrap_eq_type typ' tstr2) ^ ")"
    2.87 -	  else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
    2.88 -      end
    2.89 -and string_of_term (UVar(x,_)) = x
    2.90 -  | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms)
    2.91 +fun string_of_term (UVar(x,_)) = x
    2.92    | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs))
    2.93    | string_of_term (Fun (name,typs,terms)) = 
    2.94 -      let val terms_as_strings = map string_of_term terms
    2.95 -	  val typs' = if !keep_types then map string_of_fol_type typs else []
    2.96 -      in  name ^ (paren_pack (terms_as_strings @ typs'))  end;
    2.97 +      let val typs' = if !keep_types then map string_of_fol_type typs else []
    2.98 +      in  name ^ (paren_pack (map string_of_term terms @ typs'))  end;
    2.99 +
   2.100 +fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2)
   2.101 +  | string_of_pair _ = raise ERROR ("equality predicate requires two arguments");
   2.102 +
   2.103 +fun string_of_equality ts =
   2.104 +  let val (s1,s2) = string_of_pair ts
   2.105 +  in "equal(" ^ s1 ^ "," ^ s2 ^ ")" end;
   2.106  
   2.107  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   2.108 -fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
   2.109 -  | string_of_predicate (Predicate(name,typs,terms)) = 
   2.110 -      let val terms_as_strings = map string_of_term terms
   2.111 -	  val typs' = if !keep_types then map string_of_fol_type typs else []
   2.112 -      in  name ^ (paren_pack (terms_as_strings @ typs'))  end;
   2.113 +fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts
   2.114 +  | string_of_predicate (Predicate(name,typs,ts)) = 
   2.115 +      let val typs' = if !keep_types then map string_of_fol_type typs else []
   2.116 +      in  name ^ (paren_pack (map string_of_term ts @ typs'))  end;
   2.117  
   2.118  fun string_of_clausename (cls_id,ax_name) = 
   2.119      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   2.120 @@ -746,7 +732,7 @@
   2.121    "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   2.122  
   2.123  fun dfg_tfree_clause tfree_lit =
   2.124 -  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   2.125 +  "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   2.126  
   2.127  fun string_of_arClauseID (ArityClause {axiom_name,...}) =
   2.128      arclause_prefix ^ ascii_of axiom_name;
   2.129 @@ -807,22 +793,23 @@
   2.130  (**** Produce TPTP files ****)
   2.131  
   2.132  (*Attach sign in TPTP syntax: false means negate.*)
   2.133 -fun tptp_sign true s = "++" ^ s
   2.134 -  | tptp_sign false s = "--" ^ s
   2.135 +fun tptp_sign true s = s
   2.136 +  | tptp_sign false s = "~ " ^ s
   2.137  
   2.138 -fun tptp_literal (Literal(pol,pred)) = 
   2.139 -      (if pol then "++" else "--") ^ string_of_predicate pred;
   2.140 +fun tptp_of_equality pol ts =
   2.141 +  let val (s1,s2) = string_of_pair ts
   2.142 +      val eqop = if pol then " = " else " != "
   2.143 +  in  s1 ^ eqop ^ s2  end;
   2.144  
   2.145 -fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")"
   2.146 -  | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";
   2.147 +fun tptp_literal (Literal(pol,Predicate("equal",_,ts))) = tptp_of_equality pol ts
   2.148 +  | tptp_literal (Literal(pol,pred)) = tptp_sign pol (string_of_predicate pred);
   2.149 +
   2.150 +fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
   2.151 +  | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
   2.152   
   2.153  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   2.154 -    "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   2.155 -    knd ^ "," ^ lits ^ ").\n";
   2.156 -
   2.157 -fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = 
   2.158 -    "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   2.159 -    knd ^ ",[" ^ tfree_lit ^ "]).\n";
   2.160 +    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   2.161 +    name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
   2.162  
   2.163  fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
   2.164      let val lits = map tptp_literal literals
   2.165 @@ -838,15 +825,14 @@
   2.166  fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
   2.167      let val (lits,tfree_lits) = tptp_type_lits cls 
   2.168              (*"lits" includes the typing assumptions (TVars)*)
   2.169 -	val knd = name_of_kind kind
   2.170 -	val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) 
   2.171 +	val cls_str = gen_tptp_cls(clause_id, axiom_name, kind, lits) 
   2.172      in
   2.173  	(cls_str,tfree_lits) 
   2.174      end;
   2.175  
   2.176  fun tptp_tfree_clause tfree_lit =
   2.177 -    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n";
   2.178 -
   2.179 +    "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   2.180 +    
   2.181  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   2.182        tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")")
   2.183    | tptp_of_arLit (TVarLit(b,(c,str))) =
   2.184 @@ -857,17 +843,15 @@
   2.185        val knd = name_of_kind kind
   2.186        val lits = map tptp_of_arLit (conclLit :: premLits)
   2.187    in
   2.188 -    "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ bracket_pack lits ^ ").\n"
   2.189 +    "cnf(" ^ arcls_id ^ "," ^ knd ^ "," ^ tptp_pack lits ^ ").\n"
   2.190    end;
   2.191  
   2.192  fun tptp_classrelLits sub sup = 
   2.193 -    let val tvar = "(T)"
   2.194 -    in 
   2.195 -	"[--" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]"
   2.196 -    end;
   2.197 +  let val tvar = "(T)"
   2.198 +  in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   2.199  
   2.200  fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   2.201 -  "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
   2.202 +  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
   2.203  
   2.204  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
   2.205  fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =
     3.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Nov 23 23:05:28 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Nov 24 13:24:30 2006 +0100
     3.3 @@ -250,10 +250,6 @@
     3.4  
     3.5  
     3.6  type axiom_name = string;
     3.7 -datatype kind = Axiom | Conjecture;
     3.8 -
     3.9 -fun name_of_kind Axiom = "axiom"
    3.10 -  | name_of_kind Conjecture = "conjecture";
    3.11  
    3.12  type polarity = bool;
    3.13  type indexname = Term.indexname;
    3.14 @@ -280,20 +276,13 @@
    3.15  	 Clause of {clause_id: clause_id,
    3.16  		    axiom_name: axiom_name,
    3.17  		    th: thm,
    3.18 -		    kind: kind,
    3.19 +		    kind: ResClause.kind,
    3.20  		    literals: literal list,
    3.21  		    ctypes_sorts: (ctyp_var * csort) list, 
    3.22                      ctvar_type_literals: ctype_literal list, 
    3.23                      ctfree_type_literals: ctype_literal list};
    3.24  
    3.25  
    3.26 -fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
    3.27 -fun get_axiomName (Clause cls) = #axiom_name cls;
    3.28 -fun get_clause_id (Clause cls) = #clause_id cls;
    3.29 -
    3.30 -fun get_literals (c as Clause(cls)) = #literals cls;
    3.31 -
    3.32 -
    3.33  (*********************************************************************)
    3.34  (* convert a clause with type Term.term to a clause with type clause *)
    3.35  (*********************************************************************)
    3.36 @@ -404,47 +393,37 @@
    3.37  
    3.38  fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
    3.39    | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
    3.40 -    let val args' = literals_of_term1 args P
    3.41 -    in
    3.42 -	literals_of_term1 args' Q
    3.43 -    end
    3.44 +      literals_of_term1 (literals_of_term1 args P) Q
    3.45    | literals_of_term1 (lits,ts) P =
    3.46 -    let val ((pred,ts'),pol) = predicate_of (P,true)
    3.47 -	val lits' = Literal(pol,pred)::lits
    3.48 -    in
    3.49 -	(lits',ts union ts')
    3.50 -    end;
    3.51 -
    3.52 +      let val ((pred,ts'),pol) = predicate_of (P,true)
    3.53 +      in
    3.54 +	  (Literal(pol,pred)::lits, ts union ts')
    3.55 +      end;
    3.56  
    3.57  fun literals_of_term P = literals_of_term1 ([],[]) P;
    3.58  
    3.59  (* making axiom and conjecture clauses *)
    3.60  exception MAKE_CLAUSE
    3.61 -fun make_clause(clause_id,axiom_name,kind,thm,is_user) =
    3.62 -    let val term = prop_of thm
    3.63 -	val term' = comb_of term is_user
    3.64 -	val (lits,ctypes_sorts) = literals_of_term term'
    3.65 +fun make_clause(clause_id,axiom_name,kind,th,is_user) =
    3.66 +    let val (lits,ctypes_sorts) = literals_of_term (comb_of (prop_of th) is_user)
    3.67  	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
    3.68      in
    3.69  	if forall isFalse lits
    3.70  	then error "Problem too trivial for resolution (empty clause)"
    3.71  	else
    3.72 -	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
    3.73 +	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
    3.74  		    literals = lits, ctypes_sorts = ctypes_sorts, 
    3.75  		    ctvar_type_literals = ctvar_lits,
    3.76  		    ctfree_type_literals = ctfree_lits}
    3.77      end;
    3.78  
    3.79  
    3.80 -fun make_axiom_clause thm (ax_name,cls_id,is_user) = 
    3.81 -      make_clause(cls_id,ax_name,Axiom,thm,is_user);
    3.82 - 
    3.83  fun make_axiom_clauses [] user_lemmas = []
    3.84 -  | make_axiom_clauses ((thm,(name,id))::thms) user_lemmas =
    3.85 +  | make_axiom_clauses ((th,(name,id))::ths) user_lemmas =
    3.86      let val is_user = name mem user_lemmas
    3.87 -	val cls = SOME (make_axiom_clause thm (name,id,is_user)) 
    3.88 +	val cls = SOME (make_clause(id, name, ResClause.Axiom, th, is_user)) 
    3.89  	          handle MAKE_CLAUSE => NONE
    3.90 -	val clss = make_axiom_clauses thms user_lemmas
    3.91 +	val clss = make_axiom_clauses ths user_lemmas
    3.92      in
    3.93  	case cls of NONE => clss
    3.94  		  | SOME(cls') => if isTaut cls' then clss 
    3.95 @@ -454,7 +433,7 @@
    3.96  
    3.97  fun make_conjecture_clauses_aux _ [] = []
    3.98    | make_conjecture_clauses_aux n (th::ths) =
    3.99 -      make_clause(n,"conjecture",Conjecture,th,true) ::
   3.100 +      make_clause(n,"conjecture", ResClause.Conjecture, th, true) ::
   3.101        make_conjecture_clauses_aux (n+1) ths;
   3.102  
   3.103  val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   3.104 @@ -574,13 +553,7 @@
   3.105  
   3.106  (* tptp format *)
   3.107  
   3.108 -fun tptp_literal (Literal(pol,pred)) =
   3.109 -    let val pred_string = string_of_combterm true pred
   3.110 -	val pol_str = if pol then "++" else "--"
   3.111 -    in
   3.112 -	pol_str ^ pred_string
   3.113 -    end;
   3.114 -
   3.115 +fun tptp_literal (Literal(pol,pred)) = ResClause.tptp_sign pol (string_of_combterm true pred);
   3.116   
   3.117  fun tptp_type_lits (Clause cls) = 
   3.118      let val lits = map tptp_literal (#literals cls)
   3.119 @@ -595,13 +568,9 @@
   3.120      end; 
   3.121      
   3.122      
   3.123 -fun clause2tptp cls =
   3.124 +fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   3.125      let val (lits,ctfree_lits) = tptp_type_lits cls
   3.126 -	val cls_id = get_clause_id cls
   3.127 -	val ax_name = get_axiomName cls
   3.128 -	val knd = string_of_kind cls
   3.129 -	val lits_str = ResClause.bracket_pack lits
   3.130 -	val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str)
   3.131 +	val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   3.132      in
   3.133  	(cls_str,ctfree_lits)
   3.134      end;
   3.135 @@ -638,7 +607,7 @@
   3.136      let val (lits,tfree_lits) = dfg_clause_aux cls 
   3.137          val vars = dfg_vars cls
   3.138          val tvars = ResClause.get_tvar_strs ctypes_sorts
   3.139 -	val knd = name_of_kind kind
   3.140 +	val knd = ResClause.name_of_kind kind
   3.141  	val lits_str = commas lits
   3.142  	val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   3.143      in (cls_str, tfree_lits) end;