# HG changeset patch # User paulson # Date 1138382973 -3600 # Node ID ca02a20779550755e4feb49a80aa1cb764197c0c # Parent 8559cc115673049a10cf363a0e36b59e0ae28851 tidying up SPASS output diff -r 8559cc115673 -r ca02a2077955 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Jan 27 18:29:11 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Fri Jan 27 18:29:33 2006 +0100 @@ -74,8 +74,8 @@ fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = let val clss = ResClause.make_conjecture_clauses (map prop_of ths) (*FIXME: classrel_clauses and arity_clauses*) - val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n) - axclauses [] [] [] + val probN = ResClause.clauses2dfg (!problem_name ^ "_" ^ Int.toString n) + axclauses clss val out = TextIO.openOut(pf n) in writeln_strs out [probN]; TextIO.closeOut out @@ -106,14 +106,14 @@ val spass = helper_path "SPASS_HOME" "SPASS" in ([("spass", spass, infopts ^ baseopts, probfile)] @ - (make_atp_list xs (n+1))) + make_atp_list xs (n+1)) end else if !prover = "vampire" then let val vampire = helper_path "VAMPIRE_HOME" "vampire" in ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @ - (make_atp_list xs (n+1))) (*BEWARE! spaces in options!*) + make_atp_list xs (n+1)) (*BEWARE! spaces in options!*) end else if !prover = "E" then @@ -122,7 +122,7 @@ ([("E", Eprover, "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time, probfile)] @ - (make_atp_list xs (n+1))) + make_atp_list xs (n+1)) end else error ("Invalid prover name: " ^ !prover) end diff -r 8559cc115673 -r ca02a2077955 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Fri Jan 27 18:29:11 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Fri Jan 27 18:29:33 2006 +0100 @@ -26,8 +26,7 @@ val num_of_clauses : clause -> int val clause2dfg : clause -> string * string list - val clauses2dfg : clause list -> string -> clause list -> clause list -> - (string * int) list -> (string * int) list -> string + val clauses2dfg : string -> clause list -> clause list -> string val tfree_dfg_clause : string -> string val arity_clause_thy: theory -> arityClause list @@ -103,13 +102,10 @@ val const_prefix = "c_"; val tconst_prefix = "tc_"; - val class_prefix = "class_"; - fun union_all xss = foldl (op union) [] xss; - (*Provide readable names for the more common symbolic functions*) val const_trans_table = Symtab.make [("op =", "equal"), @@ -197,8 +193,7 @@ fun make_type_class clas = class_prefix ^ ascii_of clas; - -(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) +(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****) val keep_types = ref true; @@ -213,9 +208,6 @@ type polarity = bool; -type indexname = Term.indexname; - - (* "tag" is used for vampire specific syntax *) type tag = bool; @@ -225,12 +217,10 @@ val tagged = ref false; type pred_name = string; -type sort = Term.sort; - - datatype typ_var = FOLTVar of indexname | FOLTFree of string; +(*FIXME: give the constructors more sensible names*) datatype fol_type = AtomV of string | AtomF of string | Comp of string * fol_type list; @@ -248,8 +238,8 @@ | mk_fol_type ("Comp",con,args) = Comp(con,args) - -datatype type_literal = LTVar of string | LTFree of string; +(*First string is the type class; the second is a TVar or TFfree*) +datatype type_literal = LTVar of string * string | LTFree of string * string; datatype folTerm = UVar of string * fol_type | Fun of string * fol_type list * folTerm list; @@ -270,18 +260,12 @@ literals: literal list, types_sorts: (typ_var * sort) list, tvar_type_literals: type_literal list, - tfree_type_literals: type_literal list , - tvars: string list, - predicates: (string*int) list, - functions: (string*int) list}; + tfree_type_literals: type_literal list, + predicates: (string*int) list}; exception CLAUSE of string * term; -fun get_literals (c as Clause(cls)) = #literals cls; - -fun components_of_literal (Literal (pol,pred,tag)) = ((pol,pred),tag); - fun predicate_name (Predicate(predname,_,_)) = predname; @@ -301,7 +285,7 @@ fun make_clause (clause_id,axiom_name,kind,literals, types_sorts,tvar_type_literals, - tfree_type_literals,tvars, predicates, functions) = + tfree_type_literals,predicates) = if forall isFalse literals then error "Problem too trivial for resolution (empty clause)" else @@ -309,8 +293,7 @@ literals = literals, types_sorts = types_sorts, tvar_type_literals = tvar_type_literals, tfree_type_literals = tfree_type_literals, - tvars = tvars, predicates = predicates, - functions = functions}; + predicates = predicates}; (** Some Clause destructor functions **) @@ -321,8 +304,6 @@ fun get_clause_id (Clause cls) = #clause_id cls; -fun funcs_of_cls (Clause cls) = #functions cls; - fun preds_of_cls (Clause cls) = #predicates cls; @@ -339,23 +320,14 @@ (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and TVars it contains.*) fun type_of (Type (a, Ts)) = - let val (folTyps, (ts, funcs)) = types_of Ts + let val (folTyps, ts) = types_of Ts val t = make_fixed_type_const a - in - (Comp(t,folTyps), (ts, (t, length Ts)::funcs)) - end - | type_of (TFree (a,s)) = - let val t = make_fixed_type_var a - in (AtomF(t), ([((FOLTFree a),s)], [(t,0)])) end - | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), ([((FOLTVar v),s)], [])) + in (Comp(t,folTyps), ts) end + | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) + | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)]) and types_of Ts = - let val foltyps_ts = map type_of Ts - val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts - val (ts, funcslist) = ListPair.unzip ts_funcs - in - (folTyps, (union_all ts, union_all funcslist)) - end; - + let val (folTyps,ts) = ListPair.unzip (map type_of Ts) + in (folTyps, union_all ts) end; fun const_types_of (c,T) = types_of (!const_typargs (c,T)); @@ -364,12 +336,10 @@ universal vars, although it is represented as "Free(...)" by Isabelle *) val isMeta = String.isPrefix "METAHYP1_" -fun pred_name_type (Const(c,T)) = - let val (contys,(folTyps,funcs)) = const_types_of (c,T) - in (make_fixed_const c, (contys,folTyps), funcs) end +fun pred_name_type (Const(c,T)) = (make_fixed_const c, const_types_of (c,T)) | pred_name_type (Free(x,T)) = if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) - else (make_fixed_var x, ([],[]), []) + else (make_fixed_var x, ([],[])) | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v) | pred_name_type t = raise CLAUSE("Predicate input unexpected", t); @@ -381,87 +351,51 @@ let val (folT,_) = type_of T; in folT end; -fun fun_name_type (Const("op =",T)) args = (*FIXME: Is this special treatment of = needed??*) - let val t = make_fixed_const "op =" - in (t, ([eq_arg_type T], []), [(t,2)]) end - | fun_name_type (Const(c,T)) args = - let val t = make_fixed_const c - val (contys, (folTyps,funcs)) = const_types_of (c,T) - val arity = num_typargs(c,T) + length args - in - (t, (contys,folTyps), ((t,arity)::funcs)) - end - | fun_name_type (Free(x,T)) args = - let val t = make_fixed_var x - in (t, ([],[]), [(t, length args)]) end +fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T)) + | fun_name_type (Free(x,T)) args = + if isMeta x then raise CLAUSE("Function Not First Order", Free(x,T)) + else (make_fixed_var x, ([],[])) | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f); - fun term_of (Var(ind_nm,T)) = - let val (folType,(ts,funcs)) = type_of T - in - (UVar(make_schematic_var ind_nm, folType), (ts, funcs)) - end + let val (folType,ts) = type_of T + in (UVar(make_schematic_var ind_nm, folType), ts) end | term_of (Free(x,T)) = - let val (folType, (ts,funcs)) = type_of T + let val (folType, ts) = type_of T in - if isMeta x then (UVar(make_schematic_var(x,0),folType), - (ts, ((make_schematic_var(x,0)),0)::funcs)) - else - (Fun(make_fixed_var x, [folType], []), - (ts, ((make_fixed_var x),0)::funcs)) + if isMeta x then (UVar(make_schematic_var(x,0),folType), ts) + else (Fun(make_fixed_var x, [folType], []), ts) end - | term_of (Const(c,T)) = (* impossible to be equality *) - let val (contys, (folTyps,funcs)) = const_types_of (c,T) - in - (Fun(make_fixed_const c, contys, []), - (folTyps, ((make_fixed_const c),0)::funcs)) - end | term_of app = let val (f,args) = strip_comb app - val _ = case f of Const(_,_) => () - | Free(s,_) => - if isMeta s - then raise CLAUSE("Function Not First Order 2", f) - else () - | _ => raise CLAUSE("Function Not First Order 3", f); - val (funName,(contys,ts1),funcs) = fun_name_type f args - val (args',(ts2,funcs')) = terms_of args + val (funName,(contys,ts1)) = fun_name_type f args + val (args',ts2) = terms_of args in (Fun(funName,contys,args'), - (union_all (ts1::ts2), - union_all(funcs::funcs'))) + (union_all (ts1::ts2))) end -and terms_of ts = - let val (args, ts_funcs) = ListPair.unzip (map term_of ts) - in - (args, ListPair.unzip ts_funcs) - end +and terms_of ts = ListPair.unzip (map term_of ts) fun pred_of (Const("op =", typ), args) = let val arg_typ = eq_arg_type typ - val (args',(ts,funcs)) = terms_of args + val (args',ts) = terms_of args val equal_name = make_fixed_const "op =" in (Predicate(equal_name,[arg_typ],args'), union_all ts, - [((make_fixed_var equal_name), 2)], - union_all funcs) + [((make_fixed_var equal_name), 2)]) end | pred_of (pred,args) = - let val (predName,(predType,ts1), pfuncs) = pred_name_type pred - val (args',(ts2,ffuncs)) = terms_of args + let val (predName, (predType,ts1)) = pred_name_type pred + val (args',ts2) = terms_of args val ts3 = union_all (ts1::ts2) - val ffuncs' = union_all ffuncs - val newfuncs = pfuncs union ffuncs' val arity = case pred of Const (c,T) => num_typargs(c,T) + length args | _ => length args in - (Predicate(predName,predType,args'), ts3, - [(predName, arity)], newfuncs) + (Predicate(predName,predType,args'), ts3, [(predName, arity)]) end; @@ -474,20 +408,20 @@ (pred_of (strip_comb term), polarity, tag); fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P - | literals_of_term1 (args as (lits, ts, preds, funcs)) (Const("op |",_) $ P $ Q) = - let val (lits', ts', preds', funcs') = literals_of_term1 args P + | literals_of_term1 (args as (lits, ts, preds)) (Const("op |",_) $ P $ Q) = + let val (lits', ts', preds') = literals_of_term1 args P in - literals_of_term1 (lits', ts', preds' union preds, funcs' union funcs) Q + literals_of_term1 (lits', ts', preds' union preds) Q end - | literals_of_term1 (lits, ts, preds, funcs) P = - let val ((pred, ts', preds', funcs'), pol, tag) = predicate_of (P,true,false) + | literals_of_term1 (lits, ts, preds) P = + let val ((pred, ts', preds'), pol, tag) = predicate_of (P,true,false) val lits' = Literal(pol,pred,tag) :: lits in - (lits', ts union ts', preds' union preds, funcs' union funcs) + (lits', ts union ts', preds' union preds) end; -val literals_of_term = literals_of_term1 ([],[],[],[]); +val literals_of_term = literals_of_term1 ([],[],[]); @@ -649,12 +583,8 @@ (*Equality of two clauses up to variable renaming*) -fun clause_eq (cls1,cls2) = - let val lits1 = get_literals cls1 - val lits2 = get_literals cls2 - in - length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[])) - end; +fun clause_eq (Clause{literals=lits1,...}, Clause{literals=lits2,...}) = + length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[])); (*** Hash function for clauses ***) @@ -671,32 +601,24 @@ fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0) | hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0)); -fun hash_clause clause = Word.toIntX (xor_words (map hash1_literal (get_literals clause))); +fun hash_clause (Clause{literals,...}) = + Word.toIntX (xor_words (map hash1_literal literals)); -(* FIX: not sure what to do with these funcs *) - -(*Make literals for sorted type variables*) +(*Make literals for sorted type variables. FIXME: can it use map?*) fun sorts_on_typs (_, []) = ([]) | sorts_on_typs (v, "HOL.type" :: s) = sorts_on_typs (v,s) (*IGNORE sort "type"*) - | sorts_on_typs ((FOLTVar indx), (s::ss)) = - LTVar((make_type_class s) ^ - "(" ^ (make_schematic_type_var indx) ^ ")") :: - (sorts_on_typs ((FOLTVar indx), ss)) - | sorts_on_typs ((FOLTFree x), (s::ss)) = - LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var x) ^ ")") :: - (sorts_on_typs ((FOLTFree x), ss)); + | sorts_on_typs ((FOLTVar indx), s::ss) = + LTVar(make_type_class s, make_schematic_type_var indx) :: + sorts_on_typs ((FOLTVar indx), ss) + | sorts_on_typs ((FOLTFree x), s::ss) = + LTFree(make_type_class s, make_fixed_type_var x) :: + sorts_on_typs ((FOLTFree x), ss); -(*UGLY: seems to be parsing the "show sorts" output, removing anything that - starts with a left parenthesis.*) -fun remove_type str = hd (String.fields (fn c => c = #"(") str); - -fun pred_of_sort (LTVar x) = ((remove_type x),1) -| pred_of_sort (LTFree x) = ((remove_type x),1) - - +fun pred_of_sort (LTVar (s,ty)) = (s,1) +| pred_of_sort (LTFree (s,ty)) = (s,1) (*Given a list of sorted type variables, return two separate lists. The first is for TVars, the second for TFrees.*) @@ -744,17 +666,13 @@ end | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss) -(* FIX add preds and funcs to add typs aux here *) - fun make_axiom_clause_thm thm (ax_name,cls_id) = - let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm) + let val (lits,types_sorts, preds) = literals_of_term (prop_of thm) val lits' = sort_lits lits val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds - val tvars = get_tvar_strs types_sorts in make_clause(cls_id,ax_name,Axiom, - lits',types_sorts,tvar_lits,tfree_lits, - tvars, preds, funcs) + lits',types_sorts,tvar_lits,tfree_lits,preds) end; @@ -762,13 +680,11 @@ fun make_conjecture_clause n t = let val _ = check_is_fol_term t handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t) - val (lits,types_sorts, preds, funcs) = literals_of_term t + val (lits,types_sorts, preds) = literals_of_term t val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds - val tvars = get_tvar_strs types_sorts in make_clause(n,"conjecture",Conjecture, - lits,types_sorts,tvar_lits,tfree_lits, - tvars, preds, funcs) + lits,types_sorts,tvar_lits,tfree_lits,preds) end; fun make_conjecture_clauses_aux _ [] = [] @@ -782,14 +698,12 @@ fun make_axiom_clause term (ax_name,cls_id) = let val _ = check_is_fol_term term handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) - val (lits,types_sorts, preds,funcs) = literals_of_term term + val (lits,types_sorts, preds) = literals_of_term term val lits' = sort_lits lits val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds - val tvars = get_tvar_strs types_sorts in make_clause(cls_id,ax_name,Axiom, - lits',types_sorts,tvar_lits,tfree_lits, - tvars, preds,funcs) + lits',types_sorts,tvar_lits,tfree_lits,preds) end; @@ -799,11 +713,9 @@ exception ARCLAUSE of string; - type class = string; type tcons = string; - datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string); datatype arityClause = @@ -814,8 +726,8 @@ premLits: arLit list}; -fun get_TVars 0 = [] - | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1); +fun gen_TVars 0 = [] + | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); fun pack_sort(_,[]) = [] | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*) @@ -827,7 +739,7 @@ (*Arity of type constructor tcon :: (arg1,...,argN)res*) fun make_axiom_arity_clause (tcons, n, (res,args)) = let val nargs = length args - val tvars = get_TVars nargs + val tvars = gen_TVars nargs val tvars_srts = ListPair.zip (tvars,args) val tvars_srts' = union_all(map pack_sort tvars_srts) val false_tvars_srts' = map (pair false) tvars_srts' @@ -891,13 +803,13 @@ type classrelClauses = classrelClause list Symtab.table; val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; -fun classrel_clauses_classrel (C: Sorts.classes) = map classrelClauses_of (Graph.dest C); + +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; - -(****!!!! Changed for typed equality !!!!****) - 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 @@ -943,13 +855,8 @@ if pol then pred_string else "not(" ^pred_string ^ ")" end; - -(* FIX: what does this mean? *) -(*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")" - | dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*) - -fun dfg_of_typeLit (LTVar x) = x - | dfg_of_typeLit (LTFree x) = x ; +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 ([],[]) = "" @@ -985,11 +892,9 @@ let val Predicate (predname, _, 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; @@ -1003,94 +908,47 @@ union_all(map get_uvars folterms) end - -fun dfg_tvars (Clause cls) =(#tvars cls) - - - -(* make this return funcs and preds too? *) fun string_of_predname (Predicate("equal",_,terms)) = "EQUALITY" | string_of_predname (Predicate(name,_,terms)) = name - - - -fun concat_with sep [] = "" - | concat_with sep [x] = "(" ^ x ^ ")" - | concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs); fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred) ^ " " ^ ax_name -fun dfg_clause cls = +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)*) + (*"lits" includes the typing assumptions (TVars)*) val vars = dfg_vars cls - val tvars = dfg_tvars cls - val knd = string_of_kind cls + val tvars = get_tvar_strs types_sorts + val preds = preds_of_cls cls + val knd = name_of_kind kind val lits_str = commas lits - val cls_id = get_clause_id cls - val axname = get_axiomName cls - val cls_str = gen_dfg_cls(cls_id,axname,knd,lits_str,tvars, vars) - fun typ_clss k [] = [] - | typ_clss k (tfree :: tfrees) = - (gen_dfg_type_cls(cls_id,axname,knd,tfree,k, tvars,vars)) :: - (typ_clss (k+1) tfrees) - in - cls_str :: (typ_clss 0 tfree_lits) - end; + 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) +fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")" fun string_of_preds preds = - "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n"; + "predicates[" ^ commas(map string_of_arity preds) ^ "].\n"; fun string_of_funcs funcs = - "functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ; - + "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ; fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; - fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n"; - fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n"; -fun string_of_descrip () = - "list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n" - - -fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n"; - - -fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------"; - +fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; -fun clause2dfg cls = - let val (lits,tfree_lits) = dfg_clause_aux cls - (*"lits" includes the typing assumptions (TVars)*) - val cls_id = get_clause_id cls - val ax_name = get_axiomName cls - val vars = dfg_vars cls - val tvars = dfg_tvars cls - val funcs = funcs_of_cls cls - val preds = preds_of_cls cls - val knd = string_of_kind cls - val lits_str = commas lits - val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) - in - (cls_str,tfree_lits) - end; - - +fun string_of_descrip name = "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")." - fun gen_dfg_file probname axioms conjectures funcs preds = let val axstrs_tfrees = (map clause2dfg axioms) val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees @@ -1102,35 +960,47 @@ val funcstr = string_of_funcs funcs val predstr = string_of_preds preds in - (string_of_start probname) ^ (string_of_descrip ()) ^ - (string_of_symbols funcstr predstr) ^ - (string_of_axioms axstr) ^ - (string_of_conjectures conjstr) ^ (string_of_end ()) + string_of_start probname ^ string_of_descrip probname ^ + string_of_symbols funcstr predstr ^ + string_of_axioms axstr ^ + string_of_conjectures conjstr ^ "end_problem.\n" end; -fun clauses2dfg [] probname axioms conjectures funcs preds = - let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs - val preds' = (union_all(map preds_of_cls axioms)) @ preds - in - gen_dfg_file probname axioms conjectures funcs' preds' - end - | clauses2dfg (cls::clss) probname axioms conjectures funcs preds = - let val (lits,tfree_lits) = dfg_clause_aux cls - (*"lits" includes the typing assumptions (TVars)*) - val cls_id = get_clause_id cls - val ax_name = get_axiomName cls - val vars = dfg_vars cls - val tvars = dfg_tvars cls - val funcs' = (funcs_of_cls cls) union funcs - val preds' = (preds_of_cls cls) union preds - val knd = string_of_kind cls - val lits_str = concat_with ", " lits - val axioms' = if knd = "axiom" then (cls::axioms) else axioms - val conjectures' = - if knd = "conjecture" then (cls::conjectures) else conjectures - in - clauses2dfg clss probname axioms' conjectures' funcs' preds' - end; +fun add_clause_preds (cls,preds) = (preds_of_cls cls) union preds; +val preds_of_clauses = foldl add_clause_preds [] + +(*FIXME: can replace expensive list operations (ins) by trees (symtab)*) + +fun add_foltype_funcs (AtomV _, funcs) = funcs + | add_foltype_funcs (AtomF a, funcs) = (a,0) ins funcs + | add_foltype_funcs (Comp(a,tys), funcs) = + foldl add_foltype_funcs ((a, length tys) ins funcs) tys; + +fun add_folterm_funcs (UVar _, funcs) = funcs + | add_folterm_funcs (Fun(a,tys,[]), funcs) = (a,0) ins 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 ((a, length tys + length tms) ins 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; + +val funcs_of_clauses = foldl add_clause_funcs [] + + +fun clauses2dfg probname axioms conjectures = + let val clss = conjectures @ axioms + in + gen_dfg_file probname axioms conjectures + (funcs_of_clauses clss) (preds_of_clauses clss) + end fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) = @@ -1186,8 +1056,8 @@ tagged_pol ^ pred_string end; -fun tptp_of_typeLit (LTVar x) = "--" ^ x - | tptp_of_typeLit (LTFree x) = "++" ^ x; +fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")" + | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")"; fun gen_tptp_cls (cls_id,ax_name,knd,lits) =