src/HOL/Tools/res_atp.ML
changeset 20022 b07a138b4e7d
parent 19894 7c7e15b27145
child 20131 c89ee2f4efd5
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 06 11:26:49 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 06 12:18:17 2006 +0200
     1.3 @@ -503,8 +503,8 @@
     1.4  fun make_unique ht xs = 
     1.5        (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
     1.6  
     1.7 -fun mem_thm thm [] = false
     1.8 -  | mem_thm thm ((thm',name)::thms_names) = equal_thm (thm,thm') orelse mem_thm thm thms_names;
     1.9 +fun mem_thm th [] = false
    1.10 +  | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
    1.11  
    1.12  fun insert_thms [] thms_names = thms_names
    1.13    | insert_thms ((thm,name)::thms_names) thms_names' =
    1.14 @@ -596,6 +596,7 @@
    1.15      then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
    1.16      else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities);
    1.17  
    1.18 +(*Called by the oracle-based methods declared in res_atp_methods.ML*)
    1.19  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
    1.20      let val conj_cls = make_clauses conjectures 
    1.21  	val hyp_cls = cnf_hyps_thms ctxt
    1.22 @@ -604,18 +605,20 @@
    1.23  	val rm_black_cls = blacklist_filter included_thms 
    1.24  	val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
    1.25  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
    1.26 -	val axclauses_as_thms = get_relevant_clauses ctxt cla_simp_atp_clauses user_cls (map prop_of goal_cls)
    1.27 +	val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses
    1.28 +	                            user_cls (map prop_of goal_cls)
    1.29  	val thy = ProofContext.theory_of ctxt
    1.30 -	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
    1.31 -				    | Fol => FOL
    1.32 -				    | Hol => HOL
    1.33 +	val prob_logic = case mode of 
    1.34 +                            Auto => problem_logic_goals [map prop_of goal_cls]
    1.35 +			  | Fol => FOL
    1.36 +			  | Hol => HOL
    1.37  	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
    1.38  	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.39  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.40          val writer = if dfg then dfg_writer else tptp_writer 
    1.41  	val file = atp_input_file()
    1.42      in
    1.43 -	(writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
    1.44 +	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses);
    1.45  	 Output.debug ("Writing to " ^ file);
    1.46  	 file)
    1.47      end;
    1.48 @@ -690,35 +693,39 @@
    1.49      Watcher.callResProvers(childout,atp_list);
    1.50      Output.debug "Sent commands to watcher!"
    1.51    end
    1.52 +  
    1.53 +fun trace_array fname =
    1.54 +  let val path = File.tmp_path (Path.basic fname)
    1.55 +  in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
    1.56  
    1.57 -(*We write out problem files for each subgoal. Argument pf generates filenames,
    1.58 +(*We write out problem files for each subgoal. Argument probfile generates filenames,
    1.59    and allows the suppression of the suffix "_1" in problem-generation mode.
    1.60    FIXME: does not cope with &&, and it isn't easy because one could have multiple
    1.61    subgoals, each involving &&.*)
    1.62 -fun write_problem_files pf (ctxt,th)  =
    1.63 +fun write_problem_files probfile (ctxt,th)  =
    1.64    let val goals = Thm.prems_of th
    1.65        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    1.66        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
    1.67        val rm_blacklist_cls = blacklist_filter included_thms
    1.68        val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
    1.69        val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals 
    1.70 -      val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
    1.71 -                     Int.toString (length axclauses))
    1.72 +      val _ = Output.debug ("total clauses from thms = " ^ Int.toString (length axclauses))
    1.73        val thy = ProofContext.theory_of ctxt
    1.74        fun get_neg_subgoals n =
    1.75  	  if n=0 then []
    1.76  	  else
    1.77 -	      let val st = Seq.hd (EVERY'
    1.78 -				       [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
    1.79 +	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
    1.80 +	                                   skolemize_tac] n th)
    1.81  		  val negs = Option.valOf (metahyps_thms n st)
    1.82  		  val negs_clauses = make_clauses negs
    1.83  	      in
    1.84 -		  negs_clauses::(get_neg_subgoals (n - 1))
    1.85 +		  negs_clauses :: get_neg_subgoals (n-1)
    1.86  	      end
    1.87        val neg_subgoals = get_neg_subgoals (length goals) 
    1.88 -      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
    1.89 -						 | Fol => FOL
    1.90 -						 | Hol => HOL
    1.91 +      val goals_logic = case !linkup_logic_mode of
    1.92 +                            Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
    1.93 +			  | Fol => FOL
    1.94 +			  | Hol => HOL
    1.95        val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
    1.96        val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.97        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.98 @@ -726,11 +733,15 @@
    1.99        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   1.100        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   1.101        fun write_all [] _ = []
   1.102 -	| write_all (subgoal::subgoals) k =
   1.103 -	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
   1.104 -      val thm_names = Array.fromList (map (#1 o #2) axclauses)
   1.105 +	| write_all (sub::subgoals) k =
   1.106 +	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses),
   1.107 +	    probfile k) :: write_all subgoals (k-1)
   1.108 +      val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals))
   1.109 +      val thm_names = Array.fromList clnames
   1.110 +      val _ = if !Output.show_debug_msgs 
   1.111 +              then trace_array "thm_names" thm_names else ()
   1.112    in
   1.113 -      (write_all neg_subgoals (length goals), thm_names)
   1.114 +      (filenames, thm_names)
   1.115    end;
   1.116  
   1.117  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   1.118 @@ -766,9 +777,9 @@
   1.119        (fn (ctxt,th) =>
   1.120         if Thm.no_prems th then ()
   1.121         else 
   1.122 -         let val pf = if Thm.nprems_of th = 1 then probfile_nosuffix 
   1.123 -         	      else prob_pathname
   1.124 -         in ignore (write_problem_files pf (ctxt,th)) end);
   1.125 +         let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   1.126 +          	            else prob_pathname
   1.127 +         in ignore (write_problem_files probfile (ctxt,th)) end);
   1.128  
   1.129  
   1.130  (** the Isar toplevel hook **)