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