53 val tfree_prefix : string |
53 val tfree_prefix : string |
54 val tptp_arity_clause : arityClause -> string |
54 val tptp_arity_clause : arityClause -> string |
55 val tptp_classrelClause : classrelClause -> string |
55 val tptp_classrelClause : classrelClause -> string |
56 val tptp_of_typeLit : type_literal -> string |
56 val tptp_of_typeLit : type_literal -> string |
57 val tptp_tfree_clause : string -> string |
57 val tptp_tfree_clause : string -> string |
58 val tptp_write_file: thm list -> string -> (clause list * classrelClause list * arityClause list) -> unit |
58 val tptp_write_file: term list -> string -> ((Term.term * (string * int)) list * classrelClause list * arityClause list) -> unit |
59 val tvar_prefix : string |
59 val tvar_prefix : string |
60 val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list) |
60 val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list) |
61 val types_ord : fol_type list * fol_type list -> order |
61 val types_ord : fol_type list * fol_type list -> order |
62 val union_all : ''a list list -> ''a list |
62 val union_all : ''a list list -> ''a list |
63 val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit |
63 val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit |
617 NONE) |
617 NONE) |
618 else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)) |
618 else SOME (make_clause(cls_id, ax_name, Axiom, sort_lits lits, types_sorts)) |
619 end; |
619 end; |
620 |
620 |
621 |
621 |
|
622 fun make_axiom_clauses_terms [] = [] |
|
623 | make_axiom_clauses_terms ((tm,(name,id))::tms) = |
|
624 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 |
|
625 | NONE => make_axiom_clauses_terms tms; |
|
626 |
622 (**** Isabelle arities ****) |
627 (**** Isabelle arities ****) |
623 |
628 |
624 exception ARCLAUSE of string; |
629 exception ARCLAUSE of string; |
625 |
630 |
626 type class = string; |
631 type class = string; |
1022 |
1027 |
1023 fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = |
1028 fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = |
1024 "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" |
1029 "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" |
1025 |
1030 |
1026 (* write out a subgoal as tptp clauses to the file "xxxx_N"*) |
1031 (* write out a subgoal as tptp clauses to the file "xxxx_N"*) |
1027 fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = |
1032 fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) = |
1028 let |
1033 let |
1029 val clss = make_conjecture_clauses (map prop_of ths) |
1034 val clss = make_conjecture_clauses terms |
|
1035 val axclauses' = make_axiom_clauses_terms axclauses |
1030 val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) |
1036 val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) |
1031 val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) |
1037 val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) |
1032 val out = TextIO.openOut filename |
1038 val out = TextIO.openOut filename |
1033 in |
1039 in |
1034 List.app (curry TextIO.output out o #1 o clause2tptp) axclauses; |
1040 List.app (curry TextIO.output out o #1 o clause2tptp) axclauses'; |
1035 writeln_strs out tfree_clss; |
1041 writeln_strs out tfree_clss; |
1036 writeln_strs out tptp_clss; |
1042 writeln_strs out tptp_clss; |
1037 List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses; |
1043 List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses; |
1038 List.app (curry TextIO.output out o tptp_arity_clause) arity_clauses; |
1044 List.app (curry TextIO.output out o tptp_arity_clause) arity_clauses; |
1039 TextIO.closeOut out |
1045 TextIO.closeOut out |