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