# HG changeset patch # User quigley # Date 1125077767 -7200 # Node ID ce2a1aeb42aaa031159e29d3dfe17dc123dd09d3 # Parent e2b19c92ef51ce665e4462c1b86125d05af172d6 DFG output now works for untyped rules (ML "ResClause.untyped();") diff -r e2b19c92ef51 -r ce2a1aeb42aa src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Fri Aug 26 10:01:06 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Aug 26 19:36:07 2005 +0200 @@ -112,7 +112,7 @@ val use_simpset: bool ref val use_nameless: bool ref val write_out_clasimp : string -> theory -> term -> - (ResClause.clause * thm) Array.array * int (* * ResClause.clause list *) + (ResClause.clause * thm) Array.array * int * ResClause.clause list end; @@ -245,7 +245,7 @@ val _= TextIO.flushOut out; val _= TextIO.closeOut out in - (clause_arr, num_of_clauses) + (clause_arr, num_of_clauses, clauses) end; diff -r e2b19c92ef51 -r ce2a1aeb42aa src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Aug 26 10:01:06 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Aug 26 19:36:07 2005 +0200 @@ -274,7 +274,7 @@ (*** hyps/local axioms just now ***) val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile, ">", (File.platform_path wholefile)]) (*** check if the directory exists and, if not, create it***) - val _ = + (* val _ = if !SpassComm.spass then if File.exists dfg_dir then warning("dfg dir exists") @@ -292,7 +292,16 @@ dfg_path^"/ax_prob"^"_"^(probID)^".dfg" else - (File.platform_path wholefile) + (File.platform_path wholefile)*) + + (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*) + (* from clasimpset onto problem file *) + val newfile = if !SpassComm.spass + then + probfile + else + (File.platform_path wholefile) + val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n") in @@ -516,10 +525,10 @@ val _ = File.append (File.tmp_path (Path.basic "child_command")) (childCmd^"\n") (* now get the number of the subgoal from the filename *) - val sg_num = if (!SpassComm.spass ) + val sg_num = (*if (!SpassComm.spass ) then int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) - else + else*) int_of_string(hd (rev(explode childCmd))) val childIncoming = pollChildInput childInput diff -r e2b19c92ef51 -r ce2a1aeb42aa src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Aug 26 10:01:06 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Aug 26 19:36:07 2005 +0200 @@ -16,11 +16,17 @@ (*val spass: bool ref*) val vampire: bool ref val custom_spass: string list ref + val hook_count: int ref +(* val invoke_atp: Toplevel.transition -> Toplevel.transition*) end; structure ResAtp: RES_ATP = struct + +val call_atp = ref false; +val hook_count = ref 0; + fun debug_tac tac = (debug "testing"; tac); val full_spass = ref false; @@ -56,6 +62,7 @@ val hyps_file = File.tmp_path (Path.basic "hyps"); val prob_file = File.tmp_path (Path.basic "prob"); val dummy_tac = all_tac; +val _ =debug (File.platform_path prob_file); (**** for Isabelle/ML interface ****) @@ -135,20 +142,31 @@ (* write out a subgoal as DFG clauses to the file "probN" *) (* where N is the number of this subgoal *) (*********************************************************************) -(* -fun dfg_inputs_tfrees thms n tfrees = - let val _ = (debug ("in dfg_inputs_tfrees 0")) - val clss = map (ResClause.make_conjecture_clause_thm) thms + +(*fun dfg_inputs_tfrees thms n tfrees axclauses= + let val clss = map (ResClause.make_conjecture_clause_thm) thms val _ = (debug ("in dfg_inputs_tfrees 1")) - val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss) - val _ = (debug ("in dfg_inputs_tfrees 2")) - val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) - val _ = (debug ("in dfg_inputs_tfrees 3")) + val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss) + val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) + val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) + val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees + val out = TextIO.openOut(probfile) + in + (ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; debug probfile) + end; +*) +fun dfg_inputs_tfrees thms n tfrees axclauses = + let val clss = map (ResClause.make_conjecture_clause_thm) thms val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) + val _ = warning ("about to write out dfg prob file "^probfile) + (*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss) + val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *) + val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees val out = TextIO.openOut(probfile) in - (ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; debug probfile - end;*) + (ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile ) + end; + (*********************************************************************) (* call SPASS with settings and problem file for the current subgoal *) @@ -210,18 +228,22 @@ (* then call dummy_tac - should be call_res_tac *) (**********************************************************) -fun get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm n sko_thms = - if n = 0 then - (call_resolve_tac (rev sko_thms) - sign sg_terms (childin, childout, pid) (List.length sg_terms); - dummy_tac thm) - else - SELECT_GOAL - (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac, - METAHYPS (fn negs => - (tptp_inputs_tfrees (make_clauses negs) n tfrees; - get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n - 1) - (negs::sko_thms); dummy_tac))]) n thm; + +fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses = + if n=0 then + (call_resolve_tac (rev sko_thms) + sign sg_terms (childin, childout, pid) (List.length sg_terms); + dummy_tac thm) + else + + ( SELECT_GOAL + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, + METAHYPS(fn negs => (if !SpassComm.spass then + dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses + else + tptp_inputs_tfrees (make_clauses negs) n tfrees; + get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms) axclauses; dummy_tac))]) n thm ) + (**********************************************) @@ -230,7 +252,7 @@ (* in proof reconstruction *) (**********************************************) -fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = +fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) axclauses = let val prems = Thm.prems_of thm (*val sg_term = get_nth k prems*) @@ -243,7 +265,7 @@ (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) (* recursive call to pick up the remaining subgoals *) (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) - get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] + get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] axclauses end; @@ -255,11 +277,11 @@ (* write to file "hyps" *) (**************************************************) -fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = +fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses= let val tfree_lits = isar_atp_h thms in debug ("in isar_atp_aux"); - isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) + isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) axclauses end; (******************************************************************) @@ -281,10 +303,10 @@ val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems) (*set up variables for writing out the clasimps to a tptp file*) - val (clause_arr, num_of_clauses) = + val (clause_arr, num_of_clauses, axclauses) = ResClasimp.write_out_clasimp (File.platform_path clasimp_file) thy (hd prems) (*FIXME: hack!! need to do all prems*) - val _ = debug ("clasimp_file is " ^ File.platform_path clasimp_file) + val _ = debug ("clasimp_file is " ^ File.platform_path clasimp_file ^ " with " ^ (string_of_int num_of_clauses)^ " clauses") val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses) val pid_string = string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid))) @@ -293,7 +315,7 @@ debug ("initial thm: " ^ thm_string); debug ("subgoals: " ^ prems_string); debug ("pid: "^ pid_string); - isar_atp_aux thms thm (length prems) (childin, childout, pid); + isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses; () end); @@ -340,10 +362,13 @@ (** the Isar toplevel hook **) val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state => + let + val proof = Toplevel.proof_of state val (ctxt, (_, goal)) = Proof.get_goal proof handle Proof.STATE _ => error "No goal present"; + val thy = ProofContext.theory_of ctxt; (* FIXME presently unused *) @@ -356,6 +381,8 @@ Pretty.string_of (ProofContext.pretty_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)))); debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal)); + hook_count := !hook_count +1; + debug ("in hook for time: " ^(string_of_int (!hook_count)) ); ResClause.init thy; isar_atp' (ctxt, ProofContext.prems_of ctxt, goal) end); diff -r e2b19c92ef51 -r ce2a1aeb42aa src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Fri Aug 26 10:01:06 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Fri Aug 26 19:36:07 2005 +0200 @@ -1,4 +1,5 @@ (* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ Copyright 2004 University of Cambridge @@ -6,6 +7,7 @@ Typed equality is treated differently. *) +(* works for writeoutclasimp on typed *) signature RES_CLAUSE = sig exception ARCLAUSE of string @@ -20,18 +22,27 @@ 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 special_equal : bool ref + val clause_info : clause -> string * string + val typed : unit -> unit + val untyped : unit -> unit + + 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 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 clause_info : clause -> string * string val tptp_clauses2str : string list -> string - val typed : unit -> unit - val untyped : unit -> unit val clause2tptp : clause -> string * string list val tfree_clause : string -> string val schematic_var_prefix : string @@ -45,7 +56,7 @@ val class_prefix : string end; -structure ResClause : RES_CLAUSE = +structure ResClause: RES_CLAUSE = struct (* Added for typed equality *) @@ -56,19 +67,22 @@ val schematic_var_prefix = "V_"; val fixed_var_prefix = "v_"; -val tvar_prefix = "T_"; -val tfree_prefix = "t_"; + +val tvar_prefix = "Typ_"; +val tfree_prefix = "typ_"; + val clause_prefix = "cls_"; val arclause_prefix = "arcls_" -val const_prefix = "c_"; -val tconst_prefix = "tc_"; +val const_prefix = "const_"; +val tconst_prefix = "tconst_"; val class_prefix = "class_"; + (**** some useful functions ****) val const_trans_table = @@ -82,10 +96,7 @@ ("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. @@ -99,6 +110,7 @@ fun ascii_of_c c = if Char.isAlphaNum c then String.str c else if c = #"_" then "__" + 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)) @@ -110,6 +122,7 @@ end; + (*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) @@ -118,25 +131,27 @@ fun ascii_of_indexname (v,0) = ascii_of v | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; -fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); +(* another version of above functions that remove chars that may not be allowed by Vampire *) +fun make_schematic_var v = schematic_var_prefix ^ (ascii_of 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 = +fun make_fixed_const c = const_prefix ^ (ascii_of c); +fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c); + +fun make_type_class clas = class_prefix ^ (ascii_of clas); + + + +fun lookup_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); + | NONE => make_fixed_const c; @@ -165,11 +180,16 @@ type tag = bool; + +fun string_of_indexname (name,index) = name ^ "_" ^ (string_of_int index); + + val id_ref = ref 0; - fun generate_id () = - let val id = !id_ref - in id_ref := id + 1; id end; + let val id = !id_ref + in + (id_ref:=id + 1; id) + end; @@ -204,7 +224,11 @@ literals: literal list, types_sorts: (typ_var * sort) list, tvar_type_literals: type_literal list, - tfree_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; @@ -214,14 +238,15 @@ (*** make clauses ***) -fun make_clause (clause_id,axiom_name,kind,literals, - types_sorts,tvar_type_literals, - tfree_type_literals) = - 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}; +fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals,tvars, predicates, functions) = + 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}; + + +fun type_of (Type (a, [])) = let val t = make_fixed_type_const a + in + (t,([],[(t,0)])) + end (*Definitions of the current theory--to allow suppressing types.*) val curr_defs = ref Defs.empty; @@ -229,32 +254,77 @@ (*Initialize the type suppression mechanism with the current theory before producing any clauses!*) fun init thy = (curr_defs := Theory.defs_of thy); +(*<<<<<<< res_clause.ML +*) + +(*Types aren't needed if the constant has at most one definition and is monomorphic*) +(*fun no_types_needed s = + (case Defs.fast_overloading_info (!curr_defs) s of + NONE => true + | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T)) +=======*) fun no_types_needed s = Defs.monomorphic (!curr_defs) s; +(*>>>>>>> 1.18*) + (*Flatten a type to a string while accumulating sort constraints on the TFress and TVars it contains.*) -fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) +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) = ListPair.unzip foltyps_ts - val ts' = ResLib.flat_noDup ts - in - (((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)), ts') - end - | type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)]) - | type_of (TVar (v, s)) = (make_schematic_type_var v, [((FOLTVar v),s)]); + 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 ^ (ResLib.list_to_string folTyps)),(ts', ((t,(length Ts))::funcs')) ) + end + | type_of (TFree (a, s)) = let val t = make_fixed_type_const a + in + (t, ([((FOLTFree a),s)],[(t,0)]) ) + end + + | type_of (TVar (v, s)) = let val t =make_schematic_type_var ( v) + in + (t, ([((FOLTVar v),s)], [(*(t,0)*)])) + end + +(* added: checkMeta: string -> bool *) +(* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *) +fun checkMeta s = + let val chars = explode s + in + ["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars + end; fun maybe_type_of c T = - if no_types_needed c then ("",[]) else type_of 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)) = (make_fixed_const c, maybe_type_of c T) + +fun pred_name_type (Const(c,T)) = (let val t = make_fixed_const c + val (typof,(folTyps,funcs)) = type_of T + + in + (t, (typof,folTyps), (funcs)) + end) | pred_name_type (Free(x,T)) = - if isMeta x then raise CLAUSE("Predicate Not First Order") - else (make_fixed_var x, type_of T) + let val is_meta = checkMeta x + in + if is_meta then (raise CLAUSE("Predicate Not First Order")) else + (let val t = (make_fixed_var x) + val (typof,(folTyps, funcs)) = type_of T + in + (t, (typof,folTyps),funcs) + end) + + end | pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") | pred_name_type _ = raise CLAUSE("Predicate input unexpected"); @@ -267,74 +337,108 @@ in folT end; + -fun fun_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T) - | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T) - | fun_name_type _ = raise CLAUSE("Function Not First Order"); - -(* FIX - add in funcs and stuff to this *) +(* FIX: retest with lcp's changes *) +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) then + (length args)(*+ 1*) (*(length folTyps) *) + else + (length args)(* -1*) + in + (t, (typof,folTyps), ((t,arity)::funcs)) + end) + + | fun_name_type (Free(x,T)) args = (let val t = (make_fixed_var x) + val (typof,(folTyps,funcs)) = type_of T + val arity = if (!keep_types) then + (length args) (*+ 1*) (*(length folTyps)*) + else + (length args) (*-1*)(*(length args) + 1*)(*(length folTyps)*) + in + (t, (typof,folTyps), ((t,0)::funcs)) + end) + + | fun_name_type _ args = raise CLAUSE("Function Not First Order"); + fun term_of (Var(ind_nm,T)) = - let val (folType,ts) = type_of T - in - (UVar(make_schematic_var ind_nm, folType), ts) - end + let val (folType,(ts,funcs)) = type_of T + in + (UVar(make_schematic_var(string_of_indexname ind_nm),folType),(ts, (funcs))) + end | term_of (Free(x,T)) = - let val (folType,ts) = type_of T - in - 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 (folType,ts) = type_of T - in - (Fun(make_fixed_const c,folType,[]), ts) - end - | term_of (app as (t $ a)) = - let val (f,args) = strip_comb app - fun term_of_aux () = - let val (funName,(funType,ts1)) = fun_name_type f - val (args',ts2) = ListPair.unzip (map term_of args) - val ts3 = ResLib.flat_noDup (ts1::ts2) - in - (Fun(funName,funType,args'),ts3) - end - fun term_of_eq ((Const ("op =", typ)),args) = - let val arg_typ = eq_arg_type typ - val (args',ts) = ListPair.unzip (map term_of args) - val equal_name = make_fixed_const ("op =") - in - (Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts) - 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") - else term_of_aux() - | _ => raise CLAUSE("Function Not First Order") - end + let val is_meta = checkMeta x + val (folType,(ts, funcs)) = type_of T + in + if is_meta then (UVar(make_schematic_var x,folType),(ts, (((make_schematic_var x),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(lookup_const c,folType,[]),(ts, (((lookup_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 = lookup_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 (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux () + | _ => raise CLAUSE("Function Not First Order") + end | term_of _ = raise CLAUSE("Function Not First Order"); + + fun pred_of_eq ((Const ("op =", typ)),args) = let val arg_typ = eq_arg_type typ - val (args',ts) = ListPair.unzip (map term_of args) - val equal_name = make_fixed_const "op =" + val (args',ts_funcs) = ListPair.unzip (map term_of args) + val (ts,funcs) = ListPair.unzip ( ts_funcs) + val equal_name = lookup_const "op =" in - (Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts) + (Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts,([((make_fixed_var equal_name),2)]:(string*int)list), (ResLib.flat_noDup (funcs))) end; - +(* CHECK arity for predicate is set to (2*args) to account for type info. Is this right? *) (* changed for non-equality predicate *) (* The input "pred" cannot be an equality *) fun pred_of_nonEq (pred,args) = - let val (predName,(predType,ts1)) = pred_name_type pred - val (args',ts2) = ListPair.unzip (map term_of 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 pred_arity = (*if ((length ts3) <> 0) + then + ((length args) +(length ts3)) + else*) + (* just doing length args if untyped seems to work*) + (if !keep_types then (length args)+1 else (length args)) in - (Predicate(predName,predType,args'),ts3) + (Predicate(predName,predType,args'),ts3, [(predName, pred_arity)], newfuncs) end; @@ -348,44 +452,86 @@ end; -fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term (P,lits_ts) - | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts)) = - let val (lits',ts') = literals_of_term (P,(lits,ts)) - in - literals_of_term (Q, (lits',ts')) - end - | literals_of_term ((Const("Not",_) $ P),(lits,ts)) = - let val (pred,ts') = predicate_of P - val lits' = Literal(false,pred,false) :: lits - val ts'' = ResLib.no_rep_app ts ts' - in - (lits',ts'') - end - | literals_of_term (P,(lits,ts)) = - let val (pred,ts') = predicate_of P - val lits' = Literal(true,pred,false) :: lits - val ts'' = ResLib.no_rep_app ts ts' - in - (lits',ts'') - end; - -fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[])); - + +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 ((Const("Not",_) $ P),(lits,ts), preds, funcs) = + let val (pred,ts', preds', funcs') = predicate_of P + val lits' = Literal(false,pred,false) :: lits + val ts'' = ResLib.no_rep_app ts ts' + in + (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) + end + | literals_of_term (P,(lits,ts), preds, funcs) = + let val (pred,ts', preds', funcs') = predicate_of P + val lits' = Literal(true,pred,false) :: 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 (_, []) = [] +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)) + (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)); + +fun takeUntil ch [] res = (res, []) + | takeUntil ch (x::xs) res = if x = ch + then + (res, xs) + else + takeUntil ch xs (res@[x]) + +fun remove_type str = let val exp = explode str + val (first,rest) = (takeUntil "(" exp []) + in + implode first + end + +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 [] = ([],[]) +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_aux [] = ([],[]) | add_typs_aux ((FOLTVar(indx),s)::tss) = let val vs = sorts_on_typs (FOLTVar(indx), s) val (vss,fss) = add_typs_aux tss @@ -397,46 +543,93 @@ val (vss,fss) = add_typs_aux tss in (vss, ResLib.no_rep_app fs fss) - end; + end;*) -fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls) + +fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds (** make axiom clauses, hypothesis clauses and conjecture clauses. **) - + +local + fun replace_dot "." = "_" + | replace_dot "'" = "" + | replace_dot c = c; + +in + +fun proper_ax_name ax_name = + let val chars = explode ax_name + in + implode (map replace_dot chars) + end; +end; -fun make_conjecture_clause_thm thm = - let val (lits,types_sorts) = literals_of_thm thm - val cls_id = generate_id() - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts - in - make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) +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) = + let val (vstrs) = get_tvar_strs tss + in + (distinct( vstrs)) + end; + +(* FIX add preds and funcs to add typs aux here *) + +fun make_axiom_clause_thm thm (name,number)= + let val (lits,types_sorts, preds, funcs) = literals_of_thm thm + val cls_id = number + val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds + val tvars = get_tvar_strs types_sorts + val ax_name = proper_ax_name name + in + make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) end; -fun make_axiom_clause term (axname,cls_id) = - let val (lits,types_sorts) = literals_of_term (term,([],[])) - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + +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 (name,number)= + let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[]) + val cls_id = number + val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds + val tvars = get_tvar_strs types_sorts + val ax_name = proper_ax_name name in - make_clause(cls_id,axname,Axiom,lits,types_sorts,tvar_lits,tfree_lits) + 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) = literals_of_term (term,([],[])) + let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) val cls_id = generate_id() - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + 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) + 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) = literals_of_term (term,([],[])) + let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) val cls_id = generate_id() - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + 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) + make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) end; @@ -525,11 +718,11 @@ -(***** convert clauses to tptp format *****) +(***** convert clauses to DFG format *****) -fun string_of_clauseID (Clause cls) = - clause_prefix ^ string_of_int (#clause_id cls); +fun string_of_clauseID (Clause cls) = clause_prefix ^ (string_of_int (#clause_id cls)); + fun string_of_kind (Clause cls) = name_of_kind (#kind cls); @@ -550,6 +743,7 @@ "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" end + and string_of_term (UVar(x,_)) = x | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) @@ -565,8 +759,128 @@ (* Changed for typed equality *) (* 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) +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) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) + else name ^ (ResLib.list_to_string terms_as_strings) + end; + + + +(********************************) +(* Code for producing DFG files *) +(********************************) + +fun dfg_literal (Literal(pol,pred,tag)) = + let val pred_string = string_of_predicate pred + val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")" + in + tagged_pol + 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 strlist [] = "" +| strlist (x::[]) = x +| strlist (x::xs) = x ^ "," ^ (strlist xs) + + +fun gen_dfg_cls (cls_id,ax_name,knd,lits, tvars,vars) = + let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) + val forall_str = if (vars = []) andalso (tvars = []) + then + "" + else + "forall([" ^ (strlist (vars@tvars))^ "]" + in + if forall_str = "" + then + "clause( %(" ^ knd ^ ")\n" ^ "or(" ^ lits ^ ") ,\n" ^ cls_id ^ ax_str ^ ")." + else + "clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or(" ^ lits ^ ")),\n" ^ cls_id ^ ax_str ^ ")." + end; + + + +fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars, vars) = + let val forall_str = if (vars = []) andalso (tvars = []) + then + "" + else + "forall([" ^ (strlist (vars@tvars))^"]" + in + if forall_str = "" + then + "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ tfree_lit ^ ") ,\n" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ ")." + else + "clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ ")." + end; + + + +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(str,typ)) =(*if (substring (str, 0,2))= "V_" then *)[str] (*else []*) +| get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) + + +fun is_uvar (UVar(str,typ)) = true +| is_uvar (Fun (str,typ,tlist)) = false; + +fun uvar_name (UVar(str,typ)) = str +| uvar_name _ = (raise CLAUSE("Not a variable")); + + +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) + val vars = ResLib.flat_noDup(map get_uvars folterms) + in + vars + 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 @@ -576,14 +890,247 @@ else name ^ (ResLib.list_to_string 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 concat_with_comma [] = "" + | concat_with_comma [x] = x + | concat_with_comma (x::xs) = x ^ ", " ^ (concat_with_comma 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 cls_id = string_of_clauseID cls + val ax_name = string_of_axiomName cls + val knd = string_of_kind cls + val lits_str = concat_with_comma lits + val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) + fun typ_clss k [] = [] + | typ_clss k (tfree :: tfrees) = + (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: (typ_clss (k+1) tfrees) + in + cls_str :: (typ_clss 0 tfree_lits) + end; + +fun clause_info cls = + let + val cls_id = string_of_clauseID cls + val ax_name = string_of_axiomName cls + in + ((ax_name^""), cls_id) + end; + + + +fun zip_concat name [] = [] +| zip_concat name ((str, num)::xs) = (((str^name), num)::(zip_concat name xs)) + + +(*fun funcs_of_cls (Clause cls) = let val funcs = #functions cls + val name = #axiom_name cls + in + zip_concat name funcs + end; + + +fun preds_of_cls (Clause cls) = let val preds = #predicates cls +; val name = ("foo"^(#axiom_name cls)) + in + zip_concat name preds + end +*) + +fun funcs_of_cls (Clause cls) = #functions cls; + + +fun preds_of_cls (Clause cls) = #predicates cls; + + + + +fun string_of_arity (name, num) = name ^"," ^ (string_of_int 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 = string_of_clauseID cls + val ax_name = string_of_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 = concat_with_comma 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 fname axioms conjectures funcs preds tfrees= + 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) \\ tfrees) + 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 fname) ^ (string_of_descrip ()) ^ (string_of_symbols funcstr predstr ) ^ + (string_of_axioms axstr)^ + (string_of_conjectures conjstr) ^ (string_of_end ()) + end; + + + +fun clauses2dfg [] filename axioms conjectures funcs preds tfrees= + 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 filename axioms conjectures funcs' preds' tfrees + (*(filename, axioms, conjectures, funcs, preds)*) + end +|clauses2dfg (cls::clss) filename axioms conjectures funcs preds tfrees = + let val (lits,tfree_lits) = dfg_clause_aux (cls) (*"lits" includes the typing assumptions (TVars)*) + val cls_id = string_of_clauseID cls + val ax_name = string_of_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 filename axioms' conjectures' funcs' preds' tfrees + end; + + +fun fileout f str = let val out = TextIO.openOut(f) + in + ResLib.writeln_strs out (str); TextIO.closeOut out + end; + +(*val filestr = clauses2dfg newcls "flump" [] [] [] []; +*) +(* fileout "flump.dfg" [filestr];*) + + +(*FIX: ask Jia what this is for *) + + +fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); + + +fun string_of_arLit (TConsLit(b,(c,t,args))) = + let val pol = if b then "++" else "--" + val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) + in + pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" + end + | string_of_arLit (TVarLit(b,(c,str))) = + let val pol = if b then "++" else "--" + in + pol ^ c ^ "(" ^ str ^ ")" + end; +fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); + + +fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); + + +fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); + +(*FIX: would this have variables in a forall? *) + +fun dfg_arity_clause arcls = + let val arcls_id = string_of_arClauseID arcls + val concl_lit = string_of_conclLit arcls + val prems_lits = strings_of_premLits arcls + val knd = string_of_arKind arcls + val all_lits = concl_lit :: prems_lits + in + + "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^ arcls_id ^ ")." + end; + + +val clrelclause_prefix = "relcls_"; + +(* FIX later. Doesn't seem to be used in clasimp *) + +(*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 ^ string_of_int(#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; + *) + +(********************************) +(* 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 "--") + val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---") + else (if pol then "++" else "--") in tagged_pol ^ pred_string end; @@ -595,26 +1142,19 @@ fun gen_tptp_cls (cls_id,ax_name,knd,lits) = - let val ax_str = (if ax_name = "" then "" else ("_" ^ ascii_of ax_name)) + let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) in "input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." end; -fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = - "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ - knd ^ ",[" ^ tfree_lit ^ "])."; + +fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; fun tptp_clause_aux (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 [] + 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; @@ -633,7 +1173,13 @@ cls_str :: (typ_clss 0 tfree_lits) end; -fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls); +fun clause_info cls = + let + val cls_id = string_of_clauseID cls + val ax_name = string_of_axiomName cls + in + ((ax_name^""), cls_id) + end; fun clause2tptp cls = @@ -648,8 +1194,7 @@ end; -fun tfree_clause tfree_lit = - "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; +fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; val delim = "\n"; val tptp_clauses2str = ResLib.list2str_sep delim; @@ -710,5 +1255,5 @@ in "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." end; - + end;