# HG changeset patch # User paulson # Date 1138721826 -3600 # Node ID 7cfc21ee0370a3f4cc5bb7c2e04dd4111d7b87f1 # Parent f8e4322c9567bcb1760d01a5acebd10c82a7ba34 working SPASS support; much tidying diff -r f8e4322c9567 -r 7cfc21ee0370 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Jan 31 16:26:18 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Jan 31 16:37:06 2006 +0100 @@ -6,82 +6,61 @@ Typed equality is treated differently. *) -(* works for writeoutclasimp on typed *) signature RES_CLAUSE = sig + exception CLAUSE of string * term + type clause and arityClause and classrelClause + type fol_type + type typ_var + type type_literal + 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 check_var_pairs: ''a * ''b -> (''a * ''b) list -> int + val classrel_clauses_thy: theory -> classrelClause list + val clause_eq : clause * clause -> bool + val clause_prefix : string + val clause2tptp : clause -> string * string list + val const_prefix : string + val dfg_write_file: thm list -> string -> (clause list * classrelClause list * arityClause list) -> unit + 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 get_axiomName : clause -> string + val hash_clause : clause -> int + val init : theory -> unit + val isMeta : string -> bool + val isTaut : clause -> bool val keep_types : bool ref - val special_equal : bool ref - val tagged : bool ref - - exception ARCLAUSE of string - exception CLAUSE of string * term - type arityClause - type classrelClause - type clause - val init : theory -> unit + val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order val make_axiom_clause : Term.term -> string * int -> clause val make_conjecture_clauses : term list -> clause list - val get_axiomName : clause -> string - val isTaut : clause -> bool + val make_fixed_const : string -> string + val make_fixed_type_const : string -> string + val make_fixed_type_var : string -> string + val make_fixed_var : string -> string + val make_schematic_type_var : string * int -> string + val make_schematic_var : string * int -> string + val make_type_class : string -> string + val mk_fol_type: string * string * fol_type list -> fol_type + val mk_typ_var_sort : Term.typ -> typ_var * sort val num_of_clauses : clause -> int - - val arity_clause_thy: theory -> arityClause list - val classrel_clauses_thy: theory -> classrelClause list - + 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 val tptp_arity_clause : arityClause -> string val tptp_classrelClause : classrelClause -> string - val tptp_clause : clause -> string list - val clause2tptp : clause -> string * string list + val tptp_of_typeLit : type_literal -> string val tptp_tfree_clause : string -> string - val schematic_var_prefix : string - val fixed_var_prefix : string + val tptp_write_file: thm list -> string -> (clause list * classrelClause list * arityClause list) -> unit val tvar_prefix : string - val tfree_prefix : string - val clause_prefix : string - val arclause_prefix : string - val const_prefix : string - val tconst_prefix : string - val class_prefix : string - + val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list) + val types_ord : fol_type list * fol_type list -> order val union_all : ''a list list -> ''a list - val ascii_of : String.string -> String.string - val paren_pack : string list -> string - val bracket_pack : string list -> string - val make_schematic_var : String.string * int -> string - val make_fixed_var : String.string -> string - val make_schematic_type_var : string * int -> string - val make_fixed_type_var : string -> string - val make_fixed_const : String.string -> string - val make_fixed_type_const : String.string -> string - val make_type_class : String.string -> string - val isMeta : String.string -> bool - - type typ_var - val mk_typ_var_sort : Term.typ -> typ_var * sort - type type_literal - val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list - val gen_tptp_cls : int * string * string * string -> string - val gen_tptp_type_cls : int * string * string * string * int -> string - val tptp_of_typeLit : type_literal -> string - - (*for hashing*) - val clause_eq : clause * clause -> bool - val hash_clause : clause -> int - - val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order - type fol_type - val types_ord : fol_type list * fol_type list -> order - val string_of_fol_type : fol_type -> string - val mk_fol_type: string * string * fol_type list -> fol_type - val types_eq: fol_type list * fol_type list -> - (string*string) list * (string*string) list -> - bool * ((string*string) list * (string*string) list) - val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int - - val dfg_write_file: thm list -> string -> - (clause list * classrelClause list * arityClause list) -> unit - val tptp_write_file: thm list -> string -> - (clause list * classrelClause list * arityClause list) -> unit val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit end; @@ -361,8 +340,7 @@ val (funName,(contys,ts1)) = fun_name_type f args val (args',ts2) = terms_of args in - (Fun(funName,contys,args'), - (union_all (ts1::ts2))) + (Fun(funName,contys,args'), union_all (ts1::ts2)) end and terms_of ts = ListPair.unzip (map term_of ts) @@ -671,7 +649,8 @@ type class = string; type tcons = string; -datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string); +datatype arLit = TConsLit of bool * (class * tcons * string list) + | TVarLit of bool * (class * string); datatype arityClause = ArityClause of {clause_id: clause_id, @@ -688,8 +667,9 @@ | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*) | pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); -fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); -fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); +fun make_TVarLit (b, (cls,str)) = TVarLit(b, (cls,str)); +fun make_TConsLit (b, (cls,tcons,tvars)) = + TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars)); (*Arity of type constructor tcon :: (arg1,...,argN)res*) fun make_axiom_arity_clause (tcons, n, (res,args)) = @@ -717,25 +697,33 @@ (**** Isabelle class relations ****) datatype classrelClause = - ClassrelClause of {clause_id: clause_id, + ClassrelClause of {axiom_name: axiom_name, subclass: class, superclass: class}; fun make_axiom_classrelClause n subclass superclass = - ClassrelClause {clause_id = n, - subclass = subclass, superclass = superclass}; + ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^ + "_" ^ Int.toString n, + subclass = make_type_class subclass, + superclass = make_type_class superclass}; fun classrelClauses_of_aux n sub [] = [] | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*) classrelClauses_of_aux n sub sups | classrelClauses_of_aux n sub (sup::sups) = - ClassrelClause {clause_id = n, subclass = sub, superclass = sup} - :: classrelClauses_of_aux (n+1) sub sups; + make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups; fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups; +val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; -(***** Isabelle arities *****) +fun classrel_clauses_classrel (C: Sorts.classes) = + map classrelClauses_of (Graph.dest C); + +val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; + + +(** Isabelle arities **) fun arity_clause _ (tcons, []) = [] | arity_clause n (tcons, ("HOL.type",_)::ars) = (*Should be ignored*) @@ -753,17 +741,79 @@ in multi_arity_clause (Symtab.dest arities) end; -(* Isabelle classes *) +(**** Find occurrences of predicates in clauses ****) + +(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong + function (it flags repeated declarations of a function, even with the same arity)*) + +fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; + +fun add_predicate_preds (Predicate(pname,tys,tms), preds) = + if pname = "equal" then preds (*equality is built-in and requires no declaration*) + else Symtab.update (pname, length tys + length tms) preds + +fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds) + +fun add_type_sort_preds ((FOLTVar indx,s), preds) = + update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s))) + | add_type_sort_preds ((FOLTFree x,s), preds) = + update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s))); -type classrelClauses = classrelClause list Symtab.table; +fun add_clause_preds (Clause {literals, types_sorts, ...}, preds) = + foldl add_literal_preds (foldl add_type_sort_preds preds types_sorts) literals + handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities") + +fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) = + Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); -val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; +fun add_arityClause_preds (ArityClause {conclLit,...}, preds) = + let val TConsLit(_, (tclass, _, _)) = conclLit + in Symtab.update (tclass,1) preds end; + +fun preds_of_clauses clauses clsrel_clauses arity_clauses = + Symtab.dest + (foldl add_classrelClause_preds + (foldl add_arityClause_preds + (foldl add_clause_preds Symtab.empty clauses) + arity_clauses) + clsrel_clauses) -fun classrel_clauses_classrel (C: Sorts.classes) = - map classrelClauses_of (Graph.dest C); +(*** Find occurrences of functions in clauses ***) + +fun add_foltype_funcs (AtomV _, funcs) = funcs + | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs + | add_foltype_funcs (Comp(a,tys), funcs) = + foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; + +fun add_folterm_funcs (UVar _, funcs) = funcs + | add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,0) funcs + (*A constant is a special case: it has no type argument even if overloaded*) + | add_folterm_funcs (Fun(a,tys,tms), funcs) = + foldl add_foltype_funcs + (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) + tms) + tys -val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; +fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = + foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys; + +fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs) + +fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) = + let val TConsLit(_, (_, tcons, tvars)) = conclLit + in Symtab.update (tcons, length tvars) funcs end; +fun add_clause_funcs (Clause {literals, ...}, funcs) = + foldl add_literal_funcs funcs literals + handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") + +fun funcs_of_clauses clauses arity_clauses = + Symtab.dest (foldl add_arityClause_funcs + (foldl add_clause_funcs Symtab.empty clauses) + arity_clauses) + + +(**** String-oriented operations ****) fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; @@ -803,10 +853,7 @@ fun writeln_strs os = List.app (fn s => TextIO.output (os,s)); - -(********************************) -(* Code for producing DFG files *) -(********************************) +(**** Producing DFG files ****) (*Attach sign in DFG syntax: false means negate.*) fun dfg_sign true s = s @@ -817,63 +864,40 @@ fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))" | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")"; -(*Make the string of universal quantifiers for a clause*) -fun forall_open ([],[]) = "" - | forall_open (vars,tvars) = "forall([" ^ (commas (tvars@vars))^ "],\n" +(*Enclose the clause body by quantifiers, if necessary*) +fun dfg_forall [] body = body + | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")" -fun forall_close ([],[]) = "" - | forall_close (vars,tvars) = ")" - -fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = - "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ - "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ +fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) = + "clause( %(" ^ knd ^ ")\n" ^ + dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ string_of_clausename (cls_id,ax_name) ^ ").\n\n"; -(*FIXME: UNUSED*) -fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = - "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ - "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ - string_of_type_clsname (cls_id,ax_name,idx) ^ ").\n\n"; - -fun dfg_clause_aux (Clause cls) = - let val lits = map dfg_literal (#literals cls) +fun dfg_clause_aux (Clause{literals, tvar_type_literals, tfree_type_literals, ...}) = + let val lits = map dfg_literal literals val tvar_lits_strs = - if !keep_types then map dfg_of_typeLit (#tvar_type_literals cls) + if !keep_types then map dfg_of_typeLit tvar_type_literals else [] val tfree_lits = - if !keep_types then map dfg_of_typeLit (#tfree_type_literals cls) + if !keep_types then map dfg_of_typeLit tfree_type_literals else [] in (tvar_lits_strs @ lits, tfree_lits) end; - fun dfg_folterms (Literal(pol,pred,tag)) = let val Predicate (_, _, folterms) = pred in folterms end fun get_uvars (UVar(a,typ)) = [a] -| get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist) - -fun is_uvar (UVar _) = true -| is_uvar (Fun _) = false; + | get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist) -fun uvar_name (UVar(a,_)) = a -| uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT)); - -fun dfg_vars (Clause cls) = - let val lits = #literals cls - val folterms = List.concat (map dfg_folterms lits) +fun dfg_vars (Clause {literals,...}) = + let val folterms = List.concat (map dfg_folterms literals) in union_all(map get_uvars folterms) end -fun string_of_predname (Predicate("equal",_,terms)) = "EQUALITY" - | string_of_predname (Predicate(name,_,terms)) = name - -fun dfg_pred (Literal(pol,pred,tag)) ax_name = - (string_of_predname pred) ^ " " ^ ax_name - fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,types_sorts,...}) = let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) @@ -881,7 +905,7 @@ val tvars = get_tvar_strs types_sorts val knd = name_of_kind kind val lits_str = commas lits - val cls_str = gen_dfg_cls(clause_id,axiom_name,knd,lits_str,tvars,vars) + val cls_str = gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) in (cls_str, tfree_lits) end; fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")" @@ -895,142 +919,69 @@ fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; -fun write_axioms (out, strs) = - (TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); - writeln_strs out strs; - TextIO.output (out, "end_of_list.\n\n")); - -fun write_conjectures (out, strs) = - (TextIO.output (out, "list_of_clauses(conjectures,cnf).\n"); - writeln_strs out strs; - TextIO.output (out, "end_of_list.\n\n")); - fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; fun string_of_descrip name = - "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" + "list_of_descriptions.\nname({*" ^ name ^ + "*}).\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" - -(*** Find all occurrences of predicates in types, terms, literals... ***) - -(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong - function (it flags repeated declarations of a function, even with the same arity)*) - -fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; - -fun add_predicate_preds (Predicate(pname,tys,tms), preds) = - if pname = "equal" then preds (*equality is built-in and requires no declaration*) - else Symtab.update (pname, length tys + length tms) preds - -fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds) - -fun add_type_sort_preds ((FOLTVar indx,s), preds) = - update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s))) - | add_type_sort_preds ((FOLTFree x,s), preds) = - update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s))); - -fun add_clause_preds (Clause {literals, types_sorts, ...}, preds) = - foldl add_literal_preds (foldl add_type_sort_preds preds types_sorts) literals - handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities") - -val preds_of_clauses = Symtab.dest o (foldl add_clause_preds Symtab.empty) - - -(*** Find all occurrences of functions in types, terms, literals... ***) - -fun add_foltype_funcs (AtomV _, funcs) = funcs - | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs - | add_foltype_funcs (Comp(a,tys), funcs) = - foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; - -fun add_folterm_funcs (UVar _, funcs) = funcs - | add_folterm_funcs (Fun(a,tys,[]), funcs) = Symtab.update (a,0) funcs - (*A constant is a special case: it has no type argument even if overloaded*) - | add_folterm_funcs (Fun(a,tys,tms), funcs) = - foldl add_foltype_funcs - (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) - tms) - tys - -fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = - foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys; - -fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs) - -fun add_clause_funcs (Clause {literals, ...}, funcs) = - foldl add_literal_funcs funcs literals - handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities") - -val funcs_of_clauses = Symtab.dest o (foldl add_clause_funcs Symtab.empty) - fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) = arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id; -fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); - fun dfg_of_arLit (TConsLit(pol,(c,t,args))) = dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")") | dfg_of_arLit (TVarLit(pol,(c,str))) = dfg_sign pol (c ^ "(" ^ str ^ ")") -fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls); - -fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls); - fun dfg_classrelLits sub sup = let val tvar = "(T)" in "not(" ^ sub ^ tvar ^ "), " ^ sup ^ tvar end; -fun dfg_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = - let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ - Int.toString clause_id - val lits = dfg_classrelLits (make_type_class subclass) (make_type_class superclass) +fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = + "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^ + axiom_name ^ ").\n\n"; + +fun dfg_arity_clause (arcls as ArityClause{kind,conclLit,premLits,...}) = + let val arcls_id = string_of_arClauseID arcls + val knd = name_of_kind kind + val TConsLit(_, (_,_,tvars)) = conclLit + val lits = map dfg_of_arLit (conclLit :: premLits) in - "clause(\nor( " ^ lits ^ ")),\n" ^ - relcls_id ^ ").\n\n" - end; - -fun dfg_arity_clause arcls = - let val arcls_id = string_of_arClauseID arcls - val concl_lit = dfg_of_conclLit arcls - val prems_lits = dfg_of_premLits arcls - val knd = string_of_arKind arcls - val all_lits = concl_lit :: prems_lits - in - "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ bracket_pack all_lits ^ ")),\n" ^ - arcls_id ^ ").\n\n" + "clause( %(" ^ knd ^ ")\n" ^ + dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^ + arcls_id ^ ").\n\n" end; (* write out a subgoal in DFG format to the file "xxxx_N"*) fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = let val conjectures = make_conjecture_clauses (map prop_of ths) - val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) - val classrel_cls = map dfg_classrelClause classrel_clauses - val arity_cls = map dfg_arity_clause arity_clauses + val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures) val clss = conjectures @ axclauses - val funcs = (funcs_of_clauses clss) - and preds = (preds_of_clauses clss) + val funcs = funcs_of_clauses clss arity_clauses + and preds = preds_of_clauses clss classrel_clauses arity_clauses val out = TextIO.openOut filename and probname = Path.pack (Path.base (Path.unpack filename)) - val axstrs_tfrees = (map clause2dfg axclauses) - val (axstrs, _) = ListPair.unzip axstrs_tfrees + val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses) val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) - val funcstr = string_of_funcs funcs - val predstr = string_of_preds preds in - TextIO.output (out, string_of_start probname); - TextIO.output (out, string_of_descrip probname); - TextIO.output (out, string_of_symbols funcstr predstr); - write_axioms (out, axstrs); - write_conjectures (out, tfree_clss@dfg_clss); - TextIO.output (out, "end_problem.\n"); - TextIO.closeOut out + TextIO.output (out, string_of_start probname); + TextIO.output (out, string_of_descrip probname); + TextIO.output (out, string_of_symbols (string_of_funcs funcs) (string_of_preds preds)); + TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); + writeln_strs out axstrs; + List.app (curry TextIO.output out o dfg_classrelClause) classrel_clauses; + List.app (curry TextIO.output out o dfg_arity_clause) arity_clauses; + TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); + writeln_strs out tfree_clss; + writeln_strs out dfg_clss; + TextIO.output (out, "end_of_list.\n\nend_problem.\n"); + TextIO.closeOut out end; @@ -1038,7 +989,12 @@ (* code to produce TPTP files *) (********************************) -fun tptp_literal (Literal(pol,pred,tag)) = + +(*Attach sign in TPTP syntax: false means negate.*) +fun tptp_sign true s = "++" ^ s + | tptp_sign false s = "--" ^ s + +fun tptp_literal (Literal(pol,pred,tag)) = (*FIXME REMOVE TAGGING*) let val pred_string = string_of_predicate pred val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---") @@ -1107,32 +1063,17 @@ fun tptp_of_arLit (TConsLit(b,(c,t,args))) = - let val pol = if b then "++" else "--" - val arg_strs = paren_pack args - in - pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" - end + tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")") | tptp_of_arLit (TVarLit(b,(c,str))) = - let val pol = if b then "++" else "--" - in - pol ^ c ^ "(" ^ str ^ ")" - end; + tptp_sign b (c ^ "(" ^ str ^ ")") - -fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls); - -fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls); - -fun tptp_arity_clause arcls = - let val arcls_id = string_of_arClauseID arcls - val concl_lit = tptp_of_conclLit arcls - val prems_lits = tptp_of_premLits arcls - val knd = string_of_arKind arcls - val all_lits = concl_lit :: prems_lits - in - "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ - (bracket_pack all_lits) ^ ").\n" - end; +fun tptp_arity_clause (arcls as ArityClause{kind,conclLit,premLits,...}) = + let val arcls_id = string_of_arClauseID arcls + val knd = name_of_kind kind + val lits = map tptp_of_arLit (conclLit :: premLits) + in + "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ bracket_pack lits ^ ").\n" + end; fun tptp_classrelLits sub sup = let val tvar = "(T)" @@ -1140,13 +1081,8 @@ "[--" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" end; -fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = - let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ - Int.toString clause_id - val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass) - in - "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ").\n" - end; +fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) = + "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" (* write out a subgoal as tptp clauses to the file "xxxx_N"*) fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = @@ -1154,17 +1090,14 @@ val clss = make_conjecture_clauses (map prop_of ths) val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) - val classrel_cls = map tptp_classrelClause classrel_clauses - val arity_cls = map tptp_arity_clause arity_clauses val out = TextIO.openOut filename in List.app (writeln_strs out o tptp_clause) axclauses; writeln_strs out tfree_clss; writeln_strs out tptp_clss; - writeln_strs out classrel_cls; - writeln_strs out arity_cls; + List.app (curry TextIO.output out o tptp_classrelClause) classrel_clauses; + List.app (curry TextIO.output out o tptp_arity_clause) arity_clauses; TextIO.closeOut out end; - end;