Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
authorpaulson
Wed Jan 03 11:06:52 2007 +0100 (2007-01-03)
changeset 2197872c21698a055
parent 21977 7f7177a95189
child 21979 80e10f181c46
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
src/HOL/Tools/res_reconstruct.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Jan 03 11:06:52 2007 +0100
     1.3 @@ -0,0 +1,605 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Claire Quigley and L C Paulson
     1.6 +    Copyright   2004  University of Cambridge
     1.7 +*)
     1.8 +
     1.9 +(***************************************************************************)
    1.10 +(*  Code to deal with the transfer of proofs from a Vampire process          *)
    1.11 +(***************************************************************************)
    1.12 +signature RES_RECONSTRUCT =
    1.13 +  sig
    1.14 +    val checkEProofFound: 
    1.15 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.16 +          string * thm * int * string Vector.vector -> bool
    1.17 +    val checkVampProofFound: 
    1.18 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.19 +          string * thm * int * string Vector.vector -> bool
    1.20 +    val checkSpassProofFound:  
    1.21 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.22 +          string * thm * int * string Vector.vector -> bool
    1.23 +    val signal_parent:  
    1.24 +          TextIO.outstream * Posix.Process.pid * string * string -> unit
    1.25 +    val nospaces: string -> string
    1.26 +
    1.27 +  end;
    1.28 +
    1.29 +structure ResReconstruct =
    1.30 +struct
    1.31 +
    1.32 +val trace_path = Path.basic "atp_trace";
    1.33 +
    1.34 +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    1.35 +              else ();
    1.36 +
    1.37 +(*Full proof reconstruction wanted*)
    1.38 +val full = ref true;
    1.39 +
    1.40 +(**** PARSING OF TSTP FORMAT ****)
    1.41 +
    1.42 +(*Syntax trees, either termlist or formulae*)
    1.43 +datatype stree = Int of int | Br of string * stree list;
    1.44 +
    1.45 +fun atom x = Br(x,[]);
    1.46 +
    1.47 +fun scons (x,y) = Br("cons", [x,y]);
    1.48 +val listof = foldl scons (atom "nil");
    1.49 +
    1.50 +(*Strings enclosed in single quotes, e.g. filenames*)
    1.51 +val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode;
    1.52 +
    1.53 +(*Intended for $true and $false*)
    1.54 +fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE);
    1.55 +val truefalse = $$"$" |-- Symbol.scan_id >> (atom o tf);
    1.56 +
    1.57 +(*Integer constants, typically proof line numbers*)
    1.58 +fun is_digit s = Char.isDigit (String.sub(s,0));
    1.59 +val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
    1.60 +
    1.61 +(*Generalized FO terms, which include filenames, numbers, etc.*)
    1.62 +fun termlist x = (term -- Scan.repeat ($$"," |-- term) >> op::) x
    1.63 +and term x = (quoted >> atom || integer>>Int || truefalse ||
    1.64 +              Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
    1.65 +              $$"(" |-- term --| $$")" ||
    1.66 +              $$"[" |-- termlist --| $$"]" >> listof) x;
    1.67 +
    1.68 +fun negate t = Br("c_Not", [t]);
    1.69 +fun equate (t1,t2) = Br("c_equal", [t1,t2]);
    1.70 +
    1.71 +(*Apply equal or not-equal to a term*)
    1.72 +fun syn_equal (t, NONE) = t
    1.73 +  | syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2)
    1.74 +  | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2));
    1.75 +
    1.76 +(*Literals can involve negation, = and !=.*)
    1.77 +val literal = $$"~" |-- term >> negate || 
    1.78 +              (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal) ;
    1.79 +
    1.80 +val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ;
    1.81 +
    1.82 +(*Clause: a list of literals separated by the disjunction sign*)
    1.83 +val clause = $$"(" |-- literals --| $$")";
    1.84 +
    1.85 +val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
    1.86 +
    1.87 +(*<cnf_annotated> ::=Ęcnf(<name>,<formula_role>,<cnf_formula><annotations>).
    1.88 +  The <name> could be an identifier, but we assume integers.*)
    1.89 +val tstp_line = (Scan.this_string "cnf" -- $$"(") |-- 
    1.90 +                integer --| $$"," -- Symbol.scan_id --| $$"," -- 
    1.91 +                clause -- Scan.option annotations --| $$ ")";
    1.92 +
    1.93 +
    1.94 +(**** DUPLICATE of Susanto's code to remove ASCII armouring from names in proof files ****)
    1.95 +
    1.96 +(*original file: Isabelle_ext.sml*)
    1.97 +
    1.98 +val A_min_spc = Char.ord #"A" - Char.ord #" ";
    1.99 +
   1.100 +fun cList2int chs = getOpt (Int.fromString (String.implode (rev chs)), 0);
   1.101 +
   1.102 +(*why such a tiny range?*)
   1.103 +fun check_valid_int x =
   1.104 +  let val val_x = cList2int x
   1.105 +  in (length x = 3) andalso (val_x >= 123) andalso (val_x <= 126)
   1.106 +  end;
   1.107 +
   1.108 +fun normalise_s s [] st_ sti =
   1.109 +      String.implode(rev(
   1.110 +        if st_
   1.111 +        then if null sti
   1.112 +             then (#"_" :: s)
   1.113 +             else if check_valid_int sti
   1.114 +                  then (Char.chr (cList2int sti) :: s)
   1.115 +                  else (sti @ (#"_" :: s))
   1.116 +        else s))
   1.117 +  | normalise_s s (#"_"::cs) st_ sti =
   1.118 +      if st_
   1.119 +      then let val s' = if null sti
   1.120 +                        then (#"_"::s)
   1.121 +                        else if check_valid_int sti
   1.122 +                             then (Char.chr (cList2int sti) :: s)
   1.123 +                             else (sti @ (#"_" :: s))
   1.124 +           in normalise_s s' cs false [] 
   1.125 +           end
   1.126 +      else normalise_s s cs true []
   1.127 +  | normalise_s s (c::cs) true sti =
   1.128 +      if (Char.isDigit c)
   1.129 +      then normalise_s s cs true (c::sti)
   1.130 +      else let val s' = if null sti
   1.131 +                        then if ((c >= #"A") andalso (c<= #"P"))
   1.132 +                             then ((Char.chr(Char.ord c - A_min_spc))::s)
   1.133 +                             else (c :: (#"_" :: s))
   1.134 +                        else if check_valid_int sti
   1.135 +                             then (Char.chr (cList2int sti) :: s)
   1.136 +                             else (sti @ (#"_" :: s))
   1.137 +           in normalise_s s' cs false []
   1.138 +           end
   1.139 +  | normalise_s s (c::cs) _ _ = normalise_s (c::s) cs false [];
   1.140 +
   1.141 +(*This version does not look for standard prefixes first.*)
   1.142 +fun normalise_string s = normalise_s [] (String.explode s) false [];
   1.143 +
   1.144 +
   1.145 +(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   1.146 +
   1.147 +exception STREE of stree;
   1.148 +
   1.149 +(*If string s has the prefix s1, return the result of deleting it.*)
   1.150 +fun strip_prefix s1 s = 
   1.151 +  if String.isPrefix s1 s then SOME (normalise_string (String.extract (s, size s1, NONE)))
   1.152 +  else NONE;
   1.153 +
   1.154 +(*Invert the table of translations between Isabelle and ATPs*)
   1.155 +val type_const_trans_table_inv =
   1.156 +      Symtab.make (map swap (Symtab.dest ResClause.type_const_trans_table));
   1.157 +
   1.158 +fun invert_type_const c =
   1.159 +    case Symtab.lookup type_const_trans_table_inv c of
   1.160 +        SOME c' => c'
   1.161 +      | NONE => c;
   1.162 +
   1.163 +fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS);
   1.164 +fun make_var (b,T) = Var((b,0),T);
   1.165 +
   1.166 +(*Type variables are given the basic sort, HOL.type. Some will later be constrained
   1.167 +  by information from type literals, or by type inference.*)
   1.168 +fun type_of_stree t =
   1.169 +  case t of
   1.170 +      Int _ => raise STREE t
   1.171 +    | Br (a,ts) => 
   1.172 +        let val Ts = map type_of_stree ts
   1.173 +        in 
   1.174 +          case strip_prefix ResClause.tconst_prefix a of
   1.175 +              SOME b => Type(invert_type_const b, Ts)
   1.176 +            | NONE => 
   1.177 +                if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   1.178 +                else 
   1.179 +                case strip_prefix ResClause.tfree_prefix a of
   1.180 +                    SOME b => TFree("'" ^ b, HOLogic.typeS)
   1.181 +                  | NONE => 
   1.182 +                case strip_prefix ResClause.tvar_prefix a of
   1.183 +                    SOME b => make_tvar b
   1.184 +                  | NONE => make_tvar a   (*Variable from the ATP, say X1*)
   1.185 +        end;
   1.186 +
   1.187 +(*Invert the table of translations between Isabelle and ATPs*)
   1.188 +val const_trans_table_inv =
   1.189 +      Symtab.make (map swap (Symtab.dest ResClause.const_trans_table));
   1.190 +
   1.191 +fun invert_const c =
   1.192 +    case Symtab.lookup const_trans_table_inv c of
   1.193 +        SOME c' => c'
   1.194 +      | NONE => c;
   1.195 +
   1.196 +(*The number of type arguments of a constant, zero if it's monomorphic*)
   1.197 +fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s));
   1.198 +
   1.199 +(*Generates a constant, given its type arguments*)
   1.200 +fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
   1.201 +
   1.202 +(*First-order translation. No types are known for variables. HOLogic.typeT should allow
   1.203 +  them to be inferred.*)
   1.204 +fun term_of_stree thy t =
   1.205 +  case t of
   1.206 +      Int _ => raise STREE t
   1.207 +    | Br (a,ts) => 
   1.208 +        case strip_prefix ResClause.const_prefix a of
   1.209 +            SOME "equal" => 
   1.210 +              if length ts = 2 then
   1.211 +                list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree thy) ts)
   1.212 +              else raise STREE t  (*equality needs two arguments*)
   1.213 +          | SOME b => 
   1.214 +              let val c = invert_const b
   1.215 +                  val nterms = length ts - num_typargs thy c
   1.216 +                  val us = List.map (term_of_stree thy) (List.take(ts,nterms))
   1.217 +                  val Ts = List.map type_of_stree (List.drop(ts,nterms))
   1.218 +              in  list_comb(const_of thy (c, Ts), us)  end
   1.219 +          | NONE => (*a variable, not a constant*)
   1.220 +              let val T = HOLogic.typeT
   1.221 +                  val opr = (*a Free variable is typically a Skolem function*)
   1.222 +                    case strip_prefix ResClause.fixed_var_prefix a of
   1.223 +                        SOME b => Free(b,T)
   1.224 +                      | NONE => 
   1.225 +                    case strip_prefix ResClause.schematic_var_prefix a of
   1.226 +                        SOME b => make_var (b,T)
   1.227 +                      | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
   1.228 +              in  list_comb (opr, List.map (term_of_stree thy) ts)  end;
   1.229 +
   1.230 +(*Type class literal applied to a type. Returns triple of polarity, class, type.*)                  
   1.231 +fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t
   1.232 +  | constraint_of_stree pol t = case t of
   1.233 +        Int _ => raise STREE t
   1.234 +      | Br (a,ts) => 
   1.235 +            (case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
   1.236 +                 (SOME b, [T]) => (pol, b, T)
   1.237 +               | _ => raise STREE t);
   1.238 +
   1.239 +(** Accumulate type constraints in a clause: negative type literals **)
   1.240 +
   1.241 +fun addix (key,z)  = Vartab.map_default (key,[]) (cons z);
   1.242 +
   1.243 +fun add_constraint ((false, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
   1.244 +  | add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt
   1.245 +  | add_constraint (_, vt) = vt;
   1.246 +
   1.247 +(*False literals (which E includes in its proofs) are deleted*)
   1.248 +val nofalses = filter (not o equal HOLogic.false_const);
   1.249 +
   1.250 +(*Accumulate sort constraints in vt, with "real" literals in lits.*)
   1.251 +fun lits_of_strees thy (vt, lits) [] = (vt, rev (nofalses lits))
   1.252 +  | lits_of_strees thy (vt, lits) (t::ts) = 
   1.253 +      lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits) ts
   1.254 +      handle STREE _ => 
   1.255 +      lits_of_strees thy (vt, term_of_stree thy t :: lits) ts;
   1.256 +
   1.257 +(*Update TVars/TFrees with detected sort constraints.*)
   1.258 +fun fix_sorts vt =
   1.259 +  let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
   1.260 +        | tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s))
   1.261 +        | tysubst (TFree (x, s)) = TFree (x, getOpt (Vartab.lookup vt (x,~1), s))
   1.262 +      fun tmsubst (Const (a, T)) = Const (a, tysubst T)
   1.263 +        | tmsubst (Free (a, T)) = Free (a, tysubst T)
   1.264 +        | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
   1.265 +        | tmsubst (t as Bound _) = t
   1.266 +        | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
   1.267 +        | tmsubst (t $ u) = tmsubst t $ tmsubst u;
   1.268 +  in fn t => if Vartab.is_empty vt then t else tmsubst t end;
   1.269 +
   1.270 +(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
   1.271 +  vt0 holds the initial sort constraints, from the conjecture clauses.*)
   1.272 +fun clause_of_strees_aux thy vt0 ts = 
   1.273 +  case lits_of_strees thy (vt0,[]) ts of
   1.274 +      (_, []) => HOLogic.false_const
   1.275 +    | (vt, lits) => 
   1.276 +        let val dt = fix_sorts vt (foldr1 HOLogic.mk_disj lits)
   1.277 +            val infer = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
   1.278 +        in 
   1.279 +           #1(infer (K NONE) (K NONE) (Name.make_context []) true ([dt], HOLogic.boolT))
   1.280 +        end; 
   1.281 +
   1.282 +(*Quantification over a list of Vars. FUXNE: for term.ML??*)
   1.283 +fun list_all_var ([], t: term) = t
   1.284 +  | list_all_var ((v as Var(ix,T)) :: vars, t) =
   1.285 +        (all T) $ Abs(string_of_indexname ix, T, abstract_over (v,t));
   1.286 +
   1.287 +fun gen_all_vars t = list_all_var (term_vars t, t);
   1.288 +
   1.289 +fun clause_of_strees thy vt0 ts =
   1.290 +  gen_all_vars (HOLogic.mk_Trueprop (clause_of_strees_aux thy vt0 ts));
   1.291 +
   1.292 +fun ints_of_stree_aux (Int n, ns) = n::ns
   1.293 +  | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
   1.294 +
   1.295 +fun ints_of_stree t = ints_of_stree_aux (t, []);
   1.296 +
   1.297 +fun decode_tstp thy vt0 (name, role, ts, annots) =
   1.298 +  let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
   1.299 +  in  (name, role, clause_of_strees thy vt0 ts, deps)  end;
   1.300 +
   1.301 +fun dest_tstp ((((name, role), ts), annots), chs) =
   1.302 +  case chs of
   1.303 +          "."::_ => (name, role, ts, annots)
   1.304 +        | _ => error ("TSTP line not terminated by \".\": " ^ implode chs);
   1.305 +
   1.306 +
   1.307 +(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
   1.308 +
   1.309 +fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt
   1.310 +  | add_tfree_constraint (_, vt) = vt;
   1.311 +
   1.312 +fun tfree_constraints_of_clauses vt [] = vt
   1.313 +  | tfree_constraints_of_clauses vt ([lit]::tss) = 
   1.314 +      (tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
   1.315 +       handle STREE _ => (*not a positive type constraint: ignore*)
   1.316 +       tfree_constraints_of_clauses vt tss)
   1.317 +  | tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss;
   1.318 +
   1.319 +
   1.320 +(**** Translation of TSTP files to Isar Proofs ****)
   1.321 +
   1.322 +fun decode_tstp_list thy tuples =
   1.323 +  let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
   1.324 +  in  map (decode_tstp thy vt0) tuples  end;
   1.325 +
   1.326 +fun isar_lines ctxt =
   1.327 +  let val string_of = ProofContext.string_of_term ctxt
   1.328 +      fun doline hs (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
   1.329 +            "assume " ^ lname ^ ": \"" ^ string_of t ^ "\"\n"
   1.330 +        | doline hs (lname, t, deps) =
   1.331 +            hs ^ lname ^ ": \"" ^ string_of t ^ 
   1.332 +            "\"\n  by (meson " ^ space_implode " " deps ^ ")\n"
   1.333 +      fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
   1.334 +        | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
   1.335 +  in setmp show_sorts true dolines end;
   1.336 +
   1.337 +fun notequal t (_,t',_) = not (t aconv t');
   1.338 +
   1.339 +fun eq_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   1.340 +
   1.341 +fun replace_dep (old, new) dep = if dep=old then new else [dep];
   1.342 +
   1.343 +fun replace_deps (old, new) (lno, t, deps) = 
   1.344 +      (lno, t, List.concat (map (replace_dep (old, new)) deps));
   1.345 +
   1.346 +(*Discard axioms and also False conjecture clauses (which can only contain type information).
   1.347 +  Consolidate adjacent lines that prove the same clause, since they differ only in type
   1.348 +  information.*)
   1.349 +fun add_prfline ((lno, "axiom", t, []), lines) =  (*axioms are not proof lines*)
   1.350 +      if eq_false t then lines   (*must be clsrel/clsarity: type information*)
   1.351 +      else (case take_prefix (notequal t) lines of
   1.352 +               (_,[]) => lines   (*no repetition of proof line*)
   1.353 +             | (pre, (lno',t',deps')::post) => 
   1.354 +                 pre @ map (replace_deps (lno', [lno])) post)
   1.355 +  | add_prfline ((lno, role, t, []), lines) =  (*no deps: conjecture clause*)
   1.356 +      if eq_false t then lines   (*must be tfree_tcs: type information*)
   1.357 +      else (lno, t, []) :: lines
   1.358 +  | add_prfline ((lno, role, t, deps), lines) =
   1.359 +      (case term_tvars t of (*Delete line if it has TVars: they are forbidden in goals*)
   1.360 +          _::_ => map (replace_deps (lno, deps)) lines
   1.361 +        | [] => 
   1.362 +            case take_prefix (notequal t) lines of
   1.363 +               (_,[]) => (lno, t, deps) :: lines   (*no repetition of proof line*)
   1.364 +             | (pre, (lno',t',deps')::post) => 
   1.365 +                 (lno, t', deps) ::  (*replace later line by earlier one*)
   1.366 +                 (pre @ map (replace_deps (lno', [lno])) post));
   1.367 +
   1.368 +(*Replace numeric proof lines by strings.*)
   1.369 +fun stringify_deps thm_names deps_map [] = []
   1.370 +  | stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
   1.371 +      if lno <= Vector.length thm_names  (*axiom*)
   1.372 +      then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines 
   1.373 +      else let val lname = "L" ^ Int.toString (length deps_map)
   1.374 +               fun fix lno = if lno <= Vector.length thm_names  
   1.375 +                             then SOME(Vector.sub(thm_names,lno-1))
   1.376 +                             else AList.lookup op= deps_map lno;
   1.377 +           in  (lname, t, List.mapPartial fix deps) ::
   1.378 +               stringify_deps thm_names ((lno,lname)::deps_map) lines
   1.379 +           end;
   1.380 +
   1.381 +fun decode_tstp_file ctxt (cnfs,thm_names) =
   1.382 +  let val tuples = map (dest_tstp o tstp_line o explode) cnfs
   1.383 +      val lines = foldr add_prfline [] (decode_tstp_list (ProofContext.theory_of ctxt) tuples)
   1.384 +  in  String.concat (isar_lines ctxt (stringify_deps thm_names [] lines))  end;
   1.385 +
   1.386 +(*Could use split_lines, but it can return blank lines...*)
   1.387 +val lines = String.tokens (equal #"\n");
   1.388 +
   1.389 +val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
   1.390 +
   1.391 +(*The output to the watcher must be a SINGLE line...clearly \t must not be used.*)
   1.392 +val encode_newlines = String.translate (fn c => if c = #"\n" then "\t" else str c);
   1.393 +val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c);
   1.394 +
   1.395 +fun signal_success probfile toParent ppid msg = 
   1.396 +  (trace ("\nReporting Success for" ^ probfile ^ "\n" ^ msg);
   1.397 +   TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n");
   1.398 +   TextIO.output (toParent, probfile ^ "\n");
   1.399 +   TextIO.flushOut toParent;
   1.400 +   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   1.401 +
   1.402 +fun tstp_extract proofextract probfile toParent ppid th sgno thm_names = 
   1.403 +  let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   1.404 +      and ctxt = ProofContext.init (Thm.theory_of_thm th)
   1.405 +       (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
   1.406 +         then to setupWatcher and checkChildren...but is it needed?*)
   1.407 +  in  
   1.408 +    signal_success probfile toParent ppid 
   1.409 +      (decode_tstp_file ctxt (cnfs,thm_names))
   1.410 +  end;
   1.411 +
   1.412 +
   1.413 +(**** retrieve the axioms that were used in the proof ****)
   1.414 +
   1.415 +(*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
   1.416 +fun get_axiom_names (thm_names: string vector) step_nums = 
   1.417 +    let fun is_axiom n = n <= Vector.length thm_names 
   1.418 +        fun index i = Vector.sub(thm_names, i-1)
   1.419 +        val axnums = List.filter is_axiom step_nums
   1.420 +        val axnames = sort_distinct string_ord (map index axnums)
   1.421 +    in
   1.422 +	if length axnums = length step_nums then "UNSOUND!!" :: axnames
   1.423 +	else axnames
   1.424 +    end
   1.425 +
   1.426 + (*String contains multiple lines. We want those of the form 
   1.427 +     "253[0:Inp] et cetera..."
   1.428 +  A list consisting of the first number in each line is returned. *)
   1.429 +fun get_spass_linenums proofstr = 
   1.430 +  let val toks = String.tokens (not o Char.isAlphaNum)
   1.431 +      fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
   1.432 +        | inputno _ = NONE
   1.433 +      val lines = String.tokens (fn c => c = #"\n") proofstr
   1.434 +  in  List.mapPartial (inputno o toks) lines  end
   1.435 +
   1.436 +fun get_axiom_names_spass proofstr thm_names =
   1.437 +   get_axiom_names thm_names (get_spass_linenums proofstr);
   1.438 +    
   1.439 +fun not_comma c = c <>  #",";
   1.440 +
   1.441 +(*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
   1.442 +fun parse_tstp_line s =
   1.443 +  let val ss = Substring.full (unprefix "cnf(" (nospaces s))
   1.444 +      val (intf,rest) = Substring.splitl not_comma ss
   1.445 +      val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
   1.446 +      (*We only allow negated_conjecture because the line number will be removed in
   1.447 +        get_axiom_names above, while suppressing the UNSOUND warning*)
   1.448 +      val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
   1.449 +                 then Substring.string intf 
   1.450 +                 else "error" 
   1.451 +  in  Int.fromString ints  end
   1.452 +  handle Fail _ => NONE; 
   1.453 +
   1.454 +fun get_axiom_names_tstp proofstr thm_names =
   1.455 +   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
   1.456 +    
   1.457 + (*String contains multiple lines. We want those of the form 
   1.458 +     "*********** [448, input] ***********".
   1.459 +  A list consisting of the first number in each line is returned. *)
   1.460 +fun get_vamp_linenums proofstr = 
   1.461 +  let val toks = String.tokens (not o Char.isAlphaNum)
   1.462 +      fun inputno [ntok,"input"] = Int.fromString ntok
   1.463 +        | inputno _ = NONE
   1.464 +      val lines = String.tokens (fn c => c = #"\n") proofstr
   1.465 +  in  List.mapPartial (inputno o toks) lines  end
   1.466 +
   1.467 +fun get_axiom_names_vamp proofstr thm_names =
   1.468 +   get_axiom_names thm_names (get_vamp_linenums proofstr);
   1.469 +    
   1.470 +fun rules_to_string [] = "NONE"
   1.471 +  | rules_to_string xs = space_implode "  " xs
   1.472 +
   1.473 +
   1.474 +(*The signal handler in watcher.ML must be able to read the output of this.*)
   1.475 +fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names = 
   1.476 + (trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   1.477 +         " num of clauses is " ^ string_of_int (Vector.length thm_names));
   1.478 +  signal_success probfile toParent ppid 
   1.479 +    ("Lemmas used in automatic proof: " ^ rules_to_string (getax proofstr thm_names)))
   1.480 + handle e => (*FIXME: exn handler is too general!*)
   1.481 +  (trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);
   1.482 +   TextIO.output (toParent, "Translation failed for the proof: " ^ 
   1.483 +                  String.toString proofstr ^ "\n");
   1.484 +   TextIO.output (toParent, probfile);
   1.485 +   TextIO.flushOut toParent;
   1.486 +   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   1.487 +
   1.488 +val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
   1.489 +
   1.490 +val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   1.491 +
   1.492 +val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   1.493 +
   1.494 +
   1.495 +(**** Extracting proofs from an ATP's output ****)
   1.496 +
   1.497 +(*Return everything in s that comes before the string t*)
   1.498 +fun cut_before t s = 
   1.499 +  let val (s1,s2) = Substring.position t (Substring.full s)
   1.500 +  in  if Substring.size s2 = 0 then error "cut_before: string not found" 
   1.501 +      else Substring.string s2
   1.502 +  end;
   1.503 +
   1.504 +val start_E = "# Proof object starts here."
   1.505 +val end_E   = "# Proof object ends here."
   1.506 +val start_V6 = "%================== Proof: ======================"
   1.507 +val end_V6   = "%==============  End of proof. =================="
   1.508 +val start_V8 = "=========== Refutation =========="
   1.509 +val end_V8 = "======= End of refutation ======="
   1.510 +val end_SPASS = "Formulae used in the proof"
   1.511 +
   1.512 +(*********************************************************************************)
   1.513 +(*  Inspect the output of an ATP process to see if it has found a proof,     *)
   1.514 +(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   1.515 +(*********************************************************************************)
   1.516 +
   1.517 +(*Returns "true" if it successfully returns a lemma list, otherwise "false", but this
   1.518 +  return value is currently never used!*)
   1.519 +fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   1.520 + let fun transferInput currentString =
   1.521 +      let val thisLine = TextIO.inputLine fromChild
   1.522 +      in
   1.523 +	if thisLine = "" (*end of file?*)
   1.524 +	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   1.525 +	             "\naccumulated text: " ^ currentString);
   1.526 +	      false)                    
   1.527 +	else if String.isPrefix endS thisLine
   1.528 +	then let val proofextract = currentString ^ cut_before endS thisLine
   1.529 +	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   1.530 +			  	  else if endS = end_SPASS then spass_lemma_list
   1.531 +			  	  else e_lemma_list
   1.532 +	     in
   1.533 +	       trace ("\nExtracted proof:\n" ^ proofextract); 
   1.534 +	       if !full andalso String.isPrefix "cnf(" proofextract
   1.535 +	       then tstp_extract proofextract probfile toParent ppid th sgno thm_names
   1.536 +	       else lemma_list proofextract probfile toParent ppid thm_names;
   1.537 +	       true
   1.538 +	     end
   1.539 +	else transferInput (currentString^thisLine)
   1.540 +      end
   1.541 + in
   1.542 +     transferInput ""
   1.543 + end 
   1.544 +
   1.545 +
   1.546 +(*The signal handler in watcher.ML must be able to read the output of this.*)
   1.547 +fun signal_parent (toParent, ppid, msg, probfile) =
   1.548 + (TextIO.output (toParent, msg);
   1.549 +  TextIO.output (toParent, probfile ^ "\n");
   1.550 +  TextIO.flushOut toParent;
   1.551 +  trace ("\nSignalled parent: " ^ msg ^ probfile);
   1.552 +  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.553 +  (*Give the parent time to respond before possibly sending another signal*)
   1.554 +  OS.Process.sleep (Time.fromMilliseconds 600));
   1.555 +
   1.556 +(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   1.557 +fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   1.558 + let val thisLine = TextIO.inputLine fromChild
   1.559 + in   
   1.560 +     trace thisLine;
   1.561 +     if thisLine = "" 
   1.562 +     then (trace "\nNo proof output seen"; false)
   1.563 +     else if String.isPrefix start_V8 thisLine
   1.564 +     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.565 +     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   1.566 +             (String.isPrefix "Refutation not found" thisLine)
   1.567 +     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.568 +	   true)
   1.569 +     else checkVampProofFound  (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.570 +  end
   1.571 +
   1.572 +(*Called from watcher. Returns true if the E process has returned a verdict.*)
   1.573 +fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   1.574 + let val thisLine = TextIO.inputLine fromChild  
   1.575 + in   
   1.576 +     trace thisLine;
   1.577 +     if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.578 +     else if String.isPrefix start_E thisLine
   1.579 +     then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.580 +     else if String.isPrefix "# Problem is satisfiable" thisLine
   1.581 +     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.582 +	   true)
   1.583 +     else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   1.584 +     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.585 +	   true)
   1.586 +     else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.587 + end;
   1.588 +
   1.589 +(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   1.590 +fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   1.591 + let val thisLine = TextIO.inputLine fromChild  
   1.592 + in    
   1.593 +     trace thisLine;
   1.594 +     if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.595 +     else if String.isPrefix "Here is a proof" thisLine
   1.596 +     then      
   1.597 +        startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.598 +     else if thisLine = "SPASS beiseite: Completion found.\n"
   1.599 +     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.600 +	   true)
   1.601 +     else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   1.602 +             thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.603 +     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.604 +	   true)
   1.605 +    else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.606 + end
   1.607 +
   1.608 +end;