(* Author: Jia Meng, Cambridge University Computer Laboratory ID: $Id: res_clause.ML,v 1.30 2005/09/20 16:43:39 paulson Exp $ Copyright 2004 University of Cambridge ML data structure for storing/printing FOL clauses and arity clauses. Typed equality is treated differently. *) (* works for writeoutclasimp on typed *) signature RES_CLAUSE = sig 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 val classrelClauses_of : string * string list -> classrelClause list type clause val init : theory -> unit val make_axiom_arity_clause : string * (string * string list list) -> arityClause val make_axiom_classrelClause : string * string option -> classrelClause val make_axiom_clause : Term.term -> string * int -> clause val make_conjecture_clause : Term.term -> clause val make_conjecture_clause_thm : Thm.thm -> clause val make_hypothesis_clause : Term.term -> clause val get_axiomName : clause -> string val isTaut : clause -> bool val num_of_clauses : clause -> int val dfg_clauses2str : string list -> string val clause2dfg : clause -> string * string list val clauses2dfg : clause list -> string -> clause list -> clause list -> (string * int) list -> (string * int) list -> string val tfree_dfg_clause : string -> string val tptp_arity_clause : arityClause -> string val tptp_classrelClause : classrelClause -> string val tptp_clause : clause -> string list val tptp_clauses2str : string list -> string val clause2tptp : clause -> string * string list val tfree_clause : string -> string val schematic_var_prefix : string val fixed_var_prefix : string 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 end; structure ResClause: RES_CLAUSE = struct (* Added for typed equality *) val special_equal = ref false; (* by default,equality does not carry type information *) val eq_typ_wrapper = "typeinfo"; (* default string *) val schematic_var_prefix = "V_"; val fixed_var_prefix = "v_"; val tvar_prefix = "T_"; val tfree_prefix = "t_"; val clause_prefix = "cls_"; val arclause_prefix = "clsarity_" val clrelclause_prefix = "clsrel_"; val const_prefix = "c_"; val tconst_prefix = "tc_"; val class_prefix = "class_"; (**** some useful functions ****) val const_trans_table = Symtab.make [("op =", "equal"), ("op <=", "lessequals"), ("op <", "less"), ("op &", "and"), ("op |", "or"), ("op +", "plus"), ("op -", "minus"), ("op *", "times"), ("op -->", "implies"), ("{}", "emptyset"), ("op :", "in"), ("op Un", "union"), ("op Int", "inter")]; val type_const_trans_table = Symtab.make [("*", "t_prod"), ("+", "t_sum"), ("~=>", "t_map")]; (*Escaping of special characters. Alphanumeric characters are left unchanged. The character _ goes to __ Characters in the range ASCII space to / go to _A to _P, respectively. Other printing characters go to _NNN where NNN is the decimal ASCII code.*) local val A_minus_space = Char.ord #"A" - Char.ord #" "; fun ascii_of_c c = if Char.isAlphaNum c then String.str c else if c = #"_" then "__" else if #" " <= c andalso c <= #"/" then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c)) else "" in val ascii_of = String.translate ascii_of_c; end; (* convert a list of strings into one single string; surrounded by brackets *) fun paren_pack strings = "(" ^ commas strings ^ ")"; fun bracket_pack strings = "[" ^ commas strings ^ "]"; (*Remove the initial ' character from a type variable, if it is present*) fun trim_type_var s = if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) else error ("trim_type: Malformed type variable encountered: " ^ s); fun ascii_of_indexname (v,0) = ascii_of v | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); (*Type variables contain _H because the character ' translates to that.*) fun make_schematic_type_var (x,i) = tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); fun make_fixed_const c = case Symtab.lookup const_trans_table c of SOME c' => c' | NONE => const_prefix ^ ascii_of c; fun make_fixed_type_const c = case Symtab.lookup type_const_trans_table c of SOME c' => c' | NONE => tconst_prefix ^ ascii_of c; 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. *****) val keep_types = ref true; datatype kind = Axiom | Hypothesis | Conjecture; fun name_of_kind Axiom = "axiom" | name_of_kind Hypothesis = "hypothesis" | name_of_kind Conjecture = "conjecture"; type clause_id = int; type axiom_name = string; type polarity = bool; type indexname = Term.indexname; (* "tag" is used for vampire specific syntax *) type tag = bool; val id_ref = ref 0; fun generate_id () = let val id = !id_ref in id_ref := id + 1; id end; (**** Isabelle FOL clauses ****) val tagged = ref false; type pred_name = string; type sort = Term.sort; type fol_type = string; datatype type_literal = LTVar of string | LTFree of string; datatype folTerm = UVar of string * fol_type | Fun of string * fol_type * folTerm list; datatype predicate = Predicate of pred_name * fol_type * folTerm list; datatype literal = Literal of polarity * predicate * tag; datatype typ_var = FOLTVar of indexname | FOLTFree of string; (* ML datatype used to repsent one single clause: disjunction of literals. *) datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, kind: kind, 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}; exception CLAUSE of string * term; (*** make clauses ***) fun isFalse (Literal (pol,Predicate(a,_,[]),_)) = (pol andalso a = "c_False") orelse (not pol andalso a = "c_True") | isFalse _ = false; fun isTrue (Literal (pol,Predicate(a,_,[]),_)) = (pol andalso a = "c_True") orelse (not pol andalso a = "c_False") | isTrue _ = false; fun isTaut (Clause {literals,...}) = exists isTrue literals; fun make_clause (clause_id,axiom_name,kind,literals, types_sorts,tvar_type_literals, tfree_type_literals,tvars, predicates, functions) = if forall isFalse literals then error "Problem too trivial for resolution (empty clause)" else Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, literals = literals, types_sorts = types_sorts, tvar_type_literals = tvar_type_literals, tfree_type_literals = tfree_type_literals, tvars = tvars, predicates = predicates, functions = functions}; (** Some Clause destructor functions **) fun string_of_kind (Clause cls) = name_of_kind (#kind cls); fun get_axiomName (Clause cls) = #axiom_name cls; 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; (*Definitions of the current theory--to allow suppressing types.*) val curr_defs = ref Defs.empty; (*Initialize the type suppression mechanism with the current theory before producing any clauses!*) fun init thy = (curr_defs := Theory.defs_of thy); fun no_types_needed s = Defs.monomorphic (!curr_defs) s; (*Flatten a type to a string while accumulating sort constraints on the TFress and TVars it contains.*) fun type_of (Type (a, [])) = let val t = make_fixed_type_const a in (t,([],[(t,0)])) end | type_of (Type (a, Ts)) = let val foltyps_ts = map type_of Ts val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts val (ts, funcslist) = ListPair.unzip ts_funcs val ts' = ResLib.flat_noDup ts val funcs' = ResLib.flat_noDup funcslist val t = make_fixed_type_const a in ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') ) end | type_of (TFree (a, s)) = let val t = make_fixed_type_var a in (t, ([((FOLTFree a),s)],[(t,0)]) ) end | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], [])) fun maybe_type_of c T = if no_types_needed c then ("",([],[])) else type_of T; (* Any variables created via the METAHYPS tactical should be treated as universal vars, although it is represented as "Free(...)" by Isabelle *) val isMeta = String.isPrefix "METAHYP1_" fun pred_name_type (Const(c,T)) = let val (typof,(folTyps,funcs)) = maybe_type_of c T in (make_fixed_const c, (typof,folTyps), funcs) end | 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, ("",[]), []) | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v) | pred_name_type t = raise CLAUSE("Predicate input unexpected", t); (* For type equality *) (* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) (* Find type of equality arg *) fun eq_arg_type (Type("fun",[T,_])) = let val (folT,_) = type_of T; in folT end; fun fun_name_type (Const(c,T)) args = let val t = make_fixed_const c val (typof, (folTyps,funcs)) = maybe_type_of c T val arity = if !keep_types andalso not (no_types_needed c) then 1 + length args else length args in (t, (typof,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_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 | term_of (Free(x,T)) = let val (folType, (ts,funcs)) = 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)) end | term_of (Const(c,T)) = (* impossible to be equality *) let val (folType,(ts,funcs)) = type_of T in (Fun(make_fixed_const c, folType, []), (ts, ((make_fixed_const c),0)::funcs)) end | term_of (app as (t $ a)) = let val (f,args) = strip_comb app fun term_of_aux () = let val (funName,(funType,ts1),funcs) = fun_name_type f args val (args',ts_funcs) = ListPair.unzip (map term_of args) val (ts2,funcs') = ListPair.unzip ts_funcs val ts3 = ResLib.flat_noDup (ts1::ts2) val funcs'' = ResLib.flat_noDup((funcs::funcs')) in (Fun(funName,funType,args'), (ts3,funcs'')) end fun term_of_eq ((Const ("op =", typ)),args) = let val arg_typ = eq_arg_type typ val (args',ts_funcs) = ListPair.unzip (map term_of args) val (ts,funcs) = ListPair.unzip ts_funcs val equal_name = make_fixed_const ("op =") in (Fun(equal_name,arg_typ,args'), (ResLib.flat_noDup ts, (make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs)) end in case f of Const ("op =", typ) => term_of_eq (f,args) | Const(_,_) => term_of_aux () | Free(s,_) => if isMeta s then raise CLAUSE("Function Not First Order 2", f) else term_of_aux() | _ => raise CLAUSE("Function Not First Order 3", f) end | term_of t = raise CLAUSE("Function Not First Order 4", t); fun pred_of (Const("op =", typ), args) = let val arg_typ = eq_arg_type typ val (args',ts_funcs) = ListPair.unzip (map term_of args) val (ts,funcs) = ListPair.unzip ts_funcs val equal_name = make_fixed_const "op =" in (Predicate(equal_name,arg_typ,args'), ResLib.flat_noDup ts, [((make_fixed_var equal_name), 2)], (ResLib.flat_noDup funcs)) end | pred_of (pred,args) = let val (predName,(predType,ts1), pfuncs) = pred_name_type pred val (args',ts_funcs) = ListPair.unzip (map term_of args) val (ts2,ffuncs) = ListPair.unzip ts_funcs val ts3 = ResLib.flat_noDup (ts1::ts2) val ffuncs' = (ResLib.flat_noDup ffuncs) val newfuncs = distinct (pfuncs@ffuncs') val arity = case pred of Const (c,_) => if !keep_types andalso not (no_types_needed c) then 1 + length args else length args | _ => length args in (Predicate(predName,predType,args'), ts3, [(predName, arity)], newfuncs) end; (*Treatment of literals, possibly negated or tagged*) fun predicate_of ((Const("Not",_) $ P), polarity, tag) = predicate_of (P, not polarity, tag) | predicate_of ((Const("HOL.tag",_) $ P), polarity, tag) = predicate_of (P, polarity, true) | predicate_of (term,polarity,tag) = (pred_of (strip_comb term), polarity, tag); fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs) | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs) in literals_of_term(Q, (lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs)) end | literals_of_term (P,(lits,ts), preds, funcs) = let val ((pred,ts', preds', funcs'), pol, tag) = predicate_of (P,true,false) val lits' = Literal(pol,pred,tag) :: lits val ts'' = ResLib.no_rep_app ts ts' in (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) end; fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []); (* FIX: not sure what to do with these funcs *) (*Make literals for sorted type variables*) 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)); (*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) (*Given a list of sorted type variables, return two separate lists. The first is for TVars, the second for TFrees.*) fun add_typs_aux [] preds = ([],[], preds) | add_typs_aux ((FOLTVar indx,s)::tss) preds = let val vs = sorts_on_typs (FOLTVar indx, s) val preds' = (map pred_of_sort vs)@preds val (vss,fss, preds'') = add_typs_aux tss preds' in (ResLib.no_rep_app vs vss, fss, preds'') end | add_typs_aux ((FOLTFree x,s)::tss) preds = let val fs = sorts_on_typs (FOLTFree x, s) val preds' = (map pred_of_sort fs)@preds val (vss,fss, preds'') = add_typs_aux tss preds' in (vss, ResLib.no_rep_app fs fss,preds'') end; fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds (** make axiom clauses, hypothesis clauses and conjecture clauses. **) fun get_tvar_strs [] = [] | get_tvar_strs ((FOLTVar indx,s)::tss) = let val vstr = make_schematic_type_var indx val vstrs = get_tvar_strs tss in (distinct( vstr:: vstrs)) 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_thm thm 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) end; fun make_conjecture_clause_thm thm = let val (lits,types_sorts, preds, funcs) = literals_of_thm thm val cls_id = generate_id() val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds val tvars = get_tvar_strs types_sorts in make_clause(cls_id,"",Conjecture, lits,types_sorts,tvar_lits,tfree_lits, tvars, preds, funcs) end; fun make_axiom_clause term (ax_name,cls_id) = let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[]) 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) end; fun make_hypothesis_clause term = let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) val cls_id = generate_id() val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds val tvars = get_tvar_strs types_sorts in make_clause(cls_id,"",Hypothesis, lits,types_sorts,tvar_lits,tfree_lits, tvars, preds, funcs) end; fun make_conjecture_clause term = let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) val cls_id = generate_id() val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds val tvars = get_tvar_strs types_sorts in make_clause(cls_id,"",Conjecture, lits,types_sorts,tvar_lits,tfree_lits, tvars, preds, funcs) end; (**** Isabelle arities ****) 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 = ArityClause of {clause_id: clause_id, kind: kind, conclLit: arLit, premLits: arLit list}; fun get_TVars 0 = [] | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1); fun pack_sort(_,[]) = raise ARCLAUSE("Empty Sort Found") | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] | 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_arity_clause (clause_id,kind,conclLit,premLits) = ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits}; fun make_axiom_arity_clause (tcons,(res,args)) = let val cls_id = generate_id() val nargs = length args val tvars = get_TVars nargs val conclLit = make_TConsLit(true,(res,tcons,tvars)) val tvars_srts = ListPair.zip (tvars,args) val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) val false_tvars_srts' = ResLib.pair_ins false tvars_srts' val premLits = map make_TVarLit false_tvars_srts' in make_arity_clause (cls_id,Axiom,conclLit,premLits) end; (*The number of clauses generated from cls, including type clauses*) fun num_of_clauses (Clause cls) = let val num_tfree_lits = if !keep_types then length (#tfree_type_literals cls) else 0 in 1 + num_tfree_lits end; (**** Isabelle class relations ****) datatype classrelClause = ClassrelClause of {clause_id: clause_id, subclass: class, superclass: class option}; fun make_classrelClause (clause_id,subclass,superclass) = ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass}; fun make_axiom_classrelClause (subclass,superclass) = let val cls_id = generate_id() val sub = make_type_class subclass val sup = case superclass of NONE => NONE | SOME s => SOME (make_type_class s) in make_classrelClause(cls_id,sub,sup) end; fun classrelClauses_of_aux (sub,[]) = [] | classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); fun classrelClauses_of (sub,sups) = case sups of [] => [make_axiom_classrelClause (sub,NONE)] | _ => classrelClauses_of_aux (sub, sups); (****!!!! 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 && if we specifically ask for types to be included. *) fun string_of_equality (typ,terms) = let val [tstr1,tstr2] = map string_of_term terms in if !keep_types andalso !special_equal then "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ (wrap_eq_type typ tstr2) ^ ")" else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" end and string_of_term (UVar(x,_)) = x | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) | string_of_term (Fun (name,typ,[])) = name | string_of_term (Fun (name,typ,terms)) = let val terms' = map string_of_term terms in if !keep_types andalso typ<>"" then name ^ (paren_pack (terms' @ [typ])) else name ^ (paren_pack terms') end; (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) | string_of_predicate (Predicate(name,_,[])) = name | string_of_predicate (Predicate(name,typ,terms)) = let val terms_as_strings = map string_of_term terms in if !keep_types andalso typ<>"" then name ^ (paren_pack (terms_as_strings @ [typ])) else name ^ (paren_pack terms_as_strings) end; fun string_of_clausename (cls_id,ax_name) = clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; fun string_of_type_clsname (cls_id,ax_name,idx) = string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); (********************************) (* Code for producing DFG files *) (********************************) fun dfg_literal (Literal(pol,pred,tag)) = let val pred_string = string_of_predicate pred in 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 ; (*Make the string of universal quantifiers for a clause*) fun forall_open ([],[]) = "" | forall_open (vars,tvars) = "forall([" ^ (commas (tvars@vars))^ "],\n" 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" ^ string_of_clausename (cls_id,ax_name) ^ ")."; 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) ^ ")."; fun dfg_clause_aux (Clause cls) = let val lits = map dfg_literal (#literals cls) val tvar_lits_strs = if !keep_types then map dfg_of_typeLit (#tvar_type_literals cls) else [] val tfree_lits = if !keep_types then map dfg_of_typeLit (#tfree_type_literals cls) else [] in (tvar_lits_strs @ lits, tfree_lits) end; fun dfg_folterms (Literal(pol,pred,tag)) = let val Predicate (predname, foltype, folterms) = pred in folterms end fun get_uvars (UVar(a,typ)) = [a] | get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) fun is_uvar (UVar _) = true | is_uvar (Fun _) = false; fun uvar_name (UVar(a,_)) = a | uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT)); fun mergelist [] = [] | mergelist (x::xs ) = x @ mergelist xs fun dfg_vars (Clause cls) = let val lits = #literals cls val folterms = mergelist(map dfg_folterms lits) in ResLib.flat_noDup(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",typ,terms)) = "EQUALITY" | string_of_predname (Predicate(name,_,[])) = name | string_of_predname (Predicate(name,typ,terms)) = name (* make this return funcs and preds too? *) fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) | string_of_predicate (Predicate(name,_,[])) = name | string_of_predicate (Predicate(name,typ,terms)) = let val terms_as_strings = map string_of_term terms in if !keep_types andalso typ<>"" then name ^ (paren_pack (terms_as_strings @ [typ])) else name ^ (paren_pack terms_as_strings) end; 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 = let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) val vars = dfg_vars cls val tvars = dfg_tvars cls val knd = string_of_kind cls 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; fun string_of_arity (name, num) = name ^ "," ^ (Int.toString num) fun string_of_preds preds = "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n"; fun string_of_funcs funcs = "functions[" ^ (concat_with ", " (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%------------------------------------------------------------------------------"; val delim = "\n"; val dfg_clauses2str = ResLib.list2str_sep delim; 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 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 val axstr = ResLib.list2str_sep delim axstrs val conjstrs_tfrees = (map clause2dfg conjectures) val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs) 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 ()) end; fun clauses2dfg [] probname axioms conjectures funcs preds = let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs val preds' = (ResLib.flat_noDup(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' = distinct((funcs_of_cls cls)@funcs) val preds' = distinct((preds_of_cls cls)@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 string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ Int.toString(#clause_id arcls); fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); (*FIXME!!! currently is TPTP format!*) fun dfg_of_arLit (TConsLit(b,(c,t,args))) = let val pol = if b then "++" else "--" val arg_strs = (case args of [] => "" | _ => paren_pack args) in pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" end | dfg_of_arLit (TVarLit(b,(c,str))) = let val pol = if b then "++" else "--" in pol ^ c ^ "(" ^ str ^ ")" end; fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls); fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls); (*FIXME: would this have variables in a forall? *) 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 ^ ")." end; (********************************) (* code to produce TPTP files *) (********************************) fun tptp_literal (Literal(pol,pred,tag)) = let val pred_string = string_of_predicate pred val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---") else (if pol then "++" else "--") in tagged_pol ^ pred_string end; fun tptp_of_typeLit (LTVar x) = "--" ^ x | tptp_of_typeLit (LTFree x) = "++" ^ x; fun gen_tptp_cls (cls_id,ax_name,knd,lits) = "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ knd ^ "," ^ lits ^ ")."; fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; fun tptp_type_lits (Clause cls) = let val lits = map tptp_literal (#literals cls) val tvar_lits_strs = if !keep_types then (map tptp_of_typeLit (#tvar_type_literals cls)) else [] val tfree_lits = if !keep_types then (map tptp_of_typeLit (#tfree_type_literals cls)) else [] in (tvar_lits_strs @ lits, tfree_lits) end; fun tptp_clause cls = let val (lits,tfree_lits) = tptp_type_lits cls (*"lits" includes the typing assumptions (TVars)*) val cls_id = get_clause_id cls val ax_name = get_axiomName cls val knd = string_of_kind cls val lits_str = bracket_pack lits val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] | typ_clss k (tfree :: tfrees) = gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: typ_clss (k+1) tfrees in cls_str :: (typ_clss 0 tfree_lits) end; fun clause2tptp cls = let val (lits,tfree_lits) = tptp_type_lits cls (*"lits" includes the typing assumptions (TVars)*) val cls_id = get_clause_id cls val ax_name = get_axiomName cls val knd = string_of_kind cls val lits_str = bracket_pack lits val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) in (cls_str,tfree_lits) end; fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; val delim = "\n"; val tptp_clauses2str = ResLib.list2str_sep delim; fun tptp_of_arLit (TConsLit(b,(c,t,args))) = let val pol = if b then "++" else "--" val arg_strs = (case args of [] => "" | _ => paren_pack args) in pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" end | tptp_of_arLit (TVarLit(b,(c,str))) = let val pol = if b then "++" else "--" in pol ^ c ^ "(" ^ str ^ ")" end; 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) ^ ")." end; fun tptp_classrelLits sub sup = let val tvar = "(T)" in case sup of NONE => "[++" ^ sub ^ tvar ^ "]" | (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" end; fun tptp_classrelClause (ClassrelClause cls) = let val relcls_id = clrelclause_prefix ^ Int.toString(#clause_id cls) val sub = #subclass cls val sup = #superclass cls val lits = tptp_classrelLits sub sup in "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." end; end;