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