tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
authormengj
Tue Mar 07 03:58:50 2006 +0100 (2006-03-07)
changeset 1919792404b5c20ad
parent 19196 62ee8c10d796
child 19198 e6f1ff40ba99
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Mar 07 03:56:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Mar 07 03:58:50 2006 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4    val tptp_classrelClause : classrelClause -> string
     1.5    val tptp_of_typeLit : type_literal -> string
     1.6    val tptp_tfree_clause : string -> string
     1.7 -  val tptp_write_file: thm list -> string -> (clause list * classrelClause list * arityClause list) -> unit
     1.8 +  val tptp_write_file: term list -> string -> ((Term.term * (string * int)) list * classrelClause list * arityClause list) -> unit
     1.9    val tvar_prefix : string
    1.10    val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list)
    1.11    val types_ord : fol_type list * fol_type list -> order
    1.12 @@ -619,6 +619,11 @@
    1.13      end;
    1.14  
    1.15  
    1.16 +fun make_axiom_clauses_terms [] = []
    1.17 +  | make_axiom_clauses_terms ((tm,(name,id))::tms) =
    1.18 +    case make_axiom_clause tm (name,id) of SOME cls => if isTaut cls then make_axiom_clauses_terms tms else cls :: make_axiom_clauses_terms tms
    1.19 +						    | NONE => make_axiom_clauses_terms tms;
    1.20 +    
    1.21  (**** Isabelle arities ****)
    1.22  
    1.23  exception ARCLAUSE of string;
    1.24 @@ -1024,14 +1029,15 @@
    1.25    "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
    1.26  
    1.27  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.28 -fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) =
    1.29 +fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) =
    1.30    let
    1.31 -    val clss = make_conjecture_clauses (map prop_of ths)
    1.32 +    val clss = make_conjecture_clauses terms
    1.33 +    val axclauses' = make_axiom_clauses_terms axclauses
    1.34      val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
    1.35      val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
    1.36      val out = TextIO.openOut filename
    1.37    in
    1.38 -    List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
    1.39 +    List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
    1.40      writeln_strs out tfree_clss;
    1.41      writeln_strs out tptp_clss;
    1.42      List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses;