src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17235 8e55ad29b690
parent 17122 278eb6251dc0
child 17306 5cde710a8a23
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 02 17:55:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 02 21:29:33 2005 +0200
     1.3 @@ -217,6 +217,26 @@
     1.4     end
     1.5      
     1.6  
     1.7 +fun get_axiom_names_E proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
     1.8 +   let 
     1.9 +     (* not sure why this is necessary again, but seems to be *)
    1.10 +      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.11 +      val step_nums =get_linenums proofstr
    1.12 +  
    1.13 +     (***********************************************)
    1.14 +     (* here need to add the clauses from clause_arr*)
    1.15 +     (***********************************************)
    1.16 +  
    1.17 +      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.18 +      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    1.19 +  
    1.20 +      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.21 +                         (concat clasimp_names)
    1.22 +      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.23 +   in
    1.24 +      clasimp_names
    1.25 +   end
    1.26 +
    1.27  (***********************************************)
    1.28  (* get axioms for reconstruction               *)
    1.29  (***********************************************)
    1.30 @@ -419,6 +439,46 @@
    1.31      end;
    1.32  
    1.33  
    1.34 +fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.35 + let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
    1.36 +               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
    1.37 +                "goalstr is: "^goalstring^" num of clauses is: "^
    1.38 +                (string_of_int num_of_clauses))
    1.39 +
    1.40 +    (***********************************)
    1.41 +    (* get vampire axiom names         *)
    1.42 +    (***********************************)
    1.43 +
    1.44 +     val (axiom_names) = get_axiom_names_E proofstr  thms clause_arr  num_of_clauses
    1.45 +     val ax_str = "Rules from clasimpset used in proof found by E: " ^
    1.46 +                  rules_to_string axiom_names
    1.47 +    in 
    1.48 +	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
    1.49 +         TextIO.output (toParent, ax_str^"\n");
    1.50 +	 TextIO.flushOut toParent;
    1.51 +	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    1.52 +	 TextIO.flushOut toParent;
    1.53 +	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
    1.54 +	 TextIO.flushOut toParent;
    1.55 +
    1.56 +	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.57 +	(* Attempt to prevent several signals from turning up simultaneously *)
    1.58 +	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
    1.59 +    end
    1.60 +    handle _ => 
    1.61 +    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
    1.62 +    in 
    1.63 +	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
    1.64 +	TextIO.flushOut toParent;
    1.65 +	 TextIO.output (toParent, thmstring^"\n");
    1.66 +	 TextIO.flushOut toParent;
    1.67 +	 TextIO.output (toParent, goalstring^"\n");
    1.68 +	 TextIO.flushOut toParent;
    1.69 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.70 +	(* Attempt to prevent several signals from turning up simultaneously *)
    1.71 +	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
    1.72 +    end;
    1.73 +
    1.74  (* val proofstr = "1582[0:Inp] || -> v_P*.\
    1.75                   \1583[0:Inp] || v_P* -> .\
    1.76  		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)