1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 24 07:43:38 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 24 10:23:24 2005 +0200
1.3 @@ -3,6 +3,9 @@
1.4 Copyright 2004 University of Cambridge
1.5 *)
1.6
1.7 +structure ReconOrderClauses =
1.8 +struct
1.9 +
1.10 (*----------------------------------------------*)
1.11 (* Reorder clauses for use in binary resolution *)
1.12 (*----------------------------------------------*)
1.13 @@ -21,8 +24,6 @@
1.14 | numlist n = (numlist (n - 1))@[n]
1.15
1.16
1.17 -
1.18 -
1.19 fun last(x::xs) = if xs=[] then x else last xs
1.20 fun butlast []= []
1.21 | butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
1.22 @@ -38,21 +39,13 @@
1.23 then
1.24 (res, xs)
1.25 else
1.26 - takeUntil ch xs (res@[x])
1.27 + takeUntil ch xs (res@[x]);
1.28 +
1.29 fun contains_eq str = inlist "=" str
1.30
1.31 fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
1.32 - in
1.33 - if ((last uptoeq) = "~")
1.34 - then
1.35 - false
1.36 - else
1.37 - true
1.38 - end
1.39 + in (last uptoeq) <> "~" end
1.40
1.41 -
1.42 -
1.43 -
1.44 fun get_eq_strs str = if eq_not_neq str (*not an inequality *)
1.45 then
1.46 let val (left, right) = takeUntil "=" str []
1.47 @@ -69,7 +62,6 @@
1.48
1.49 fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
1.50 val (x_lhs, x_rhs) = get_eq_strs x
1.51 -
1.52 in
1.53 (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
1.54 end
1.55 @@ -88,111 +80,107 @@
1.56
1.57
1.58
1.59 -fun var_pos_eq vars x y = String.size x = String.size y andalso
1.60 - let val xs = explode x
1.61 - val ys = explode y
1.62 - val xsys = ListPair.zip (xs,ys)
1.63 - val are_var_pairs = map (var_equiv vars) xsys
1.64 - in
1.65 - all_true are_var_pairs
1.66 - end
1.67 +fun var_pos_eq vars x y =
1.68 + String.size x = String.size y andalso
1.69 + let val xs = explode x
1.70 + val ys = explode y
1.71 + val xsys = ListPair.zip (xs,ys)
1.72 + val are_var_pairs = map (var_equiv vars) xsys
1.73 + in
1.74 + all_true are_var_pairs
1.75 + end;
1.76 +
1.77 +fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list
1.78 + | pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) =
1.79 + let val y = explode x
1.80 + val b = explode a
1.81 + in
1.82 + if b = y
1.83 + then
1.84 + (pos_num, symlist, nsymlist)
1.85 + else
1.86 + if (var_pos_eq allvars a x)
1.87 + then (* Equal apart from meta-vars having different names *)
1.88 + (pos_num, symlist, nsymlist)
1.89 + else
1.90 + if (contains_eq b) andalso (contains_eq y)
1.91 + then
1.92 + if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y )
1.93 + then (* both are equalities and equal under sym*)
1.94 + (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
1.95 + else
1.96 + if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y)
1.97 + then (* if they're equal under not_sym *)
1.98 + (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
1.99 + else
1.100 + raise Not_in_list
1.101 + else
1.102 + raise Not_in_list
1.103 + end
1.104 + | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) =
1.105 + let val y = explode x
1.106 + val b = explode a
1.107 + in
1.108 + if b = y
1.109 + then
1.110 + (pos_num, symlist, nsymlist)
1.111 +
1.112 + else
1.113 + if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
1.114 + then
1.115 + (pos_num, symlist, nsymlist)
1.116 + else
1.117 + if (contains_eq b) andalso (contains_eq y)
1.118 + then
1.119 + if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
1.120 + then
1.121 + (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
1.122 + if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
1.123 + then
1.124 + (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
1.125 + else
1.126 + pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
1.127 + else
1.128 + pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
1.129 +
1.130 + end;
1.131
1.132
1.133 -fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list
1.134 - |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) =
1.135 - let val y = explode x
1.136 - val b = explode a
1.137 - in
1.138 - if b = y
1.139 - then
1.140 - (pos_num, symlist, nsymlist)
1.141 - else
1.142 - if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
1.143 - then
1.144 - (pos_num, symlist, nsymlist)
1.145 - else
1.146 - if (contains_eq b) andalso (contains_eq y)
1.147 - then
1.148 - if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
1.149 - then
1.150 - (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
1.151 - if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
1.152 - then
1.153 - (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
1.154 - else
1.155 - raise Not_in_list
1.156 - else
1.157 - raise Not_in_list
1.158 -
1.159 - end
1.160 -
1.161 - | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) =
1.162 - let val y = explode x
1.163 - val b = explode a
1.164 - in
1.165 - if b = y
1.166 - then
1.167 - (pos_num, symlist, nsymlist)
1.168 -
1.169 - else
1.170 - if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
1.171 - then
1.172 - (pos_num, symlist, nsymlist)
1.173 - else
1.174 - if (contains_eq b) andalso (contains_eq y)
1.175 - then
1.176 - if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
1.177 - then
1.178 - (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
1.179 - if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
1.180 - then
1.181 - (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
1.182 - else
1.183 - pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
1.184 - else
1.185 - pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
1.186 -
1.187 - end
1.188 + (* in
1.189 + if b = y
1.190 + then
1.191 + (pos_num, symlist, nsymlist)
1.192 + else if (contains_eq b) andalso (contains_eq y)
1.193 + then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
1.194 + then if (switch_equal b y ) (* if they're equal under sym *)
1.195 + then
1.196 + (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
1.197 + else
1.198 + pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.199 + else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *)
1.200 + then if (switch_equal b y ) (* if they're equal under not_sym *)
1.201 + then
1.202 + (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
1.203 + else
1.204 + pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.205 + else
1.206 + pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.207 + else
1.208 + pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.209 + else
1.210 + pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.211 + end
1.212
1.213 -
1.214 -
1.215 -
1.216 -
1.217 -
1.218 -
1.219 - (* in
1.220 - if b = y
1.221 - then
1.222 - (pos_num, symlist, nsymlist)
1.223 - else if (contains_eq b) andalso (contains_eq y)
1.224 - then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
1.225 - then if (switch_equal b y ) (* if they're equal under sym *)
1.226 - then
1.227 - (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
1.228 - else
1.229 - pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.230 - else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *)
1.231 - then if (switch_equal b y ) (* if they're equal under not_sym *)
1.232 - then
1.233 - (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
1.234 - else
1.235 - pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.236 - else
1.237 - pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.238 - else
1.239 - pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.240 - else
1.241 - pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
1.242 - end
1.243 -
1.244 - *)
1.245 + *)
1.246
1.247
1.248 (* checkorder Spass Isabelle [] *)
1.249
1.250 -fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
1.251 +fun checkorder [] strlist allvars (numlist, symlist, not_symlist) =
1.252 + (numlist,symlist, not_symlist)
1.253 | checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =
1.254 - let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist)
1.255 + let val (posnum, symlist', not_symlist') =
1.256 + pos_in_list x strlist allvars (0, symlist, not_symlist)
1.257 in
1.258 checkorder xs strlist allvars ((numlist@[posnum]), symlist', not_symlist')
1.259 end
1.260 @@ -206,26 +194,28 @@
1.261 (ch >= "a" andalso ch <= "z")
1.262
1.263
1.264 -fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
1.265 +fun is_alpha_space_or_neg_or_eq ch =
1.266 + (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
1.267
1.268 fun lit_string sg t =
1.269 - let val termstr = Sign.string_of_term sg t
1.270 - val exp_term = explode termstr
1.271 - in
1.272 - implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
1.273 - end
1.274 + let val termstr = Sign.string_of_term sg t
1.275 + val exp_term = explode termstr
1.276 + in
1.277 + implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
1.278 + end
1.279
1.280 fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
1.281
1.282
1.283 -fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
1.284 +fun is_alpha_space_or_neg_or_eq_or_bracket ch =
1.285 + is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
1.286
1.287 fun lit_string_bracket sg t =
1.288 - let val termstr = Sign.string_of_term sg t
1.289 - val exp_term = explode termstr
1.290 - in
1.291 - implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term)
1.292 - end
1.293 + let val termstr = Sign.string_of_term sg t
1.294 + val exp_term = explode termstr
1.295 + in
1.296 + implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term)
1.297 + end;
1.298
1.299 fun get_meta_lits_bracket thm =
1.300 map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
1.301 @@ -239,14 +229,17 @@
1.302
1.303
1.304
1.305 - (* resulting thm, clause-strs in spass order, vars *)
1.306 +(* resulting thm, clause-strs in spass order, vars *)
1.307
1.308 fun rearrange_clause thm res_strlist allvars =
1.309 - let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *)
1.310 - val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
1.311 - val symmed = apply_rule sym symlist thm
1.312 - val not_symmed = apply_rule not_sym not_symlist symmed
1.313 -
1.314 - in
1.315 - ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
1.316 - end
1.317 + let val isa_strlist = get_meta_lits thm
1.318 + (* change this to use Jia's code to get same looking thing as isastrlist? *)
1.319 + val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
1.320 + val symmed = apply_rule sym symlist thm
1.321 + val not_symmed = apply_rule not_sym not_symlist symmed
1.322 + in
1.323 + ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
1.324 + end
1.325 +
1.326 +end;
1.327 +
2.1 --- a/src/HOL/Tools/ATP/recon_parse.ML Tue May 24 07:43:38 2005 +0200
2.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML Tue May 24 10:23:24 2005 +0200
2.3 @@ -436,23 +436,21 @@
2.4 dropUntilNot ch xs
2.5
2.6
2.7 -
2.8 -
2.9 -
2.10 fun remove_spaces str [] = str
2.11 | remove_spaces str (x::[]) = if x = " "
2.12 then
2.13 str
2.14 else
2.15 (str^x)
2.16 -| remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) []
2.17 - val (next) = dropUntilNot " " rest
2.18 - in
2.19 - if next = []
2.20 - then
2.21 - (str^(implode first))
2.22 - else remove_spaces (str^(implode first)^" ") next
2.23 - end
2.24 +| remove_spaces str (x::xs) =
2.25 + let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) []
2.26 + val (next) = dropUntilNot " " rest
2.27 + in
2.28 + if next = []
2.29 + then
2.30 + (str^(implode first))
2.31 + else remove_spaces (str^(implode first)^" ") next
2.32 + end
2.33
2.34
2.35 fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
2.36 @@ -461,25 +459,25 @@
2.37 fun all_spaces xs = List.filter (not_equal " " ) xs
2.38
2.39 fun just_change_space [] = []
2.40 -| just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
2.41 - in
2.42 - if (all_spaces newstrs = [] ) (* all type_info *) then
2.43 - (clausenum, step, newstrs)::(just_change_space xs)
2.44 - else
2.45 - (clausenum, step, newstrs)::(just_change_space xs)
2.46 - end
2.47 -
2.48 -
2.49 -
2.50 +| just_change_space ((clausenum, step, strs)::xs) =
2.51 + let val newstrs = remove_space_strs strs
2.52 + in
2.53 + if (all_spaces newstrs = [] ) (* all type_info *)
2.54 + then
2.55 + (clausenum, step, newstrs)::(just_change_space xs)
2.56 + else
2.57 + (clausenum, step, newstrs)::(just_change_space xs)
2.58 + end;
2.59
2.60 fun change_space [] = []
2.61 -| change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
2.62 - in
2.63 - if (all_spaces newstrs = [] ) (* all type_info *)
2.64 - then
2.65 - (clausenum, step, T_info, newstrs)::(change_space xs)
2.66 - else
2.67 - (clausenum, step, P_info, newstrs)::(change_space xs)
2.68 - end
2.69 +| change_space ((clausenum, step, strs)::xs) =
2.70 + let val newstrs = remove_space_strs strs
2.71 + in
2.72 + if (all_spaces newstrs = [] ) (* all type_info *)
2.73 + then
2.74 + (clausenum, step, T_info, newstrs)::(change_space xs)
2.75 + else
2.76 + (clausenum, step, P_info, newstrs)::(change_space xs)
2.77 + end
2.78
2.79 end;
3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 24 07:43:38 2005 +0200
3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 24 10:23:24 2005 +0200
3.3 @@ -107,10 +107,13 @@
3.4
3.5 (*** get a string representing the Isabelle ordered axioms ***)
3.6
3.7 -fun origAx_to_string (num,(meta,thmvars)) =let val clause_strs = get_meta_lits_bracket meta
3.8 - in
3.9 - (string_of_int num)^"OrigAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
3.10 - end
3.11 +fun origAx_to_string (num,(meta,thmvars)) =
3.12 + let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
3.13 + in
3.14 + (string_of_int num)^"OrigAxiom()"^"["^
3.15 + (clause_strs_to_string clause_strs "")^"]"^"["^
3.16 + (thmvars_to_string thmvars "")^"]"
3.17 + end
3.18
3.19
3.20 fun origAxs_to_string [] str = str
3.21 @@ -122,20 +125,20 @@
3.22
3.23 (*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
3.24
3.25 -fun extraAx_to_string (num, (meta,thmvars)) = let val clause_strs = get_meta_lits_bracket meta
3.26 - in
3.27 - (string_of_int num)^"ExtraAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
3.28 - end
3.29 -
3.30 -
3.31 +fun extraAx_to_string (num, (meta,thmvars)) =
3.32 + let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
3.33 + in
3.34 + (string_of_int num)^"ExtraAxiom()"^"["^
3.35 + (clause_strs_to_string clause_strs "")^"]"^
3.36 + "["^(thmvars_to_string thmvars "")^"]"
3.37 + end;
3.38
3.39 -fun extraAxs_to_string [] str = str
3.40 -| extraAxs_to_string (x::xs) str = let val newstr = extraAx_to_string x
3.41 - in
3.42 - extraAxs_to_string xs (str^newstr)
3.43 - end
3.44 -
3.45 -
3.46 +fun extraAxs_to_string [] str = str
3.47 +| extraAxs_to_string (x::xs) str =
3.48 + let val newstr = extraAx_to_string x
3.49 + in
3.50 + extraAxs_to_string xs (str^newstr)
3.51 + end;
3.52
3.53 fun is_axiom ( num:int,Axiom, str) = true
3.54 | is_axiom (num, _,_) = false
3.55 @@ -156,7 +159,7 @@
3.56 | get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
3.57 *)
3.58 (*FIX - should this have vars in it? *)
3.59 -fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true)
3.60 +fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true)
3.61 handle _ => false
3.62
3.63 fun assoc_out_of_order a [] = raise Noassoc
3.64 @@ -202,94 +205,94 @@
3.65 (* add array and table here, so can retrieve clasimp axioms *)
3.66
3.67 fun get_axioms_used proof_steps thms clause_arr num_of_clauses =
3.68 - let
3.69 - (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
3.70 - val _ = TextIO.output (outfile, thmstring)
3.71 -
3.72 - val _ = TextIO.closeOut outfile*)
3.73 - (* not sure why this is necessary again, but seems to be *)
3.74 + let
3.75 + (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
3.76 + val _ = TextIO.output (outfile, thmstring)
3.77 +
3.78 + val _ = TextIO.closeOut outfile*)
3.79 + (* not sure why this is necessary again, but seems to be *)
3.80
3.81 - val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
3.82 - val axioms = get_init_axioms proof_steps
3.83 - val step_nums = get_step_nums axioms []
3.84 + val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
3.85 + val axioms = get_init_axioms proof_steps
3.86 + val step_nums = get_step_nums axioms []
3.87
3.88 - (***********************************************)
3.89 - (* here need to add the clauses from clause_arr*)
3.90 - (***********************************************)
3.91 + (***********************************************)
3.92 + (* here need to add the clauses from clause_arr*)
3.93 + (***********************************************)
3.94
3.95 - (* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums
3.96 - val clasimp_names = map #1 clasimp_names_cls
3.97 - val clasimp_cls = map #2 clasimp_names_cls
3.98 - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names
3.99 - val _ = TextIO.output (outfile,clasimp_namestr)
3.100 -
3.101 - val _ = TextIO.closeOut outfile
3.102 + (* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums
3.103 + val clasimp_names = map #1 clasimp_names_cls
3.104 + val clasimp_cls = map #2 clasimp_names_cls
3.105 + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names
3.106 + val _ = TextIO.output (outfile,clasimp_namestr)
3.107 +
3.108 + val _ = TextIO.closeOut outfile
3.109 *)
3.110
3.111 - val clauses =(*(clasimp_cls)@*)( make_clauses thms)
3.112 -
3.113 - val vars = map thm_vars clauses
3.114 -
3.115 - val distvars = distinct (fold append vars [])
3.116 - val clause_terms = map prop_of clauses
3.117 - val clause_frees = List.concat (map term_frees clause_terms)
3.118 + val clauses =(*(clasimp_cls)@*)( make_clauses thms)
3.119 +
3.120 + val vars = map thm_vars clauses
3.121 +
3.122 + val distvars = distinct (fold append vars [])
3.123 + val clause_terms = map prop_of clauses
3.124 + val clause_frees = List.concat (map term_frees clause_terms)
3.125
3.126 - val frees = map lit_string_with_nums clause_frees;
3.127 + val frees = map lit_string_with_nums clause_frees;
3.128
3.129 - val distfrees = distinct frees
3.130 + val distfrees = distinct frees
3.131
3.132 - val metas = map Meson.make_meta_clause clauses
3.133 - val ax_strs = map #3 axioms
3.134 + val metas = map Meson.make_meta_clause clauses
3.135 + val ax_strs = map #3 axioms
3.136
3.137 - (* literals of -all- axioms, not just those used by spass *)
3.138 - val meta_strs = map get_meta_lits metas
3.139 -
3.140 - val metas_and_strs = ListPair.zip (metas,meta_strs)
3.141 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));
3.142 - val _ = TextIO.output (outfile, onestr ax_strs)
3.143 -
3.144 - val _ = TextIO.closeOut outfile
3.145 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));
3.146 - val _ = TextIO.output (outfile, onestr meta_strs)
3.147 - val _ = TextIO.closeOut outfile
3.148 + (* literals of -all- axioms, not just those used by spass *)
3.149 + val meta_strs = map ReconOrderClauses.get_meta_lits metas
3.150 +
3.151 + val metas_and_strs = ListPair.zip (metas,meta_strs)
3.152 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));
3.153 + val _ = TextIO.output (outfile, onestr ax_strs)
3.154 +
3.155 + val _ = TextIO.closeOut outfile
3.156 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));
3.157 + val _ = TextIO.output (outfile, onestr meta_strs)
3.158 + val _ = TextIO.closeOut outfile
3.159
3.160 - (* get list of axioms as thms with their variables *)
3.161 + (* get list of axioms as thms with their variables *)
3.162
3.163 - val ax_metas = get_assoc_snds ax_strs metas_and_strs []
3.164 - val ax_vars = map thm_vars ax_metas
3.165 - val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
3.166 + val ax_metas = get_assoc_snds ax_strs metas_and_strs []
3.167 + val ax_vars = map thm_vars ax_metas
3.168 + val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
3.169
3.170 - (* get list of extra axioms as thms with their variables *)
3.171 - val extra_metas = add_if_not_inlist metas ax_metas []
3.172 - val extra_vars = map thm_vars extra_metas
3.173 - val extra_with_vars = if (not (extra_metas = []) )
3.174 - then
3.175 - ListPair.zip (extra_metas,extra_vars)
3.176 - else
3.177 - []
3.178 + (* get list of extra axioms as thms with their variables *)
3.179 + val extra_metas = add_if_not_inlist metas ax_metas []
3.180 + val extra_vars = map thm_vars extra_metas
3.181 + val extra_with_vars = if (not (extra_metas = []) )
3.182 + then
3.183 + ListPair.zip (extra_metas,extra_vars)
3.184 + else
3.185 + []
3.186
3.187 - (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
3.188 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
3.189 + (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
3.190 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
3.191
3.192 - val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
3.193 - val _ = TextIO.closeOut outfile
3.194 - val foo_metas = File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
3.195 - val foo_metas2 = File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
3.196 - val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2])
3.197 - val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
3.198 - val ax_metas_str = TextIO.inputLine (infile)
3.199 - val _ = TextIO.closeIn infile
3.200 - val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
3.201 -
3.202 - in
3.203 - (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
3.204 - end
3.205 -
3.206 + val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
3.207 + val _ = TextIO.closeOut outfile
3.208 + val foo_metas = File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
3.209 + val foo_metas2 = File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
3.210 + val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2])
3.211 + val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
3.212 + val ax_metas_str = TextIO.inputLine (infile)
3.213 + val _ = TextIO.closeIn infile
3.214 + val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
3.215 +
3.216 + in
3.217 + (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
3.218 + end
3.219 +
3.220 fun numclstr (vars, []) str = str
3.221 | numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
3.222 - in
3.223 - numclstr (vars,rest) newstr
3.224 - end
3.225 +in
3.226 +numclstr (vars,rest) newstr
3.227 +end
3.228
3.229 (*
3.230
3.231 @@ -366,101 +369,101 @@
3.232 val dummy_tac = PRIMITIVE(fn thm => thm );
3.233
3.234 fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
3.235 - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));
3.236 - (* val sign = sign_of_thm thm
3.237 - val prems = prems_of thm
3.238 - val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
3.239 - val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
3.240 - val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
3.241 - (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
3.242 - val _ = TextIO.closeOut outfile
3.243 + let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));
3.244 + (* val sign = sign_of_thm thm
3.245 + val prems = prems_of thm
3.246 + val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
3.247 + val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
3.248 + val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
3.249 +(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
3.250 + val _ = TextIO.closeOut outfile
3.251
3.252 - val tokens = #1(lex proofstr)
3.253 + val tokens = #1(lex proofstr)
3.254
3.255 -
3.256 +
3.257
3.258 - (***********************************)
3.259 - (* parse spass proof into datatype *)
3.260 - (***********************************)
3.261 + (***********************************)
3.262 + (* parse spass proof into datatype *)
3.263 + (***********************************)
3.264
3.265 - val proof_steps1 = parse tokens
3.266 - val proof_steps = just_change_space proof_steps1
3.267 + val proof_steps1 = parse tokens
3.268 + val proof_steps = just_change_space proof_steps1
3.269
3.270 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
3.271 - val _ = TextIO.closeOut outfile
3.272 -
3.273 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
3.274 - val _ = TextIO.closeOut outfile
3.275 - (************************************)
3.276 - (* recreate original subgoal as thm *)
3.277 - (************************************)
3.278 -
3.279 - (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
3.280 - (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
3.281 - (* subgoal this is, and turn it into meta_clauses *)
3.282 - (* should prob add array and table here, so that we can get axioms*)
3.283 - (* produced from the clasimpset rather than the problem *)
3.284 - val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses
3.285 -
3.286 - (*val numcls_string = numclstr ( vars, numcls) ""*)
3.287 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
3.288 - val _ = TextIO.closeOut outfile
3.289 -
3.290 - (************************************)
3.291 - (* translate proof *)
3.292 - (************************************)
3.293 - 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 "")))
3.294 - val _ = TextIO.closeOut outfile
3.295 - val (newthm,proof) = translate_proof numcls proof_steps vars
3.296 - 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 "")))
3.297 - val _ = TextIO.closeOut outfile
3.298 - (***************************************************)
3.299 - (* transfer necessary steps as strings to Isabelle *)
3.300 - (***************************************************)
3.301 - (* turn the proof into a string *)
3.302 - val reconProofStr = proofs_to_string proof ""
3.303 - (* do the bit for the Isabelle ordered axioms at the top *)
3.304 - val ax_nums = map #1 numcls
3.305 - val ax_strs = map get_meta_lits_bracket (map #2 numcls)
3.306 - val numcls_strs = ListPair.zip (ax_nums,ax_strs)
3.307 - val num_cls_vars = map (addvars vars) numcls_strs;
3.308 - val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
3.309 -
3.310 - val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
3.311 - val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
3.312 - val frees_str = "["^(thmvars_to_string frees "")^"]"
3.313 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
3.314 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
3.315 + val _ = TextIO.closeOut outfile
3.316 +
3.317 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
3.318 + val _ = TextIO.closeOut outfile
3.319 + (************************************)
3.320 + (* recreate original subgoal as thm *)
3.321 + (************************************)
3.322 +
3.323 + (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
3.324 + (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
3.325 + (* subgoal this is, and turn it into meta_clauses *)
3.326 + (* should prob add array and table here, so that we can get axioms*)
3.327 + (* produced from the clasimpset rather than the problem *)
3.328 + val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses
3.329 +
3.330 + (*val numcls_string = numclstr ( vars, numcls) ""*)
3.331 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
3.332 + val _ = TextIO.closeOut outfile
3.333 +
3.334 + (************************************)
3.335 + (* translate proof *)
3.336 + (************************************)
3.337 + 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 "")))
3.338 + val _ = TextIO.closeOut outfile
3.339 + val (newthm,proof) = translate_proof numcls proof_steps vars
3.340 + 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 "")))
3.341 + val _ = TextIO.closeOut outfile
3.342 + (***************************************************)
3.343 + (* transfer necessary steps as strings to Isabelle *)
3.344 + (***************************************************)
3.345 + (* turn the proof into a string *)
3.346 + val reconProofStr = proofs_to_string proof ""
3.347 + (* do the bit for the Isabelle ordered axioms at the top *)
3.348 + val ax_nums = map #1 numcls
3.349 + val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
3.350 + val numcls_strs = ListPair.zip (ax_nums,ax_strs)
3.351 + val num_cls_vars = map (addvars vars) numcls_strs;
3.352 + val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
3.353 +
3.354 + val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
3.355 + val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
3.356 + val frees_str = "["^(thmvars_to_string frees "")^"]"
3.357 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
3.358
3.359 - val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
3.360 - val _ = TextIO.closeOut outfile
3.361 - val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
3.362 - in
3.363 - TextIO.output (toParent, reconstr^"\n");
3.364 - TextIO.flushOut toParent;
3.365 - TextIO.output (toParent, thmstring^"\n");
3.366 - TextIO.flushOut toParent;
3.367 - TextIO.output (toParent, goalstring^"\n");
3.368 - TextIO.flushOut toParent;
3.369 -
3.370 - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
3.371 - (* Attempt to prevent several signals from turning up simultaneously *)
3.372 - Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
3.373 - end
3.374 - handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
3.375 + val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
3.376 + val _ = TextIO.closeOut outfile
3.377 + val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
3.378 + in
3.379 + TextIO.output (toParent, reconstr^"\n");
3.380 + TextIO.flushOut toParent;
3.381 + TextIO.output (toParent, thmstring^"\n");
3.382 + TextIO.flushOut toParent;
3.383 + TextIO.output (toParent, goalstring^"\n");
3.384 + TextIO.flushOut toParent;
3.385 +
3.386 + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
3.387 + (* Attempt to prevent several signals from turning up simultaneously *)
3.388 + Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
3.389 + end
3.390 + handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
3.391
3.392 - val _ = TextIO.output (outfile, ("In exception handler"));
3.393 - val _ = TextIO.closeOut outfile
3.394 - in
3.395 - TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
3.396 - TextIO.flushOut toParent;
3.397 - TextIO.output (toParent, thmstring^"\n");
3.398 - TextIO.flushOut toParent;
3.399 - TextIO.output (toParent, goalstring^"\n");
3.400 - TextIO.flushOut toParent;
3.401 - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
3.402 - (* Attempt to prevent several signals from turning up simultaneously *)
3.403 - Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
3.404 - end)
3.405 + val _ = TextIO.output (outfile, ("In exception handler"));
3.406 + val _ = TextIO.closeOut outfile
3.407 + in
3.408 + TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
3.409 + TextIO.flushOut toParent;
3.410 + TextIO.output (toParent, thmstring^"\n");
3.411 + TextIO.flushOut toParent;
3.412 + TextIO.output (toParent, goalstring^"\n");
3.413 + TextIO.flushOut toParent;
3.414 + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
3.415 + (* Attempt to prevent several signals from turning up simultaneously *)
3.416 + Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
3.417 + end)
3.418
3.419
3.420
3.421 @@ -742,9 +745,9 @@
3.422 val axioms = get_axioms axioms_and_steps
3.423
3.424 val steps = Library.drop (origax_num, axioms_and_steps)
3.425 - val firststeps = butlast steps
3.426 - val laststep = last steps
3.427 - val goalstring = implode(butlast(explode goalstring))
3.428 + val firststeps = ReconOrderClauses.butlast steps
3.429 + val laststep = ReconOrderClauses.last steps
3.430 + val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
3.431
3.432 val isar_proof =
3.433 ("show \""^goalstring^"\"\n")^
4.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 24 07:43:38 2005 +0200
4.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 24 10:23:24 2005 +0200
4.3 @@ -55,8 +55,9 @@
4.4 |P_info
4.5
4.6
4.7 -fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
4.8 -
4.9 +fun is_alpha_space_digit_or_neg ch =
4.10 + (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse
4.11 + (ReconOrderClauses.is_digit ch) orelse ( ch = " ");
4.12
4.13
4.14 fun lit_string_with_nums t = let val termstr = Term.string_of_term t
4.15 @@ -73,30 +74,29 @@
4.16 (************************************************)
4.17
4.18 fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
4.19 - let val this_axiom = valOf (assoc (clauses,clausenum))
4.20 - val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)
4.21 - val thmvars = thm_vars res
4.22 - in
4.23 - (res, (Axiom,clause_strs,thmvars ) )
4.24 - end
4.25 - handle Option => reconstruction_failed "follow_axiom"
4.26 + let val this_axiom = valOf (assoc (clauses,clausenum))
4.27 + val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)
4.28 + val thmvars = thm_vars res
4.29 + in
4.30 + (res, (Axiom,clause_strs,thmvars ) )
4.31 + end
4.32 + handle Option => reconstruction_failed "follow_axiom"
4.33
4.34 (****************************************)
4.35 (* Reconstruct a binary resolution step *)
4.36 (****************************************)
4.37
4.38 (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
4.39 -fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
4.40 - = let
4.41 - val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
4.42 - val thm2 = valOf (assoc (thml,clause2))
4.43 - val res = thm1 RSN ((lit2 +1), thm2)
4.44 - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
4.45 - val thmvars = thm_vars res
4.46 - in
4.47 - (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
4.48 - end
4.49 - handle Option => reconstruction_failed "follow_binary"
4.50 +fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
4.51 + let val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
4.52 + val thm2 = valOf (assoc (thml,clause2))
4.53 + val res = thm1 RSN ((lit2 +1), thm2)
4.54 + val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
4.55 + val thmvars = thm_vars res
4.56 + in
4.57 + (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
4.58 + end
4.59 + handle Option => reconstruction_failed "follow_binary"
4.60
4.61
4.62
4.63 @@ -105,17 +105,17 @@
4.64 (******************************************************)
4.65
4.66
4.67 -fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
4.68 - = let
4.69 - val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
4.70 - val thm2 = valOf (assoc (thml,clause2))
4.71 - val res = thm1 RSN ((lit2 +1), thm2)
4.72 - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
4.73 - val thmvars = thm_vars res
4.74 - in
4.75 - (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
4.76 - end
4.77 - handle Option => reconstruction_failed "follow_mrr"
4.78 +fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
4.79 + let val thm1 = select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
4.80 + val thm2 = valOf (assoc (thml,clause2))
4.81 + val res = thm1 RSN ((lit2 +1), thm2)
4.82 + val (res', numlist, symlist, nsymlist) =
4.83 + (ReconOrderClauses.rearrange_clause res clause_strs allvars)
4.84 + val thmvars = thm_vars res
4.85 + in
4.86 + (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
4.87 + end
4.88 + handle Option => reconstruction_failed "follow_mrr"
4.89
4.90
4.91 (*******************************************)
4.92 @@ -123,11 +123,13 @@
4.93 (*******************************************)
4.94
4.95 fun mksubstlist [] sublist = sublist
4.96 - |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b
4.97 - val avar = Var(a,vartype)
4.98 - val newlist = ((avar,b)::sublist) in
4.99 - mksubstlist rest newlist
4.100 - end;
4.101 + |mksubstlist ((a, (_, b)) :: rest) sublist =
4.102 + let val vartype = type_of b
4.103 + val avar = Var(a,vartype)
4.104 + val newlist = ((avar,b)::sublist)
4.105 + in
4.106 + mksubstlist rest newlist
4.107 + end;
4.108
4.109 (* based on Tactic.distinct_subgoals_tac *)
4.110
4.111 @@ -135,7 +137,7 @@
4.112 let val (frozth,thawfn) = freeze_thaw state
4.113 val froz_prems = cprems_of frozth
4.114 val assumed = implies_elim_list frozth (map assume froz_prems)
4.115 - val new_prems = remove_nth lit froz_prems
4.116 + val new_prems = ReconOrderClauses.remove_nth lit froz_prems
4.117 val implied = implies_intr_list new_prems assumed
4.118 in
4.119 Seq.single (thawfn implied)
4.120 @@ -150,44 +152,46 @@
4.121 (*************************************)
4.122
4.123 (*FIXME: share code with that in Tools/reconstruction.ML*)
4.124 -fun follow_factor clause lit1 lit2 allvars thml clause_strs=
4.125 - let
4.126 - val th = valOf (assoc (thml,clause))
4.127 - val prems = prems_of th
4.128 - val sign = sign_of_thm th
4.129 - val fac1 = get_nth (lit1+1) prems
4.130 - val fac2 = get_nth (lit2+1) prems
4.131 - val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
4.132 - val newenv = getnewenv unif_env
4.133 - val envlist = Envir.alist_of newenv
4.134 -
4.135 - val (t1,t2)::_ = mksubstlist envlist []
4.136 - in
4.137 - if (is_Var t1)
4.138 - then
4.139 - let
4.140 - val str1 = lit_string_with_nums t1;
4.141 - val str2 = lit_string_with_nums t2;
4.142 - val facthm = read_instantiate [(str1,str2)] th;
4.143 - val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
4.144 - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
4.145 - val thmvars = thm_vars res'
4.146 - in
4.147 - (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars))
4.148 - end
4.149 - else
4.150 - let
4.151 - val str2 = lit_string_with_nums t1;
4.152 - val str1 = lit_string_with_nums t2;
4.153 - val facthm = read_instantiate [(str1,str2)] th;
4.154 - val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
4.155 - val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
4.156 - val thmvars = thm_vars res'
4.157 - in
4.158 - (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars))
4.159 - end
4.160 - end
4.161 - handle Option => reconstruction_failed "follow_factor"
4.162 +fun follow_factor clause lit1 lit2 allvars thml clause_strs =
4.163 + let
4.164 + val th = valOf (assoc (thml,clause))
4.165 + val prems = prems_of th
4.166 + val sign = sign_of_thm th
4.167 + val fac1 = ReconOrderClauses.get_nth (lit1+1) prems
4.168 + val fac2 = ReconOrderClauses.get_nth (lit2+1) prems
4.169 + val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
4.170 + val newenv = getnewenv unif_env
4.171 + val envlist = Envir.alist_of newenv
4.172 +
4.173 + val (t1,t2)::_ = mksubstlist envlist []
4.174 + in
4.175 + if (is_Var t1)
4.176 + then
4.177 + let
4.178 + val str1 = lit_string_with_nums t1;
4.179 + val str2 = lit_string_with_nums t2;
4.180 + val facthm = read_instantiate [(str1,str2)] th;
4.181 + val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
4.182 + val (res', numlist, symlist, nsymlist) =
4.183 + ReconOrderClauses.rearrange_clause res clause_strs allvars
4.184 + val thmvars = thm_vars res'
4.185 + in
4.186 + (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars))
4.187 + end
4.188 + else
4.189 + let
4.190 + val str2 = lit_string_with_nums t1;
4.191 + val str1 = lit_string_with_nums t2;
4.192 + val facthm = read_instantiate [(str1,str2)] th;
4.193 + val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
4.194 + val (res', numlist, symlist, nsymlist) =
4.195 + ReconOrderClauses.rearrange_clause res clause_strs allvars
4.196 + val thmvars = thm_vars res'
4.197 + in
4.198 + (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars))
4.199 + end
4.200 + end
4.201 + handle Option => reconstruction_failed "follow_factor"
4.202
4.203
4.204
4.205 @@ -216,28 +220,29 @@
4.206 val rev_ssubst = rotate_prems 1 ssubst;
4.207
4.208
4.209 -fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
4.210 - let
4.211 - val th1 = valOf (assoc (thml,clause1))
4.212 - val th2 = valOf (assoc (thml,clause2))
4.213 - val eq_lit_th = select_literal (lit1+1) th1
4.214 - val mod_lit_th = select_literal (lit2+1) th2
4.215 - val eqsubst = eq_lit_th RSN (2,rev_subst)
4.216 - val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
4.217 - val newth' =negate_head newth
4.218 - val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars
4.219 - handle Not_in_list => let
4.220 - val mod_lit_th' = mod_lit_th RS not_sym
4.221 - val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
4.222 - val newth' =negate_head newth
4.223 - in
4.224 - (rearrange_clause newth' clause_strs allvars)
4.225 - end)
4.226 - val thmvars = thm_vars res
4.227 - in
4.228 - (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
4.229 - end
4.230 - handle Option => reconstruction_failed "follow_standard_para"
4.231 +fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
4.232 + let
4.233 + val th1 = valOf (assoc (thml,clause1))
4.234 + val th2 = valOf (assoc (thml,clause2))
4.235 + val eq_lit_th = select_literal (lit1+1) th1
4.236 + val mod_lit_th = select_literal (lit2+1) th2
4.237 + val eqsubst = eq_lit_th RSN (2,rev_subst)
4.238 + val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
4.239 + val newth' =negate_head newth
4.240 + val (res, numlist, symlist, nsymlist) =
4.241 + (ReconOrderClauses.rearrange_clause newth' clause_strs allvars
4.242 + handle Not_in_list =>
4.243 + let val mod_lit_th' = mod_lit_th RS not_sym
4.244 + val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
4.245 + val newth' =negate_head newth
4.246 + in
4.247 + ReconOrderClauses.rearrange_clause newth' clause_strs allvars
4.248 + end)
4.249 + val thmvars = thm_vars res
4.250 + in
4.251 + (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
4.252 + end
4.253 + handle Option => reconstruction_failed "follow_standard_para"
4.254
4.255 (*
4.256 fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
4.257 @@ -293,26 +298,24 @@
4.258 (* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *)
4.259 (* changed negate_nead to negate_head here too*)
4.260 (* clause1, lit1 is thing to rewrite with *)
4.261 -fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs=
4.262 -
4.263 - let val th1 = valOf (assoc (thml,clause1))
4.264 - val th2 = valOf (assoc (thml,clause2))
4.265 - val eq_lit_th = select_literal (lit1+1) th1
4.266 - val mod_lit_th = select_literal (lit2+1) th2
4.267 - val eqsubst = eq_lit_th RSN (2,rev_subst)
4.268 - val eq_lit_prem_num = length (prems_of eq_lit_th)
4.269 - val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
4.270 - val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
4.271 -eqsubst)
4.272 -
4.273 - val newthm = negate_head newth
4.274 - val newthm' = delete_assumps eq_lit_prem_num newthm
4.275 - val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
4.276 - val thmvars = thm_vars res
4.277 - in
4.278 - (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars))
4.279 - end
4.280 - handle Option => reconstruction_failed "follow_rewrite"
4.281 +fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs =
4.282 + let val th1 = valOf (assoc (thml,clause1))
4.283 + val th2 = valOf (assoc (thml,clause2))
4.284 + val eq_lit_th = select_literal (lit1+1) th1
4.285 + val mod_lit_th = select_literal (lit2+1) th2
4.286 + val eqsubst = eq_lit_th RSN (2,rev_subst)
4.287 + val eq_lit_prem_num = length (prems_of eq_lit_th)
4.288 + val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
4.289 + val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
4.290 + val newthm = negate_head newth
4.291 + val newthm' = delete_assumps eq_lit_prem_num newthm
4.292 + val (res, numlist, symlist, nsymlist) =
4.293 + ReconOrderClauses.rearrange_clause newthm clause_strs allvars
4.294 + val thmvars = thm_vars res
4.295 + in
4.296 + (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars))
4.297 + end
4.298 + handle Option => reconstruction_failed "follow_rewrite"
4.299
4.300
4.301
4.302 @@ -321,17 +324,18 @@
4.303 (*****************************************)
4.304
4.305
4.306 -fun follow_obvious (clause1, lit1) allvars thml clause_strs=
4.307 - let val th1 = valOf (assoc (thml,clause1))
4.308 - val prems1 = prems_of th1
4.309 - val newthm = refl RSN ((lit1+ 1), th1)
4.310 - handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
4.311 - val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
4.312 - val thmvars = thm_vars res
4.313 - in
4.314 - (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
4.315 - end
4.316 - handle Option => reconstruction_failed "follow_obvious"
4.317 +fun follow_obvious (clause1, lit1) allvars thml clause_strs =
4.318 + let val th1 = valOf (assoc (thml,clause1))
4.319 + val prems1 = prems_of th1
4.320 + val newthm = refl RSN ((lit1+ 1), th1)
4.321 + handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
4.322 + val (res, numlist, symlist, nsymlist) =
4.323 + ReconOrderClauses.rearrange_clause newthm clause_strs allvars
4.324 + val thmvars = thm_vars res
4.325 + in
4.326 + (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
4.327 + end
4.328 + handle Option => reconstruction_failed "follow_obvious"
4.329
4.330 (**************************************************************************************)
4.331 (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
4.332 @@ -436,28 +440,29 @@
4.333
4.334 *)
4.335
4.336 -fun replace_clause_strs [] recons newrecons= (newrecons)
4.337 -| replace_clause_strs ((thmnum, thm)::thml) ((clausenum,(step,clause_strs,thmvars))::recons) newrecons =
4.338 - let val new_clause_strs = get_meta_lits_bracket thm
4.339 - in
4.340 - replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
4.341 - end
4.342 +fun replace_clause_strs [] recons newrecons = (newrecons)
4.343 +| replace_clause_strs ((thmnum, thm)::thml)
4.344 + ((clausenum,(step,clause_strs,thmvars))::recons) newrecons =
4.345 + let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm
4.346 + in
4.347 + replace_clause_strs thml recons
4.348 + ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
4.349 + end
4.350
4.351
4.352 fun follow clauses [] allvars thml recons =
4.353 - let
4.354 - val new_recons = replace_clause_strs thml recons []
4.355 - in
4.356 - ((snd( hd thml)), new_recons)
4.357 - end
4.358 -
4.359 - | follow clauses (h::t) allvars thml recons
4.360 - = let
4.361 - val (thml', recons') = follow_line clauses allvars thml h recons
4.362 - val (thm, recons_list) = follow clauses t allvars thml' recons'
4.363 - in
4.364 - (thm,recons_list)
4.365 - end
4.366 + let
4.367 + val new_recons = replace_clause_strs thml recons []
4.368 + in
4.369 + (#2(hd thml), new_recons)
4.370 + end
4.371 + | follow clauses (h::t) allvars thml recons =
4.372 + let
4.373 + val (thml', recons') = follow_line clauses allvars thml h recons
4.374 + val (thm, recons_list) = follow clauses t allvars thml' recons'
4.375 + in
4.376 + (thm,recons_list)
4.377 + end
4.378
4.379
4.380
4.381 @@ -481,4 +486,5 @@
4.382
4.383
4.384 fun remove_tinfo [] = []
4.385 -| remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)
4.386 + | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
4.387 + (clausenum, step , newstrs)::(remove_tinfo xs)
5.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 24 07:43:38 2005 +0200
5.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 24 10:23:24 2005 +0200
5.3 @@ -12,18 +12,10 @@
5.4
5.5 structure ResClasimp : RES_CLASIMP =
5.6 struct
5.7 -fun has_name th = not((Thm.name_of_thm th )= "")
5.8 -fun has_name_pair (a,b) = not_equal a "";
5.9 -
5.10 -fun stick [] = []
5.11 -| stick (x::xs) = x@(stick xs )
5.12
5.13 -fun filterlist p [] = []
5.14 -| filterlist p (x::xs) = if p x
5.15 - then
5.16 - (x::(filterlist p xs))
5.17 - else
5.18 - filterlist p xs
5.19 +fun has_name th = ((Thm.name_of_thm th) <> "")
5.20 +
5.21 +fun has_name_pair (a,b) = (a <> "");
5.22
5.23
5.24 (* changed, now it also finds out the name of the theorem. *)
5.25 @@ -37,73 +29,64 @@
5.26 | concat_with_stop [x] = x
5.27 | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
5.28
5.29 -fun remove_symb str = if String.isPrefix "List.op @." str
5.30 - then
5.31 - ((String.substring(str,0,5))^(String.extract (str, 10, NONE)))
5.32 - else
5.33 - str
5.34 -
5.35 -fun remove_spaces str = let val strlist = String.tokens Char.isSpace str
5.36 - val spaceless = concat strlist
5.37 - val strlist' = String.tokens Char.isPunct spaceless
5.38 - in
5.39 - concat_with_stop strlist'
5.40 - end
5.41 +fun remove_symb str =
5.42 + if String.isPrefix "List.op @." str
5.43 + then ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
5.44 + else str;
5.45
5.46 -fun remove_symb_pair (str, thm) = let val newstr = remove_symb str
5.47 - in
5.48 - (newstr, thm)
5.49 - end
5.50 -
5.51 +fun remove_spaces str =
5.52 + let val strlist = String.tokens Char.isSpace str
5.53 + val spaceless = concat strlist
5.54 + val strlist' = String.tokens Char.isPunct spaceless
5.55 + in
5.56 + concat_with_stop strlist'
5.57 + end
5.58
5.59 -fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str
5.60 - in
5.61 - (newstr, thm)
5.62 - end
5.63 +fun remove_symb_pair (str, thm) = (remove_symb str, thm);
5.64
5.65 -
5.66 +fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
5.67
5.68
5.69 (*Insert th into the result provided the name is not "".*)
5.70 fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
5.71
5.72
5.73 -fun write_out_clasimp filename = let
5.74 - val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
5.75 - val named_claset = filterlist has_name_pair claset_rules;
5.76 - val claset_names = map remove_spaces_pair (named_claset)
5.77 - val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []);
5.78 -
5.79 +fun write_out_clasimp filename =
5.80 + let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
5.81 + val named_claset = List.filter has_name_pair claset_rules;
5.82 + val claset_names = map remove_spaces_pair (named_claset)
5.83 + val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
5.84
5.85 - val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
5.86 - val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules);
5.87 - val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
5.88 + val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
5.89 + val named_simpset =
5.90 + map remove_spaces_pair (List.filter has_name_pair simpset_rules)
5.91 + val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
5.92
5.93 - val cls_thms = (claset_cls_thms@simpset_cls_thms);
5.94 - val cls_thms_list = stick cls_thms;
5.95 + val cls_thms = (claset_cls_thms@simpset_cls_thms);
5.96 + val cls_thms_list = List.concat cls_thms;
5.97
5.98 - (*********************************************************)
5.99 - (* create array and put clausename, number pairs into it *)
5.100 - (*********************************************************)
5.101 - val num_of_clauses = 0;
5.102 - val clause_arr = Array.fromList cls_thms_list;
5.103 -
5.104 - val num_of_clauses= (List.length cls_thms_list);
5.105 + (*********************************************************)
5.106 + (* create array and put clausename, number pairs into it *)
5.107 + (*********************************************************)
5.108 + val num_of_clauses = 0;
5.109 + val clause_arr = Array.fromList cls_thms_list;
5.110 +
5.111 + val num_of_clauses = List.length cls_thms_list;
5.112
5.113 - (*************************************************)
5.114 - (* Write out clauses as tptp strings to filename *)
5.115 - (*************************************************)
5.116 - val clauses = map #1(cls_thms_list);
5.117 - val cls_tptp_strs = map ResClause.tptp_clause clauses;
5.118 - (* list of lists of tptp string clauses *)
5.119 - val stick_clasrls = stick cls_tptp_strs;
5.120 - val out = TextIO.openOut filename;
5.121 - val _= ResLib.writeln_strs out stick_clasrls;
5.122 - val _= TextIO.flushOut out;
5.123 - val _= TextIO.closeOut out
5.124 - in
5.125 - (clause_arr, num_of_clauses)
5.126 - end;
5.127 + (*************************************************)
5.128 + (* Write out clauses as tptp strings to filename *)
5.129 + (*************************************************)
5.130 + val clauses = map #1(cls_thms_list);
5.131 + val cls_tptp_strs = map ResClause.tptp_clause clauses;
5.132 + (* list of lists of tptp string clauses *)
5.133 + val stick_clasrls = List.concat cls_tptp_strs;
5.134 + val out = TextIO.openOut filename;
5.135 + val _= ResLib.writeln_strs out stick_clasrls;
5.136 + val _= TextIO.flushOut out;
5.137 + val _= TextIO.closeOut out
5.138 + in
5.139 + (clause_arr, num_of_clauses)
5.140 + end;
5.141
5.142
5.143 end;
6.1 --- a/src/HOL/Tools/ATP/watcher.ML Tue May 24 07:43:38 2005 +0200
6.2 +++ b/src/HOL/Tools/ATP/watcher.ML Tue May 24 10:23:24 2005 +0200
6.3 @@ -164,44 +164,45 @@
6.4 fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n");
6.5 TextIO.flushOut toWatcherStr)
6.6 | callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
6.7 - let val dfg_dir = File.tmp_path (Path.basic "dfg");
6.8 - (*** need to check here if the directory exists and, if not, create it***)
6.9 - val outfile = TextIO.openAppend(File.sysify_path
6.10 - (File.tmp_path (Path.basic"thmstring_in_watcher"))); val _ = TextIO.output (outfile,
6.11 - (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
6.12 - val _ = TextIO.closeOut outfile
6.13 - (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
6.14 - val probID = last(explode probfile)
6.15 - val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
6.16 - (*** only include problem and clasimp for the moment, not sure how to refer to ***)
6.17 - (*** hyps/local axioms just now ***)
6.18 - val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)])
6.19 - val dfg_create =if File.exists dfg_dir
6.20 - then
6.21 - ((warning("dfg dir exists"));())
6.22 - else
6.23 - File.mkdir dfg_dir;
6.24 -
6.25 - val dfg_path = File.sysify_path dfg_dir;
6.26 - val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
6.27 - (*val _ = Posix.Process.wait ()*)
6.28 - (*val _ =Unix.reap exec_tptp2x*)
6.29 - val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
6.30 -
6.31 - in
6.32 - goals_being_watched := (!goals_being_watched) + 1;
6.33 - Posix.Process.sleep(Time.fromSeconds 1);
6.34 - (warning ("probfile is: "^probfile));
6.35 - (warning("dfg file is: "^newfile));
6.36 - (warning ("wholefile is: "^(File.sysify_path wholefile)));
6.37 - sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
6.38 -(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
6.39 - TextIO.flushOut toWatcherStr;
6.40 - Unix.reap exec_tptp2x;
6.41 -
6.42 - callResProvers (toWatcherStr,args)
6.43 -
6.44 - end
6.45 + let val dfg_dir = File.tmp_path (Path.basic "dfg");
6.46 + (*** need to check here if the directory exists and, if not, create it***)
6.47 + val outfile = TextIO.openAppend(File.sysify_path
6.48 + (File.tmp_path (Path.basic"thmstring_in_watcher")));
6.49 + val _ = TextIO.output (outfile,
6.50 + (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
6.51 + val _ = TextIO.closeOut outfile
6.52 + (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
6.53 + val probID = ReconOrderClauses.last(explode probfile)
6.54 + val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
6.55 + (*** only include problem and clasimp for the moment, not sure how to refer to ***)
6.56 + (*** hyps/local axioms just now ***)
6.57 + val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)])
6.58 + val dfg_create =if File.exists dfg_dir
6.59 + then
6.60 + ((warning("dfg dir exists"));())
6.61 + else
6.62 + File.mkdir dfg_dir;
6.63 +
6.64 + val dfg_path = File.sysify_path dfg_dir;
6.65 + val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
6.66 + (*val _ = Posix.Process.wait ()*)
6.67 + (*val _ =Unix.reap exec_tptp2x*)
6.68 + val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
6.69 +
6.70 + in
6.71 + goals_being_watched := (!goals_being_watched) + 1;
6.72 + Posix.Process.sleep(Time.fromSeconds 1);
6.73 + (warning ("probfile is: "^probfile));
6.74 + (warning("dfg file is: "^newfile));
6.75 + (warning ("wholefile is: "^(File.sysify_path wholefile)));
6.76 + sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
6.77 + (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
6.78 + TextIO.flushOut toWatcherStr;
6.79 + Unix.reap exec_tptp2x;
6.80 +
6.81 + callResProvers (toWatcherStr,args)
6.82 +
6.83 + end
6.84 (*
6.85 fun callResProversStr (toWatcherStr, []) = "End of calls\n"
6.86
6.87 @@ -327,374 +328,375 @@
6.88
6.89
6.90
6.91 -fun setupWatcher (thm,clause_arr, num_of_clauses) = let
6.92 - (** pipes for communication between parent and watcher **)
6.93 - val p1 = Posix.IO.pipe ()
6.94 - val p2 = Posix.IO.pipe ()
6.95 - fun closep () = (
6.96 - Posix.IO.close (#outfd p1);
6.97 - Posix.IO.close (#infd p1);
6.98 - Posix.IO.close (#outfd p2);
6.99 - Posix.IO.close (#infd p2)
6.100 - )
6.101 - (***********************************************************)
6.102 - (****** fork a watcher process and get it set up and going *)
6.103 - (***********************************************************)
6.104 - fun startWatcher (procList) =
6.105 - (case Posix.Process.fork() (***************************************)
6.106 - of SOME pid => pid (* parent - i.e. main Isabelle process *)
6.107 - (***************************************)
6.108 -
6.109 - (*************************)
6.110 - | NONE => let (* child - i.e. watcher *)
6.111 - val oldchildin = #infd p1 (*************************)
6.112 - val fromParent = Posix.FileSys.wordToFD 0w0
6.113 - val oldchildout = #outfd p2
6.114 - val toParent = Posix.FileSys.wordToFD 0w1
6.115 - val fromParentIOD = Posix.FileSys.fdToIOD fromParent
6.116 - val fromParentStr = openInFD ("_exec_in_parent", fromParent)
6.117 - val toParentStr = openOutFD ("_exec_out_parent", toParent)
6.118 - val sign = sign_of_thm thm
6.119 - val prems = prems_of thm
6.120 - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
6.121 - val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
6.122 - (* tracing *)
6.123 - (*val tenth_ax = fst( Array.sub(clause_arr, 1))
6.124 - val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
6.125 - val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
6.126 - val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))
6.127 - val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))
6.128 - val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )
6.129 - *)
6.130 - (*val goalstr = string_of_thm (the_goal)
6.131 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));
6.132 - val _ = TextIO.output (outfile,goalstr )
6.133 - val _ = TextIO.closeOut outfile*)
6.134 - fun killChildren [] = ()
6.135 - | killChildren (child_handle::children) = (killChild child_handle; killChildren children)
6.136 +fun setupWatcher (thm,clause_arr, num_of_clauses) =
6.137 + let
6.138 + (** pipes for communication between parent and watcher **)
6.139 + val p1 = Posix.IO.pipe ()
6.140 + val p2 = Posix.IO.pipe ()
6.141 + fun closep () = (
6.142 + Posix.IO.close (#outfd p1);
6.143 + Posix.IO.close (#infd p1);
6.144 + Posix.IO.close (#outfd p2);
6.145 + Posix.IO.close (#infd p2)
6.146 + )
6.147 + (***********************************************************)
6.148 + (****** fork a watcher process and get it set up and going *)
6.149 + (***********************************************************)
6.150 + fun startWatcher (procList) =
6.151 + (case Posix.Process.fork() (***************************************)
6.152 + of SOME pid => pid (* parent - i.e. main Isabelle process *)
6.153 + (***************************************)
6.154 +
6.155 + (*************************)
6.156 + | NONE => let (* child - i.e. watcher *)
6.157 + val oldchildin = #infd p1 (*************************)
6.158 + val fromParent = Posix.FileSys.wordToFD 0w0
6.159 + val oldchildout = #outfd p2
6.160 + val toParent = Posix.FileSys.wordToFD 0w1
6.161 + val fromParentIOD = Posix.FileSys.fdToIOD fromParent
6.162 + val fromParentStr = openInFD ("_exec_in_parent", fromParent)
6.163 + val toParentStr = openOutFD ("_exec_out_parent", toParent)
6.164 + val sign = sign_of_thm thm
6.165 + val prems = prems_of thm
6.166 + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
6.167 + val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
6.168 + (* tracing *)
6.169 + (*val tenth_ax = fst( Array.sub(clause_arr, 1))
6.170 + val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
6.171 + val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
6.172 + val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))
6.173 + val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))
6.174 + val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )
6.175 + *)
6.176 + (*val goalstr = string_of_thm (the_goal)
6.177 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));
6.178 + val _ = TextIO.output (outfile,goalstr )
6.179 + val _ = TextIO.closeOut outfile*)
6.180 + fun killChildren [] = ()
6.181 + | killChildren (child_handle::children) = (killChild child_handle; killChildren children)
6.182
6.183 -
6.184 -
6.185 - (*************************************************************)
6.186 - (* take an instream and poll its underlying reader for input *)
6.187 - (*************************************************************)
6.188 +
6.189 +
6.190 + (*************************************************************)
6.191 + (* take an instream and poll its underlying reader for input *)
6.192 + (*************************************************************)
6.193
6.194 - fun pollParentInput () =
6.195 -
6.196 - let val pd = OS.IO.pollDesc (fromParentIOD)
6.197 - in
6.198 - if (isSome pd ) then
6.199 - let val pd' = OS.IO.pollIn (valOf pd)
6.200 - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
6.201 - in
6.202 - if null pdl
6.203 - then
6.204 - NONE
6.205 - else if (OS.IO.isIn (hd pdl))
6.206 - then
6.207 - (SOME ( getCmds (toParentStr, fromParentStr, [])))
6.208 - else
6.209 - NONE
6.210 - end
6.211 - else
6.212 - NONE
6.213 - end
6.214 -
6.215 -
6.216 + fun pollParentInput () =
6.217 +
6.218 + let val pd = OS.IO.pollDesc (fromParentIOD)
6.219 + in
6.220 + if (isSome pd ) then
6.221 + let val pd' = OS.IO.pollIn (valOf pd)
6.222 + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
6.223 + in
6.224 + if null pdl
6.225 + then
6.226 + NONE
6.227 + else if (OS.IO.isIn (hd pdl))
6.228 + then
6.229 + (SOME ( getCmds (toParentStr, fromParentStr, [])))
6.230 + else
6.231 + NONE
6.232 + end
6.233 + else
6.234 + NONE
6.235 + end
6.236 +
6.237 +
6.238
6.239 - fun pollChildInput (fromStr) =
6.240 - let val iod = getInIoDesc fromStr
6.241 - in
6.242 - if isSome iod
6.243 - then
6.244 - let val pd = OS.IO.pollDesc (valOf iod)
6.245 - in
6.246 - if (isSome pd ) then
6.247 - let val pd' = OS.IO.pollIn (valOf pd)
6.248 - val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
6.249 - in
6.250 - if null pdl
6.251 - then
6.252 - NONE
6.253 - else if (OS.IO.isIn (hd pdl))
6.254 - then
6.255 - SOME (getCmd (TextIO.inputLine fromStr))
6.256 - else
6.257 - NONE
6.258 - end
6.259 - else
6.260 - NONE
6.261 - end
6.262 - else
6.263 - NONE
6.264 - end
6.265 + fun pollChildInput (fromStr) =
6.266 + let val iod = getInIoDesc fromStr
6.267 + in
6.268 + if isSome iod
6.269 + then
6.270 + let val pd = OS.IO.pollDesc (valOf iod)
6.271 + in
6.272 + if (isSome pd ) then
6.273 + let val pd' = OS.IO.pollIn (valOf pd)
6.274 + val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
6.275 + in
6.276 + if null pdl
6.277 + then
6.278 + NONE
6.279 + else if (OS.IO.isIn (hd pdl))
6.280 + then
6.281 + SOME (getCmd (TextIO.inputLine fromStr))
6.282 + else
6.283 + NONE
6.284 + end
6.285 + else
6.286 + NONE
6.287 + end
6.288 + else
6.289 + NONE
6.290 + end
6.291
6.292
6.293 - (****************************************************************************)
6.294 - (* Check all vampire processes currently running for output *)
6.295 - (****************************************************************************)
6.296 - (*********************************)
6.297 - fun checkChildren ([], toParentStr) = [] (*** no children to check ********)
6.298 - (*********************************)
6.299 - | checkChildren ((childProc::otherChildren), toParentStr) =
6.300 - let val (childInput,childOutput) = cmdstreamsOf childProc
6.301 - val child_handle= cmdchildHandle childProc
6.302 - (* childCmd is the .dfg file that the problem is in *)
6.303 - val childCmd = fst(snd (cmdchildInfo childProc))
6.304 - (* now get the number of the subgoal from the filename *)
6.305 - val sg_num = int_of_string(get_nth 5 (rev(explode childCmd)))
6.306 - val childIncoming = pollChildInput childInput
6.307 - val parentID = Posix.ProcEnv.getppid()
6.308 - val prover = cmdProver childProc
6.309 - val thmstring = cmdThm childProc
6.310 - val sign = sign_of_thm thm
6.311 - val prems = prems_of thm
6.312 - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
6.313 - val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
6.314 - val goalstring = cmdGoal childProc
6.315 -
6.316 - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));
6.317 - val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
6.318 - val _ = TextIO.closeOut outfile
6.319 - in
6.320 - if (isSome childIncoming)
6.321 - then
6.322 - (* check here for prover label on child*)
6.323 -
6.324 - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
6.325 - val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
6.326 - val _ = TextIO.closeOut outfile
6.327 - val childDone = (case prover of
6.328 - (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) )
6.329 - in
6.330 - if childDone (**********************************************)
6.331 - then (* child has found a proof and transferred it *)
6.332 - (**********************************************)
6.333 + (****************************************************************************)
6.334 + (* Check all vampire processes currently running for output *)
6.335 + (****************************************************************************)
6.336 + (*********************************)
6.337 + fun checkChildren ([], toParentStr) = [] (*** no children to check ********)
6.338 + (*********************************)
6.339 + | checkChildren ((childProc::otherChildren), toParentStr) =
6.340 + let val (childInput,childOutput) = cmdstreamsOf childProc
6.341 + val child_handle= cmdchildHandle childProc
6.342 + (* childCmd is the .dfg file that the problem is in *)
6.343 + val childCmd = fst(snd (cmdchildInfo childProc))
6.344 + (* now get the number of the subgoal from the filename *)
6.345 + val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
6.346 + val childIncoming = pollChildInput childInput
6.347 + val parentID = Posix.ProcEnv.getppid()
6.348 + val prover = cmdProver childProc
6.349 + val thmstring = cmdThm childProc
6.350 + val sign = sign_of_thm thm
6.351 + val prems = prems_of thm
6.352 + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
6.353 + val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
6.354 + val goalstring = cmdGoal childProc
6.355 +
6.356 + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));
6.357 + val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
6.358 + val _ = TextIO.closeOut outfile
6.359 + in
6.360 + if (isSome childIncoming)
6.361 + then
6.362 + (* check here for prover label on child*)
6.363 +
6.364 + let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
6.365 + val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
6.366 + val _ = TextIO.closeOut outfile
6.367 + val childDone = (case prover of
6.368 + (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) )
6.369 + in
6.370 + if childDone (**********************************************)
6.371 + then (* child has found a proof and transferred it *)
6.372 + (**********************************************)
6.373
6.374 - (**********************************************)
6.375 - (* Remove this child and go on to check others*)
6.376 - (**********************************************)
6.377 - ( Unix.reap child_handle;
6.378 - checkChildren(otherChildren, toParentStr))
6.379 - else
6.380 - (**********************************************)
6.381 - (* Keep this child and go on to check others *)
6.382 - (**********************************************)
6.383 + (**********************************************)
6.384 + (* Remove this child and go on to check others*)
6.385 + (**********************************************)
6.386 + ( Unix.reap child_handle;
6.387 + checkChildren(otherChildren, toParentStr))
6.388 + else
6.389 + (**********************************************)
6.390 + (* Keep this child and go on to check others *)
6.391 + (**********************************************)
6.392
6.393 - (childProc::(checkChildren (otherChildren, toParentStr)))
6.394 - end
6.395 - else
6.396 - let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
6.397 - val _ = TextIO.output (outfile,"No child output " )
6.398 - val _ = TextIO.closeOut outfile
6.399 - in
6.400 - (childProc::(checkChildren (otherChildren, toParentStr)))
6.401 - end
6.402 - end
6.403 + (childProc::(checkChildren (otherChildren, toParentStr)))
6.404 + end
6.405 + else
6.406 + let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
6.407 + val _ = TextIO.output (outfile,"No child output " )
6.408 + val _ = TextIO.closeOut outfile
6.409 + in
6.410 + (childProc::(checkChildren (otherChildren, toParentStr)))
6.411 + end
6.412 + end
6.413
6.414 -
6.415 - (********************************************************************)
6.416 - (* call resolution processes *)
6.417 - (* settings should be a list of strings *)
6.418 - (* e.g. ["-t 300", "-m 100000"] *)
6.419 - (* takes list of (string, string, string list, string)list proclist *)
6.420 - (********************************************************************)
6.421 +
6.422 + (********************************************************************)
6.423 + (* call resolution processes *)
6.424 + (* settings should be a list of strings *)
6.425 + (* e.g. ["-t 300", "-m 100000"] *)
6.426 + (* takes list of (string, string, string list, string)list proclist *)
6.427 + (********************************************************************)
6.428
6.429
6.430 - (*** add subgoal id num to this *)
6.431 - fun execCmds [] procList = procList
6.432 - | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList =
6.433 - if (prover = "spass")
6.434 - then
6.435 - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
6.436 - val (instr, outstr)=Unix.streamsOf childhandle
6.437 - val newProcList = (((CMDPROC{
6.438 - prover = prover,
6.439 - cmd = file,
6.440 - thmstring = thmstring,
6.441 - goalstring = goalstring,
6.442 - proc_handle = childhandle,
6.443 - instr = instr,
6.444 - outstr = outstr })::procList))
6.445 - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));
6.446 - val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
6.447 - val _ = TextIO.closeOut outfile
6.448 - in
6.449 - execCmds cmds newProcList
6.450 - end
6.451 - else
6.452 - let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
6.453 - val (instr, outstr)=Unix.streamsOf childhandle
6.454 - val newProcList = (((CMDPROC{
6.455 - prover = prover,
6.456 - cmd = file,
6.457 - thmstring = thmstring,
6.458 - goalstring = goalstring,
6.459 - proc_handle = childhandle,
6.460 - instr = instr,
6.461 - outstr = outstr })::procList))
6.462 - in
6.463 - execCmds cmds newProcList
6.464 - end
6.465 +(*** add subgoal id num to this *)
6.466 + fun execCmds [] procList = procList
6.467 + | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList =
6.468 + if (prover = "spass")
6.469 + then
6.470 + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
6.471 + val (instr, outstr)=Unix.streamsOf childhandle
6.472 + val newProcList = (((CMDPROC{
6.473 + prover = prover,
6.474 + cmd = file,
6.475 + thmstring = thmstring,
6.476 + goalstring = goalstring,
6.477 + proc_handle = childhandle,
6.478 + instr = instr,
6.479 + outstr = outstr })::procList))
6.480 + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));
6.481 + val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
6.482 + val _ = TextIO.closeOut outfile
6.483 + in
6.484 + execCmds cmds newProcList
6.485 + end
6.486 + else
6.487 + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
6.488 + val (instr, outstr)=Unix.streamsOf childhandle
6.489 + val newProcList = (((CMDPROC{
6.490 + prover = prover,
6.491 + cmd = file,
6.492 + thmstring = thmstring,
6.493 + goalstring = goalstring,
6.494 + proc_handle = childhandle,
6.495 + instr = instr,
6.496 + outstr = outstr })::procList))
6.497 + in
6.498 + execCmds cmds newProcList
6.499 + end
6.500
6.501
6.502
6.503 - (****************************************)
6.504 - (* call resolution processes remotely *)
6.505 - (* settings should be a list of strings *)
6.506 - (* e.g. ["-t 300", "-m 100000"] *)
6.507 - (****************************************)
6.508 -
6.509 - (* fun execRemoteCmds [] procList = procList
6.510 - | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList =
6.511 - let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
6.512 - in
6.513 - execRemoteCmds cmds newProcList
6.514 - end
6.515 + (****************************************)
6.516 + (* call resolution processes remotely *)
6.517 + (* settings should be a list of strings *)
6.518 + (* e.g. ["-t 300", "-m 100000"] *)
6.519 + (****************************************)
6.520 +
6.521 + (* fun execRemoteCmds [] procList = procList
6.522 + | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList =
6.523 + let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
6.524 + in
6.525 + execRemoteCmds cmds newProcList
6.526 + end
6.527 *)
6.528
6.529 - fun printList (outStr, []) = ()
6.530 - | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))
6.531 + fun printList (outStr, []) = ()
6.532 + | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))
6.533
6.534
6.535 - (**********************************************)
6.536 - (* Watcher Loop *)
6.537 - (**********************************************)
6.538 + (**********************************************)
6.539 + (* Watcher Loop *)
6.540 + (**********************************************)
6.541 +
6.542
6.543
6.544
6.545 -
6.546 - fun keepWatching (toParentStr, fromParentStr,procList) =
6.547 - let fun loop (procList) =
6.548 - (
6.549 - let val cmdsFromIsa = pollParentInput ()
6.550 - fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n");
6.551 - TextIO.flushOut toParentStr;
6.552 - killChildren (map (cmdchildHandle) procList);
6.553 - ())
6.554 -
6.555 - in
6.556 - (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
6.557 - (**********************************)
6.558 - if (isSome cmdsFromIsa) then (* deal with input from Isabelle *)
6.559 - ( (**********************************)
6.560 - if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
6.561 - then
6.562 - (
6.563 - let val child_handles = map cmdchildHandle procList
6.564 - in
6.565 - killChildren child_handles;
6.566 - (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([])
6.567 - end
6.568 -
6.569 - )
6.570 - else
6.571 - (
6.572 - if ((length procList)<10) (********************)
6.573 - then (* Execute locally *)
6.574 - ( (********************)
6.575 - let
6.576 - val newProcList = execCmds (valOf cmdsFromIsa) procList
6.577 - val parentID = Posix.ProcEnv.getppid()
6.578 - val newProcList' =checkChildren (newProcList, toParentStr)
6.579 - in
6.580 - (*Posix.Process.sleep (Time.fromSeconds 1);*)
6.581 - loop (newProcList')
6.582 - end
6.583 - )
6.584 - else (*********************************)
6.585 - (* Execute remotely *)
6.586 - (* (actually not remote for now )*)
6.587 - ( (*********************************)
6.588 - let
6.589 - val newProcList = execCmds (valOf cmdsFromIsa) procList
6.590 - val parentID = Posix.ProcEnv.getppid()
6.591 - val newProcList' =checkChildren (newProcList, toParentStr)
6.592 - in
6.593 - (*Posix.Process.sleep (Time.fromSeconds 1);*)
6.594 - loop (newProcList')
6.595 - end
6.596 - )
6.597 + fun keepWatching (toParentStr, fromParentStr,procList) =
6.598 + let fun loop (procList) =
6.599 + (
6.600 + let val cmdsFromIsa = pollParentInput ()
6.601 + fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n");
6.602 + TextIO.flushOut toParentStr;
6.603 + killChildren (map (cmdchildHandle) procList);
6.604 + ())
6.605 +
6.606 + in
6.607 + (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
6.608 + (**********************************)
6.609 + if (isSome cmdsFromIsa) then (* deal with input from Isabelle *)
6.610 + ( (**********************************)
6.611 + if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
6.612 + then
6.613 + (
6.614 + let val child_handles = map cmdchildHandle procList
6.615 + in
6.616 + killChildren child_handles;
6.617 + (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([])
6.618 + end
6.619 +
6.620 + )
6.621 + else
6.622 + (
6.623 + if ((length procList)<10) (********************)
6.624 + then (* Execute locally *)
6.625 + ( (********************)
6.626 + let
6.627 + val newProcList = execCmds (valOf cmdsFromIsa) procList
6.628 + val parentID = Posix.ProcEnv.getppid()
6.629 + val newProcList' =checkChildren (newProcList, toParentStr)
6.630 + in
6.631 + (*Posix.Process.sleep (Time.fromSeconds 1);*)
6.632 + loop (newProcList')
6.633 + end
6.634 + )
6.635 + else (*********************************)
6.636 + (* Execute remotely *)
6.637 + (* (actually not remote for now )*)
6.638 + ( (*********************************)
6.639 + let
6.640 + val newProcList = execCmds (valOf cmdsFromIsa) procList
6.641 + val parentID = Posix.ProcEnv.getppid()
6.642 + val newProcList' =checkChildren (newProcList, toParentStr)
6.643 + in
6.644 + (*Posix.Process.sleep (Time.fromSeconds 1);*)
6.645 + loop (newProcList')
6.646 + end
6.647 + )
6.648
6.649
6.650
6.651 - )
6.652 - ) (******************************)
6.653 - else (* No new input from Isabelle *)
6.654 - (******************************)
6.655 - ( let val newProcList = checkChildren ((procList), toParentStr)
6.656 - in
6.657 - Posix.Process.sleep (Time.fromSeconds 1);
6.658 - loop (newProcList)
6.659 - end
6.660 -
6.661 - )
6.662 - end)
6.663 - in
6.664 - loop (procList)
6.665 - end
6.666 -
6.667 -
6.668 - in
6.669 - (***************************)
6.670 - (*** Sort out pipes ********)
6.671 - (***************************)
6.672 + )
6.673 + ) (******************************)
6.674 + else (* No new input from Isabelle *)
6.675 + (******************************)
6.676 + ( let val newProcList = checkChildren ((procList), toParentStr)
6.677 + in
6.678 + Posix.Process.sleep (Time.fromSeconds 1);
6.679 + loop (newProcList)
6.680 + end
6.681 +
6.682 + )
6.683 + end)
6.684 + in
6.685 + loop (procList)
6.686 + end
6.687 +
6.688 +
6.689 + in
6.690 + (***************************)
6.691 + (*** Sort out pipes ********)
6.692 + (***************************)
6.693
6.694 - Posix.IO.close (#outfd p1);
6.695 - Posix.IO.close (#infd p2);
6.696 - Posix.IO.dup2{old = oldchildin, new = fromParent};
6.697 - Posix.IO.close oldchildin;
6.698 - Posix.IO.dup2{old = oldchildout, new = toParent};
6.699 - Posix.IO.close oldchildout;
6.700 + Posix.IO.close (#outfd p1);
6.701 + Posix.IO.close (#infd p2);
6.702 + Posix.IO.dup2{old = oldchildin, new = fromParent};
6.703 + Posix.IO.close oldchildin;
6.704 + Posix.IO.dup2{old = oldchildout, new = toParent};
6.705 + Posix.IO.close oldchildout;
6.706
6.707 - (***************************)
6.708 - (* start the watcher loop *)
6.709 - (***************************)
6.710 - keepWatching (toParentStr, fromParentStr, procList);
6.711 + (***************************)
6.712 + (* start the watcher loop *)
6.713 + (***************************)
6.714 + keepWatching (toParentStr, fromParentStr, procList);
6.715
6.716
6.717 - (****************************************************************************)
6.718 - (* fake return value - actually want the watcher to loop until killed *)
6.719 - (****************************************************************************)
6.720 - Posix.Process.wordToPid 0w0
6.721 -
6.722 - end);
6.723 - (* end case *)
6.724 + (****************************************************************************)
6.725 + (* fake return value - actually want the watcher to loop until killed *)
6.726 + (****************************************************************************)
6.727 + Posix.Process.wordToPid 0w0
6.728 +
6.729 + end);
6.730 + (* end case *)
6.731
6.732
6.733 - val _ = TextIO.flushOut TextIO.stdOut
6.734 + val _ = TextIO.flushOut TextIO.stdOut
6.735
6.736 - (*******************************)
6.737 - (*** set watcher going ********)
6.738 - (*******************************)
6.739 + (*******************************)
6.740 + (*** set watcher going ********)
6.741 + (*******************************)
6.742
6.743 - val procList = []
6.744 - val pid = startWatcher (procList)
6.745 - (**************************************************)
6.746 - (* communication streams to watcher *)
6.747 - (**************************************************)
6.748 + val procList = []
6.749 + val pid = startWatcher (procList)
6.750 + (**************************************************)
6.751 + (* communication streams to watcher *)
6.752 + (**************************************************)
6.753
6.754 - val instr = openInFD ("_exec_in", #infd p2)
6.755 - val outstr = openOutFD ("_exec_out", #outfd p1)
6.756 -
6.757 - in
6.758 - (*******************************)
6.759 - (* close the child-side fds *)
6.760 - (*******************************)
6.761 - Posix.IO.close (#outfd p2);
6.762 - Posix.IO.close (#infd p1);
6.763 - (* set the fds close on exec *)
6.764 - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
6.765 - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
6.766 -
6.767 - (*******************************)
6.768 - (* return value *)
6.769 - (*******************************)
6.770 - PROC{pid = pid,
6.771 - instr = instr,
6.772 - outstr = outstr
6.773 - }
6.774 - end;
6.775 + val instr = openInFD ("_exec_in", #infd p2)
6.776 + val outstr = openOutFD ("_exec_out", #outfd p1)
6.777 +
6.778 + in
6.779 + (*******************************)
6.780 + (* close the child-side fds *)
6.781 + (*******************************)
6.782 + Posix.IO.close (#outfd p2);
6.783 + Posix.IO.close (#infd p1);
6.784 + (* set the fds close on exec *)
6.785 + Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
6.786 + Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
6.787 +
6.788 + (*******************************)
6.789 + (* return value *)
6.790 + (*******************************)
6.791 + PROC{pid = pid,
6.792 + instr = instr,
6.793 + outstr = outstr
6.794 + }
6.795 + end;
6.796
6.797
6.798
7.1 --- a/src/HOL/Tools/res_atp.ML Tue May 24 07:43:38 2005 +0200
7.2 +++ b/src/HOL/Tools/res_atp.ML Tue May 24 10:23:24 2005 +0200
7.3 @@ -245,19 +245,18 @@
7.4 (**********************************************)
7.5
7.6 fun isar_atp_goal' thm k n tfree_lits (childin, childout, pid) =
7.7 - if (k > n)
7.8 - then ()
7.9 - else
7.10 - (let val prems = prems_of thm
7.11 - val sg_term = get_nth n prems
7.12 - val thmstring = string_of_thm thm
7.13 - in
7.14 -
7.15 - (warning("in isar_atp_goal'"));
7.16 - (warning("thmstring in isar_atp_goal': "^thmstring));
7.17 - isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm;
7.18 - isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid)
7.19 - end);
7.20 + if (k > n)
7.21 + then ()
7.22 + else
7.23 + let val prems = prems_of thm
7.24 + val sg_term = ReconOrderClauses.get_nth n prems
7.25 + val thmstring = string_of_thm thm
7.26 + in
7.27 + (warning("in isar_atp_goal'"));
7.28 + (warning("thmstring in isar_atp_goal': "^thmstring));
7.29 + isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm;
7.30 + isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid)
7.31 + end;
7.32
7.33
7.34 fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) =