src/HOL/Tools/res_atp.ML

Definitions produced by packages are now blacklisted.

(*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
    ID: $Id$
    Copyright 2004 University of Cambridge

ATPs with TPTP format input.
*)

(*FIXME: Do we need this signature?*)
signature RES_ATP =
sig
  val prover: string ref
  val custom_spass: string list ref
  val destdir: string ref
  val helper_path: string -> string -> string
  val problem_name: string ref
  val time_limit: int ref
   
  datatype mode = Auto | Fol | Hol
  val linkup_logic_mode : mode ref
  val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
  val vampire_time: int ref
  val eprover_time: int ref
  val spass_time: int ref
  val run_vampire: int -> unit
  val run_eprover: int -> unit
  val run_spass: int -> unit
  val vampireLimit: unit -> int
  val eproverLimit: unit -> int
  val spassLimit: unit -> int
  val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    Method.src -> Proof.context -> Proof.method
  val cond_rm_tmp: string -> unit
  val keep_atp_input: bool ref
  val fol_keep_types: bool ref
  val hol_full_types: unit -> unit
  val hol_partial_types: unit -> unit
  val hol_const_types_only: unit -> unit
  val hol_no_types: unit -> unit
  val hol_typ_level: unit -> ResHolClause.type_level
  val include_all: bool ref
  val run_relevance_filter: bool ref
  val run_blacklist_filter: bool ref
  val blacklist: string list ref
  val add_all : unit -> unit
  val add_claset : unit -> unit
  val add_simpset : unit -> unit
  val add_clasimp : unit -> unit
  val add_atpset : unit -> unit
  val rm_all : unit -> unit
  val rm_claset : unit -> unit
  val rm_simpset : unit -> unit
  val rm_atpset : unit -> unit
  val rm_clasimp : unit -> unit
end;

structure ResAtp =
struct

(********************************************************************)
(* some settings for both background automatic ATP calling procedure*)
(* and also explicit ATP invocation methods                         *)
(********************************************************************)

(*** background linkup ***)
val call_atp = ref false; 
val hook_count = ref 0;
val time_limit = ref 80;
val prover = ref "E";   (* use E as the default prover *)
val custom_spass =   (*specialized options for SPASS*)
      ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
val destdir = ref "";   (*Empty means write files to /tmp*)
val problem_name = ref "prob";

