# HG changeset patch # User paulson # Date 1138700353 -3600 # Node ID a113b6839df1fe74b79c2ff8c07533b116cb81fc # Parent bd83590be0f7b428d0fbaa82d8f2e124ce42573a reorganization of code to support DFG otuput diff -r bd83590be0f7 -r a113b6839df1 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Jan 31 00:51:15 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Tue Jan 31 10:39:13 2006 +0100 @@ -13,7 +13,6 @@ val helper_path: string -> string -> string val problem_name: string ref val time_limit: int ref - val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit end; structure ResAtp: RES_ATP = @@ -49,39 +48,6 @@ fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; - -(**** For running in Isar ****) - -fun writeln_strs _ [] = () - | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss); - -(* write out a subgoal as tptp clauses to the file "xxxx_N"*) -fun tptp_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = - let - val clss = ResClause.make_conjecture_clauses (map prop_of ths) - val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) - val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss) - val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses - val arity_cls = map ResClause.tptp_arity_clause arity_clauses - val out = TextIO.openOut(pf n) - in - writeln_strs out (List.concat (map ResClause.tptp_clause axclauses)); - writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls); - TextIO.closeOut out - end; - -(* write out a subgoal in DFG format to the file "xxxx_N"*) -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 (!problem_name ^ "_" ^ Int.toString n) - axclauses clss - val out = TextIO.openOut(pf n) - in - writeln_strs out [probN]; TextIO.closeOut out - end; - - (* call prover with settings and problem file for the current subgoal *) fun watcher_call_provers sign sg_terms (childin, childout, pid) = let @@ -145,14 +111,15 @@ val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else [] val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) - val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees + val write = if !prover = "spass" then ResClause.dfg_write_file + else ResClause.tptp_write_file fun writenext n = if n=0 then [] else (SELECT_GOAL (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, METAHYPS(fn negs => - (write (make_clauses negs) pf n + (write (make_clauses negs) (pf n) (axclauses,classrel_clauses,arity_clauses); all_tac))]) n th; pf n :: writenext (n-1)) diff -r bd83590be0f7 -r a113b6839df1 src/HOL/Tools/res_atp_setup.ML --- a/src/HOL/Tools/res_atp_setup.ML Tue Jan 31 00:51:15 2006 +0100 +++ b/src/HOL/Tools/res_atp_setup.ML Tue Jan 31 10:39:13 2006 +0100 @@ -325,7 +325,7 @@ val (clss,errs) = tptp_ax_fn rules val clss' = ResClause.union_all clss in - ResAtp.writeln_strs out clss'; + ResClause.writeln_strs out clss'; TextIO.closeOut out; ([file],errs) end; @@ -353,11 +353,11 @@ fun atp_conjectures_h_g filt_conj_fn hyp_cls = let val (tptp_h_clss,tfree_litss) = filt_conj_fn hyp_cls val tfree_lits = ResClause.union_all tfree_litss - val tfree_clss = map ResClause.tfree_clause tfree_lits + val tfree_clss = map ResClause.tptp_tfree_clause tfree_lits val hypsfile = hyps_file () val out = TextIO.openOut(hypsfile) in - ResAtp.writeln_strs out (tfree_clss @ tptp_h_clss); + ResClause.writeln_strs out (tfree_clss @ tptp_h_clss); TextIO.closeOut out; warning hypsfile; ([hypsfile],tfree_lits) end; @@ -368,11 +368,11 @@ fun atp_conjectures_c_g filt_conj_fn conj_cls n tfrees = let val (tptp_c_clss,tfree_litss) = filt_conj_fn conj_cls - val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees) + val tfree_clss = map ResClause.tptp_tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees) val probfile = prob_file n val out = TextIO.openOut(probfile) in - ResAtp.writeln_strs out (tfree_clss @ tptp_c_clss); + ResClause.writeln_strs out (tfree_clss @ tptp_c_clss); TextIO.closeOut out; warning probfile; probfile @@ -410,7 +410,7 @@ let val tsfile = types_sorts_file () val out = TextIO.openOut(tsfile) in - ResAtp.writeln_strs out (classrel_cls @ arity_cls); + ResClause.writeln_strs out (classrel_cls @ arity_cls); TextIO.closeOut out; [tsfile] end diff -r bd83590be0f7 -r a113b6839df1 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Jan 31 00:51:15 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Jan 31 10:39:13 2006 +0100 @@ -25,9 +25,6 @@ val isTaut : clause -> bool val num_of_clauses : clause -> int - val clauses2dfg : string -> clause list -> clause list -> string - val tfree_dfg_clause : string -> string - val arity_clause_thy: theory -> arityClause list val classrel_clauses_thy: theory -> classrelClause list @@ -35,7 +32,7 @@ val tptp_classrelClause : classrelClause -> string val tptp_clause : clause -> string list val clause2tptp : clause -> string * string list - val tfree_clause : string -> string + val tptp_tfree_clause : string -> string val schematic_var_prefix : string val fixed_var_prefix : string val tvar_prefix : string @@ -76,9 +73,16 @@ val types_ord : fol_type list * fol_type list -> order val string_of_fol_type : fol_type -> string val mk_fol_type: string * string * fol_type list -> fol_type - val types_eq :fol_type list * fol_type list -> - (string * string) list * (string * string) list -> bool * ((string * string) list * (string * string) list) + val types_eq: fol_type list * fol_type list -> + (string*string) list * (string*string) list -> + bool * ((string*string) list * (string*string) list) val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int + + val dfg_write_file: thm list -> string -> + (clause list * classrelClause list * arityClause list) -> unit + val tptp_write_file: thm list -> string -> + (clause list * classrelClause list * arityClause list) -> unit + val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit end; structure ResClause : RES_CLAUSE = @@ -794,17 +798,21 @@ fun string_of_type_clsname (cls_id,ax_name,idx) = string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); + +(*Write a list of strings to a file*) +fun writeln_strs os = List.app (fn s => TextIO.output (os,s)); + (********************************) (* 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; +(*Attach sign in DFG syntax: false means negate.*) +fun dfg_sign true s = s + | dfg_sign false s = "not(" ^ s ^ ")" + +fun dfg_literal (Literal(pol,pred,tag)) = dfg_sign pol (string_of_predicate pred) fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))" | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")"; @@ -819,13 +827,13 @@ 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) ^ ")."; + string_of_clausename (cls_id,ax_name) ^ ").\n\n"; (*FIXME: UNUSED*) fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ - string_of_type_clsname (cls_id,ax_name,idx) ^ ")."; + string_of_type_clsname (cls_id,ax_name,idx) ^ ").\n\n"; fun dfg_clause_aux (Clause cls) = let val lits = map dfg_literal (#literals cls) @@ -887,35 +895,24 @@ 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 write_axioms (out, strs) = + (TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); + writeln_strs out strs; + TextIO.output (out, "end_of_list.\n\n")); -fun string_of_conjectures conjstr = - "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n"; +fun write_conjectures (out, strs) = + (TextIO.output (out, "list_of_clauses(conjectures,cnf).\n"); + writeln_strs out strs; + TextIO.output (out, "end_of_list.\n\n")); fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; -fun string_of_descrip name = "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" - -fun tfree_dfg_clause tfree_lit = - "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")." +fun string_of_descrip name = + "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" -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 = (space_implode "\n" axstrs) ^ "\n\n" - val (conjstrs, atfrees) = ListPair.unzip (map clause2dfg conjectures) - val tfree_clss = map tfree_dfg_clause (union_all atfrees) - val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n" - val funcstr = string_of_funcs funcs - val predstr = string_of_preds preds - in - 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 dfg_tfree_clause tfree_lit = + "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" + (*** Find all occurrences of predicates in types, terms, literals... ***) @@ -969,42 +966,34 @@ val funcs_of_clauses = Symtab.dest o (foldl add_clause_funcs Symtab.empty) - -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,...}) = arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id; 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 = 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_arLit (TConsLit(pol,(c,t,args))) = + dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")") + | dfg_of_arLit (TVarLit(pol,(c,str))) = + dfg_sign pol (c ^ "(" ^ str ^ ")") - fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls); - fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls); - +fun dfg_classrelLits sub sup = + let val tvar = "(T)" + in + "not(" ^ sub ^ tvar ^ "), " ^ sup ^ tvar + end; -(*FIXME: would this have variables in a forall? *) +fun dfg_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = + let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ + Int.toString clause_id + val lits = dfg_classrelLits (make_type_class subclass) (make_type_class superclass) + in + "clause(\nor( " ^ lits ^ ")),\n" ^ + relcls_id ^ ").\n\n" + end; fun dfg_arity_clause arcls = let val arcls_id = string_of_arClauseID arcls @@ -1013,8 +1002,35 @@ 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 ^ ")." + "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ bracket_pack all_lits ^ ")),\n" ^ + arcls_id ^ ").\n\n" + end; + +(* write out a subgoal in DFG format to the file "xxxx_N"*) +fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = + let + val conjectures = make_conjecture_clauses (map prop_of ths) + val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures) + val classrel_cls = map dfg_classrelClause classrel_clauses + val arity_cls = map dfg_arity_clause arity_clauses + val clss = conjectures @ axclauses + val funcs = (funcs_of_clauses clss) + and preds = (preds_of_clauses clss) + val out = TextIO.openOut filename + and probname = Path.pack (Path.base (Path.unpack filename)) + val axstrs_tfrees = (map clause2dfg axclauses) + val (axstrs, _) = ListPair.unzip axstrs_tfrees + val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) + val funcstr = string_of_funcs funcs + val predstr = string_of_preds preds + in + TextIO.output (out, string_of_start probname); + TextIO.output (out, string_of_descrip probname); + TextIO.output (out, string_of_symbols funcstr predstr); + write_axioms (out, axstrs); + write_conjectures (out, tfree_clss@dfg_clss); + TextIO.output (out, "end_problem.\n"); + TextIO.closeOut out end; @@ -1037,11 +1053,11 @@ fun gen_tptp_cls (cls_id,ax_name,knd,lits) = "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ - knd ^ "," ^ lits ^ ")."; + knd ^ "," ^ lits ^ ").\n"; 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 ^ "])."; + knd ^ ",[" ^ tfree_lit ^ "]).\n"; fun tptp_type_lits (Clause cls) = let val lits = map tptp_literal (#literals cls) @@ -1086,8 +1102,8 @@ end; -fun tfree_clause tfree_lit = - "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; +fun tptp_tfree_clause tfree_lit = + "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n"; fun tptp_of_arLit (TConsLit(b,(c,t,args))) = @@ -1115,7 +1131,7 @@ val all_lits = concl_lit :: prems_lits in "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ - (bracket_pack all_lits) ^ ")." + (bracket_pack all_lits) ^ ").\n" end; fun tptp_classrelLits sub sup = @@ -1129,7 +1145,26 @@ Int.toString clause_id val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass) in - "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." + "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ").\n" end; +(* write out a subgoal as tptp clauses to the file "xxxx_N"*) +fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = + let + val clss = make_conjecture_clauses (map prop_of ths) + val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) + val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss) + val classrel_cls = map tptp_classrelClause classrel_clauses + val arity_cls = map tptp_arity_clause arity_clauses + val out = TextIO.openOut filename + in + List.app (writeln_strs out o tptp_clause) axclauses; + writeln_strs out tfree_clss; + writeln_strs out tptp_clss; + writeln_strs out classrel_cls; + writeln_strs out arity_cls; + TextIO.closeOut out + end; + + end;