Added new functions to handle HOL goals and lemmas.
authormengj
Fri Oct 28 02:27:19 2005 +0200 (2005-10-28)
changeset 180016ca14bec7cd5
parent 18000 ac059afd6b86
child 18002 35ec4681d38f
Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.
src/HOL/Tools/res_atp_setup.ML
     1.1 --- a/src/HOL/Tools/res_atp_setup.ML	Fri Oct 28 02:25:57 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp_setup.ML	Fri Oct 28 02:27:19 2005 +0200
     1.3 @@ -11,10 +11,6 @@
     1.4  val filter_ax = ref false;
     1.5  
     1.6  
     1.7 -fun writeln_strs _   []      = ()
     1.8 -  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
     1.9 -
    1.10 -
    1.11  fun warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm));
    1.12  
    1.13  fun warning_thms_n n thms nm =
    1.14 @@ -36,7 +32,7 @@
    1.15  val prob_file = File.tmp_path (Path.basic "prob");
    1.16  val hyps_file = File.tmp_path (Path.basic "hyps");
    1.17  
    1.18 -
    1.19 +val types_sorts_file =  File.tmp_path (Path.basic "typsorts");
    1.20  
    1.21  (*******************************************************)
    1.22  (* operations on Isabelle theorems:                    *)
    1.23 @@ -45,14 +41,8 @@
    1.24  (* CNF                                                 *)
    1.25  (*******************************************************)
    1.26  
    1.27 -fun repeat_RS thm1 thm2 =
    1.28 -    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    1.29 -    in
    1.30 -        if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    1.31 -    end;
    1.32 -
    1.33  (* a special version of repeat_RS *)
    1.34 -fun repeat_someI_ex thm = repeat_RS thm someI_ex;
    1.35 +fun repeat_someI_ex thm = ResAxioms.repeat_RS thm someI_ex;
    1.36  
    1.37  val include_simpset = ref false;
    1.38  val include_claset = ref false; 
    1.39 @@ -101,14 +91,22 @@
    1.40  (***************** TPTP format *********************************)
    1.41  
    1.42  (* convert each (sub)goal clause (Thm.thm) into one or more TPTP clauses.  The additional TPTP clauses are tfree_lits.  Write the output TPTP clauses to a problem file *)
    1.43 -fun tptp_form thms n tfrees =
    1.44 -    let val clss = ResClause.make_conjecture_clauses (map prop_of thms)
    1.45 -	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.46 +
    1.47 +fun mk_conjectures is_fol terms =
    1.48 +    if is_fol then
    1.49 +	ListPair.unzip (map ResClause.clause2tptp (ResClause.make_conjecture_clauses terms))
    1.50 +    else
    1.51 +	ListPair.unzip (map ResHolClause.clause2tptp (ResHolClause.make_conjecture_clauses terms));
    1.52 +
    1.53 +
    1.54 +fun tptp_form_g is_fol thms n tfrees =
    1.55 +    let val terms = map prop_of thms
    1.56 +	val (tptp_clss,tfree_litss) = mk_conjectures is_fol terms
    1.57  	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
    1.58  	val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
    1.59  	val out = TextIO.openOut(probfile)		 	
    1.60      in
    1.61 -	writeln_strs out (tfree_clss @ tptp_clss);
    1.62 +	ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
    1.63  	TextIO.closeOut out;
    1.64  	warning probfile; (* show the location for debugging *)
    1.65  	probfile (* return the location *)
    1.66 @@ -116,25 +114,31 @@
    1.67      end;
    1.68  
    1.69  
    1.70 -fun tptp_hyps [] = ([], [])
    1.71 -  | tptp_hyps thms =
    1.72 -    let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
    1.73 +val tptp_form = tptp_form_g true;
    1.74 +val tptp_formH = tptp_form_g false;
    1.75 +
    1.76 +fun tptp_hyps_g _ [] = ([], [])
    1.77 +  | tptp_hyps_g is_fol thms =
    1.78 +    let val mk_nnf = if is_fol then make_nnf else make_nnf1
    1.79 +	val prems = map (skolemize o mk_nnf o ObjectLogic.atomize_thm) thms
    1.80          val prems' = map repeat_someI_ex prems
    1.81          val prems'' = make_clauses prems'
    1.82          val prems''' = ResAxioms.rm_Eps [] prems''
    1.83 -        val clss = ResClause.make_conjecture_clauses prems'''
    1.84 -	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
    1.85 +	val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'''
    1.86  	val tfree_lits = ResClause.union_all tfree_litss
    1.87  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    1.88          val hypsfile = File.platform_path hyps_file
    1.89          val out = TextIO.openOut(hypsfile)
    1.90      in
    1.91 -        writeln_strs out (tfree_clss @ tptp_clss);
    1.92 +        ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
    1.93          TextIO.closeOut out; warning hypsfile;
    1.94          ([hypsfile],tfree_lits)
    1.95      end;
    1.96   
    1.97  
    1.98 +val tptp_hyps = tptp_hyps_g true;
    1.99 +val tptp_hypsH = tptp_hyps_g false;
   1.100 +
   1.101  fun subtract_simpset thy ctxt =
   1.102    let
   1.103      val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
   1.104 @@ -148,33 +152,52 @@
   1.105      val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
   1.106    in map ResAxioms.pairname (subtract netI1 netI2 @ subtract netE1 netE2) end;
   1.107  
   1.108 +
   1.109 +fun mk_axioms is_fol rules =
   1.110 +    if is_fol then 
   1.111 +	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
   1.112 +	     val (clss',names) = ListPair.unzip clss
   1.113 +	     val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
   1.114 +	 in tptpclss end)
   1.115 +    else
   1.116 +	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairsH rules)
   1.117 +	     val (clss',names) = ListPair.unzip clss
   1.118 +	     val (tptpclss,_) = ListPair.unzip(map ResHolClause.clause2tptp clss')
   1.119 +	 in tptpclss end)
   1.120 +
   1.121 +
   1.122  local
   1.123  
   1.124 -fun write_rules [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
   1.125 -  | write_rules rules file =
   1.126 +fun write_rules_g is_fol [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
   1.127 +  | write_rules_g is_fol rules file =
   1.128      let val out = TextIO.openOut(file)
   1.129 -	val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
   1.130 -	val (clss',names) = ListPair.unzip clss
   1.131 -	val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
   1.132 +	val tptpclss = mk_axioms is_fol rules
   1.133      in
   1.134 -	writeln_strs out tptpclss;
   1.135 +	ResAtp.writeln_strs out tptpclss;
   1.136  	TextIO.closeOut out; warning file;
   1.137  	[file]
   1.138      end;
   1.139  
   1.140 +
   1.141 +val write_rules = write_rules_g true;
   1.142 +val write_rulesH = write_rules_g false;
   1.143 +
   1.144  in
   1.145  
   1.146  (* TPTP Isabelle theorems *)
   1.147 -fun tptp_cnf_rules (clasetR,simpsetR) =
   1.148 +fun tptp_cnf_rules_g write_rules (clasetR,simpsetR) =
   1.149      let val simpfile = File.platform_path simpset_file
   1.150  	val clafile =  File.platform_path claset_file
   1.151      in
   1.152  	(write_rules clasetR clafile) @ (write_rules simpsetR simpfile)
   1.153      end;
   1.154  
   1.155 +val tptp_cnf_rules = tptp_cnf_rules_g write_rules;
   1.156 +val tptp_cnf_rulesH = tptp_cnf_rules_g write_rulesH;
   1.157 +
   1.158  end
   1.159  
   1.160 -fun tptp_cnf_clasimp ctxt (include_claset,include_simpset) =
   1.161 +fun tptp_cnf_clasimp_g tptp_cnf_rules ctxt (include_claset,include_simpset) =
   1.162      let val local_claR = if include_claset then get_local_claR ctxt else (subtract_claset (ProofContext.theory_of ctxt) ctxt)
   1.163  	val local_simpR = if include_simpset then get_local_simpR ctxt else (subtract_simpset (ProofContext.theory_of ctxt) ctxt)
   1.164  
   1.165 @@ -183,36 +206,73 @@
   1.166      end;
   1.167  
   1.168  
   1.169 +val tptp_cnf_clasimp = tptp_cnf_clasimp_g tptp_cnf_rules;
   1.170 +val tptp_cnf_clasimpH = tptp_cnf_clasimp_g tptp_cnf_rulesH;
   1.171 +
   1.172 +
   1.173 +fun tptp_types_sorts thy = 
   1.174 +    let val classrel_clauses = ResClause.classrel_clauses_thy thy
   1.175 +	val arity_clauses = ResClause.arity_clause_thy thy
   1.176 +	val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
   1.177 +	val arity_cls = map ResClause.tptp_arity_clause arity_clauses
   1.178 +	fun write_ts () =
   1.179 +	    let val tsfile = File.platform_path types_sorts_file
   1.180 +		val out = TextIO.openOut(tsfile)
   1.181 +	    in
   1.182 +		ResAtp.writeln_strs out (classrel_cls @ arity_cls);
   1.183 +		TextIO.closeOut out;
   1.184 +		[tsfile]
   1.185 +	    end
   1.186 +    in
   1.187 +	if (List.null arity_cls andalso List.null classrel_cls) then []
   1.188 +	else
   1.189 +	    write_ts ()
   1.190 +    end;
   1.191 +
   1.192 +
   1.193 +
   1.194  (*FIXME: a function that does not perform any filtering now *)
   1.195  fun find_relevant_ax ctxt = tptp_cnf_clasimp ctxt (true,true);
   1.196  
   1.197  
   1.198 -
   1.199  (***************************************************************)
   1.200  (* setup ATPs as Isabelle methods                               *)
   1.201  (***************************************************************)
   1.202 -fun atp_meth' tac prems ctxt = 
   1.203 +fun atp_meth_g tptp_hyps tptp_cnf_clasimp tac prems ctxt = 
   1.204      let val rules = if !filter_ax then find_relevant_ax ctxt 
   1.205  		    else tptp_cnf_clasimp ctxt (!include_claset, !include_simpset) 
   1.206  	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
   1.207 -	val files = hyps @ rules
   1.208 +	val thy = ProofContext.theory_of ctxt
   1.209 +	val tsfile = tptp_types_sorts thy
   1.210 +	val files = hyps @ rules @ tsfile
   1.211      in
   1.212  	Method.METHOD (fn facts =>
   1.213  			  if !debug then (warning_thms_n (length facts) facts "facts";HEADGOAL (tac ctxt files tfrees)) 
   1.214  			  else HEADGOAL (tac ctxt files tfrees))
   1.215      end;
   1.216  
   1.217 +val atp_meth_f = atp_meth_g tptp_hyps tptp_cnf_clasimp;
   1.218  
   1.219 -fun atp_meth tac prems ctxt =
   1.220 +val atp_meth_h = atp_meth_g tptp_hypsH tptp_cnf_clasimpH;
   1.221 +
   1.222 +
   1.223 +fun atp_meth_G atp_meth tac prems ctxt =
   1.224      let val _ = ResClause.init (ProofContext.theory_of ctxt)
   1.225      in    
   1.226 -	if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth' tac prems ctxt)
   1.227 -	else (atp_meth' tac prems ctxt)
   1.228 +	if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth tac prems ctxt)
   1.229 +	else (atp_meth tac prems ctxt)
   1.230      end;
   1.231  	
   1.232 -val atp_method = Method.bang_sectioned_args rules_modifiers o atp_meth;
   1.233 +
   1.234 +val atp_meth_H = atp_meth_G atp_meth_h;
   1.235 +
   1.236 +val atp_meth_F = atp_meth_G atp_meth_f;
   1.237  
   1.238  
   1.239 +val atp_method_H = Method.bang_sectioned_args rules_modifiers o atp_meth_H;
   1.240 +
   1.241 +val atp_method_F = Method.bang_sectioned_args rules_modifiers o atp_meth_F;
   1.242 +
   1.243  
   1.244  
   1.245  (*************Remove tmp files********************************)