src/HOL/Tools/res_reconstruct.ML
changeset 24425 ca97c6f3d9cd
parent 24387 cf2470f64b1d
child 24493 d4380e9b287b
     1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri Aug 24 14:15:58 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Fri Aug 24 14:16:44 2007 +0200
     1.3 @@ -7,22 +7,30 @@
     1.4  (*  Code to deal with the transfer of proofs from a prover process         *)
     1.5  (***************************************************************************)
     1.6  signature RES_RECONSTRUCT =
     1.7 -  sig
     1.8 -    val checkEProofFound:
     1.9 -          TextIO.instream * TextIO.outstream * Posix.Process.pid *
    1.10 -          string * Proof.context * thm * int * string Vector.vector -> bool
    1.11 -    val checkVampProofFound:
    1.12 -          TextIO.instream * TextIO.outstream * Posix.Process.pid *
    1.13 -          string * Proof.context * thm * int * string Vector.vector -> bool
    1.14 -    val checkSpassProofFound:
    1.15 -          TextIO.instream * TextIO.outstream * Posix.Process.pid *
    1.16 -          string * Proof.context * thm * int * string Vector.vector -> bool
    1.17 -    val signal_parent:
    1.18 -          TextIO.outstream * Posix.Process.pid * string * string -> unit
    1.19 +sig
    1.20 +  datatype atp = E | SPASS | Vampire
    1.21 +  val modulus:     int ref
    1.22 +  val recon_sorts: bool ref
    1.23 +  val checkEProofFound:
    1.24 +	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    1.25 +	string * Proof.context * thm * int * string Vector.vector -> bool
    1.26 +  val checkVampProofFound:
    1.27 +	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    1.28 +	string * Proof.context * thm * int * string Vector.vector -> bool
    1.29 +  val checkSpassProofFound:
    1.30 +	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    1.31 +	string * Proof.context * thm * int * string Vector.vector -> bool
    1.32 +  val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit
    1.33 +  val txt_path: string -> Path.T
    1.34 +  val fix_sorts: sort Vartab.table -> term -> term
    1.35 +  val invert_const: string -> string
    1.36 +  val invert_type_const: string -> string
    1.37 +  val num_typargs: Context.theory -> string -> int
    1.38 +  val make_tvar: string -> typ
    1.39 +  val strip_prefix: string -> string -> string option
    1.40 +end;
    1.41  
    1.42 -  end;
    1.43 -
    1.44 -structure ResReconstruct =
    1.45 +structure ResReconstruct : RES_RECONSTRUCT =
    1.46  struct
    1.47  
    1.48  val trace_path = Path.basic "atp_trace";
    1.49 @@ -30,8 +38,7 @@
    1.50  fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    1.51                else ();
    1.52  
    1.53 -(*Full proof reconstruction wanted*)
    1.54 -val full = ref true;
    1.55 +datatype atp = E | SPASS | Vampire;
    1.56  
    1.57  val recon_sorts = ref true;
    1.58  
    1.59 @@ -467,13 +474,6 @@
    1.60      OS.Process.sleep (Time.fromMilliseconds 600)
    1.61    end;
    1.62  
    1.63 -fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
    1.64 -  let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
    1.65 -  in
    1.66 -    signal_success probfile toParent ppid
    1.67 -      (decode_tstp_file cnfs ctxt th sgno thm_names)
    1.68 -  end;
    1.69 -
    1.70  
    1.71  (**** retrieve the axioms that were used in the proof ****)
    1.72  
    1.73 @@ -491,15 +491,15 @@
    1.74   (*String contains multiple lines. We want those of the form
    1.75       "253[0:Inp] et cetera..."
    1.76    A list consisting of the first number in each line is returned. *)
    1.77 -fun get_spass_linenums proofstr =
    1.78 +fun get_spass_linenums proofextract =
    1.79    let val toks = String.tokens (not o Char.isAlphaNum)
    1.80        fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    1.81          | inputno _ = NONE
    1.82 -      val lines = String.tokens (fn c => c = #"\n") proofstr
    1.83 +      val lines = String.tokens (fn c => c = #"\n") proofextract
    1.84    in  List.mapPartial (inputno o toks) lines  end
    1.85  
    1.86 -fun get_axiom_names_spass proofstr thm_names =
    1.87 -   get_axiom_names thm_names (get_spass_linenums proofstr);
    1.88 +fun get_axiom_names_spass proofextract thm_names =
    1.89 +   get_axiom_names thm_names (get_spass_linenums proofextract);
    1.90  
    1.91  fun not_comma c = c <>  #",";
    1.92  
    1.93 @@ -516,47 +516,43 @@
    1.94    in  Int.fromString ints  end
    1.95    handle Fail _ => NONE;
    1.96  
    1.97 -fun get_axiom_names_tstp proofstr thm_names =
    1.98 -   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
    1.99 +fun get_axiom_names_tstp proofextract thm_names =
   1.100 +   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
   1.101  
   1.102   (*String contains multiple lines. We want those of the form
   1.103       "*********** [448, input] ***********".
   1.104    A list consisting of the first number in each line is returned. *)
   1.105 -fun get_vamp_linenums proofstr =
   1.106 +fun get_vamp_linenums proofextract =
   1.107    let val toks = String.tokens (not o Char.isAlphaNum)
   1.108        fun inputno [ntok,"input"] = Int.fromString ntok
   1.109          | inputno _ = NONE
   1.110 -      val lines = String.tokens (fn c => c = #"\n") proofstr
   1.111 +      val lines = String.tokens (fn c => c = #"\n") proofextract
   1.112    in  List.mapPartial (inputno o toks) lines  end
   1.113  
   1.114 -fun get_axiom_names_vamp proofstr thm_names =
   1.115 -   get_axiom_names thm_names (get_vamp_linenums proofstr);
   1.116 +fun get_axiom_names_vamp proofextract thm_names =
   1.117 +   get_axiom_names thm_names (get_vamp_linenums proofextract);
   1.118 +
   1.119 +fun get_axiom_names E       = get_axiom_names_tstp
   1.120 +  | get_axiom_names SPASS   = get_axiom_names_spass
   1.121 +  | get_axiom_names Vampire = get_axiom_names_vamp;
   1.122  
   1.123  fun rules_to_metis [] = "metis"
   1.124    | rules_to_metis xs = "(metis " ^ space_implode " " xs ^ ")"
   1.125  
   1.126 +fun metis_line atp proofextract thm_names =
   1.127 +  "apply " ^ rules_to_metis (get_axiom_names atp proofextract thm_names);
   1.128  
   1.129  (*The signal handler in watcher.ML must be able to read the output of this.*)
   1.130 -fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names =
   1.131 - (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   1.132 -         " num of clauses is " ^ string_of_int (Vector.length thm_names));
   1.133 -  signal_success probfile toParent ppid
   1.134 -    ("apply " ^ rules_to_metis (getax proofstr thm_names))
   1.135 - )
   1.136 - handle e => (*FIXME: exn handler is too general!*)
   1.137 -  (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);
   1.138 -   TextIO.output (toParent, "Translation failed for the proof: " ^
   1.139 -                  String.toString proofstr ^ "\n");
   1.140 -   TextIO.output (toParent, probfile);
   1.141 -   TextIO.flushOut toParent;
   1.142 -   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   1.143 +fun lemma_list atp proofextract thm_names probfile toParent ppid =
   1.144 +  signal_success probfile toParent ppid (metis_line atp proofextract thm_names);
   1.145  
   1.146 -val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
   1.147 -
   1.148 -val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   1.149 -
   1.150 -val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   1.151 -
   1.152 +fun tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno =
   1.153 +  let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   1.154 +      val line1 = metis_line atp proofextract thm_names
   1.155 +  in
   1.156 +    signal_success probfile toParent ppid
   1.157 +      (line1 ^ "\n" ^ decode_tstp_file cnfs ctxt th sgno thm_names)
   1.158 +  end;
   1.159  
   1.160  (**** Extracting proofs from an ATP's output ****)
   1.161  
   1.162 @@ -592,16 +588,22 @@
   1.163        | SOME thisLine =>
   1.164  	if String.isPrefix endS thisLine
   1.165  	then let val proofextract = currentString ^ cut_before endS thisLine
   1.166 -	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   1.167 -			  	  else if endS = end_SPASS then spass_lemma_list
   1.168 -			  	  else e_lemma_list
   1.169 +	         val atp = if endS = end_V8 then Vampire
   1.170 +			   else if endS = end_SPASS then SPASS
   1.171 +			   else E
   1.172  	     in
   1.173  	       trace ("\nExtracted proof:\n" ^ proofextract);
   1.174 -	       if !full andalso String.isPrefix "cnf(" proofextract
   1.175 -	       then tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names
   1.176 -	       else lemma_list proofextract probfile toParent ppid thm_names;
   1.177 +	       if String.isPrefix "cnf(" proofextract
   1.178 +	       then tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno
   1.179 +	       else lemma_list atp proofextract thm_names probfile toParent ppid;
   1.180  	       true
   1.181  	     end
   1.182 +	     handle e => (*FIXME: exn handler is too general!*)
   1.183 +	      (trace ("\nstartTransfer: In exception handler: " ^ Toplevel.exn_message e);
   1.184 +	       TextIO.output (toParent, "Translation failed\n" ^ probfile);
   1.185 +	       TextIO.flushOut toParent;
   1.186 +	       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.187 +	       true)
   1.188  	else transferInput (currentString^thisLine))
   1.189   in
   1.190       transferInput ""