src/HOL/Tools/res_reconstruct.ML
author paulson
Thu Jan 04 17:55:12 2007 +0100 (2007-01-04)
changeset 21999 0cf192e489e2
parent 21979 80e10f181c46
child 22012 adf68479ae1b
permissions -rwxr-xr-x
improvements to proof reconstruction. Some files loaded in a different order
     1 (*  ID:         $Id$
     2     Author:     L C Paulson and Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 (***************************************************************************)
     7 (*  Code to deal with the transfer of proofs from a prover process         *)
     8 (***************************************************************************)
     9 signature RES_RECONSTRUCT =
    10   sig
    11     val checkEProofFound: 
    12           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    13           string * thm * int * string Vector.vector -> bool
    14     val checkVampProofFound: 
    15           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    16           string * thm * int * string Vector.vector -> bool
    17     val checkSpassProofFound:  
    18           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    19           string * thm * int * string Vector.vector -> bool
    20     val signal_parent:  
    21           TextIO.outstream * Posix.Process.pid * string * string -> unit
    22     val nospaces: string -> string
    23 
    24   end;
    25 
    26 structure ResReconstruct =
    27 struct
    28 
    29 val trace_path = Path.basic "atp_trace";
    30 
    31 fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    32               else ();
    33 
    34 (*Full proof reconstruction wanted*)
    35 val full = ref true;
    36 
    37 (**** PARSING OF TSTP FORMAT ****)
    38 
    39 (*Syntax trees, either termlist or formulae*)
    40 datatype stree = Int of int | Br of string * stree list;
    41 
    42 fun atom x = Br(x,[]);
    43 
    44 fun scons (x,y) = Br("cons", [x,y]);
    45 val listof = foldl scons (atom "nil");
    46 
    47 (*Strings enclosed in single quotes, e.g. filenames*)
    48 val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode;
    49 
    50 (*Intended for $true and $false*)
    51 fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE);
    52 val truefalse = $$"$" |-- Symbol.scan_id >> (atom o tf);
    53 
    54 (*Integer constants, typically proof line numbers*)
    55 fun is_digit s = Char.isDigit (String.sub(s,0));
    56 val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
    57 
    58 (*Generalized FO terms, which include filenames, numbers, etc.*)
    59 fun termlist x = (term -- Scan.repeat ($$"," |-- term) >> op::) x
    60 and term x = (quoted >> atom || integer>>Int || truefalse ||
    61               Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
    62               $$"(" |-- term --| $$")" ||
    63               $$"[" |-- termlist --| $$"]" >> listof) x;
    64 
    65 fun negate t = Br("c_Not", [t]);
    66 fun equate (t1,t2) = Br("c_equal", [t1,t2]);
    67 
    68 (*Apply equal or not-equal to a term*)
    69 fun syn_equal (t, NONE) = t
    70   | syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2)
    71   | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2));
    72 
    73 (*Literals can involve negation, = and !=.*)
    74 val literal = $$"~" |-- term >> negate || 
    75               (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal) ;
    76 
    77 val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ;
    78 
    79 (*Clause: a list of literals separated by the disjunction sign*)
    80 val clause = $$"(" |-- literals --| $$")";
    81 
    82 val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
    83 
    84 (*<cnf_annotated> ::=Ęcnf(<name>,<formula_role>,<cnf_formula><annotations>).
    85   The <name> could be an identifier, but we assume integers.*)
    86 val tstp_line = (Scan.this_string "cnf" -- $$"(") |-- 
    87                 integer --| $$"," -- Symbol.scan_id --| $$"," -- 
    88                 clause -- Scan.option annotations --| $$ ")";
    89 
    90 
    91 (**** DUPLICATE of Susanto's code to remove ASCII armouring from names in proof files ****)
    92 
    93 (*original file: Isabelle_ext.sml*)
    94 
    95 val A_min_spc = Char.ord #"A" - Char.ord #" ";
    96 
    97 fun cList2int chs = getOpt (Int.fromString (String.implode (rev chs)), 0);
    98 
    99 (*why such a tiny range?*)
   100 fun check_valid_int x =
   101   let val val_x = cList2int x
   102   in (length x = 3) andalso (val_x >= 123) andalso (val_x <= 126)
   103   end;
   104 
   105 fun normalise_s s [] st_ sti =
   106       String.implode(rev(
   107         if st_
   108         then if null sti
   109              then (#"_" :: s)
   110              else if check_valid_int sti
   111                   then (Char.chr (cList2int sti) :: s)
   112                   else (sti @ (#"_" :: s))
   113         else s))
   114   | normalise_s s (#"_"::cs) st_ sti =
   115       if st_
   116       then let val s' = if null sti
   117                         then (#"_"::s)
   118                         else if check_valid_int sti
   119                              then (Char.chr (cList2int sti) :: s)
   120                              else (sti @ (#"_" :: s))
   121            in normalise_s s' cs false [] 
   122            end
   123       else normalise_s s cs true []
   124   | normalise_s s (c::cs) true sti =
   125       if (Char.isDigit c)
   126       then normalise_s s cs true (c::sti)
   127       else let val s' = if null sti
   128                         then if ((c >= #"A") andalso (c<= #"P"))
   129                              then ((Char.chr(Char.ord c - A_min_spc))::s)
   130                              else (c :: (#"_" :: s))
   131                         else if check_valid_int sti
   132                              then (Char.chr (cList2int sti) :: s)
   133                              else (sti @ (#"_" :: s))
   134            in normalise_s s' cs false []
   135            end
   136   | normalise_s s (c::cs) _ _ = normalise_s (c::s) cs false [];
   137 
   138 (*This version does not look for standard prefixes first.*)
   139 fun normalise_string s = normalise_s [] (String.explode s) false [];
   140 
   141 
   142 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   143 
   144 exception STREE of stree;
   145 
   146 (*If string s has the prefix s1, return the result of deleting it.*)
   147 fun strip_prefix s1 s = 
   148   if String.isPrefix s1 s then SOME (normalise_string (String.extract (s, size s1, NONE)))
   149   else NONE;
   150 
   151 (*Invert the table of translations between Isabelle and ATPs*)
   152 val type_const_trans_table_inv =
   153       Symtab.make (map swap (Symtab.dest ResClause.type_const_trans_table));
   154 
   155 fun invert_type_const c =
   156     case Symtab.lookup type_const_trans_table_inv c of
   157         SOME c' => c'
   158       | NONE => c;
   159 
   160 fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS);
   161 fun make_var (b,T) = Var((b,0),T);
   162 
   163 (*Type variables are given the basic sort, HOL.type. Some will later be constrained
   164   by information from type literals, or by type inference.*)
   165 fun type_of_stree t =
   166   case t of
   167       Int _ => raise STREE t
   168     | Br (a,ts) => 
   169         let val Ts = map type_of_stree ts
   170         in 
   171           case strip_prefix ResClause.tconst_prefix a of
   172               SOME b => Type(invert_type_const b, Ts)
   173             | NONE => 
   174                 if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   175                 else 
   176                 case strip_prefix ResClause.tfree_prefix a of
   177                     SOME b => TFree("'" ^ b, HOLogic.typeS)
   178                   | NONE => 
   179                 case strip_prefix ResClause.tvar_prefix a of
   180                     SOME b => make_tvar b
   181                   | NONE => make_tvar a   (*Variable from the ATP, say X1*)
   182         end;
   183 
   184 (*Invert the table of translations between Isabelle and ATPs*)
   185 val const_trans_table_inv =
   186       Symtab.make (map swap (Symtab.dest ResClause.const_trans_table));
   187 
   188 fun invert_const c =
   189     case Symtab.lookup const_trans_table_inv c of
   190         SOME c' => c'
   191       | NONE => c;
   192 
   193 (*The number of type arguments of a constant, zero if it's monomorphic*)
   194 fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s));
   195 
   196 (*Generates a constant, given its type arguments*)
   197 fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
   198 
   199 (*First-order translation. No types are known for variables. HOLogic.typeT should allow
   200   them to be inferred.*)
   201 fun term_of_stree thy t =
   202   case t of
   203       Int _ => raise STREE t
   204     | Br (a,ts) => 
   205         case strip_prefix ResClause.const_prefix a of
   206             SOME "equal" => 
   207               if length ts = 2 then
   208                 list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree thy) ts)
   209               else raise STREE t  (*equality needs two arguments*)
   210           | SOME b => 
   211               let val c = invert_const b
   212                   val nterms = length ts - num_typargs thy c
   213                   val us = List.map (term_of_stree thy) (List.take(ts,nterms))
   214                   val Ts = List.map type_of_stree (List.drop(ts,nterms))
   215               in  list_comb(const_of thy (c, Ts), us)  end
   216           | NONE => (*a variable, not a constant*)
   217               let val T = HOLogic.typeT
   218                   val opr = (*a Free variable is typically a Skolem function*)
   219                     case strip_prefix ResClause.fixed_var_prefix a of
   220                         SOME b => Free(b,T)
   221                       | NONE => 
   222                     case strip_prefix ResClause.schematic_var_prefix a of
   223                         SOME b => make_var (b,T)
   224                       | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
   225               in  list_comb (opr, List.map (term_of_stree thy) ts)  end;
   226 
   227 (*Type class literal applied to a type. Returns triple of polarity, class, type.*)                  
   228 fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t
   229   | constraint_of_stree pol t = case t of
   230         Int _ => raise STREE t
   231       | Br (a,ts) => 
   232             (case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
   233                  (SOME b, [T]) => (pol, b, T)
   234                | _ => raise STREE t);
   235 
   236 (** Accumulate type constraints in a clause: negative type literals **)
   237 
   238 fun addix (key,z)  = Vartab.map_default (key,[]) (cons z);
   239 
   240 fun add_constraint ((false, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
   241   | add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt
   242   | add_constraint (_, vt) = vt;
   243 
   244 (*False literals (which E includes in its proofs) are deleted*)
   245 val nofalses = filter (not o equal HOLogic.false_const);
   246 
   247 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   248 fun lits_of_strees thy (vt, lits) [] = (vt, rev (nofalses lits))
   249   | lits_of_strees thy (vt, lits) (t::ts) = 
   250       lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits) ts
   251       handle STREE _ => 
   252       lits_of_strees thy (vt, term_of_stree thy t :: lits) ts;
   253 
   254 (*Update TVars/TFrees with detected sort constraints.*)
   255 fun fix_sorts vt =
   256   let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
   257         | tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s))
   258         | tysubst (TFree (x, s)) = TFree (x, getOpt (Vartab.lookup vt (x,~1), s))
   259       fun tmsubst (Const (a, T)) = Const (a, tysubst T)
   260         | tmsubst (Free (a, T)) = Free (a, tysubst T)
   261         | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
   262         | tmsubst (t as Bound _) = t
   263         | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
   264         | tmsubst (t $ u) = tmsubst t $ tmsubst u;
   265   in fn t => if Vartab.is_empty vt then t else tmsubst t end;
   266 
   267 (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
   268   vt0 holds the initial sort constraints, from the conjecture clauses.*)
   269 fun clause_of_strees_aux thy vt0 ts = 
   270   case lits_of_strees thy (vt0,[]) ts of
   271       (_, []) => HOLogic.false_const
   272     | (vt, lits) => 
   273         let val dt = fix_sorts vt (foldr1 HOLogic.mk_disj lits)
   274             val infer = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
   275         in 
   276            #1(infer (K NONE) (K NONE) (Name.make_context []) true ([dt], HOLogic.boolT))
   277         end; 
   278 
   279 (*Quantification over a list of Vars. FUXNE: for term.ML??*)
   280 fun list_all_var ([], t: term) = t
   281   | list_all_var ((v as Var(ix,T)) :: vars, t) =
   282       (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
   283 
   284 fun gen_all_vars t = list_all_var (term_vars t, t);
   285 
   286 fun clause_of_strees thy vt0 ts =
   287   gen_all_vars (HOLogic.mk_Trueprop (clause_of_strees_aux thy vt0 ts));
   288 
   289 fun ints_of_stree_aux (Int n, ns) = n::ns
   290   | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
   291 
   292 fun ints_of_stree t = ints_of_stree_aux (t, []);
   293 
   294 fun decode_tstp thy vt0 (name, role, ts, annots) =
   295   let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
   296   in  (name, role, clause_of_strees thy vt0 ts, deps)  end;
   297 
   298 fun dest_tstp ((((name, role), ts), annots), chs) =
   299   case chs of
   300           "."::_ => (name, role, ts, annots)
   301         | _ => error ("TSTP line not terminated by \".\": " ^ implode chs);
   302 
   303 
   304 (** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
   305 
   306 fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
   307   | add_tfree_constraint (_, vt) = vt;
   308 
   309 fun tfree_constraints_of_clauses vt [] = vt
   310   | tfree_constraints_of_clauses vt ([lit]::tss) = 
   311       (tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
   312        handle STREE _ => (*not a positive type constraint: ignore*)
   313        tfree_constraints_of_clauses vt tss)
   314   | tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss;
   315 
   316 
   317 (**** Translation of TSTP files to Isar Proofs ****)
   318 
   319 fun decode_tstp_list thy tuples =
   320   let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
   321   in  map (decode_tstp thy vt0) tuples  end;
   322 
   323 (*FIXME: simmilar function in res_atp. Move to HOLogic?*)
   324 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
   325   | dest_disj_aux t disjs = t::disjs;
   326 
   327 fun dest_disj t = dest_disj_aux t [];
   328 
   329 val sort_lits = sort Term.fast_term_ord o dest_disj o HOLogic.dest_Trueprop o strip_all_body;
   330 
   331 fun permuted_clause t =
   332   let val lits = sort_lits t
   333       fun perm [] = NONE
   334         | perm (ctm::ctms) = 
   335             if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm
   336             else perm ctms
   337   in perm end;
   338 
   339 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   340   ATP may have their literals reordered.*)
   341 fun isar_lines ctxt ctms =
   342   let val string_of = ProofContext.string_of_term ctxt
   343       fun doline hs (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
   344            (case permuted_clause t ctms of
   345                 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
   346               | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
   347         | doline hs (lname, t, deps) =
   348             hs ^ lname ^ ": \"" ^ string_of t ^ 
   349             "\"\n  by (meson " ^ space_implode " " deps ^ ")\n"
   350       fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
   351         | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
   352   in setmp show_sorts true dolines end;
   353 
   354 fun notequal t (_,t',_) = not (t aconv t');
   355 
   356 fun eq_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   357 
   358 fun replace_dep (old, new) dep = if dep=old then new else [dep];
   359 
   360 fun replace_deps (old, new) (lno, t, deps) = 
   361       (lno, t, List.concat (map (replace_dep (old, new)) deps));
   362 
   363 (*Discard axioms and also False conjecture clauses (which can only contain type information).
   364   Consolidate adjacent lines that prove the same clause, since they differ only in type
   365   information.*)
   366 fun add_prfline ((lno, "axiom", t, []), lines) =  (*axioms are not proof lines*)
   367       if eq_false t then lines   (*must be clsrel/clsarity: type information*)
   368       else (case take_prefix (notequal t) lines of
   369                (_,[]) => lines   (*no repetition of proof line*)
   370              | (pre, (lno',t',deps')::post) => 
   371                  pre @ map (replace_deps (lno', [lno])) post)
   372   | add_prfline ((lno, role, t, []), lines) =  (*no deps: conjecture clause*)
   373       if eq_false t then lines   (*must be tfree_tcs: type information*)
   374       else (lno, t, []) :: lines
   375   | add_prfline ((lno, role, t, deps), lines) =
   376       (case term_tvars t of (*Delete line if it has TVars: they are forbidden in goals*)
   377           _::_ => map (replace_deps (lno, deps)) lines
   378         | [] => 
   379             case take_prefix (notequal t) lines of
   380                (_,[]) => (lno, t, deps) :: lines   (*no repetition of proof line*)
   381              | (pre, (lno',t',deps')::post) => 
   382                  (lno, t', deps) ::  (*replace later line by earlier one*)
   383                  (pre @ map (replace_deps (lno', [lno])) post));
   384 
   385 (*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
   386 fun stringify_deps thm_names deps_map [] = []
   387   | stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
   388       if lno <= Vector.length thm_names  (*axiom*)
   389       then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines 
   390       else let val lname = Int.toString (length deps_map)
   391                fun fix lno = if lno <= Vector.length thm_names  
   392                              then SOME(Vector.sub(thm_names,lno-1))
   393                              else AList.lookup op= deps_map lno;
   394            in  (lname, t, List.mapPartial fix deps) ::
   395                stringify_deps thm_names ((lno,lname)::deps_map) lines
   396            end;
   397 
   398 val proofstart = "\nproof (neg_clausify)\n";
   399 
   400 fun isar_header [] = proofstart
   401   | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
   402 
   403 fun decode_tstp_file cnfs th sgno thm_names =
   404   let val tuples = map (dest_tstp o tstp_line o explode) cnfs
   405       and ctxt = ProofContext.init (Thm.theory_of_thm th)
   406        (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
   407          then to setupWatcher and checkChildren...but is it really needed?*)
   408       val decoded_tuples = decode_tstp_list (ProofContext.theory_of ctxt) tuples
   409       val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
   410       val ccls = map forall_intr_vars ccls
   411       val lines = foldr add_prfline [] decoded_tuples
   412       and clines = map (fn th => string_of_thm th ^ "\n") ccls
   413   in  
   414       isar_header (map #1 fixes) ^ 
   415       String.concat (clines @ isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
   416   end;
   417 
   418 (*Could use split_lines, but it can return blank lines...*)
   419 val lines = String.tokens (equal #"\n");
   420 
   421 val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
   422 
   423 (*The output to the watcher must be a SINGLE line...clearly \t must not be used.*)
   424 val encode_newlines = String.translate (fn c => if c = #"\n" then "\t" else str c);
   425 val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c);
   426 
   427 fun signal_success probfile toParent ppid msg = 
   428   (trace ("\nReporting Success for" ^ probfile ^ "\n" ^ msg);
   429    TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n");
   430    TextIO.output (toParent, probfile ^ "\n");
   431    TextIO.flushOut toParent;
   432    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   433 
   434 fun tstp_extract proofextract probfile toParent ppid th sgno thm_names = 
   435   let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   436   in  
   437     signal_success probfile toParent ppid 
   438       (decode_tstp_file cnfs th sgno thm_names)
   439   end;
   440 
   441 
   442 (**** retrieve the axioms that were used in the proof ****)
   443 
   444 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
   445 fun get_axiom_names (thm_names: string vector) step_nums = 
   446     let fun is_axiom n = n <= Vector.length thm_names 
   447         fun index i = Vector.sub(thm_names, i-1)
   448         val axnums = List.filter is_axiom step_nums
   449         val axnames = sort_distinct string_ord (map index axnums)
   450     in
   451 	if length axnums = length step_nums then "UNSOUND!!" :: axnames
   452 	else axnames
   453     end
   454 
   455  (*String contains multiple lines. We want those of the form 
   456      "253[0:Inp] et cetera..."
   457   A list consisting of the first number in each line is returned. *)
   458 fun get_spass_linenums proofstr = 
   459   let val toks = String.tokens (not o Char.isAlphaNum)
   460       fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
   461         | inputno _ = NONE
   462       val lines = String.tokens (fn c => c = #"\n") proofstr
   463   in  List.mapPartial (inputno o toks) lines  end
   464 
   465 fun get_axiom_names_spass proofstr thm_names =
   466    get_axiom_names thm_names (get_spass_linenums proofstr);
   467     
   468 fun not_comma c = c <>  #",";
   469 
   470 (*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
   471 fun parse_tstp_line s =
   472   let val ss = Substring.full (unprefix "cnf(" (nospaces s))
   473       val (intf,rest) = Substring.splitl not_comma ss
   474       val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
   475       (*We only allow negated_conjecture because the line number will be removed in
   476         get_axiom_names above, while suppressing the UNSOUND warning*)
   477       val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
   478                  then Substring.string intf 
   479                  else "error" 
   480   in  Int.fromString ints  end
   481   handle Fail _ => NONE; 
   482 
   483 fun get_axiom_names_tstp proofstr thm_names =
   484    get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
   485     
   486  (*String contains multiple lines. We want those of the form 
   487      "*********** [448, input] ***********".
   488   A list consisting of the first number in each line is returned. *)
   489 fun get_vamp_linenums proofstr = 
   490   let val toks = String.tokens (not o Char.isAlphaNum)
   491       fun inputno [ntok,"input"] = Int.fromString ntok
   492         | inputno _ = NONE
   493       val lines = String.tokens (fn c => c = #"\n") proofstr
   494   in  List.mapPartial (inputno o toks) lines  end
   495 
   496 fun get_axiom_names_vamp proofstr thm_names =
   497    get_axiom_names thm_names (get_vamp_linenums proofstr);
   498     
   499 fun rules_to_string [] = "NONE"
   500   | rules_to_string xs = space_implode "  " xs
   501 
   502 
   503 (*The signal handler in watcher.ML must be able to read the output of this.*)
   504 fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names = 
   505  (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   506          " num of clauses is " ^ string_of_int (Vector.length thm_names));
   507   signal_success probfile toParent ppid 
   508     ("Lemmas used in automatic proof: " ^ rules_to_string (getax proofstr thm_names)))
   509  handle e => (*FIXME: exn handler is too general!*)
   510   (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);
   511    TextIO.output (toParent, "Translation failed for the proof: " ^ 
   512                   String.toString proofstr ^ "\n");
   513    TextIO.output (toParent, probfile);
   514    TextIO.flushOut toParent;
   515    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   516 
   517 val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
   518 
   519 val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   520 
   521 val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   522 
   523 
   524 (**** Extracting proofs from an ATP's output ****)
   525 
   526 (*Return everything in s that comes before the string t*)
   527 fun cut_before t s = 
   528   let val (s1,s2) = Substring.position t (Substring.full s)
   529   in  if Substring.size s2 = 0 then error "cut_before: string not found" 
   530       else Substring.string s2
   531   end;
   532 
   533 val start_E = "# Proof object starts here."
   534 val end_E   = "# Proof object ends here."
   535 val start_V6 = "%================== Proof: ======================"
   536 val end_V6   = "%==============  End of proof. =================="
   537 val start_V8 = "=========== Refutation =========="
   538 val end_V8 = "======= End of refutation ======="
   539 val end_SPASS = "Formulae used in the proof"
   540 
   541 (*********************************************************************************)
   542 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
   543 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   544 (*********************************************************************************)
   545 
   546 (*Returns "true" if it successfully returns a lemma list, otherwise "false", but this
   547   return value is currently never used!*)
   548 fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   549  let fun transferInput currentString =
   550       let val thisLine = TextIO.inputLine fromChild
   551       in
   552 	if thisLine = "" (*end of file?*)
   553 	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   554 	             "\naccumulated text: " ^ currentString);
   555 	      false)                    
   556 	else if String.isPrefix endS thisLine
   557 	then let val proofextract = currentString ^ cut_before endS thisLine
   558 	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   559 			  	  else if endS = end_SPASS then spass_lemma_list
   560 			  	  else e_lemma_list
   561 	     in
   562 	       trace ("\nExtracted proof:\n" ^ proofextract); 
   563 	       if !full andalso String.isPrefix "cnf(" proofextract
   564 	       then tstp_extract proofextract probfile toParent ppid th sgno thm_names
   565 	       else lemma_list proofextract probfile toParent ppid thm_names;
   566 	       true
   567 	     end
   568 	else transferInput (currentString^thisLine)
   569       end
   570  in
   571      transferInput ""
   572  end 
   573 
   574 
   575 (*The signal handler in watcher.ML must be able to read the output of this.*)
   576 fun signal_parent (toParent, ppid, msg, probfile) =
   577  (TextIO.output (toParent, msg);
   578   TextIO.output (toParent, probfile ^ "\n");
   579   TextIO.flushOut toParent;
   580   trace ("\nSignalled parent: " ^ msg ^ probfile);
   581   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   582   (*Give the parent time to respond before possibly sending another signal*)
   583   OS.Process.sleep (Time.fromMilliseconds 600));
   584 
   585 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   586 fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   587  let val thisLine = TextIO.inputLine fromChild
   588  in   
   589      trace thisLine;
   590      if thisLine = "" 
   591      then (trace "\nNo proof output seen"; false)
   592      else if String.isPrefix start_V8 thisLine
   593      then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   594      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   595              (String.isPrefix "Refutation not found" thisLine)
   596      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   597 	   true)
   598      else checkVampProofFound  (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   599   end
   600 
   601 (*Called from watcher. Returns true if the E process has returned a verdict.*)
   602 fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   603  let val thisLine = TextIO.inputLine fromChild  
   604  in   
   605      trace thisLine;
   606      if thisLine = "" then (trace "\nNo proof output seen"; false)
   607      else if String.isPrefix start_E thisLine
   608      then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   609      else if String.isPrefix "# Problem is satisfiable" thisLine
   610      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   611 	   true)
   612      else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   613      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   614 	   true)
   615      else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   616  end;
   617 
   618 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   619 fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   620  let val thisLine = TextIO.inputLine fromChild  
   621  in    
   622      trace thisLine;
   623      if thisLine = "" then (trace "\nNo proof output seen"; false)
   624      else if String.isPrefix "Here is a proof" thisLine
   625      then      
   626         startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   627      else if thisLine = "SPASS beiseite: Completion found.\n"
   628      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   629 	   true)
   630      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   631              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   632      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   633 	   true)
   634     else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   635  end
   636 
   637 end;