src/HOL/Tools/res_atp.ML
author paulson
Wed Sep 13 12:20:21 2006 +0200 (2006-09-13)
changeset 20526 756c4f1fd04c
parent 20457 85414caac94a
child 20532 64181717e37c
permissions -rw-r--r--
Extended the blacklist with higher-order theorems. Restructured. Added checks to
ensure that no higher-order clauses are output in first-order mode.
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 (*FIXME: Do we need this signature?*)
     9 signature RES_ATP =
    10 sig
    11   val prover: string ref
    12   val custom_spass: string list ref
    13   val destdir: string ref
    14   val helper_path: string -> string -> string
    15   val problem_name: string ref
    16   val time_limit: int ref
    17    
    18   datatype mode = Auto | Fol | Hol
    19   val linkup_logic_mode : mode ref
    20   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    21   val vampire_time: int ref
    22   val eprover_time: int ref
    23   val spass_time: int ref
    24   val run_vampire: int -> unit
    25   val run_eprover: int -> unit
    26   val run_spass: int -> unit
    27   val vampireLimit: unit -> int
    28   val eproverLimit: unit -> int
    29   val spassLimit: unit -> int
    30   val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    31     Method.src -> Proof.context -> Proof.method
    32   val cond_rm_tmp: string -> unit
    33   val keep_atp_input: bool ref
    34   val fol_keep_types: bool ref
    35   val hol_full_types: unit -> unit
    36   val hol_partial_types: unit -> unit
    37   val hol_const_types_only: unit -> unit
    38   val hol_no_types: unit -> unit
    39   val hol_typ_level: unit -> ResHolClause.type_level
    40   val include_all: bool ref
    41   val run_relevance_filter: bool ref
    42   val run_blacklist_filter: bool ref
    43   val blacklist: string list ref
    44   val add_all : unit -> unit
    45   val add_claset : unit -> unit
    46   val add_simpset : unit -> unit
    47   val add_clasimp : unit -> unit
    48   val add_atpset : unit -> unit
    49   val rm_all : unit -> unit
    50   val rm_claset : unit -> unit
    51   val rm_simpset : unit -> unit
    52   val rm_atpset : unit -> unit
    53   val rm_clasimp : unit -> unit
    54 end;
    55 
    56 structure ResAtp =
    57 struct
    58 
    59 (********************************************************************)
    60 (* some settings for both background automatic ATP calling procedure*)
    61 (* and also explicit ATP invocation methods                         *)
    62 (********************************************************************)
    63 
    64 (*** background linkup ***)
    65 val call_atp = ref false; 
    66 val hook_count = ref 0;
    67 val time_limit = ref 80;
    68 val prover = ref "E";   (* use E as the default prover *)
    69 val custom_spass =   (*specialized options for SPASS*)
    70       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    71 val destdir = ref "";   (*Empty means write files to /tmp*)
    72 val problem_name = ref "prob";
    73 
    74 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    75   it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
    76 fun helper_path evar base =
    77   case getenv evar of
    78       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    79     | home => 
    80         let val path = home ^ "/" ^ base
    81         in  if File.exists (File.unpack_platform_path path) then path 
    82 	    else error ("Could not find the file " ^ path)
    83 	end;  
    84 
    85 fun probfile_nosuffix _ = 
    86   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    87   else if File.exists (File.unpack_platform_path (!destdir))
    88   then !destdir ^ "/" ^ !problem_name
    89   else error ("No such directory: " ^ !destdir);
    90 
    91 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    92 
    93 
    94 (*** ATP methods ***)
    95 val vampire_time = ref 60;
    96 val eprover_time = ref 60;
    97 val spass_time = ref 60;
    98 
    99 fun run_vampire time =  
   100     if (time >0) then vampire_time:= time
   101     else vampire_time:=60;
   102 
   103 fun run_eprover time = 
   104     if (time > 0) then eprover_time:= time
   105     else eprover_time:=60;
   106 
   107 fun run_spass time = 
   108     if (time > 0) then spass_time:=time
   109     else spass_time:=60;
   110 
   111 
   112 fun vampireLimit () = !vampire_time;
   113 fun eproverLimit () = !eprover_time;
   114 fun spassLimit () = !spass_time;
   115 
   116 val keep_atp_input = ref false;
   117 val fol_keep_types = ResClause.keep_types;
   118 val hol_full_types = ResHolClause.full_types;
   119 val hol_partial_types = ResHolClause.partial_types;
   120 val hol_const_types_only = ResHolClause.const_types_only;
   121 val hol_no_types = ResHolClause.no_types;
   122 fun hol_typ_level () = ResHolClause.find_typ_level ();
   123 fun is_typed_hol () = 
   124     let val tp_level = hol_typ_level()
   125     in
   126 	not (tp_level = ResHolClause.T_NONE)
   127     end;
   128 val include_combS = ResHolClause.include_combS;
   129 val include_min_comb = ResHolClause.include_min_comb;
   130 
   131 fun atp_input_file () =
   132     let val file = !problem_name 
   133     in
   134 	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   135 	else if File.exists (File.unpack_platform_path (!destdir))
   136 	then !destdir ^ "/" ^ file
   137 	else error ("No such directory: " ^ !destdir)
   138     end;
   139 
   140 val include_all = ref false;
   141 val include_simpset = ref false;
   142 val include_claset = ref false; 
   143 val include_atpset = ref true;
   144 
   145 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   146 fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
   147 fun rm_all() = include_all:=false;
   148 
   149 fun add_simpset() = include_simpset:=true;
   150 fun rm_simpset() = include_simpset:=false;
   151 
   152 fun add_claset() = include_claset:=true;
   153 fun rm_claset() = include_claset:=false;
   154 
   155 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   156 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   157 
   158 fun add_atpset() = include_atpset:=true;
   159 fun rm_atpset() = include_atpset:=false;
   160 
   161 
   162 (**** relevance filter ****)
   163 val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
   164 val run_blacklist_filter = ref true;
   165 
   166 (******************************************************************)
   167 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   168 (******************************************************************)
   169 
   170 datatype logic = FOL | HOL | HOLC | HOLCS;
   171 
   172 fun string_of_logic FOL = "FOL"
   173   | string_of_logic HOL = "HOL"
   174   | string_of_logic HOLC = "HOLC"
   175   | string_of_logic HOLCS = "HOLCS";
   176 
   177 fun is_fol_logic FOL = true
   178   | is_fol_logic  _ = false
   179 
   180 (*HOLCS will not occur here*)
   181 fun upgrade_lg HOLC _ = HOLC
   182   | upgrade_lg HOL HOLC = HOLC
   183   | upgrade_lg HOL _ = HOL
   184   | upgrade_lg FOL lg = lg; 
   185 
   186 (* check types *)
   187 fun has_bool_hfn (Type("bool",_)) = true
   188   | has_bool_hfn (Type("fun",_)) = true
   189   | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
   190   | has_bool_hfn _ = false;
   191 
   192 fun is_hol_fn tp =
   193     let val (targs,tr) = strip_type tp
   194     in
   195 	exists (has_bool_hfn) (tr::targs)
   196     end;
   197 
   198 fun is_hol_pred tp =
   199     let val (targs,tr) = strip_type tp
   200     in
   201 	exists (has_bool_hfn) targs
   202     end;
   203 
   204 exception FN_LG of term;
   205 
   206 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   207     if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   208   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   209     if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   210   | fn_lg (t as Var(f,tp)) (lg,seen) =
   211     if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
   212   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
   213   | fn_lg f _ = raise FN_LG(f); 
   214 
   215 
   216 fun term_lg [] (lg,seen) = (lg,seen)
   217   | term_lg (tm::tms) (FOL,seen) =
   218       let val (f,args) = strip_comb tm
   219 	  val (lg',seen') = if f mem seen then (FOL,seen) 
   220 			    else fn_lg f (FOL,seen)
   221       in
   222 	if is_fol_logic lg' then ()
   223         else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
   224         term_lg (args@tms) (lg',seen')
   225       end
   226   | term_lg _ (lg,seen) = (lg,seen)
   227 
   228 exception PRED_LG of term;
   229 
   230 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   231       if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
   232   | pred_lg (t as Free(P,tp)) (lg,seen) =
   233       if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
   234   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
   235   | pred_lg P _ = raise PRED_LG(P);
   236 
   237 
   238 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   239   | lit_lg P (lg,seen) =
   240       let val (pred,args) = strip_comb P
   241 	  val (lg',seen') = if pred mem seen then (lg,seen) 
   242 			    else pred_lg pred (lg,seen)
   243       in
   244 	if is_fol_logic lg' then ()
   245 	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
   246 	term_lg args (lg',seen')
   247       end;
   248 
   249 fun lits_lg [] (lg,seen) = (lg,seen)
   250   | lits_lg (lit::lits) (FOL,seen) =
   251       let val (lg,seen') = lit_lg lit (FOL,seen)
   252       in
   253 	if is_fol_logic lg then ()
   254 	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
   255 	lits_lg lits (lg,seen')
   256       end
   257   | lits_lg lits (lg,seen) = (lg,seen);
   258 
   259 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
   260     dest_disj_aux t (dest_disj_aux t' disjs)
   261   | dest_disj_aux t disjs = t::disjs;
   262 
   263 fun dest_disj t = dest_disj_aux t [];
   264 
   265 fun logic_of_clause tm (lg,seen) =
   266     let val tm' = HOLogic.dest_Trueprop tm
   267 	val disjs = dest_disj tm'
   268     in
   269 	lits_lg disjs (lg,seen)
   270     end;
   271 
   272 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   273   | logic_of_clauses (cls::clss) (FOL,seen) =
   274     let val (lg,seen') = logic_of_clause cls (FOL,seen)
   275 	val _ =
   276           if is_fol_logic lg then ()
   277           else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
   278     in
   279 	logic_of_clauses clss (lg,seen')
   280     end
   281   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   282 
   283 fun problem_logic_goals_aux [] (lg,seen) = lg
   284   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   285     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   286     
   287 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   288 
   289 (***************************************************************)
   290 (* Retrieving and filtering lemmas                             *)
   291 (***************************************************************)
   292 
   293 (*** white list and black list of lemmas ***)
   294 
   295 (*The rule subsetI is frequently omitted by the relevance filter.*)
   296 val whitelist = ref [subsetI]; 
   297 
   298 (*Names of theorems and theorem lists to be banned. The final numeric suffix of
   299   theorem lists is first removed.
   300 
   301   These theorems typically produce clauses that are prolific (match too many equality or
   302   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   303   FIXME: this blacklist needs to be maintained using theory data and added to using
   304   an attribute.*)
   305 val blacklist = ref
   306   ["Datatype.prod.size",
   307    "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   308    "Datatype.unit.inducts",
   309    "Datatype.unit.split_asm", 
   310    "Datatype.unit.split",
   311    "Datatype.unit.splits",
   312    "Divides.dvd_0_left_iff",
   313    "Finite_Set.card_0_eq",
   314    "Finite_Set.card_infinite",
   315    "Finite_Set.Max_ge",
   316    "Finite_Set.Max_in",
   317    "Finite_Set.Max_le_iff",
   318    "Finite_Set.Max_less_iff",
   319    "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   320    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   321    "Finite_Set.Min_ge_iff",
   322    "Finite_Set.Min_gr_iff",
   323    "Finite_Set.Min_in",
   324    "Finite_Set.Min_le",
   325    "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
   326    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   327    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   328    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   329    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   330    "HOL.split_if_asm",     (*splitting theorem*)
   331    "HOL.split_if",         (*splitting theorem*)
   332    "IntDef.abs_split",
   333    "IntDef.Integ.Abs_Integ_inject",
   334    "IntDef.Integ.Abs_Integ_inverse",
   335    "IntDiv.zdvd_0_left",
   336    "List.append_eq_append_conv",
   337    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   338    "List.in_listsD",
   339    "List.in_listsI",
   340    "List.lists.Cons",
   341    "List.listsE",
   342    "Nat.less_one", (*not directional? obscure*)
   343    "Nat.not_gr0",
   344    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   345    "NatArith.of_nat_0_eq_iff",
   346    "NatArith.of_nat_eq_0_iff",
   347    "NatArith.of_nat_le_0_iff",
   348    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   349    "NatSimprocs.divide_less_0_iff_number_of",
   350    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   351    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   352    "NatSimprocs.le_minus_iff_1", (*not directional*)
   353    "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   354    "NatSimprocs.less_minus_iff_1", (*not directional*)
   355    "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   356    "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   357    "NatSimprocs.minus_le_iff_1", (*not directional*)
   358    "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   359    "NatSimprocs.minus_less_iff_1", (*not directional*)
   360    "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   361    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   362    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   363    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   364    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   365    "NatSimprocs.zero_less_divide_iff_number_of",
   366    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   367    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   368    "OrderedGroup.join_0_eq_0",
   369    "OrderedGroup.meet_0_eq_0",
   370    "OrderedGroup.pprt_eq_0",   (*obscure*)
   371    "OrderedGroup.pprt_eq_id",   (*obscure*)
   372    "OrderedGroup.pprt_mono",   (*obscure*)
   373    "Orderings.split_max",      (*splitting theorem*)
   374    "Orderings.split_min",      (*splitting theorem*)
   375    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   376    "Parity.power_eq_0_iff_number_of",
   377    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   378    "Parity.power_less_zero_eq_number_of",
   379    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   380    "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   381    "Power.zero_less_power_abs_iff",
   382    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   383    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   384    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   385    "Product_Type.split_split_asm",             (*splitting theorem*)
   386    "Product_Type.split_split",                 (*splitting theorem*)
   387    "Product_Type.unit_abs_eta_conv",
   388    "Product_Type.unit_induct",
   389    "Relation.diagI",
   390    "Relation.Domain_def",   (*involves an existential quantifier*)
   391    "Relation.Image_def",   (*involves an existential quantifier*)
   392    "Relation.ImageI",
   393    "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   394    "Ring_and_Field.divide_cancel_right",
   395    "Ring_and_Field.divide_divide_eq_left",
   396    "Ring_and_Field.divide_divide_eq_right",
   397    "Ring_and_Field.divide_eq_0_iff",
   398    "Ring_and_Field.divide_eq_1_iff",
   399    "Ring_and_Field.divide_eq_eq_1",
   400    "Ring_and_Field.divide_le_0_1_iff",
   401    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   402    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   403    "Ring_and_Field.divide_less_0_1_iff",
   404    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   405    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   406    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   407    "Ring_and_Field.field_mult_cancel_left",
   408    "Ring_and_Field.field_mult_cancel_right",
   409    "Ring_and_Field.inverse_le_iff_le_neg",
   410    "Ring_and_Field.inverse_le_iff_le",
   411    "Ring_and_Field.inverse_less_iff_less_neg",
   412    "Ring_and_Field.inverse_less_iff_less",
   413    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   414    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   415    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   416    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   417    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   418    "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
   419    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   420    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   421    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   422    "Set.Diff_insert0",
   423    "Set.disjoint_insert",
   424    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   425    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   426    "Set.image_Collect",      (*involves an existential quantifier*)
   427    "Set.image_def",          (*involves an existential quantifier*)
   428    "Set.insert_disjoint",
   429    "Set.Int_UNIV",  (*redundant with paramodulation*)
   430    "Set.Inter_iff", (*We already have InterI, InterE*)
   431    "Set.Inter_UNIV_conv",
   432    "Set.psubsetE",    (*too prolific and obscure*)
   433    "Set.psubsetI",
   434    "Set.singleton_insert_inj_eq'",
   435    "Set.singleton_insert_inj_eq",
   436    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   437    "Set.singletonI",
   438    "Set.Un_empty", (*redundant with paramodulation*)
   439    "Set.UNION_def",   (*involves an existential quantifier*)
   440    "Set.Union_empty_conv", (*redundant with paramodulation*)
   441    "Set.Union_iff",              (*We already have UnionI, UnionE*)
   442    "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   443    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   444    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   445    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   446    "SetInterval.ivl_subset"];  (*excessive case analysis*)
   447 
   448 
   449 (*These might be prolific but are probably OK, and min and max are basic.
   450    "Orderings.max_less_iff_conj", 
   451    "Orderings.min_less_iff_conj",
   452    "Orderings.min_max.below_inf.below_inf_conv",
   453    "Orderings.min_max.below_sup.above_sup_conv",
   454 Very prolific and somewhat obscure:
   455    "Set.InterD",
   456    "Set.UnionI",
   457 *)
   458 
   459 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   460 
   461 fun fake_thm_name th = 
   462     Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
   463 
   464 fun put_name_pair ("",th) = (fake_thm_name th, th)
   465   | put_name_pair (a,th)  = (a,th);
   466 
   467 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   468 
   469 exception HASH_CLAUSE and HASH_STRING;
   470 
   471 (*Catches (for deletion) theorems automatically generated from other theorems*)
   472 fun insert_suffixed_names ht x = 
   473      (Polyhash.insert ht (x^"_iff1", ()); 
   474       Polyhash.insert ht (x^"_iff2", ()); 
   475       Polyhash.insert ht (x^"_dest", ())); 
   476 
   477 (*Are all characters in this string digits?*)
   478 fun all_numeric s = null (String.tokens Char.isDigit s);
   479 
   480 (*Delete a suffix of the form _\d+*)
   481 fun delete_numeric_suffix s =
   482   case rev (String.fields (fn c => c = #"_") s) of
   483       last::rest => 
   484           if all_numeric last 
   485           then [s, space_implode "_" (rev rest)]
   486           else [s]
   487     | [] => [s];
   488 
   489 fun banned_thmlist s =
   490   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   491 
   492 fun make_banned_test xs = 
   493   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   494                                 (6000, HASH_STRING)
   495       fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s
   496       fun banned s = exists banned_aux (delete_numeric_suffix s)
   497   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   498       app (insert_suffixed_names ht) (!blacklist @ xs); 
   499       banned
   500   end;
   501 
   502 (** a hash function from Term.term to int, and also a hash table **)
   503 val xor_words = List.foldl Word.xorb 0w0;
   504 
   505 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   506   | hashw_term ((Free(_,_)), w) = w
   507   | hashw_term ((Var(_,_)), w) = w
   508   | hashw_term ((Bound _), w) = w
   509   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   510   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   511 
   512 fun hashw_pred (P,w) = 
   513     let val (p,args) = strip_comb P
   514     in
   515 	List.foldl hashw_term w (p::args)
   516     end;
   517 
   518 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
   519   | hash_literal P = hashw_pred(P,0w0);
   520 
   521 
   522 fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
   523   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   524   | get_literals lit lits = (lit::lits);
   525 
   526 
   527 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   528 
   529 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   530 
   531 (*Create a hash table for clauses, of the given size*)
   532 fun mk_clause_table n =
   533       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   534                        (n, HASH_CLAUSE);
   535 
   536 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   537   (name, theorem) pairs, but the theorems are hashed into the table. *)
   538 fun make_unique xs = 
   539   let val ht = mk_clause_table 2200
   540   in
   541       (app (ignore o Polyhash.peekInsert ht) (map swap xs);  
   542        map swap (Polyhash.listItems ht))
   543   end;
   544 
   545 (*FIXME: SLOW!!!*)
   546 fun mem_thm th [] = false
   547   | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
   548 
   549 (*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
   550   It would be faster to compare names, rather than theorems, and to use
   551   a symbol table or hash table.*)
   552 fun insert_thms [] thms_names = thms_names
   553   | insert_thms ((thm,name)::thms_names) thms_names' =
   554       if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
   555       else insert_thms thms_names ((thm,name)::thms_names');
   556 
   557 (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   558 fun get_relevant_clauses thy cls_thms white_cls goals =
   559   insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   560 
   561 
   562 fun display_thms [] = ()
   563   | display_thms ((name,thm)::nthms) = 
   564       let val nthm = name ^ ": " ^ (string_of_thm thm)
   565       in Output.debug nthm; display_thms nthms  end;
   566  
   567 fun all_facts_of ctxt =
   568   FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
   569   |> maps #2 |> map (`Thm.name_of_thm);
   570 
   571 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   572 fun get_clasimp_atp_lemmas ctxt user_thms = 
   573   let val included_thms =
   574 	if !include_all 
   575 	then (tap (fn ths => Output.debug
   576 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   577 	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
   578 	else 
   579 	let val claset_thms =
   580 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   581 		else []
   582 	    val simpset_thms = 
   583 		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
   584 		else []
   585 	    val atpset_thms =
   586 		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
   587 		else []
   588 	    val _ = if !Output.show_debug_msgs 
   589 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   590 		    else ()		 
   591 	in  claset_thms @ simpset_thms @ atpset_thms  end
   592       val user_rules = map (put_name_pair o ResAxioms.pairname)
   593 			   (if null user_thms then !whitelist else user_thms)
   594   in
   595       (map put_name_pair included_thms, user_rules)
   596   end;
   597 
   598 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   599 fun blacklist_filter thms = 
   600   if !run_blacklist_filter then 
   601       let val banned = make_banned_test (map #1 thms)
   602 	  fun ok (a,_) = not (banned a)
   603       in  filter ok thms  end
   604   else thms;
   605 
   606 
   607 (***************************************************************)
   608 (* ATP invocation methods setup                                *)
   609 (***************************************************************)
   610 
   611 fun cnf_hyps_thms ctxt = 
   612     let val ths = Assumption.prems_of ctxt
   613     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   614 
   615 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   616 datatype mode = Auto | Fol | Hol;
   617 
   618 val linkup_logic_mode = ref Auto;
   619 
   620 (*Ensures that no higher-order theorems "leak out"*)
   621 fun restrict_to_logic logic cls =
   622   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls 
   623 	                else cls;
   624 
   625 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   626     if is_fol_logic logic 
   627     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   628     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   629 
   630 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   631     if is_fol_logic logic 
   632     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   633     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   634 
   635 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   636 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   637     let val conj_cls = make_clauses conjectures 
   638                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   639 	val hyp_cls = cnf_hyps_thms ctxt
   640 	val goal_cls = conj_cls@hyp_cls
   641 	val logic = case mode of 
   642                             Auto => problem_logic_goals [map prop_of goal_cls]
   643 			  | Fol => FOL
   644 			  | Hol => HOL
   645 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   646 	val user_lemmas_names = map #1 user_rules
   647 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   648 	                             |> make_unique |> ResAxioms.cnf_rules_pairs
   649                                      |> restrict_to_logic logic 
   650 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   651 	val thy = ProofContext.theory_of ctxt
   652 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   653 	                            user_cls (map prop_of goal_cls)
   654 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   655 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   656 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   657         val writer = if dfg then dfg_writer else tptp_writer 
   658 	val file = atp_input_file()
   659     in
   660 	(writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   661 	 Output.debug ("Writing to " ^ file);
   662 	 file)
   663     end;
   664 
   665 
   666 (**** remove tmp files ****)
   667 fun cond_rm_tmp file = 
   668     if !keep_atp_input then Output.debug "ATP input kept..." 
   669     else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
   670     else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
   671 
   672 
   673 (****** setup ATPs as Isabelle methods ******)
   674 fun atp_meth' tac ths ctxt = 
   675     Method.SIMPLE_METHOD' HEADGOAL
   676     (tac ctxt ths);
   677 
   678 fun atp_meth tac ths ctxt = 
   679     let val thy = ProofContext.theory_of ctxt
   680 	val _ = ResClause.init thy
   681 	val _ = ResHolClause.init thy
   682     in
   683 	atp_meth' tac ths ctxt
   684     end;
   685 
   686 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   687 
   688 (***************************************************************)
   689 (* automatic ATP invocation                                    *)
   690 (***************************************************************)
   691 
   692 (* call prover with settings and problem file for the current subgoal *)
   693 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   694   let
   695     fun make_atp_list [] n = []
   696       | make_atp_list (sg_term::xs) n =
   697           let
   698             val probfile = prob_pathname n
   699             val time = Int.toString (!time_limit)
   700           in
   701             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   702             (*options are separated by Watcher.setting_sep, currently #"%"*)
   703             if !prover = "spass"
   704             then
   705               let val spass = helper_path "SPASS_HOME" "SPASS"
   706                   val sopts =
   707    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   708               in 
   709                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   710               end
   711             else if !prover = "vampire"
   712 	    then 
   713               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   714                   val casc = if !time_limit > 70 then "--mode casc%" else ""
   715                   val vopts = casc ^ "-m 100000%-t " ^ time
   716               in
   717                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   718               end
   719       	     else if !prover = "E"
   720       	     then
   721 	       let val Eprover = helper_path "E_HOME" "eproof"
   722 	       in
   723 		  ("E", Eprover, 
   724 		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
   725 		   make_atp_list xs (n+1)
   726 	       end
   727 	     else error ("Invalid prover name: " ^ !prover)
   728           end
   729 
   730     val atp_list = make_atp_list sg_terms 1
   731   in
   732     Watcher.callResProvers(childout,atp_list);
   733     Output.debug "Sent commands to watcher!"
   734   end
   735   
   736 fun trace_array fname =
   737   let val path = File.tmp_path (Path.basic fname)
   738   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   739 
   740 (*Converting a subgoal into negated conjecture clauses*)
   741 fun neg_clauses th n =
   742   let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
   743       val st = Seq.hd (EVERY' tacs n th)
   744       val negs = Option.valOf (metahyps_thms n st)
   745   in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
   746 		                       
   747 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   748   and allows the suppression of the suffix "_1" in problem-generation mode.
   749   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   750   subgoals, each involving &&.*)
   751 fun write_problem_files probfile (ctxt,th)  =
   752   let val goals = Thm.prems_of th
   753       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   754       val thy = ProofContext.theory_of ctxt
   755       fun get_neg_subgoals [] _ = []
   756         | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
   757       val goal_cls = get_neg_subgoals goals 1
   758       val logic = case !linkup_logic_mode of
   759 		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   760 	      | Fol => FOL
   761 	      | Hol => HOL
   762       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   763       val included_cls = included_thms |> blacklist_filter
   764                                        |> make_unique |> ResAxioms.cnf_rules_pairs 
   765                                        |> restrict_to_logic logic 
   766       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   767       (*clauses relevant to goal gl*)
   768       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   769                            goals
   770       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   771       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   772                        else is_typed_hol ()
   773       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
   774                              else []
   775       val _ = Output.debug ("classrel clauses = " ^ 
   776                             Int.toString (length classrel_clauses))
   777       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   778                           else []
   779       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   780       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   781       fun write_all [] [] _ = []
   782 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   783 	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
   784 	    probfile k) 
   785 	   :: write_all ccls_list axcls_list (k+1)
   786       val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   787       val thm_names = Array.fromList clnames
   788       val _ = if !Output.show_debug_msgs 
   789               then trace_array "thm_names" thm_names else ()
   790   in
   791       (filenames, thm_names)
   792   end;
   793 
   794 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   795                                     Posix.Process.pid * string list) option);
   796 
   797 fun kill_last_watcher () =
   798     (case !last_watcher_pid of 
   799          NONE => ()
   800        | SOME (_, _, pid, files) => 
   801 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   802 	   Watcher.killWatcher pid;  
   803 	   ignore (map (try OS.FileSys.remove) files)))
   804      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   805 
   806 (*writes out the current clasimpset to a tptp file;
   807   turns off xsymbol at start of function, restoring it at end    *)
   808 val isar_atp = setmp print_mode [] 
   809  (fn (ctxt, th) =>
   810   if Thm.no_prems th then ()
   811   else
   812     let
   813       val _ = kill_last_watcher()
   814       val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
   815       val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
   816     in
   817       last_watcher_pid := SOME (childin, childout, pid, files);
   818       Output.debug ("problem files: " ^ space_implode ", " files); 
   819       Output.debug ("pid: " ^ string_of_pid pid);
   820       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   821     end);
   822 
   823 val isar_atp_writeonly = setmp print_mode [] 
   824       (fn (ctxt,th) =>
   825        if Thm.no_prems th then ()
   826        else 
   827          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   828           	            else prob_pathname
   829          in ignore (write_problem_files probfile (ctxt,th)) end);
   830 
   831 
   832 (** the Isar toplevel hook **)
   833 
   834 fun invoke_atp_ml (ctxt, goal) =
   835   let val thy = ProofContext.theory_of ctxt;
   836   in
   837     Output.debug ("subgoals in isar_atp:\n" ^ 
   838 		  Pretty.string_of (ProofContext.pretty_term ctxt
   839 		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
   840     Output.debug ("current theory: " ^ Context.theory_name thy);
   841     inc hook_count;
   842     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   843     ResClause.init thy;
   844     ResHolClause.init thy;
   845     if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
   846     else isar_atp_writeonly (ctxt, goal)
   847   end;
   848 
   849 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   850  (fn state =>
   851   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   852   in  invoke_atp_ml (ctxt, goal)  end);
   853 
   854 val call_atpP =
   855   OuterSyntax.command 
   856     "ProofGeneral.call_atp" 
   857     "call automatic theorem provers" 
   858     OuterKeyword.diag
   859     (Scan.succeed invoke_atp);
   860 
   861 val _ = OuterSyntax.add_parsers [call_atpP];
   862 
   863 end;