diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Fri Jun 29 18:21:25 2007 +0200 @@ -228,7 +228,7 @@ case strip_prefix ResClause.schematic_var_prefix a of SOME b => make_var (b,T) | NONE => make_var (a,T) (*Variable from the ATP, say X1*) - in list_comb (opr, List.map (term_of_stree [] thy) (args@ts)) end; + in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; (*Type class literal applied to a type. Returns triple of polarity, class, type.*) fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t @@ -279,21 +279,18 @@ (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. vt0 holds the initial sort constraints, from the conjecture clauses.*) -fun clause_of_strees_aux ctxt vt0 ts = +fun clause_of_strees ctxt vt0 ts = let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT) end; -(*Quantification over a list of Vars. FUXNE: for term.ML??*) +(*Quantification over a list of Vars. FIXME: for term.ML??*) fun list_all_var ([], t: term) = t | list_all_var ((v as Var(ix,T)) :: vars, t) = (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t))); fun gen_all_vars t = list_all_var (term_vars t, t); -fun clause_of_strees thy vt0 ts = - gen_all_vars (HOLogic.mk_Trueprop (clause_of_strees_aux thy vt0 ts)); - fun ints_of_stree_aux (Int n, ns) = n::ns | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts; @@ -334,22 +331,62 @@ fun dest_disj t = dest_disj_aux t []; -(*Remove types from a term, to eliminate the randomness of type inference*) -fun smash_types (Const(a,_)) = Const(a,dummyT) - | smash_types (Free(a,_)) = Free(a,dummyT) - | smash_types (Var(a,_)) = Var(a,dummyT) - | smash_types (f$t) = smash_types f $ smash_types t - | smash_types t = t; +(** Finding a matching assumption. The literals may be permuted, and variable names + may disagree. We have to try all combinations of literals (quadratic!) and + match up the variable names consistently. **) + +fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) = + strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t)) + | strip_alls_aux _ t = t; + +val strip_alls = strip_alls_aux 0; + +exception MATCH_LITERAL; -val sort_lits = sort Term.fast_term_ord o dest_disj o - smash_types o HOLogic.dest_Trueprop o strip_all_body; +(*Ignore types: they are not to be trusted...*) +fun match_literal (t1$u1) (t2$u2) env = + match_literal t1 t2 (match_literal u1 u2 env) + | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = + match_literal t1 t2 env + | match_literal (Bound i1) (Bound i2) env = + if i1=i2 then env else raise MATCH_LITERAL + | match_literal (Const(a1,_)) (Const(a2,_)) env = + if a1=a2 then env else raise MATCH_LITERAL + | match_literal (Free(a1,_)) (Free(a2,_)) env = + if a1=a2 then env else raise MATCH_LITERAL + | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env + | match_literal _ _ env = raise MATCH_LITERAL; + +(*Checking that all variable associations are unique. The list env contains no + repetitions, but does it contain say (x,y) and (y,y)? *) +fun good env = + let val (xs,ys) = ListPair.unzip env + in not (has_duplicates (op=) xs orelse has_duplicates (op=) ys) end; + +(*Match one list of literals against another, ignoring types and the order of + literals. Sorting is unreliable because we don't have types or variable names.*) +fun matches_aux _ [] [] = true + | matches_aux env (lit::lits) ts = + let fun match1 us [] = false + | match1 us (t::ts) = + let val env' = match_literal lit t env + in (good env' andalso matches_aux env' lits (us@ts)) orelse + match1 (t::us) ts + end + handle MATCH_LITERAL => match1 (t::us) ts + in match1 [] ts end; + +(*Is this length test useful?*) +fun matches (lits1,lits2) = + length lits1 = length lits2 andalso + matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2); fun permuted_clause t = - let val lits = sort_lits t + let val lits = dest_disj t fun perm [] = NONE | perm (ctm::ctms) = - if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm - else perm ctms + if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm))) + then SOME ctm else perm ctms in perm end; fun have_or_show "show " lname = "show \"" @@ -364,7 +401,7 @@ SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n" | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*) | doline have (lname, t, deps) = - have_or_show have lname ^ string_of t ^ + have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^ "\"\n by (metis " ^ space_implode " " deps ^ ")\n" fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)] | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines @@ -373,7 +410,7 @@ fun notequal t (_,t',_) = not (t aconv t'); (*No "real" literals means only type information*) -fun eq_types t = t aconv (HOLogic.mk_Trueprop HOLogic.true_const); +fun eq_types t = t aconv HOLogic.true_const; fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; @@ -465,16 +502,18 @@ val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c); -(*The output to the watcher must be a SINGLE line...clearly \t must not be used.*) -val encode_newlines = String.translate (fn c => if c = #"\n" then "\t" else str c); -val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c); +val txt_path = Path.ext "txt" o Path.explode o nospaces; fun signal_success probfile toParent ppid msg = - (trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg); - TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n"); - TextIO.output (toParent, probfile ^ "\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); + let val _ = trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg) + in + (*We write the proof to a file because sending very long lines may fail...*) + File.write (txt_path probfile) msg; + TextIO.output (toParent, "Success.\n"); + TextIO.output (toParent, probfile ^ "\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2) + end; fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names = let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))