(*Return the path to a "helper" like SPASS or tptp2X, first checking that
  it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
fun helper_path evar base =
  case getenv evar of
      "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    | home => 
        let val path = home ^ "/" ^ base
        in  if File.exists (File.unpack_platform_path path) then path 
	    else error ("Could not find the file " ^ path)
	end;  

fun probfile_nosuffix _ = 
  if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
  else if File.exists (File.unpack_platform_path (!destdir))
  then !destdir ^ "/" ^ !problem_name
  else error ("No such directory: " ^ !destdir);

fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;


(*** ATP methods ***)
val vampire_time = ref 60;
val eprover_time = ref 60;
val spass_time = ref 60;

fun run_vampire time =  
    if (time >0) then vampire_time:= time
    else vampire_time:=60;

fun run_eprover time = 
    if (time > 0) then eprover_time:= time
    else eprover_time:=60;

fun run_spass time = 
    if (time > 0) then spass_time:=time
    else spass_time:=60;


fun vampireLimit () = !vampire_time;
fun eproverLimit () = !eprover_time;
fun spassLimit () = !spass_time;

val keep_atp_input = ref false;
val fol_keep_types = ResClause.keep_types;
val hol_full_types = ResHolClause.full_types;
val hol_partial_types = ResHolClause.partial_types;
val hol_const_types_only = ResHolClause.const_types_only;
val hol_no_types = ResHolClause.no_types;
fun hol_typ_level () = ResHolClause.find_typ_level ();
fun is_typed_hol () = 
    let val tp_level = hol_typ_level()
    in
	not (tp_level = ResHolClause.T_NONE)
    end;

fun atp_input_file () =
    let val file = !problem_name 
    in
	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
	else if File.exists (File.unpack_platform_path (!destdir))
	then !destdir ^ "/" ^ file
	else error ("No such directory: " ^ !destdir)
    end;

val include_all = ref false;
val include_simpset = ref false;
val include_claset = ref false; 
val include_atpset = ref true;

(*Tests show that follow_defs gives VERY poor results with "include_all"*)
fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
fun rm_all() = include_all:=false;

fun add_simpset() = include_simpset:=true;
fun rm_simpset() = include_simpset:=false;

fun add_claset() = include_claset:=true;
fun rm_claset() = include_claset:=false;

fun add_clasimp() = (include_simpset:=true;include_claset:=true);
fun rm_clasimp() = (include_simpset:=false;include_claset:=false);

fun add_atpset() = include_atpset:=true;
fun rm_atpset() = include_atpset:=false;


(**** relevance filter ****)
val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
val run_blacklist_filter = ref true;

(******************************************************************)
(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
(******************************************************************)

datatype logic = FOL | HOL | HOLC | HOLCS;

fun string_of_logic FOL = "FOL"
  | string_of_logic HOL = "HOL"
  | string_of_logic HOLC = "HOLC"
  | string_of_logic HOLCS = "HOLCS";

fun is_fol_logic FOL = true
  | is_fol_logic  _ = false

(*HOLCS will not occur here*)
fun upgrade_lg HOLC _ = HOLC
  | upgrade_lg HOL HOLC = HOLC
  | upgrade_lg HOL _ = HOL
  | upgrade_lg FOL lg = lg; 

(* check types *)
fun has_bool_hfn (Type("bool",_)) = true
  | has_bool_hfn (Type("fun",_)) = true
  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
  | has_bool_hfn _ = false;

fun is_hol_fn tp =
    let val (targs,tr) = strip_type tp
    in
	exists (has_bool_hfn) (tr::targs)
    end;

fun is_hol_pred tp =
    let val (targs,tr) = strip_type tp
    in
	exists (has_bool_hfn) targs
    end;

exception FN_LG of term;

fun fn_lg (t as Const(f,tp)) (lg,seen) = 
    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
  | fn_lg (t as Free(f,tp)) (lg,seen) = 
    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
  | fn_lg (t as Var(f,tp)) (lg,seen) =
    if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
  | fn_lg f _ = raise FN_LG(f); 


fun term_lg [] (lg,seen) = (lg,seen)
  | term_lg (tm::tms) (FOL,seen) =
      let val (f,args) = strip_comb tm
	  val (lg',seen') = if f mem seen then (FOL,seen) 
			    else fn_lg f (FOL,seen)
      in
	if is_fol_logic lg' then ()
        else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
        term_lg (args@tms) (lg',seen')
      end
  | term_lg _ (lg,seen) = (lg,seen)

exception PRED_LG of term;

fun pred_lg (t as Const(P,tp)) (lg,seen)= 
      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
  | pred_lg (t as Free(P,tp)) (lg,seen) =
      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
  | pred_lg P _ = raise PRED_LG(P);


fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
  | lit_lg P (lg,seen) =
      let val (pred,args) = strip_comb P
	  val (lg',seen') = if pred mem seen then (lg,seen) 
			    else pred_lg pred (lg,seen)
      in
	if is_fol_logic lg' then ()
	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
	term_lg args (lg',seen')
      end;

fun lits_lg [] (lg,seen) = (lg,seen)
  | lits_lg (lit::lits) (FOL,seen) =
      let val (lg,seen') = lit_lg lit (FOL,seen)
      in
	if is_fol_logic lg then ()
	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
	lits_lg lits (lg,seen')
      end
  | lits_lg lits (lg,seen) = (lg,seen);

fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
    dest_disj_aux t (dest_disj_aux t' disjs)
  | dest_disj_aux t disjs = t::disjs;

fun dest_disj t = dest_disj_aux t [];

fun logic_of_clause tm (lg,seen) =
    let val tm' = HOLogic.dest_Trueprop tm
	val disjs = dest_disj tm'
    in
	lits_lg disjs (lg,seen)
    end;

fun logic_of_clauses [] (lg,seen) = (lg,seen)
  | logic_of_clauses (cls::clss) (FOL,seen) =
    let val (lg,seen') = logic_of_clause cls (FOL,seen)
	val _ =
          if is_fol_logic lg then ()
          else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
    in
	logic_of_clauses clss (lg,seen')
    end
  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);

fun problem_logic_goals_aux [] (lg,seen) = lg
  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
    problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
    
fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);

(***************************************************************)
(* Retrieving and filtering lemmas                             *)
(***************************************************************)

(*** white list and black list of lemmas ***)

(*The rule subsetI is frequently omitted by the relevance filter.*)
val whitelist = ref [subsetI]; 

(*Names of theorems and theorem lists to be banned. The final numeric suffix of
  theorem lists is first removed.

  These theorems typically produce clauses that are prolific (match too many equality or
  membership literals) and relate to seldom-used facts. Some duplicate other rules.
  FIXME: this blacklist needs to be maintained using theory data and added to using
  an attribute.*)
val blacklist = ref
  ["Datatype.prod.size",
   "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   "Datatype.unit.inducts",
   "Datatype.unit.split_asm", 
   "Datatype.unit.split",
   "Datatype.unit.splits",
   "Divides.dvd_0_left_iff",
   "Finite_Set.card_0_eq",
   "Finite_Set.card_infinite",
   "Finite_Set.Max_ge",
   "Finite_Set.Max_in",
   "Finite_Set.Max_le_iff",
   "Finite_Set.Max_less_iff",
   "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   "Finite_Set.Min_ge_iff",
   "Finite_Set.Min_gr_iff",
   "Finite_Set.Min_in",
   "Finite_Set.Min_le",
   "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
   "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   "HOL.split_if_asm",     (*splitting theorem*)
   "HOL.split_if",         (*splitting theorem*)
   "IntDef.abs_split",
   "IntDef.Integ.Abs_Integ_inject",
   "IntDef.Integ.Abs_Integ_inverse",
   "IntDiv.zdvd_0_left",
   "List.append_eq_append_conv",
   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   "List.in_listsD",
   "List.in_listsI",
   "List.lists.Cons",
   "List.listsE",
   "Nat.less_one", (*not directional? obscure*)
   "Nat.not_gr0",
   "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   "NatArith.of_nat_0_eq_iff",
   "NatArith.of_nat_eq_0_iff",
   "NatArith.of_nat_le_0_iff",
   "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   "NatSimprocs.divide_less_0_iff_number_of",
   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   "NatSimprocs.le_minus_iff_1", (*not directional*)
   "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   "NatSimprocs.less_minus_iff_1", (*not directional*)
   "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   "NatSimprocs.minus_le_iff_1", (*not directional*)
   "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   "NatSimprocs.minus_less_iff_1", (*not directional*)
   "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   "NatSimprocs.zero_less_divide_iff_number_of",
   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   "OrderedGroup.join_0_eq_0",
   "OrderedGroup.meet_0_eq_0",
   "OrderedGroup.pprt_eq_0",   (*obscure*)
   "OrderedGroup.pprt_eq_id",   (*obscure*)
   "OrderedGroup.pprt_mono",   (*obscure*)
   "Orderings.split_max",      (*splitting theorem*)
   "Orderings.split_min",      (*splitting theorem*)
   "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   "Parity.power_eq_0_iff_number_of",
   "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   "Parity.power_less_zero_eq_number_of",
   "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   "Power.zero_less_power_abs_iff",
   "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   "Product_Type.split_split_asm",             (*splitting theorem*)
   "Product_Type.split_split",                 (*splitting theorem*)
   "Product_Type.unit_abs_eta_conv",
   "Product_Type.unit_induct",
   "Relation.diagI",
   "Relation.Domain_def",   (*involves an existential quantifier*)
   "Relation.Image_def",   (*involves an existential quantifier*)
   "Relation.ImageI",
   "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   "Ring_and_Field.divide_cancel_right",
   "Ring_and_Field.divide_divide_eq_left",
   "Ring_and_Field.divide_divide_eq_right",
   "Ring_and_Field.divide_eq_0_iff",
   "Ring_and_Field.divide_eq_1_iff",
   "Ring_and_Field.divide_eq_eq_1",
   "Ring_and_Field.divide_le_0_1_iff",
   "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   "Ring_and_Field.divide_less_0_1_iff",
   "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   "Ring_and_Field.field_mult_cancel_left",
   "Ring_and_Field.field_mult_cancel_right",
   "Ring_and_Field.inverse_le_iff_le_neg",
   "Ring_and_Field.inverse_le_iff_le",
   "Ring_and_Field.inverse_less_iff_less_neg",
   "Ring_and_Field.inverse_less_iff_less",
   "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
   "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   "Set.Diff_insert0",
   "Set.disjoint_insert",
   "Set.empty_Union_conv",   (*redundant with paramodulation*)
   "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   "Set.image_Collect",      (*involves an existential quantifier*)
   "Set.image_def",          (*involves an existential quantifier*)
   "Set.insert_disjoint",
   "Set.Int_UNIV",  (*redundant with paramodulation*)
   "Set.Inter_iff", (*We already have InterI, InterE*)
   "Set.Inter_UNIV_conv",
   "Set.psubsetE",    (*too prolific and obscure*)
   "Set.psubsetI",
   "Set.singleton_insert_inj_eq'",
   "Set.singleton_insert_inj_eq",
   "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   "Set.singletonI",
   "Set.Un_empty", (*redundant with paramodulation*)
   "Set.UNION_def",   (*involves an existential quantifier*)
   "Set.Union_empty_conv", (*redundant with paramodulation*)
   "Set.Union_iff",              (*We already have UnionI, UnionE*)
   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   "SetInterval.ivl_subset"];  (*excessive case analysis*)


(*These might be prolific but are probably OK, and min and max are basic.
   "Orderings.max_less_iff_conj", 
   "Orderings.min_less_iff_conj",
   "Orderings.min_max.below_inf.below_inf_conv",
   "Orderings.min_max.below_sup.above_sup_conv",
Very prolific and somewhat obscure:
   "Set.InterD",
   "Set.UnionI",
*)

(*** retrieve lemmas from clasimpset and atpset, may filter them ***)

(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)

exception HASH_CLAUSE and HASH_STRING;

(*Catches (for deletion) theorems automatically generated from other theorems*)
fun insert_suffixed_names ht x = 
     (Polyhash.insert ht (x^"_iff1", ()); 
      Polyhash.insert ht (x^"_iff2", ()); 
      Polyhash.insert ht (x^"_dest", ())); 

(*Are all characters in this string digits?*)
fun all_numeric s = null (String.tokens Char.isDigit s);

(*Delete a suffix of the form _\d+*)
fun delete_numeric_suffix s =
  case rev (String.fields (fn c => c = #"_") s) of
      last::rest => 
          if all_numeric last 
          then [s, space_implode "_" (rev rest)]
          else [s]
    | [] => [s];

fun banned_thmlist s =
  (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];

(*Reject theorems with names like "List.filter.filter_list_def" or
  "Accessible_Part.acc.defs", as these are definitions arising from packages*)
fun is_package_def a =
  let val l = NameSpace.unpack a
  in  length l > 2 andalso String.isSubstring "def" (List.last l)  end;

fun make_banned_test xs = 
  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
                                (6000, HASH_STRING)
      fun banned_aux s = 
            isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
      fun banned s = exists banned_aux (delete_numeric_suffix s)
  in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
      app (insert_suffixed_names ht) (!blacklist @ xs); 
      banned
  end;

(** a hash function from Term.term to int, and also a hash table **)
val xor_words = List.foldl Word.xorb 0w0;

fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
  | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
  | hashw_term ((Var(_,_)), w) = w
  | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
  | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
  | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));

fun hashw_pred (P,w) = 
    let val (p,args) = strip_comb P
    in
	List.foldl hashw_term w (p::args)
    end;

fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
  | hash_literal P = hashw_pred(P,0w0);


fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
  | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
  | get_literals lit lits = (lit::lits);


fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));

(*Versions ONLY for "faking" a theorem name. Here we take variable names into account
  so that similar theorems don't collide.  FIXME: this entire business of "faking" 
  theorem names must end!*)
fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
  | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
  | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);

fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
  | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
  | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
  | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
  | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
  | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));

