Returning both a "one-line" proof and a structured proof
authorpaulson
Fri Aug 24 14:16:44 2007 +0200 (2007-08-24)
changeset 24425ca97c6f3d9cd
parent 24424 90500d3b5b5d
child 24426 d89e409cfe4e
Returning both a "one-line" proof and a structured proof
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/watcher.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Aug 24 14:15:58 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 24 14:16:44 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature RES_ATP =
     1.6  sig
     1.7 -  val prover: string ref
     1.8 +  val prover: ResReconstruct.atp ref
     1.9    val destdir: string ref
    1.10    val helper_path: string -> string -> string
    1.11    val problem_name: string ref
    1.12 @@ -45,6 +45,8 @@
    1.13  structure ResAtp: RES_ATP =
    1.14  struct
    1.15  
    1.16 +structure Recon = ResReconstruct;
    1.17 +
    1.18  fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    1.19  
    1.20  (********************************************************************)
    1.21 @@ -55,7 +57,7 @@
    1.22  (*** background linkup ***)
    1.23  val run_blacklist_filter = ref true;
    1.24  val time_limit = ref 60;
    1.25 -val prover = ref "";
    1.26 +val prover = ref Recon.E;
    1.27  
    1.28  (*** relevance filter parameters ***)
    1.29  val run_relevance_filter = ref true;
    1.30 @@ -70,15 +72,15 @@
    1.31        "e" =>
    1.32            (max_new := 100;
    1.33             theory_const := false;
    1.34 -           prover := "E")
    1.35 +           prover := Recon.E)
    1.36      | "spass" =>
    1.37            (max_new := 40;
    1.38             theory_const := true;
    1.39 -           prover := "spass")
    1.40 +           prover := Recon.SPASS)
    1.41      | "vampire" =>
    1.42            (max_new := 60;
    1.43             theory_const := false;
    1.44 -           prover := "vampire")
    1.45 +           prover := Recon.Vampire)
    1.46      | _ => error ("No such prover: " ^ atp);
    1.47  
    1.48  val _ = set_prover "E"; (* use E as the default prover *)
    1.49 @@ -822,30 +824,26 @@
    1.50            in
    1.51              Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
    1.52              (*options are separated by Watcher.setting_sep, currently #"%"*)
    1.53 -            if !prover = "spass"
    1.54 -            then
    1.55 -              let val spass = helper_path "SPASS_HOME" "SPASS"
    1.56 -                  val sopts =
    1.57 -   "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
    1.58 -              in
    1.59 -                  ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
    1.60 -              end
    1.61 -            else if !prover = "vampire"
    1.62 -            then
    1.63 -              let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.64 -                  val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
    1.65 -              in
    1.66 -                  ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
    1.67 -              end
    1.68 -             else if !prover = "E"
    1.69 -             then
    1.70 -               let val Eprover = helper_path "E_HOME" "eproof"
    1.71 -               in
    1.72 -                  ("E", Eprover,
    1.73 -                     "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
    1.74 -                   make_atp_list xs (n+1)
    1.75 -               end
    1.76 -             else error ("Invalid prover name: " ^ !prover)
    1.77 +            case !prover of
    1.78 +                Recon.SPASS =>
    1.79 +		  let val spass = helper_path "SPASS_HOME" "SPASS"
    1.80 +		      val sopts =
    1.81 +       "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
    1.82 +		  in
    1.83 +		      ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
    1.84 +		  end
    1.85 +              | Recon.Vampire =>
    1.86 +		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.87 +		      val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
    1.88 +		  in
    1.89 +		      ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
    1.90 +		  end
    1.91 +              | Recon.E =>
    1.92 +		  let val eproof = helper_path "E_HOME" "eproof"
    1.93 +                      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
    1.94 +		  in
    1.95 +		     ("E", eproof, eopts, probfile) :: make_atp_list xs (n+1)
    1.96 +		  end
    1.97            end
    1.98  
    1.99      val atp_list = make_atp_list sg_terms 1
   1.100 @@ -885,7 +883,7 @@
   1.101        val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   1.102        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   1.103                    axcls_list
   1.104 -      val writer = if !prover = "spass" then dfg_writer else tptp_writer
   1.105 +      val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer
   1.106        fun write_all [] [] _ = []
   1.107          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   1.108              let val fname = probfile k
     2.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri Aug 24 14:15:58 2007 +0200
     2.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Fri Aug 24 14:16:44 2007 +0200
     2.3 @@ -7,22 +7,30 @@
     2.4  (*  Code to deal with the transfer of proofs from a prover process         *)
     2.5  (***************************************************************************)
     2.6  signature RES_RECONSTRUCT =
     2.7 -  sig
     2.8 -    val checkEProofFound:
     2.9 -          TextIO.instream * TextIO.outstream * Posix.Process.pid *
    2.10 -          string * Proof.context * thm * int * string Vector.vector -> bool
    2.11 -    val checkVampProofFound:
    2.12 -          TextIO.instream * TextIO.outstream * Posix.Process.pid *
    2.13 -          string * Proof.context * thm * int * string Vector.vector -> bool
    2.14 -    val checkSpassProofFound:
    2.15 -          TextIO.instream * TextIO.outstream * Posix.Process.pid *
    2.16 -          string * Proof.context * thm * int * string Vector.vector -> bool
    2.17 -    val signal_parent:
    2.18 -          TextIO.outstream * Posix.Process.pid * string * string -> unit
    2.19 +sig
    2.20 +  datatype atp = E | SPASS | Vampire
    2.21 +  val modulus:     int ref
    2.22 +  val recon_sorts: bool ref
    2.23 +  val checkEProofFound:
    2.24 +	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    2.25 +	string * Proof.context * thm * int * string Vector.vector -> bool
    2.26 +  val checkVampProofFound:
    2.27 +	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    2.28 +	string * Proof.context * thm * int * string Vector.vector -> bool
    2.29 +  val checkSpassProofFound:
    2.30 +	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    2.31 +	string * Proof.context * thm * int * string Vector.vector -> bool
    2.32 +  val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit
    2.33 +  val txt_path: string -> Path.T
    2.34 +  val fix_sorts: sort Vartab.table -> term -> term
    2.35 +  val invert_const: string -> string
    2.36 +  val invert_type_const: string -> string
    2.37 +  val num_typargs: Context.theory -> string -> int
    2.38 +  val make_tvar: string -> typ
    2.39 +  val strip_prefix: string -> string -> string option
    2.40 +end;
    2.41  
    2.42 -  end;
    2.43 -
    2.44 -structure ResReconstruct =
    2.45 +structure ResReconstruct : RES_RECONSTRUCT =
    2.46  struct
    2.47  
    2.48  val trace_path = Path.basic "atp_trace";
    2.49 @@ -30,8 +38,7 @@
    2.50  fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    2.51                else ();
    2.52  
    2.53 -(*Full proof reconstruction wanted*)
    2.54 -val full = ref true;
    2.55 +datatype atp = E | SPASS | Vampire;
    2.56  
    2.57  val recon_sorts = ref true;
    2.58  
    2.59 @@ -467,13 +474,6 @@
    2.60      OS.Process.sleep (Time.fromMilliseconds 600)
    2.61    end;
    2.62  
    2.63 -fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
    2.64 -  let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
    2.65 -  in
    2.66 -    signal_success probfile toParent ppid
    2.67 -      (decode_tstp_file cnfs ctxt th sgno thm_names)
    2.68 -  end;
    2.69 -
    2.70  
    2.71  (**** retrieve the axioms that were used in the proof ****)
    2.72  
    2.73 @@ -491,15 +491,15 @@
    2.74   (*String contains multiple lines. We want those of the form
    2.75       "253[0:Inp] et cetera..."
    2.76    A list consisting of the first number in each line is returned. *)
    2.77 -fun get_spass_linenums proofstr =
    2.78 +fun get_spass_linenums proofextract =
    2.79    let val toks = String.tokens (not o Char.isAlphaNum)
    2.80        fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    2.81          | inputno _ = NONE
    2.82 -      val lines = String.tokens (fn c => c = #"\n") proofstr
    2.83 +      val lines = String.tokens (fn c => c = #"\n") proofextract
    2.84    in  List.mapPartial (inputno o toks) lines  end
    2.85  
    2.86 -fun get_axiom_names_spass proofstr thm_names =
    2.87 -   get_axiom_names thm_names (get_spass_linenums proofstr);
    2.88 +fun get_axiom_names_spass proofextract thm_names =
    2.89 +   get_axiom_names thm_names (get_spass_linenums proofextract);
    2.90  
    2.91  fun not_comma c = c <>  #",";
    2.92  
    2.93 @@ -516,47 +516,43 @@
    2.94    in  Int.fromString ints  end
    2.95    handle Fail _ => NONE;
    2.96  
    2.97 -fun get_axiom_names_tstp proofstr thm_names =
    2.98 -   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
    2.99 +fun get_axiom_names_tstp proofextract thm_names =
   2.100 +   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
   2.101  
   2.102   (*String contains multiple lines. We want those of the form
   2.103       "*********** [448, input] ***********".
   2.104    A list consisting of the first number in each line is returned. *)
   2.105 -fun get_vamp_linenums proofstr =
   2.106 +fun get_vamp_linenums proofextract =
   2.107    let val toks = String.tokens (not o Char.isAlphaNum)
   2.108        fun inputno [ntok,"input"] = Int.fromString ntok
   2.109          | inputno _ = NONE
   2.110 -      val lines = String.tokens (fn c => c = #"\n") proofstr
   2.111 +      val lines = String.tokens (fn c => c = #"\n") proofextract
   2.112    in  List.mapPartial (inputno o toks) lines  end
   2.113  
   2.114 -fun get_axiom_names_vamp proofstr thm_names =
   2.115 -   get_axiom_names thm_names (get_vamp_linenums proofstr);
   2.116 +fun get_axiom_names_vamp proofextract thm_names =
   2.117 +   get_axiom_names thm_names (get_vamp_linenums proofextract);
   2.118 +
   2.119 +fun get_axiom_names E       = get_axiom_names_tstp
   2.120 +  | get_axiom_names SPASS   = get_axiom_names_spass
   2.121 +  | get_axiom_names Vampire = get_axiom_names_vamp;
   2.122  
   2.123  fun rules_to_metis [] = "metis"
   2.124    | rules_to_metis xs = "(metis " ^ space_implode " " xs ^ ")"
   2.125  
   2.126 +fun metis_line atp proofextract thm_names =
   2.127 +  "apply " ^ rules_to_metis (get_axiom_names atp proofextract thm_names);
   2.128  
   2.129  (*The signal handler in watcher.ML must be able to read the output of this.*)
   2.130 -fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names =
   2.131 - (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   2.132 -         " num of clauses is " ^ string_of_int (Vector.length thm_names));
   2.133 -  signal_success probfile toParent ppid
   2.134 -    ("apply " ^ rules_to_metis (getax proofstr thm_names))
   2.135 - )
   2.136 - handle e => (*FIXME: exn handler is too general!*)
   2.137 -  (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);
   2.138 -   TextIO.output (toParent, "Translation failed for the proof: " ^
   2.139 -                  String.toString proofstr ^ "\n");
   2.140 -   TextIO.output (toParent, probfile);
   2.141 -   TextIO.flushOut toParent;
   2.142 -   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   2.143 +fun lemma_list atp proofextract thm_names probfile toParent ppid =
   2.144 +  signal_success probfile toParent ppid (metis_line atp proofextract thm_names);
   2.145  
   2.146 -val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
   2.147 -
   2.148 -val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   2.149 -
   2.150 -val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   2.151 -
   2.152 +fun tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno =
   2.153 +  let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   2.154 +      val line1 = metis_line atp proofextract thm_names
   2.155 +  in
   2.156 +    signal_success probfile toParent ppid
   2.157 +      (line1 ^ "\n" ^ decode_tstp_file cnfs ctxt th sgno thm_names)
   2.158 +  end;
   2.159  
   2.160  (**** Extracting proofs from an ATP's output ****)
   2.161  
   2.162 @@ -592,16 +588,22 @@
   2.163        | SOME thisLine =>
   2.164  	if String.isPrefix endS thisLine
   2.165  	then let val proofextract = currentString ^ cut_before endS thisLine
   2.166 -	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   2.167 -			  	  else if endS = end_SPASS then spass_lemma_list
   2.168 -			  	  else e_lemma_list
   2.169 +	         val atp = if endS = end_V8 then Vampire
   2.170 +			   else if endS = end_SPASS then SPASS
   2.171 +			   else E
   2.172  	     in
   2.173  	       trace ("\nExtracted proof:\n" ^ proofextract);
   2.174 -	       if !full andalso String.isPrefix "cnf(" proofextract
   2.175 -	       then tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names
   2.176 -	       else lemma_list proofextract probfile toParent ppid thm_names;
   2.177 +	       if String.isPrefix "cnf(" proofextract
   2.178 +	       then tstp_extract atp proofextract thm_names probfile toParent ppid ctxt th sgno
   2.179 +	       else lemma_list atp proofextract thm_names probfile toParent ppid;
   2.180  	       true
   2.181  	     end
   2.182 +	     handle e => (*FIXME: exn handler is too general!*)
   2.183 +	      (trace ("\nstartTransfer: In exception handler: " ^ Toplevel.exn_message e);
   2.184 +	       TextIO.output (toParent, "Translation failed\n" ^ probfile);
   2.185 +	       TextIO.flushOut toParent;
   2.186 +	       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.187 +	       true)
   2.188  	else transferInput (currentString^thisLine))
   2.189   in
   2.190       transferInput ""
     3.1 --- a/src/HOL/Tools/watcher.ML	Fri Aug 24 14:15:58 2007 +0200
     3.2 +++ b/src/HOL/Tools/watcher.ML	Fri Aug 24 14:16:44 2007 +0200
     3.3 @@ -360,12 +360,14 @@
     3.4  
     3.5  (*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
     3.6  fun report_success i s sgtx = 
     3.7 -  let val lines = String.tokens (fn c => c = #"\n") s
     3.8 -  in  if length lines > 1 then report i (s ^ sgtx)  (*multiple commands: do the old way*)
     3.9 -      else priority (cat_lines ["Subgoal " ^ string_of_int i ^ ":", sgtx,
    3.10 -                                "  Try this command:", Markup.enclose Markup.sendback s])
    3.11 -  end;
    3.12 -
    3.13 +  let val sgline = "Subgoal " ^ string_of_int i ^ ":"
    3.14 +      val outlines = 
    3.15 +	case split_lines s of
    3.16 +	    [] => ["Received bad string: " ^ s]
    3.17 +	  | line::lines => ["  Try this command:", (*Markup.enclose Markup.sendback*) line, ""]
    3.18 +	                   @ lines
    3.19 +  in priority (cat_lines (sgline::sgtx::outlines)) end;
    3.20 +  
    3.21  fun createWatcher (ctxt, th, thm_names_list) =
    3.22   let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
    3.23       fun decr_watched() =