# HG changeset patch # User paulson # Date 1122046983 -7200 # Node ID fa26952fa7b630231f35cb182934cfa81335dae6 # Parent 6fb188ca5f918487e212daf24df56328e3ac6294 reformatting and tidying diff -r 6fb188ca5f91 -r fa26952fa7b6 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Jul 22 17:42:40 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Jul 22 17:43:03 2005 +0200 @@ -15,40 +15,6 @@ infixr 8 ++; infixr 7 >>; infixr 6 ||; - -(* -fun fill_cls_array array n [] = () -| fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x) - in - fill_cls_array array (n+1) (xs) - end; - - - -fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)= - symtable := Symtab.update((name , cls), !symtable); - - -fun memo_add_all ([], symtable) = () -| memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable) - in - memo_add_all (xs, symtable) - end - -fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of - NONE => [] - |SOME cls => cls ; - - -fun retrieve_clause array symtable clausenum = let - val (name, clnum) = Array.sub(array, clausenum) - val clauses = memo_find_clause (name, symtable) - val clause = get_nth clnum clauses - in - (name, clause) - end - *) - (* Versions that include type information *) (* FIXME rename to str_of_thm *) @@ -251,8 +217,6 @@ end - - (***********************************************) (* get axioms for reconstruction *) (***********************************************) @@ -267,12 +231,6 @@ fun get_axioms_used proof_steps thms clause_arr num_of_clauses = let - (*val outfile = TextIO.openOut(File.platform_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 [] @@ -284,7 +242,7 @@ (* 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.platform_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names + val _ = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names val _ = TextIO.output (outfile,clasimp_namestr) val _ = TextIO.closeOut outfile @@ -309,13 +267,8 @@ val meta_strs = map ReconOrderClauses.get_meta_lits metas val metas_and_strs = ListPair.zip (metas,meta_strs) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses"))); - val _ = TextIO.output (outfile, onestr ax_strs) - - val _ = TextIO.closeOut outfile - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs"))); - val _ = TextIO.output (outfile, onestr meta_strs) - val _ = TextIO.closeOut outfile + val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs) + val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs) (* get list of axioms as thms with their variables *) @@ -327,13 +280,10 @@ 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 - [] - + then ListPair.zip (extra_metas,extra_vars) + else [] (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas"))) + val _ = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas"))) val _ = TextIO.output (outfile, ((thmstrings ax_metas ""))) val _ = TextIO.closeOut outfile @@ -344,13 +294,10 @@ 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 - - - + end; + (*********************************************************************) (* Pass in spass string of proof and string version of isabelle goal *) @@ -372,122 +319,103 @@ \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\ \1454[0:Obv:1453.0] || -> .";*) -fun subst_for a b [] = "" - | subst_for a b (x :: xs) = - if x = a - then - b ^ subst_for a b xs - else - x ^ subst_for a b xs; +fun subst_for a b = String.translate (fn c => str (if c=a then b else c)); -val remove_linebreaks = subst_for "\n" "\t" o explode; -val restore_linebreaks = subst_for "\t" "\n" o explode; - +val remove_linebreaks = subst_for #"\n" #"\t"; +val restore_linebreaks = subst_for #"\t" #"\n"; fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = - let val outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile"))); - val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n num of clauses is: "^(string_of_int num_of_clauses))) - - val _ = TextIO.closeOut outfile + let val _ = File.append(File.tmp_path (Path.basic"thmstringfile")) + ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n num of clauses is: "^(string_of_int num_of_clauses)) - (***********************************) - (* parse spass proof into datatype *) - (***********************************) - - val tokens = #1(lex proofstr) - val proof_steps1 = parse tokens - val proof_steps = just_change_space proof_steps1 - val outfile = TextIO.openOut(File.platform_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.platform_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 *) + (***********************************) + (* parse spass proof into datatype *) + (***********************************) + val tokens = #1(lex proofstr) + val proof_steps1 = parse tokens + val proof_steps = just_change_space proof_steps1 + val _ = File.write (File.tmp_path (Path.basic "foo_parse")) ("Did parsing on "^proofstr) + val _ = File.write(File.tmp_path (Path.basic "foo_thmstring_at_parse")) + ("Parsing for thmstring: "^thmstring) + (************************************) + (* 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 (axiom_names) = get_axiom_names proof_steps thms clause_arr num_of_clauses - val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "") - val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring)) - val _ = TextIO.closeOut outfile - - in - TextIO.output (toParent, ax_str^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, "goalstring: "^goalstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, "thmstring: "^thmstring^"\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.platform_path(File.tmp_path (Path.basic "foo_handler"))); + val (axiom_names) = get_axiom_names proof_steps thms clause_arr num_of_clauses + val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "") + val _ = File.append(File.tmp_path (Path.basic "reconstrfile")) + ("reconstring is: "^ax_str^" "^goalstring) + in + TextIO.output (toParent, ax_str^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, "goalstring: "^goalstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, "thmstring: "^thmstring^"\n"); + TextIO.flushOut toParent; - val _ = TextIO.output (outfile, ("In exception handler")); - val _ = TextIO.closeOut outfile - in - TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, (remove_linebreaks thmstring)^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, ( (remove_linebreaks 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) + 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 _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" + in + TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" ); + TextIO.flushOut toParent; + TextIO.output (toParent, (remove_linebreaks thmstring)^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, ( (remove_linebreaks 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 fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = - let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile"))); val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses))) - val _ = TextIO.closeOut outfile + let val _ = File.append(File.tmp_path (Path.basic "thmstringfile")) + (" thmstring is: "^thmstring^"proofstr is: "^proofstr^ + "goalstr is: "^goalstring^" num of clauses is: "^ + (string_of_int num_of_clauses)) + + (***********************************) + (* get vampire axiom names *) + (***********************************) - (***********************************) - (* get vampire axiom names *) - (***********************************) - - val (axiom_names) = get_axiom_names_vamp proofstr thms clause_arr num_of_clauses - val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "") - val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring)) - val _ = TextIO.closeOut outfile - - in - TextIO.output (toParent, ax_str^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, "goalstring: "^goalstring^"\n"); - TextIO.flushOut toParent; - TextIO.output (toParent, "thmstring: "^thmstring^"\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.platform_path(File.tmp_path (Path.basic "foo_handler"))); + val (axiom_names) = get_axiom_names_vamp proofstr thms clause_arr num_of_clauses + val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "") + in + File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^" "^goalstring); + TextIO.output (toParent, ax_str^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, "goalstring: "^goalstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, "thmstring: "^thmstring^"\n"); + TextIO.flushOut toParent; - val _ = TextIO.output (outfile, ("In exception handler")); - val _ = TextIO.closeOut outfile - in - TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) ); - 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) - - + 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 _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" + in + TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) ); + 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 proofstr = "1582[0:Inp] || -> v_P*.\ @@ -495,104 +423,87 @@ \1584[0:MRR:1583.0,1582.0] || -> ."; *) fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = - let val outfile = TextIO.openOut(File.platform_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 _ = File.write(File.tmp_path (Path.basic "thmstringfile")) + (" thmstring is: "^thmstring^"proofstr is: "^proofstr) + val tokens = #1(lex proofstr) - val tokens = #1(lex proofstr) - - + (***********************************) + (* parse spass proof into datatype *) + (***********************************) + val proof_steps1 = parse tokens + val proof_steps = just_change_space proof_steps1 - (***********************************) - (* parse spass proof into datatype *) - (***********************************) - - val proof_steps1 = parse tokens - val proof_steps = just_change_space proof_steps1 - - val outfile = TextIO.openOut(File.platform_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.platform_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 *) - (************************************) + val _ = File.write (File.tmp_path (Path.basic "foo_parse")) + ("Did parsing on "^proofstr) + + val _ = File.write (File.tmp_path (Path.basic "foo_thmstring_at_parse")) + ("Parsing for thmstring: "^thmstring) + (************************************) + (* 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 _ = File.write (File.tmp_path (Path.basic "foo_axiom")) "got axioms" - (* 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.platform_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.platform_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.platform_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.platform_path(File.tmp_path (Path.basic "reconstringfile"))); + (************************************) + (* translate proof *) + (************************************) + val _ = File.write (File.tmp_path (Path.basic "foo_steps")) + ("about to translate proof, steps: " + ^(init_proofsteps_to_string proof_steps "")) + val (newthm,proof) = translate_proof numcls proof_steps vars + val _ = File.write (File.tmp_path (Path.basic "foo_steps2")) + ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")) + (***************************************************) + (* 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 _ = File.write (File.tmp_path (Path.basic "reconstringfile")) + (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) + 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; - 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.platform_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 for resolution proof:"^(remove_linebreaks proofstr) ^"\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) - - - + 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 _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler" + in + TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\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 (**********************************************************************************) @@ -889,10 +800,7 @@ (isar_lines firststeps "")^ (last_isar_line laststep)^ ("qed") - val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file"))); - - val _ = TextIO.output (outfile, isar_proof) - val _ = TextIO.closeOut outfile + val _ = File.write (File.tmp_path (Path.basic "isar_proof_file")) isar_proof in isar_proof end;