# HG changeset patch # User paulson # Date 1116923004 -7200 # Node ID 8a139c1557bf50a3ec8778a0edb0283f35a6ef33 # Parent 833be7f71ecdb23e723ef1eb48a971d016b8d2ce A new structure and reduced indentation diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 24 10:23:24 2005 +0200 @@ -3,6 +3,9 @@ Copyright 2004 University of Cambridge *) +structure ReconOrderClauses = +struct + (*----------------------------------------------*) (* Reorder clauses for use in binary resolution *) (*----------------------------------------------*) @@ -21,8 +24,6 @@ | numlist n = (numlist (n - 1))@[n] - - fun last(x::xs) = if xs=[] then x else last xs fun butlast []= [] | butlast(x::xs) = if xs=[] then [] else (x::(butlast xs)) @@ -38,21 +39,13 @@ then (res, xs) else - takeUntil ch xs (res@[x]) + takeUntil ch xs (res@[x]); + fun contains_eq str = inlist "=" str fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str []) - in - if ((last uptoeq) = "~") - then - false - else - true - end + in (last uptoeq) <> "~" end - - - fun get_eq_strs str = if eq_not_neq str (*not an inequality *) then let val (left, right) = takeUntil "=" str [] @@ -69,7 +62,6 @@ fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a val (x_lhs, x_rhs) = get_eq_strs x - in (a_lhs = x_rhs) andalso (a_rhs = x_lhs) end @@ -88,111 +80,107 @@ -fun var_pos_eq vars x y = String.size x = String.size y andalso - let val xs = explode x - val ys = explode y - val xsys = ListPair.zip (xs,ys) - val are_var_pairs = map (var_equiv vars) xsys - in - all_true are_var_pairs - end +fun var_pos_eq vars x y = + String.size x = String.size y andalso + let val xs = explode x + val ys = explode y + val xsys = ListPair.zip (xs,ys) + val are_var_pairs = map (var_equiv vars) xsys + in + all_true are_var_pairs + end; + +fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list + | pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = + let val y = explode x + val b = explode a + in + if b = y + then + (pos_num, symlist, nsymlist) + else + if (var_pos_eq allvars a x) + then (* Equal apart from meta-vars having different names *) + (pos_num, symlist, nsymlist) + else + if (contains_eq b) andalso (contains_eq y) + then + if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) + then (* both are equalities and equal under sym*) + (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) + else + if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y) + then (* if they're equal under not_sym *) + (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) + else + raise Not_in_list + else + raise Not_in_list + end + | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = + let val y = explode x + val b = explode a + in + if b = y + then + (pos_num, symlist, nsymlist) + + else + if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *) + then + (pos_num, symlist, nsymlist) + else + if (contains_eq b) andalso (contains_eq y) + then + if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*) + then + (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else + if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *) + then + (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) + else + pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist) + else + pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist) + + end; -fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list - |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = - let val y = explode x - val b = explode a - in - if b = y - then - (pos_num, symlist, nsymlist) - else - if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *) - then - (pos_num, symlist, nsymlist) - else - if (contains_eq b) andalso (contains_eq y) - then - if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*) - then - (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else - if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *) - then - (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) - else - raise Not_in_list - else - raise Not_in_list - - end - - | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = - let val y = explode x - val b = explode a - in - if b = y - then - (pos_num, symlist, nsymlist) - - else - if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *) - then - (pos_num, symlist, nsymlist) - else - if (contains_eq b) andalso (contains_eq y) - then - if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*) - then - (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else - if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *) - then - (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) - else - pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist) - else - pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist) - - end + (* in + if b = y + then + (pos_num, symlist, nsymlist) + else if (contains_eq b) andalso (contains_eq y) + then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*) + then if (switch_equal b y ) (* if they're equal under sym *) + then + (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) + else + pos_in_list a xs ((pos_num + 1), symlist, nsymlist) + else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *) + then if (switch_equal b y ) (* if they're equal under not_sym *) + then + (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) + else + pos_in_list a xs ((pos_num + 1), symlist, nsymlist) + else + pos_in_list a xs ((pos_num + 1), symlist, nsymlist) + else + pos_in_list a xs ((pos_num + 1), symlist, nsymlist) + else + pos_in_list a xs ((pos_num + 1), symlist, nsymlist) + end - - - - - - - (* in - if b = y - then - (pos_num, symlist, nsymlist) - else if (contains_eq b) andalso (contains_eq y) - then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*) - then if (switch_equal b y ) (* if they're equal under sym *) - then - (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) - else - pos_in_list a xs ((pos_num + 1), symlist, nsymlist) - else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *) - then if (switch_equal b y ) (* if they're equal under not_sym *) - then - (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) - else - pos_in_list a xs ((pos_num + 1), symlist, nsymlist) - else - pos_in_list a xs ((pos_num + 1), symlist, nsymlist) - else - pos_in_list a xs ((pos_num + 1), symlist, nsymlist) - else - pos_in_list a xs ((pos_num + 1), symlist, nsymlist) - end - - *) + *) (* checkorder Spass Isabelle [] *) -fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist) +fun checkorder [] strlist allvars (numlist, symlist, not_symlist) = + (numlist,symlist, not_symlist) | checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) = - let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) + let val (posnum, symlist', not_symlist') = + pos_in_list x strlist allvars (0, symlist, not_symlist) in checkorder xs strlist allvars ((numlist@[posnum]), symlist', not_symlist') end @@ -206,26 +194,28 @@ (ch >= "a" andalso ch <= "z") -fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") +fun is_alpha_space_or_neg_or_eq ch = + (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") fun lit_string sg t = - let val termstr = Sign.string_of_term sg t - val exp_term = explode termstr - in - implode(List.filter is_alpha_space_or_neg_or_eq exp_term) - end + let val termstr = Sign.string_of_term sg t + val exp_term = explode termstr + in + implode(List.filter is_alpha_space_or_neg_or_eq exp_term) + end fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm) -fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")") +fun is_alpha_space_or_neg_or_eq_or_bracket ch = + is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")") fun lit_string_bracket sg t = - let val termstr = Sign.string_of_term sg t - val exp_term = explode termstr - in - implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term) - end + let val termstr = Sign.string_of_term sg t + val exp_term = explode termstr + in + implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term) + end; fun get_meta_lits_bracket thm = map (lit_string_bracket (sign_of_thm thm)) (prems_of thm) @@ -239,14 +229,17 @@ - (* resulting thm, clause-strs in spass order, vars *) +(* resulting thm, clause-strs in spass order, vars *) fun rearrange_clause thm res_strlist allvars = - let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *) - val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[]) - val symmed = apply_rule sym symlist thm - val not_symmed = apply_rule not_sym not_symlist symmed - - in - ((rearrange_prems posns not_symmed), posns, symlist,not_symlist) - end + let val isa_strlist = get_meta_lits thm + (* change this to use Jia's code to get same looking thing as isastrlist? *) + val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[]) + val symmed = apply_rule sym symlist thm + val not_symmed = apply_rule not_sym not_symlist symmed + in + ((rearrange_prems posns not_symmed), posns, symlist,not_symlist) + end + +end; + diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/ATP/recon_parse.ML --- a/src/HOL/Tools/ATP/recon_parse.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_parse.ML Tue May 24 10:23:24 2005 +0200 @@ -436,23 +436,21 @@ dropUntilNot ch xs - - - fun remove_spaces str [] = str | remove_spaces str (x::[]) = if x = " " then str else (str^x) -| remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) [] - val (next) = dropUntilNot " " rest - in - if next = [] - then - (str^(implode first)) - else remove_spaces (str^(implode first)^" ") next - end +| remove_spaces str (x::xs) = + let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) [] + val (next) = dropUntilNot " " rest + in + if next = [] + then + (str^(implode first)) + else remove_spaces (str^(implode first)^" ") next + end fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs) @@ -461,25 +459,25 @@ fun all_spaces xs = List.filter (not_equal " " ) xs fun just_change_space [] = [] -| just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs - in - if (all_spaces newstrs = [] ) (* all type_info *) then - (clausenum, step, newstrs)::(just_change_space xs) - else - (clausenum, step, newstrs)::(just_change_space xs) - end - - - +| just_change_space ((clausenum, step, strs)::xs) = + let val newstrs = remove_space_strs strs + in + if (all_spaces newstrs = [] ) (* all type_info *) + then + (clausenum, step, newstrs)::(just_change_space xs) + else + (clausenum, step, newstrs)::(just_change_space xs) + end; fun change_space [] = [] -| change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs - in - if (all_spaces newstrs = [] ) (* all type_info *) - then - (clausenum, step, T_info, newstrs)::(change_space xs) - else - (clausenum, step, P_info, newstrs)::(change_space xs) - end +| change_space ((clausenum, step, strs)::xs) = + let val newstrs = remove_space_strs strs + in + if (all_spaces newstrs = [] ) (* all type_info *) + then + (clausenum, step, T_info, newstrs)::(change_space xs) + else + (clausenum, step, P_info, newstrs)::(change_space xs) + end end; diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 24 10:23:24 2005 +0200 @@ -107,10 +107,13 @@ (*** get a string representing the Isabelle ordered axioms ***) -fun origAx_to_string (num,(meta,thmvars)) =let val clause_strs = get_meta_lits_bracket meta - in - (string_of_int num)^"OrigAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]" - end +fun origAx_to_string (num,(meta,thmvars)) = + let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta + in + (string_of_int num)^"OrigAxiom()"^"["^ + (clause_strs_to_string clause_strs "")^"]"^"["^ + (thmvars_to_string thmvars "")^"]" + end fun origAxs_to_string [] str = str @@ -122,20 +125,20 @@ (*** get a string representing the Isabelle ordered axioms not used in the spass proof***) -fun extraAx_to_string (num, (meta,thmvars)) = let val clause_strs = get_meta_lits_bracket meta - in - (string_of_int num)^"ExtraAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]" - end - - +fun extraAx_to_string (num, (meta,thmvars)) = + let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta + in + (string_of_int num)^"ExtraAxiom()"^"["^ + (clause_strs_to_string clause_strs "")^"]"^ + "["^(thmvars_to_string thmvars "")^"]" + end; -fun extraAxs_to_string [] str = str -| extraAxs_to_string (x::xs) str = let val newstr = extraAx_to_string x - in - extraAxs_to_string xs (str^newstr) - end - - +fun extraAxs_to_string [] str = str +| extraAxs_to_string (x::xs) str = + let val newstr = extraAx_to_string x + in + extraAxs_to_string xs (str^newstr) + end; fun is_axiom ( num:int,Axiom, str) = true | is_axiom (num, _,_) = false @@ -156,7 +159,7 @@ | get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))]) *) (*FIX - should this have vars in it? *) -fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true) +fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) handle _ => false fun assoc_out_of_order a [] = raise Noassoc @@ -202,94 +205,94 @@ (* add array and table here, so can retrieve clasimp axioms *) fun get_axioms_used proof_steps thms clause_arr num_of_clauses = - let - (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) - val _ = TextIO.output (outfile, thmstring) - - val _ = TextIO.closeOut outfile*) - (* not sure why this is necessary again, but seems to be *) + let + (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) + val _ = TextIO.output (outfile, thmstring) + + val _ = TextIO.closeOut outfile*) + (* not sure why this is necessary again, but seems to be *) - val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val axioms = get_init_axioms proof_steps - val step_nums = get_step_nums axioms [] + val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) + val axioms = get_init_axioms proof_steps + val step_nums = get_step_nums axioms [] - (***********************************************) - (* here need to add the clauses from clause_arr*) - (***********************************************) + (***********************************************) + (* here need to add the clauses from clause_arr*) + (***********************************************) - (* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums - val clasimp_names = map #1 clasimp_names_cls - val clasimp_cls = map #2 clasimp_names_cls - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names - val _ = TextIO.output (outfile,clasimp_namestr) - - val _ = TextIO.closeOut outfile + (* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums + val clasimp_names = map #1 clasimp_names_cls + val clasimp_cls = map #2 clasimp_names_cls + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names + val _ = TextIO.output (outfile,clasimp_namestr) + + val _ = TextIO.closeOut outfile *) - val clauses =(*(clasimp_cls)@*)( make_clauses thms) - - val vars = map thm_vars clauses - - val distvars = distinct (fold append vars []) - val clause_terms = map prop_of clauses - val clause_frees = List.concat (map term_frees clause_terms) + val clauses =(*(clasimp_cls)@*)( make_clauses thms) + + val vars = map thm_vars clauses + + val distvars = distinct (fold append vars []) + val clause_terms = map prop_of clauses + val clause_frees = List.concat (map term_frees clause_terms) - val frees = map lit_string_with_nums clause_frees; + val frees = map lit_string_with_nums clause_frees; - val distfrees = distinct frees + val distfrees = distinct frees - val metas = map Meson.make_meta_clause clauses - val ax_strs = map #3 axioms + val metas = map Meson.make_meta_clause clauses + val ax_strs = map #3 axioms - (* literals of -all- axioms, not just those used by spass *) - val meta_strs = map get_meta_lits metas - - val metas_and_strs = ListPair.zip (metas,meta_strs) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses"))); - val _ = TextIO.output (outfile, onestr ax_strs) - - val _ = TextIO.closeOut outfile - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs"))); - val _ = TextIO.output (outfile, onestr meta_strs) - val _ = TextIO.closeOut outfile + (* literals of -all- axioms, not just those used by spass *) + val meta_strs = map ReconOrderClauses.get_meta_lits metas + + val metas_and_strs = ListPair.zip (metas,meta_strs) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses"))); + val _ = TextIO.output (outfile, onestr ax_strs) + + val _ = TextIO.closeOut outfile + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs"))); + val _ = TextIO.output (outfile, onestr meta_strs) + val _ = TextIO.closeOut outfile - (* get list of axioms as thms with their variables *) + (* get list of axioms as thms with their variables *) - val ax_metas = get_assoc_snds ax_strs metas_and_strs [] - val ax_vars = map thm_vars ax_metas - val ax_with_vars = ListPair.zip (ax_metas,ax_vars) + val ax_metas = get_assoc_snds ax_strs metas_and_strs [] + val ax_vars = map thm_vars ax_metas + val ax_with_vars = ListPair.zip (ax_metas,ax_vars) - (* get list of extra axioms as thms with their variables *) - val extra_metas = add_if_not_inlist metas ax_metas [] - val extra_vars = map thm_vars extra_metas - val extra_with_vars = if (not (extra_metas = []) ) - then - ListPair.zip (extra_metas,extra_vars) - else - [] + (* get list of extra axioms as thms with their variables *) + val extra_metas = add_if_not_inlist metas ax_metas [] + val extra_vars = map thm_vars extra_metas + val extra_with_vars = if (not (extra_metas = []) ) + then + ListPair.zip (extra_metas,extra_vars) + else + [] - (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas"))) + (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas"))) - val _ = TextIO.output (outfile, ((thmstrings ax_metas ""))) - val _ = TextIO.closeOut outfile - val foo_metas = File.sysify_path(File.tmp_path (Path.basic "foo_metas")) - val foo_metas2 = File.sysify_path(File.tmp_path (Path.basic "foo_metas2")) - val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2]) - val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))) - val ax_metas_str = TextIO.inputLine (infile) - val _ = TextIO.closeIn infile - val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*) - - in - (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas))) - end - + val _ = TextIO.output (outfile, ((thmstrings ax_metas ""))) + val _ = TextIO.closeOut outfile + val foo_metas = File.sysify_path(File.tmp_path (Path.basic "foo_metas")) + val foo_metas2 = File.sysify_path(File.tmp_path (Path.basic "foo_metas2")) + val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2]) + val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))) + val ax_metas_str = TextIO.inputLine (infile) + val _ = TextIO.closeIn infile + val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*) + + in + (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas))) + end + fun numclstr (vars, []) str = str | numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" " - in - numclstr (vars,rest) newstr - end +in +numclstr (vars,rest) newstr +end (* @@ -366,101 +369,101 @@ val dummy_tac = PRIMITIVE(fn thm => thm ); fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile"))); - (* val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) "" - val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*) - val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr)) - (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*) - val _ = TextIO.closeOut outfile + let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile"))); + (* val sign = sign_of_thm thm + val prems = prems_of thm + val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) "" + val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*) + val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr)) +(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*) + val _ = TextIO.closeOut outfile - val tokens = #1(lex proofstr) + val tokens = #1(lex proofstr) - + - (***********************************) - (* parse spass proof into datatype *) - (***********************************) + (***********************************) + (* parse spass proof into datatype *) + (***********************************) - val proof_steps1 = parse tokens - val proof_steps = just_change_space proof_steps1 + val proof_steps1 = parse tokens + val proof_steps = just_change_space proof_steps1 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) - val _ = TextIO.closeOut outfile - - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) - val _ = TextIO.closeOut outfile - (************************************) - (* recreate original subgoal as thm *) - (************************************) - - (* get axioms as correctly numbered clauses w.r.t. the Spass proof *) - (* need to get prems_of thm, then get right one of the prems, relating to whichever*) - (* subgoal this is, and turn it into meta_clauses *) - (* should prob add array and table here, so that we can get axioms*) - (* produced from the clasimpset rather than the problem *) - val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses - - (*val numcls_string = numclstr ( vars, numcls) ""*) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms") - val _ = TextIO.closeOut outfile - - (************************************) - (* translate proof *) - (************************************) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps"))); val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps ""))) - val _ = TextIO.closeOut outfile - val (newthm,proof) = translate_proof numcls proof_steps vars - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2"))); val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))) - val _ = TextIO.closeOut outfile - (***************************************************) - (* transfer necessary steps as strings to Isabelle *) - (***************************************************) - (* turn the proof into a string *) - val reconProofStr = proofs_to_string proof "" - (* do the bit for the Isabelle ordered axioms at the top *) - val ax_nums = map #1 numcls - val ax_strs = map get_meta_lits_bracket (map #2 numcls) - val numcls_strs = ListPair.zip (ax_nums,ax_strs) - val num_cls_vars = map (addvars vars) numcls_strs; - val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) "" - - val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else [] - val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) "" - val frees_str = "["^(thmvars_to_string frees "")^"]" - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile"))); + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr)) + val _ = TextIO.closeOut outfile + + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring)) + val _ = TextIO.closeOut outfile + (************************************) + (* recreate original subgoal as thm *) + (************************************) + + (* get axioms as correctly numbered clauses w.r.t. the Spass proof *) + (* need to get prems_of thm, then get right one of the prems, relating to whichever*) + (* subgoal this is, and turn it into meta_clauses *) + (* should prob add array and table here, so that we can get axioms*) + (* produced from the clasimpset rather than the problem *) + val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses + + (*val numcls_string = numclstr ( vars, numcls) ""*) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms") + val _ = TextIO.closeOut outfile + + (************************************) + (* translate proof *) + (************************************) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps"))); val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps ""))) + val _ = TextIO.closeOut outfile + val (newthm,proof) = translate_proof numcls proof_steps vars + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2"))); val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))) + val _ = TextIO.closeOut outfile + (***************************************************) + (* transfer necessary steps as strings to Isabelle *) + (***************************************************) + (* turn the proof into a string *) + val reconProofStr = proofs_to_string proof "" + (* do the bit for the Isabelle ordered axioms at the top *) + val ax_nums = map #1 numcls + val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls) + val numcls_strs = ListPair.zip (ax_nums,ax_strs) + val num_cls_vars = map (addvars vars) numcls_strs; + val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) "" + + val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else [] + val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) "" + val frees_str = "["^(thmvars_to_string frees "")^"]" + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile"))); - val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)) - val _ = TextIO.closeOut outfile - val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) - in - TextIO.output (toParent, reconstr^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, thmstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac - end - handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler"))); + val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)) + val _ = TextIO.closeOut outfile + val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) + in + TextIO.output (toParent, reconstr^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac + end + handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler"))); - val _ = TextIO.output (outfile, ("In exception handler")); - val _ = TextIO.closeOut outfile - in - TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, thmstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, goalstring^"\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - (* Attempt to prevent several signals from turning up simultaneously *) - Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac - end) + val _ = TextIO.output (outfile, ("In exception handler")); + val _ = TextIO.closeOut outfile + in + TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac + end) @@ -742,9 +745,9 @@ val axioms = get_axioms axioms_and_steps val steps = Library.drop (origax_num, axioms_and_steps) - val firststeps = butlast steps - val laststep = last steps - val goalstring = implode(butlast(explode goalstring)) + val firststeps = ReconOrderClauses.butlast steps + val laststep = ReconOrderClauses.last steps + val goalstring = implode(ReconOrderClauses.butlast(explode goalstring)) val isar_proof = ("show \""^goalstring^"\"\n")^ diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 24 10:23:24 2005 +0200 @@ -55,8 +55,9 @@ |P_info -fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ") - +fun is_alpha_space_digit_or_neg ch = + (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse + (ReconOrderClauses.is_digit ch) orelse ( ch = " "); fun lit_string_with_nums t = let val termstr = Term.string_of_term t @@ -73,30 +74,29 @@ (************************************************) fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = - let val this_axiom = valOf (assoc (clauses,clausenum)) - val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars) - val thmvars = thm_vars res - in - (res, (Axiom,clause_strs,thmvars ) ) - end - handle Option => reconstruction_failed "follow_axiom" + let val this_axiom = valOf (assoc (clauses,clausenum)) + val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars) + val thmvars = thm_vars res + in + (res, (Axiom,clause_strs,thmvars ) ) + end + handle Option => reconstruction_failed "follow_axiom" (****************************************) (* Reconstruct a binary resolution step *) (****************************************) (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *) -fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs - = let - val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1))) - val thm2 = valOf (assoc (thml,clause2)) - val res = thm1 RSN ((lit2 +1), thm2) - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) - val thmvars = thm_vars res - in - (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) - end - handle Option => reconstruction_failed "follow_binary" +fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = + let val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1))) + val thm2 = valOf (assoc (thml,clause2)) + val res = thm1 RSN ((lit2 +1), thm2) + val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars) + val thmvars = thm_vars res + in + (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) + end + handle Option => reconstruction_failed "follow_binary" @@ -105,17 +105,17 @@ (******************************************************) -fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs - = let - val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1))) - val thm2 = valOf (assoc (thml,clause2)) - val res = thm1 RSN ((lit2 +1), thm2) - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) - val thmvars = thm_vars res - in - (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) - end - handle Option => reconstruction_failed "follow_mrr" +fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = + let val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1))) + val thm2 = valOf (assoc (thml,clause2)) + val res = thm1 RSN ((lit2 +1), thm2) + val (res', numlist, symlist, nsymlist) = + (ReconOrderClauses.rearrange_clause res clause_strs allvars) + val thmvars = thm_vars res + in + (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) + end + handle Option => reconstruction_failed "follow_mrr" (*******************************************) @@ -123,11 +123,13 @@ (*******************************************) fun mksubstlist [] sublist = sublist - |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b - val avar = Var(a,vartype) - val newlist = ((avar,b)::sublist) in - mksubstlist rest newlist - end; + |mksubstlist ((a, (_, b)) :: rest) sublist = + let val vartype = type_of b + val avar = Var(a,vartype) + val newlist = ((avar,b)::sublist) + in + mksubstlist rest newlist + end; (* based on Tactic.distinct_subgoals_tac *) @@ -135,7 +137,7 @@ let val (frozth,thawfn) = freeze_thaw state val froz_prems = cprems_of frozth val assumed = implies_elim_list frozth (map assume froz_prems) - val new_prems = remove_nth lit froz_prems + val new_prems = ReconOrderClauses.remove_nth lit froz_prems val implied = implies_intr_list new_prems assumed in Seq.single (thawfn implied) @@ -150,44 +152,46 @@ (*************************************) (*FIXME: share code with that in Tools/reconstruction.ML*) -fun follow_factor clause lit1 lit2 allvars thml clause_strs= - let - val th = valOf (assoc (thml,clause)) - val prems = prems_of th - val sign = sign_of_thm th - val fac1 = get_nth (lit1+1) prems - val fac2 = get_nth (lit2+1) prems - val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)]) - val newenv = getnewenv unif_env - val envlist = Envir.alist_of newenv - - val (t1,t2)::_ = mksubstlist envlist [] - in - if (is_Var t1) - then - let - val str1 = lit_string_with_nums t1; - val str2 = lit_string_with_nums t2; - val facthm = read_instantiate [(str1,str2)] th; - val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) - val thmvars = thm_vars res' - in - (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars)) - end - else - let - val str2 = lit_string_with_nums t1; - val str1 = lit_string_with_nums t2; - val facthm = read_instantiate [(str1,str2)] th; - val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) - val thmvars = thm_vars res' - in - (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) - end - end - handle Option => reconstruction_failed "follow_factor" +fun follow_factor clause lit1 lit2 allvars thml clause_strs = + let + val th = valOf (assoc (thml,clause)) + val prems = prems_of th + val sign = sign_of_thm th + val fac1 = ReconOrderClauses.get_nth (lit1+1) prems + val fac2 = ReconOrderClauses.get_nth (lit2+1) prems + val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)]) + val newenv = getnewenv unif_env + val envlist = Envir.alist_of newenv + + val (t1,t2)::_ = mksubstlist envlist [] + in + if (is_Var t1) + then + let + val str1 = lit_string_with_nums t1; + val str2 = lit_string_with_nums t2; + val facthm = read_instantiate [(str1,str2)] th; + val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) + val (res', numlist, symlist, nsymlist) = + ReconOrderClauses.rearrange_clause res clause_strs allvars + val thmvars = thm_vars res' + in + (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars)) + end + else + let + val str2 = lit_string_with_nums t1; + val str1 = lit_string_with_nums t2; + val facthm = read_instantiate [(str1,str2)] th; + val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) + val (res', numlist, symlist, nsymlist) = + ReconOrderClauses.rearrange_clause res clause_strs allvars + val thmvars = thm_vars res' + in + (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) + end + end + handle Option => reconstruction_failed "follow_factor" @@ -216,28 +220,29 @@ val rev_ssubst = rotate_prems 1 ssubst; -fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= - let - val th1 = valOf (assoc (thml,clause1)) - val th2 = valOf (assoc (thml,clause2)) - val eq_lit_th = select_literal (lit1+1) th1 - val mod_lit_th = select_literal (lit2+1) th2 - val eqsubst = eq_lit_th RSN (2,rev_subst) - val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) - val newth' =negate_head newth - val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars - handle Not_in_list => let - val mod_lit_th' = mod_lit_th RS not_sym - val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst) - val newth' =negate_head newth - in - (rearrange_clause newth' clause_strs allvars) - end) - val thmvars = thm_vars res - in - (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) - end - handle Option => reconstruction_failed "follow_standard_para" +fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = + let + val th1 = valOf (assoc (thml,clause1)) + val th2 = valOf (assoc (thml,clause2)) + val eq_lit_th = select_literal (lit1+1) th1 + val mod_lit_th = select_literal (lit2+1) th2 + val eqsubst = eq_lit_th RSN (2,rev_subst) + val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) + val newth' =negate_head newth + val (res, numlist, symlist, nsymlist) = + (ReconOrderClauses.rearrange_clause newth' clause_strs allvars + handle Not_in_list => + let val mod_lit_th' = mod_lit_th RS not_sym + val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst) + val newth' =negate_head newth + in + ReconOrderClauses.rearrange_clause newth' clause_strs allvars + end) + val thmvars = thm_vars res + in + (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) + end + handle Option => reconstruction_failed "follow_standard_para" (* fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= @@ -293,26 +298,24 @@ (* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *) (* changed negate_nead to negate_head here too*) (* clause1, lit1 is thing to rewrite with *) -fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= - - let val th1 = valOf (assoc (thml,clause1)) - val th2 = valOf (assoc (thml,clause2)) - val eq_lit_th = select_literal (lit1+1) th1 - val mod_lit_th = select_literal (lit2+1) th2 - val eqsubst = eq_lit_th RSN (2,rev_subst) - val eq_lit_prem_num = length (prems_of eq_lit_th) - val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2) - val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 -eqsubst) - - val newthm = negate_head newth - val newthm' = delete_assumps eq_lit_prem_num newthm - val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars) - val thmvars = thm_vars res - in - (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) - end - handle Option => reconstruction_failed "follow_rewrite" +fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = + let val th1 = valOf (assoc (thml,clause1)) + val th2 = valOf (assoc (thml,clause2)) + val eq_lit_th = select_literal (lit1+1) th1 + val mod_lit_th = select_literal (lit2+1) th2 + val eqsubst = eq_lit_th RSN (2,rev_subst) + val eq_lit_prem_num = length (prems_of eq_lit_th) + val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2) + val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) + val newthm = negate_head newth + val newthm' = delete_assumps eq_lit_prem_num newthm + val (res, numlist, symlist, nsymlist) = + ReconOrderClauses.rearrange_clause newthm clause_strs allvars + val thmvars = thm_vars res + in + (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) + end + handle Option => reconstruction_failed "follow_rewrite" @@ -321,17 +324,18 @@ (*****************************************) -fun follow_obvious (clause1, lit1) allvars thml clause_strs= - let val th1 = valOf (assoc (thml,clause1)) - val prems1 = prems_of th1 - val newthm = refl RSN ((lit1+ 1), th1) - handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1))) - val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars) - val thmvars = thm_vars res - in - (res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) - end - handle Option => reconstruction_failed "follow_obvious" +fun follow_obvious (clause1, lit1) allvars thml clause_strs = + let val th1 = valOf (assoc (thml,clause1)) + val prems1 = prems_of th1 + val newthm = refl RSN ((lit1+ 1), th1) + handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1))) + val (res, numlist, symlist, nsymlist) = + ReconOrderClauses.rearrange_clause newthm clause_strs allvars + val thmvars = thm_vars res + in + (res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) + end + handle Option => reconstruction_failed "follow_obvious" (**************************************************************************************) (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*) @@ -436,28 +440,29 @@ *) -fun replace_clause_strs [] recons newrecons= (newrecons) -| replace_clause_strs ((thmnum, thm)::thml) ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = - let val new_clause_strs = get_meta_lits_bracket thm - in - replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons) - end +fun replace_clause_strs [] recons newrecons = (newrecons) +| replace_clause_strs ((thmnum, thm)::thml) + ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = + let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm + in + replace_clause_strs thml recons + ((clausenum,(step,new_clause_strs,thmvars))::newrecons) + end fun follow clauses [] allvars thml recons = - let - val new_recons = replace_clause_strs thml recons [] - in - ((snd( hd thml)), new_recons) - end - - | follow clauses (h::t) allvars thml recons - = let - val (thml', recons') = follow_line clauses allvars thml h recons - val (thm, recons_list) = follow clauses t allvars thml' recons' - in - (thm,recons_list) - end + let + val new_recons = replace_clause_strs thml recons [] + in + (#2(hd thml), new_recons) + end + | follow clauses (h::t) allvars thml recons = + let + val (thml', recons') = follow_line clauses allvars thml h recons + val (thm, recons_list) = follow clauses t allvars thml' recons' + in + (thm,recons_list) + end @@ -481,4 +486,5 @@ fun remove_tinfo [] = [] -| remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs) + | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = + (clausenum, step , newstrs)::(remove_tinfo xs) diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 24 10:23:24 2005 +0200 @@ -12,18 +12,10 @@ structure ResClasimp : RES_CLASIMP = struct -fun has_name th = not((Thm.name_of_thm th )= "") -fun has_name_pair (a,b) = not_equal a ""; - -fun stick [] = [] -| stick (x::xs) = x@(stick xs ) -fun filterlist p [] = [] -| filterlist p (x::xs) = if p x - then - (x::(filterlist p xs)) - else - filterlist p xs +fun has_name th = ((Thm.name_of_thm th) <> "") + +fun has_name_pair (a,b) = (a <> ""); (* changed, now it also finds out the name of the theorem. *) @@ -37,73 +29,64 @@ | concat_with_stop [x] = x | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs; -fun remove_symb str = if String.isPrefix "List.op @." str - then - ((String.substring(str,0,5))^(String.extract (str, 10, NONE))) - else - str - -fun remove_spaces str = let val strlist = String.tokens Char.isSpace str - val spaceless = concat strlist - val strlist' = String.tokens Char.isPunct spaceless - in - concat_with_stop strlist' - end +fun remove_symb str = + if String.isPrefix "List.op @." str + then ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE))) + else str; -fun remove_symb_pair (str, thm) = let val newstr = remove_symb str - in - (newstr, thm) - end - +fun remove_spaces str = + let val strlist = String.tokens Char.isSpace str + val spaceless = concat strlist + val strlist' = String.tokens Char.isPunct spaceless + in + concat_with_stop strlist' + end -fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str - in - (newstr, thm) - end +fun remove_symb_pair (str, thm) = (remove_symb str, thm); - +fun remove_spaces_pair (str, thm) = (remove_spaces str, thm); (*Insert th into the result provided the name is not "".*) fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths; -fun write_out_clasimp filename = let - val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); - val named_claset = filterlist has_name_pair claset_rules; - val claset_names = map remove_spaces_pair (named_claset) - val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []); - +fun write_out_clasimp filename = + let val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); + val named_claset = List.filter has_name_pair claset_rules; + val claset_names = map remove_spaces_pair (named_claset) + val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []); - val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context()); - val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules); - val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); + val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context()); + val named_simpset = + map remove_spaces_pair (List.filter has_name_pair simpset_rules) + val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); - val cls_thms = (claset_cls_thms@simpset_cls_thms); - val cls_thms_list = stick cls_thms; + val cls_thms = (claset_cls_thms@simpset_cls_thms); + val cls_thms_list = List.concat cls_thms; - (*********************************************************) - (* create array and put clausename, number pairs into it *) - (*********************************************************) - val num_of_clauses = 0; - val clause_arr = Array.fromList cls_thms_list; - - val num_of_clauses= (List.length cls_thms_list); + (*********************************************************) + (* create array and put clausename, number pairs into it *) + (*********************************************************) + val num_of_clauses = 0; + val clause_arr = Array.fromList cls_thms_list; + + val num_of_clauses = List.length cls_thms_list; - (*************************************************) - (* Write out clauses as tptp strings to filename *) - (*************************************************) - val clauses = map #1(cls_thms_list); - val cls_tptp_strs = map ResClause.tptp_clause clauses; - (* list of lists of tptp string clauses *) - val stick_clasrls = stick cls_tptp_strs; - val out = TextIO.openOut filename; - val _= ResLib.writeln_strs out stick_clasrls; - val _= TextIO.flushOut out; - val _= TextIO.closeOut out - in - (clause_arr, num_of_clauses) - end; + (*************************************************) + (* Write out clauses as tptp strings to filename *) + (*************************************************) + val clauses = map #1(cls_thms_list); + val cls_tptp_strs = map ResClause.tptp_clause clauses; + (* list of lists of tptp string clauses *) + val stick_clasrls = List.concat cls_tptp_strs; + val out = TextIO.openOut filename; + val _= ResLib.writeln_strs out stick_clasrls; + val _= TextIO.flushOut out; + val _= TextIO.closeOut out + in + (clause_arr, num_of_clauses) + end; end; diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Tue May 24 10:23:24 2005 +0200 @@ -164,44 +164,45 @@ fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) | callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) = - let val dfg_dir = File.tmp_path (Path.basic "dfg"); - (*** need to check here if the directory exists and, if not, create it***) - val outfile = TextIO.openAppend(File.sysify_path - (File.tmp_path (Path.basic"thmstring_in_watcher"))); val _ = TextIO.output (outfile, - (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile - (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) - val probID = last(explode probfile) - val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) - (*** only include problem and clasimp for the moment, not sure how to refer to ***) - (*** hyps/local axioms just now ***) - val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) - val dfg_create =if File.exists dfg_dir - then - ((warning("dfg dir exists"));()) - else - File.mkdir dfg_dir; - - val dfg_path = File.sysify_path dfg_dir; - val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) - (*val _ = Posix.Process.wait ()*) - (*val _ =Unix.reap exec_tptp2x*) - val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" - - in - goals_being_watched := (!goals_being_watched) + 1; - Posix.Process.sleep(Time.fromSeconds 1); - (warning ("probfile is: "^probfile)); - (warning("dfg file is: "^newfile)); - (warning ("wholefile is: "^(File.sysify_path wholefile))); - sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n")); -(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) - TextIO.flushOut toWatcherStr; - Unix.reap exec_tptp2x; - - callResProvers (toWatcherStr,args) - - end + let val dfg_dir = File.tmp_path (Path.basic "dfg"); + (*** need to check here if the directory exists and, if not, create it***) + val outfile = TextIO.openAppend(File.sysify_path + (File.tmp_path (Path.basic"thmstring_in_watcher"))); + val _ = TextIO.output (outfile, + (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")) + val _ = TextIO.closeOut outfile + (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) + val probID = ReconOrderClauses.last(explode probfile) + val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) + (*** only include problem and clasimp for the moment, not sure how to refer to ***) + (*** hyps/local axioms just now ***) + val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) + val dfg_create =if File.exists dfg_dir + then + ((warning("dfg dir exists"));()) + else + File.mkdir dfg_dir; + + val dfg_path = File.sysify_path dfg_dir; + val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) + (*val _ = Posix.Process.wait ()*) + (*val _ =Unix.reap exec_tptp2x*) + val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" + + in + goals_being_watched := (!goals_being_watched) + 1; + Posix.Process.sleep(Time.fromSeconds 1); + (warning ("probfile is: "^probfile)); + (warning("dfg file is: "^newfile)); + (warning ("wholefile is: "^(File.sysify_path wholefile))); + sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n")); + (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) + TextIO.flushOut toWatcherStr; + Unix.reap exec_tptp2x; + + callResProvers (toWatcherStr,args) + + end (* fun callResProversStr (toWatcherStr, []) = "End of calls\n" @@ -327,374 +328,375 @@ -fun setupWatcher (thm,clause_arr, num_of_clauses) = let - (** pipes for communication between parent and watcher **) - val p1 = Posix.IO.pipe () - val p2 = Posix.IO.pipe () - fun closep () = ( - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p1); - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p2) - ) - (***********************************************************) - (****** fork a watcher process and get it set up and going *) - (***********************************************************) - fun startWatcher (procList) = - (case Posix.Process.fork() (***************************************) - of SOME pid => pid (* parent - i.e. main Isabelle process *) - (***************************************) - - (*************************) - | NONE => let (* child - i.e. watcher *) - val oldchildin = #infd p1 (*************************) - val fromParent = Posix.FileSys.wordToFD 0w0 - val oldchildout = #outfd p2 - val toParent = Posix.FileSys.wordToFD 0w1 - val fromParentIOD = Posix.FileSys.fdToIOD fromParent - val fromParentStr = openInFD ("_exec_in_parent", fromParent) - val toParentStr = openOutFD ("_exec_out_parent", toParent) - val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); - (* tracing *) - (*val tenth_ax = fst( Array.sub(clause_arr, 1)) - val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) - val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) - val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) - val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) - val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) - *) - (*val goalstr = string_of_thm (the_goal) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher"))); - val _ = TextIO.output (outfile,goalstr ) - val _ = TextIO.closeOut outfile*) - fun killChildren [] = () - | killChildren (child_handle::children) = (killChild child_handle; killChildren children) +fun setupWatcher (thm,clause_arr, num_of_clauses) = + let + (** pipes for communication between parent and watcher **) + val p1 = Posix.IO.pipe () + val p2 = Posix.IO.pipe () + fun closep () = ( + Posix.IO.close (#outfd p1); + Posix.IO.close (#infd p1); + Posix.IO.close (#outfd p2); + Posix.IO.close (#infd p2) + ) + (***********************************************************) + (****** fork a watcher process and get it set up and going *) + (***********************************************************) + fun startWatcher (procList) = + (case Posix.Process.fork() (***************************************) + of SOME pid => pid (* parent - i.e. main Isabelle process *) + (***************************************) + + (*************************) + | NONE => let (* child - i.e. watcher *) + val oldchildin = #infd p1 (*************************) + val fromParent = Posix.FileSys.wordToFD 0w0 + val oldchildout = #outfd p2 + val toParent = Posix.FileSys.wordToFD 0w1 + val fromParentIOD = Posix.FileSys.fdToIOD fromParent + val fromParentStr = openInFD ("_exec_in_parent", fromParent) + val toParentStr = openOutFD ("_exec_out_parent", toParent) + val sign = sign_of_thm thm + val prems = prems_of thm + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) + val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); + (* tracing *) + (*val tenth_ax = fst( Array.sub(clause_arr, 1)) + val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) + val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) + val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) + val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) + val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) + *) + (*val goalstr = string_of_thm (the_goal) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher"))); + val _ = TextIO.output (outfile,goalstr ) + val _ = TextIO.closeOut outfile*) + fun killChildren [] = () + | killChildren (child_handle::children) = (killChild child_handle; killChildren children) - - - (*************************************************************) - (* take an instream and poll its underlying reader for input *) - (*************************************************************) + + + (*************************************************************) + (* take an instream and poll its underlying reader for input *) + (*************************************************************) - fun pollParentInput () = - - let val pd = OS.IO.pollDesc (fromParentIOD) - in - if (isSome pd ) then - let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) - in - if null pdl - then - NONE - else if (OS.IO.isIn (hd pdl)) - then - (SOME ( getCmds (toParentStr, fromParentStr, []))) - else - NONE - end - else - NONE - end - - + fun pollParentInput () = + + let val pd = OS.IO.pollDesc (fromParentIOD) + in + if (isSome pd ) then + let val pd' = OS.IO.pollIn (valOf pd) + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) + in + if null pdl + then + NONE + else if (OS.IO.isIn (hd pdl)) + then + (SOME ( getCmds (toParentStr, fromParentStr, []))) + else + NONE + end + else + NONE + end + + - fun pollChildInput (fromStr) = - let val iod = getInIoDesc fromStr - in - if isSome iod - then - let val pd = OS.IO.pollDesc (valOf iod) - in - if (isSome pd ) then - let val pd' = OS.IO.pollIn (valOf pd) - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) - in - if null pdl - then - NONE - else if (OS.IO.isIn (hd pdl)) - then - SOME (getCmd (TextIO.inputLine fromStr)) - else - NONE - end - else - NONE - end - else - NONE - end + fun pollChildInput (fromStr) = + let val iod = getInIoDesc fromStr + in + if isSome iod + then + let val pd = OS.IO.pollDesc (valOf iod) + in + if (isSome pd ) then + let val pd' = OS.IO.pollIn (valOf pd) + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) + in + if null pdl + then + NONE + else if (OS.IO.isIn (hd pdl)) + then + SOME (getCmd (TextIO.inputLine fromStr)) + else + NONE + end + else + NONE + end + else + NONE + end - (****************************************************************************) - (* Check all vampire processes currently running for output *) - (****************************************************************************) - (*********************************) - fun checkChildren ([], toParentStr) = [] (*** no children to check ********) - (*********************************) - | checkChildren ((childProc::otherChildren), toParentStr) = - let val (childInput,childOutput) = cmdstreamsOf childProc - val child_handle= cmdchildHandle childProc - (* childCmd is the .dfg file that the problem is in *) - val childCmd = fst(snd (cmdchildInfo childProc)) - (* now get the number of the subgoal from the filename *) - val sg_num = int_of_string(get_nth 5 (rev(explode childCmd))) - val childIncoming = pollChildInput childInput - val parentID = Posix.ProcEnv.getppid() - val prover = cmdProver childProc - val thmstring = cmdThm childProc - val sign = sign_of_thm thm - val prems = prems_of thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - val _ = (warning ("subgoals forked to checkChildren: "^prems_string)); - val goalstring = cmdGoal childProc - - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms"))); - val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) ) - val _ = TextIO.closeOut outfile - in - if (isSome childIncoming) - then - (* check here for prover label on child*) - - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); - val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) ) - val _ = TextIO.closeOut outfile - val childDone = (case prover of - (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) - in - if childDone (**********************************************) - then (* child has found a proof and transferred it *) - (**********************************************) + (****************************************************************************) + (* Check all vampire processes currently running for output *) + (****************************************************************************) + (*********************************) + fun checkChildren ([], toParentStr) = [] (*** no children to check ********) + (*********************************) + | checkChildren ((childProc::otherChildren), toParentStr) = + let val (childInput,childOutput) = cmdstreamsOf childProc + val child_handle= cmdchildHandle childProc + (* childCmd is the .dfg file that the problem is in *) + val childCmd = fst(snd (cmdchildInfo childProc)) + (* now get the number of the subgoal from the filename *) + val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) + val childIncoming = pollChildInput childInput + val parentID = Posix.ProcEnv.getppid() + val prover = cmdProver childProc + val thmstring = cmdThm childProc + val sign = sign_of_thm thm + val prems = prems_of thm + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) + val _ = (warning ("subgoals forked to checkChildren: "^prems_string)); + val goalstring = cmdGoal childProc + + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms"))); + val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) ) + val _ = TextIO.closeOut outfile + in + if (isSome childIncoming) + then + (* check here for prover label on child*) + + let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); + val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) ) + val _ = TextIO.closeOut outfile + val childDone = (case prover of + (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) + in + if childDone (**********************************************) + then (* child has found a proof and transferred it *) + (**********************************************) - (**********************************************) - (* Remove this child and go on to check others*) - (**********************************************) - ( Unix.reap child_handle; - checkChildren(otherChildren, toParentStr)) - else - (**********************************************) - (* Keep this child and go on to check others *) - (**********************************************) + (**********************************************) + (* Remove this child and go on to check others*) + (**********************************************) + ( Unix.reap child_handle; + checkChildren(otherChildren, toParentStr)) + else + (**********************************************) + (* Keep this child and go on to check others *) + (**********************************************) - (childProc::(checkChildren (otherChildren, toParentStr))) - end - else - let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); - val _ = TextIO.output (outfile,"No child output " ) - val _ = TextIO.closeOut outfile - in - (childProc::(checkChildren (otherChildren, toParentStr))) - end - end + (childProc::(checkChildren (otherChildren, toParentStr))) + end + else + let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); + val _ = TextIO.output (outfile,"No child output " ) + val _ = TextIO.closeOut outfile + in + (childProc::(checkChildren (otherChildren, toParentStr))) + end + end - - (********************************************************************) - (* call resolution processes *) - (* settings should be a list of strings *) - (* e.g. ["-t 300", "-m 100000"] *) - (* takes list of (string, string, string list, string)list proclist *) - (********************************************************************) + + (********************************************************************) + (* call resolution processes *) + (* settings should be a list of strings *) + (* e.g. ["-t 300", "-m 100000"] *) + (* takes list of (string, string, string list, string)list proclist *) + (********************************************************************) - (*** add subgoal id num to this *) - fun execCmds [] procList = procList - | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = - if (prover = "spass") - then - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) - val (instr, outstr)=Unix.streamsOf childhandle - val newProcList = (((CMDPROC{ - prover = prover, - cmd = file, - thmstring = thmstring, - goalstring = goalstring, - proc_handle = childhandle, - instr = instr, - outstr = outstr })::procList)) - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child"))); - val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file ) - val _ = TextIO.closeOut outfile - in - execCmds cmds newProcList - end - else - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) - val (instr, outstr)=Unix.streamsOf childhandle - val newProcList = (((CMDPROC{ - prover = prover, - cmd = file, - thmstring = thmstring, - goalstring = goalstring, - proc_handle = childhandle, - instr = instr, - outstr = outstr })::procList)) - in - execCmds cmds newProcList - end +(*** add subgoal id num to this *) + fun execCmds [] procList = procList + | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = + if (prover = "spass") + then + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ + prover = prover, + cmd = file, + thmstring = thmstring, + goalstring = goalstring, + proc_handle = childhandle, + instr = instr, + outstr = outstr })::procList)) + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child"))); + val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file ) + val _ = TextIO.closeOut outfile + in + execCmds cmds newProcList + end + else + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ + prover = prover, + cmd = file, + thmstring = thmstring, + goalstring = goalstring, + proc_handle = childhandle, + instr = instr, + outstr = outstr })::procList)) + in + execCmds cmds newProcList + end - (****************************************) - (* call resolution processes remotely *) - (* settings should be a list of strings *) - (* e.g. ["-t 300", "-m 100000"] *) - (****************************************) - - (* fun execRemoteCmds [] procList = procList - | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = - let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) - in - execRemoteCmds cmds newProcList - end + (****************************************) + (* call resolution processes remotely *) + (* settings should be a list of strings *) + (* e.g. ["-t 300", "-m 100000"] *) + (****************************************) + + (* fun execRemoteCmds [] procList = procList + | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = + let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) + in + execRemoteCmds cmds newProcList + end *) - fun printList (outStr, []) = () - | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) + fun printList (outStr, []) = () + | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) - (**********************************************) - (* Watcher Loop *) - (**********************************************) + (**********************************************) + (* Watcher Loop *) + (**********************************************) + - - fun keepWatching (toParentStr, fromParentStr,procList) = - let fun loop (procList) = - ( - let val cmdsFromIsa = pollParentInput () - fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); - TextIO.flushOut toParentStr; - killChildren (map (cmdchildHandle) procList); - ()) - - in - (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) - (**********************************) - if (isSome cmdsFromIsa) then (* deal with input from Isabelle *) - ( (**********************************) - if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) - then - ( - let val child_handles = map cmdchildHandle procList - in - killChildren child_handles; - (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) - end - - ) - else - ( - if ((length procList)<10) (********************) - then (* Execute locally *) - ( (********************) - let - val newProcList = execCmds (valOf cmdsFromIsa) procList - val parentID = Posix.ProcEnv.getppid() - val newProcList' =checkChildren (newProcList, toParentStr) - in - (*Posix.Process.sleep (Time.fromSeconds 1);*) - loop (newProcList') - end - ) - else (*********************************) - (* Execute remotely *) - (* (actually not remote for now )*) - ( (*********************************) - let - val newProcList = execCmds (valOf cmdsFromIsa) procList - val parentID = Posix.ProcEnv.getppid() - val newProcList' =checkChildren (newProcList, toParentStr) - in - (*Posix.Process.sleep (Time.fromSeconds 1);*) - loop (newProcList') - end - ) + fun keepWatching (toParentStr, fromParentStr,procList) = + let fun loop (procList) = + ( + let val cmdsFromIsa = pollParentInput () + fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); + TextIO.flushOut toParentStr; + killChildren (map (cmdchildHandle) procList); + ()) + + in + (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) + (**********************************) + if (isSome cmdsFromIsa) then (* deal with input from Isabelle *) + ( (**********************************) + if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) + then + ( + let val child_handles = map cmdchildHandle procList + in + killChildren child_handles; + (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) + end + + ) + else + ( + if ((length procList)<10) (********************) + then (* Execute locally *) + ( (********************) + let + val newProcList = execCmds (valOf cmdsFromIsa) procList + val parentID = Posix.ProcEnv.getppid() + val newProcList' =checkChildren (newProcList, toParentStr) + in + (*Posix.Process.sleep (Time.fromSeconds 1);*) + loop (newProcList') + end + ) + else (*********************************) + (* Execute remotely *) + (* (actually not remote for now )*) + ( (*********************************) + let + val newProcList = execCmds (valOf cmdsFromIsa) procList + val parentID = Posix.ProcEnv.getppid() + val newProcList' =checkChildren (newProcList, toParentStr) + in + (*Posix.Process.sleep (Time.fromSeconds 1);*) + loop (newProcList') + end + ) - ) - ) (******************************) - else (* No new input from Isabelle *) - (******************************) - ( let val newProcList = checkChildren ((procList), toParentStr) - in - Posix.Process.sleep (Time.fromSeconds 1); - loop (newProcList) - end - - ) - end) - in - loop (procList) - end - - - in - (***************************) - (*** Sort out pipes ********) - (***************************) + ) + ) (******************************) + else (* No new input from Isabelle *) + (******************************) + ( let val newProcList = checkChildren ((procList), toParentStr) + in + Posix.Process.sleep (Time.fromSeconds 1); + loop (newProcList) + end + + ) + end) + in + loop (procList) + end + + + in + (***************************) + (*** Sort out pipes ********) + (***************************) - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p2); - Posix.IO.dup2{old = oldchildin, new = fromParent}; - Posix.IO.close oldchildin; - Posix.IO.dup2{old = oldchildout, new = toParent}; - Posix.IO.close oldchildout; + Posix.IO.close (#outfd p1); + Posix.IO.close (#infd p2); + Posix.IO.dup2{old = oldchildin, new = fromParent}; + Posix.IO.close oldchildin; + Posix.IO.dup2{old = oldchildout, new = toParent}; + Posix.IO.close oldchildout; - (***************************) - (* start the watcher loop *) - (***************************) - keepWatching (toParentStr, fromParentStr, procList); + (***************************) + (* start the watcher loop *) + (***************************) + keepWatching (toParentStr, fromParentStr, procList); - (****************************************************************************) - (* fake return value - actually want the watcher to loop until killed *) - (****************************************************************************) - Posix.Process.wordToPid 0w0 - - end); - (* end case *) + (****************************************************************************) + (* fake return value - actually want the watcher to loop until killed *) + (****************************************************************************) + Posix.Process.wordToPid 0w0 + + end); + (* end case *) - val _ = TextIO.flushOut TextIO.stdOut + val _ = TextIO.flushOut TextIO.stdOut - (*******************************) - (*** set watcher going ********) - (*******************************) + (*******************************) + (*** set watcher going ********) + (*******************************) - val procList = [] - val pid = startWatcher (procList) - (**************************************************) - (* communication streams to watcher *) - (**************************************************) + val procList = [] + val pid = startWatcher (procList) + (**************************************************) + (* communication streams to watcher *) + (**************************************************) - val instr = openInFD ("_exec_in", #infd p2) - val outstr = openOutFD ("_exec_out", #outfd p1) - - in - (*******************************) - (* close the child-side fds *) - (*******************************) - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p1); - (* set the fds close on exec *) - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - - (*******************************) - (* return value *) - (*******************************) - PROC{pid = pid, - instr = instr, - outstr = outstr - } - end; + val instr = openInFD ("_exec_in", #infd p2) + val outstr = openOutFD ("_exec_out", #outfd p1) + + in + (*******************************) + (* close the child-side fds *) + (*******************************) + Posix.IO.close (#outfd p2); + Posix.IO.close (#infd p1); + (* set the fds close on exec *) + Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); + Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); + + (*******************************) + (* return value *) + (*******************************) + PROC{pid = pid, + instr = instr, + outstr = outstr + } + end; diff -r 833be7f71ecd -r 8a139c1557bf src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue May 24 07:43:38 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue May 24 10:23:24 2005 +0200 @@ -245,19 +245,18 @@ (**********************************************) fun isar_atp_goal' thm k n tfree_lits (childin, childout, pid) = - if (k > n) - then () - else - (let val prems = prems_of thm - val sg_term = get_nth n prems - val thmstring = string_of_thm thm - in - - (warning("in isar_atp_goal'")); - (warning("thmstring in isar_atp_goal': "^thmstring)); - isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; - isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) - end); + if (k > n) + then () + else + let val prems = prems_of thm + val sg_term = ReconOrderClauses.get_nth n prems + val thmstring = string_of_thm thm + in + (warning("in isar_atp_goal'")); + (warning("thmstring in isar_atp_goal': "^thmstring)); + isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; + isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) + end; fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) =