fun full_hashw_thm (th,w) = 
  let val {prop,hyps,...} = rep_thm th
  in List.foldl full_hashw_term w (prop::hyps) end

fun full_hash_thm th = full_hashw_thm (th,0w0);

fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);

(*Create a hash table for clauses, of the given size*)
fun mk_clause_table n =
      Polyhash.mkTable (hash_term o prop_of, equal_thm)
                       (n, HASH_CLAUSE);

(*Use a hash table to eliminate duplicates from xs. Argument is a list of
  (name, theorem) pairs, but the theorems are hashed into the table. *)
fun make_unique xs = 
  let val ht = mk_clause_table 2200
  in
      (app (ignore o Polyhash.peekInsert ht) (map swap xs);  
       map swap (Polyhash.listItems ht))
  end;

(*FIXME: SLOW!!!*)
fun mem_thm th [] = false
  | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;

(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
  It would be faster to compare names, rather than theorems, and to use
  a symbol table or hash table.*)
fun insert_thms [] thms_names = thms_names
  | insert_thms ((thm,name)::thms_names) thms_names' =
      if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
      else insert_thms thms_names ((thm,name)::thms_names');

(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
fun get_relevant_clauses thy cls_thms white_cls goals =
  insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);

(*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
fun fake_thm_name th = 
    Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);

fun put_name_pair ("",th) = (fake_thm_name th, th)
  | put_name_pair (a,th)  = (a,th);

fun display_thms [] = ()
  | display_thms ((name,thm)::nthms) = 
      let val nthm = name ^ ": " ^ (string_of_thm thm)
      in Output.debug nthm; display_thms nthms  end;
 
fun all_facts_of ctxt =
  FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
  |> maps #2 |> map (`Thm.name_of_thm);

(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt user_thms = 
  let val included_thms =
	if !include_all 
	then (tap (fn ths => Output.debug
	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
	else 
	let val claset_thms =
		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
		else []
	    val simpset_thms = 
		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
		else []
	    val atpset_thms =
		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
		else []
	    val _ = if !Output.show_debug_msgs 
		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
		    else ()		 
	in  claset_thms @ simpset_thms @ atpset_thms  end
      val user_rules = map (put_name_pair o ResAxioms.pairname)
			   (if null user_thms then !whitelist else user_thms)
  in
      (map put_name_pair included_thms, user_rules)
  end;

(*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
fun blacklist_filter thms = 
  if !run_blacklist_filter then 
      let val banned = make_banned_test (map #1 thms)
	  fun ok (a,_) = not (banned a)
      in  filter ok thms  end
  else thms;


(***************************************************************)
(* ATP invocation methods setup                                *)
(***************************************************************)

fun cnf_hyps_thms ctxt = 
    let val ths = Assumption.prems_of ctxt
    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;

(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
datatype mode = Auto | Fol | Hol;

val linkup_logic_mode = ref Auto;

(*Ensures that no higher-order theorems "leak out"*)
fun restrict_to_logic logic cls =
  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
	                else cls;

fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
    if is_fol_logic logic 
    then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;

fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
    if is_fol_logic logic 
    then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;

(*Called by the oracle-based methods declared in res_atp_methods.ML*)
fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
    let val conj_cls = make_clauses conjectures 
                         |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
	val hyp_cls = cnf_hyps_thms ctxt
	val goal_cls = conj_cls@hyp_cls
	val logic = case mode of 
                            Auto => problem_logic_goals [map prop_of goal_cls]
			  | Fol => FOL
			  | Hol => HOL
	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
	val cla_simp_atp_clauses = included_thms |> blacklist_filter
	                             |> make_unique |> ResAxioms.cnf_rules_pairs
                                     |> restrict_to_logic logic 
	val user_cls = ResAxioms.cnf_rules_pairs user_rules
	val thy = ProofContext.theory_of ctxt
	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
	                            user_cls (map prop_of goal_cls)
	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
        val writer = if dfg then dfg_writer else tptp_writer 
	and file = atp_input_file()
	and user_lemmas_names = map #1 user_rules
    in
	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
	Output.debug ("Writing to " ^ file);
	file
    end;


(**** remove tmp files ****)
fun cond_rm_tmp file = 
    if !keep_atp_input then Output.debug "ATP input kept..." 
    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
    else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);


(****** setup ATPs as Isabelle methods ******)
fun atp_meth' tac ths ctxt = 
    Method.SIMPLE_METHOD' HEADGOAL
    (tac ctxt ths);

fun atp_meth tac ths ctxt = 
    let val thy = ProofContext.theory_of ctxt
	val _ = ResClause.init thy
	val _ = ResHolClause.init thy
    in
	atp_meth' tac ths ctxt
    end;

fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);

(***************************************************************)
(* automatic ATP invocation                                    *)
(***************************************************************)

(* call prover with settings and problem file for the current subgoal *)
fun watcher_call_provers sign sg_terms (childin, childout, pid) =
  let
    fun make_atp_list [] n = []
      | make_atp_list (sg_term::xs) n =
          let
            val probfile = prob_pathname n
            val time = Int.toString (!time_limit)
          in
            Output.debug ("problem file in watcher_call_provers is " ^ probfile);
            (*options are separated by Watcher.setting_sep, currently #"%"*)
            if !prover = "spass"
            then
              let val spass = helper_path "SPASS_HOME" "SPASS"
                  val sopts =
   "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
              in 
                  ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
              end
            else if !prover = "vampire"
	    then 
              let val vampire = helper_path "VAMPIRE_HOME" "vampire"
                  val casc = if !time_limit > 70 then "--mode casc%" else ""
                  val vopts = casc ^ "-m 100000%-t " ^ time
              in
                  ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
              end
      	     else if !prover = "E"
      	     then
	       let val Eprover = helper_path "E_HOME" "eproof"
	       in
		  ("E", Eprover, 
		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
		   make_atp_list xs (n+1)
	       end
	     else error ("Invalid prover name: " ^ !prover)
          end

    val atp_list = make_atp_list sg_terms 1
  in
    Watcher.callResProvers(childout,atp_list);
    Output.debug "Sent commands to watcher!"
  end
  
fun trace_array fname =
  let val path = File.tmp_path (Path.basic fname)
  in  Array.app (File.append path o (fn s => s ^ "\n"))  end;

(*Converting a subgoal into negated conjecture clauses*)
fun neg_clauses th n =
  let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
      val st = Seq.hd (EVERY' tacs n th)
      val negs = Option.valOf (metahyps_thms n st)
  in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
		                       
(*We write out problem files for each subgoal. Argument probfile generates filenames,
  and allows the suppression of the suffix "_1" in problem-generation mode.
  FIXME: does not cope with &&, and it isn't easy because one could have multiple
  subgoals, each involving &&.*)
fun write_problem_files probfile (ctxt,th)  =
  let val goals = Thm.prems_of th
      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
      val thy = ProofContext.theory_of ctxt
      fun get_neg_subgoals [] _ = []
        | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
      val goal_cls = get_neg_subgoals goals 1
      val logic = case !linkup_logic_mode of
		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
	      | Fol => FOL
	      | Hol => HOL
      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
      val included_cls = included_thms |> blacklist_filter
                                       |> make_unique |> ResAxioms.cnf_rules_pairs 
                                       |> restrict_to_logic logic 
      val white_cls = ResAxioms.cnf_rules_pairs white_thms
      (*clauses relevant to goal gl*)
      val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
                           goals
      val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
      val keep_types = if is_fol_logic logic then !ResClause.keep_types 
                       else is_typed_hol ()
      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
                             else []
      val _ = Output.debug ("classrel clauses = " ^ 
                            Int.toString (length classrel_clauses))
      val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
                          else []
      val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
      val writer = if !prover = "spass" then dfg_writer else tptp_writer 
      fun write_all [] [] _ = []
	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
	    probfile k) 
	   :: write_all ccls_list axcls_list (k+1)
      val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
      val thm_names = Array.fromList clnames
      val _ = if !Output.show_debug_msgs 
              then trace_array "thm_names" thm_names else ()
  in
      (filenames, thm_names)
  end;

val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
                                    Posix.Process.pid * string list) option);

fun kill_last_watcher () =
    (case !last_watcher_pid of 
         NONE => ()
       | SOME (_, _, pid, files) => 
	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
	   Watcher.killWatcher pid;  
	   ignore (map (try OS.FileSys.remove) files)))
     handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";

(*writes out the current clasimpset to a tptp file;
  turns off xsymbol at start of function, restoring it at end    *)
val isar_atp = setmp print_mode [] 
 (fn (ctxt, th) =>
  if Thm.no_prems th then ()
  else
    let
      val _ = kill_last_watcher()
      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
    in
      last_watcher_pid := SOME (childin, childout, pid, files);
      Output.debug ("problem files: " ^ space_implode ", " files); 
      Output.debug ("pid: " ^ string_of_pid pid);
      watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    end);

val isar_atp_writeonly = setmp print_mode [] 
      (fn (ctxt,th) =>
       if Thm.no_prems th then ()
       else 
         let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
          	            else prob_pathname
         in ignore (write_problem_files probfile (ctxt,th)) end);


(** the Isar toplevel hook **)

fun invoke_atp_ml (ctxt, goal) =
  let val thy = ProofContext.theory_of ctxt;
  in
    Output.debug ("subgoals in isar_atp:\n" ^ 
		  Pretty.string_of (ProofContext.pretty_term ctxt
		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
    Output.debug ("current theory: " ^ Context.theory_name thy);
    inc hook_count;
    Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
    ResClause.init thy;
    ResHolClause.init thy;
    if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
    else isar_atp_writeonly (ctxt, goal)
  end;

val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
 (fn state =>
  let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
  in  invoke_atp_ml (ctxt, goal)  end);

val call_atpP =
  OuterSyntax.command 
    "ProofGeneral.call_atp" 
    "call automatic theorem provers" 
    OuterKeyword.diag
    (Scan.succeed invoke_atp);

val _ = OuterSyntax.add_parsers [call_atpP];

end;