src/HOL/Tools/res_atp_setup.ML
author wenzelm
Thu Aug 03 17:30:36 2006 +0200 (2006-08-03)
changeset 20328 5b240a4216b0
parent 19446 30e1178d7a3b
child 20854 f9cf9e62d11c
permissions -rw-r--r--
RuleInsts.bires_inst_tac;
     1 (* ID: $Id$ 
     2    Author: Jia Meng, NICTA
     3 
     4 *)
     5 structure ResAtpSetup =
     6 
     7 struct
     8 
     9 val keep_atp_input = ref false;
    10 val debug = ref true;
    11 
    12 val fol_keep_types = ResClause.keep_types;
    13 
    14 (* use them to set and find type levels of HOL clauses *)
    15 val hol_full_types = ResHolClause.full_types;
    16 val hol_partial_types = ResHolClause.partial_types;
    17 val hol_const_types_only = ResHolClause.const_types_only;
    18 val hol_no_types = ResHolClause.no_types;
    19 fun hol_typ_level () = ResHolClause.find_typ_level ();
    20 
    21 fun is_typed_hol () = 
    22     let val tp_level = hol_typ_level()
    23     in
    24 	not (tp_level = ResHolClause.T_NONE)
    25     end;
    26 
    27 val include_combS = ResHolClause.include_combS;
    28 val include_min_comb = ResHolClause.include_min_comb;
    29 
    30 
    31 
    32 (*******************************************************)
    33 (* set up the output paths                             *)
    34 (*******************************************************)
    35 fun full_typed_comb () =
    36     if !ResHolClause.include_combS then 
    37 	(ResAtp.helper_path "E_HOME" "additionals/full_comb_inclS"
    38 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS")
    39     else 
    40 	(ResAtp.helper_path "E_HOME" "additionals/full_comb_noS"
    41 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/full_comb_noS");
    42 
    43 fun partial_typed_comb () = 
    44     if !ResHolClause.include_combS then 
    45 	(ResAtp.helper_path "E_HOME" "additionals/par_comb_inclS"
    46 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS")
    47     else 
    48 	(ResAtp.helper_path "E_HOME" "additionals/par_comb_noS"
    49 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/par_comb_noS");
    50 
    51 fun const_typed_comb () =
    52     if !ResHolClause.include_combS then 
    53 	(ResAtp.helper_path "E_HOME" "additionals/const_comb_inclS"
    54 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS")
    55     else 
    56 	(ResAtp.helper_path "E_HOME" "additionals/const_comb_noS"
    57 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/const_comb_noS");
    58 	
    59 fun untyped_comb () = 
    60     if !ResHolClause.include_combS then 
    61 	(ResAtp.helper_path "E_HOME" "additionals/u_comb_inclS"
    62 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS")
    63     else
    64 	(ResAtp.helper_path "E_HOME" "additionals/u_comb_noS"
    65 	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_noS");
    66 
    67 
    68 fun full_typed_HOL_helper1 () =
    69     ResAtp.helper_path "E_HOME" "additionals/full_helper1"
    70     handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/full_helper1";
    71 
    72 fun partial_typed_HOL_helper1 () = 
    73     ResAtp.helper_path "E_HOME" "additionals/par_helper1"
    74     handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/par_helper1";
    75 
    76 fun const_typed_HOL_helper1 () = 
    77     ResAtp.helper_path "E_HOME" "additionals/const_helper1"
    78     handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/const_helper1";
    79 
    80 
    81 fun untyped_HOL_helper1 () = 
    82     ResAtp.helper_path "E_HOME" "additionals/u_helper1"
    83     handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_helper1";
    84 
    85 
    86 fun HOL_helper1 () =
    87     let val tp_level = !ResHolClause.typ_level
    88     in
    89 	case tp_level of ResHolClause.T_PARTIAL => (warning "Partial type helper"; partial_typed_HOL_helper1 ())
    90 		       | ResHolClause.T_FULL => (warning "Full type helper"; full_typed_HOL_helper1 ())
    91 		       | ResHolClause.T_CONST => (warning "Const type helper"; const_typed_HOL_helper1 ())
    92 		       | ResHolClause.T_NONE => (warning "Untyped helper"; untyped_HOL_helper1 ())
    93     end;
    94 
    95 
    96 fun HOL_comb () =
    97     let val tp_level = !ResHolClause.typ_level
    98     in
    99 	case tp_level of ResHolClause.T_FULL => (warning "Full type comb"; full_typed_comb ())
   100 		       | ResHolClause.T_PARTIAL => (warning "Partial type comb"; partial_typed_comb ())
   101 		       | ResHolClause.T_CONST => (warning "Const type comb"; const_typed_comb ())
   102 		       | ResHolClause.T_NONE => (warning "Untyped comb"; untyped_comb ())
   103     end;
   104 
   105 
   106 fun atp_input_file file =
   107     let val file' = !ResAtp.problem_name ^ "_" ^ file
   108     in
   109 	if !ResAtp.destdir = "" then File.platform_path (File.tmp_path (Path.basic file'))
   110 	else if File.exists (File.unpack_platform_path (!ResAtp.destdir))
   111 	then !ResAtp.destdir ^ "/" ^ file'
   112 	else error ("No such directory: " ^ !ResAtp.destdir)
   113     end;
   114 
   115 fun claset_file () = atp_input_file "claset";
   116 fun simpset_file () = atp_input_file "simp";
   117 fun local_lemma_file () = atp_input_file "locallemmas";
   118 fun hyps_file () = atp_input_file "hyps";
   119 fun prob_file _ = atp_input_file "";
   120 
   121 fun types_sorts_file () = atp_input_file "typesorts";
   122 
   123 
   124 
   125 (*******************************************************)
   126 (* operations on Isabelle theorems:                    *)
   127 (* retrieving from ProofContext,                       *)
   128 (* modifying local theorems,                           *)
   129 (* CNF                                                 *)
   130 (*******************************************************)
   131 
   132 val include_simpset = ref false;
   133 val include_claset = ref false; 
   134 
   135 val add_simpset = (fn () => include_simpset:=true);
   136 val add_claset = (fn () => include_claset:=true);
   137 val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
   138 val rm_simpset = (fn () => include_simpset:=false);
   139 val rm_claset = (fn () => include_claset:=false);
   140 val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
   141 
   142 
   143 (******************************************************************)
   144 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   145 (******************************************************************)
   146 
   147 datatype logic = FOL | HOL | HOLC | HOLCS;
   148 
   149 fun string_of_logic FOL = "FOL"
   150   | string_of_logic HOL = "HOL"
   151   | string_of_logic HOLC = "HOLC"
   152   | string_of_logic HOLCS = "HOLCS";
   153 
   154 
   155 fun is_fol_logic FOL = true
   156   | is_fol_logic  _ = false
   157 
   158 
   159 (*HOLCS will not occur here*)
   160 fun upgrade_lg HOLC _ = HOLC
   161   | upgrade_lg HOL HOLC = HOLC
   162   | upgrade_lg HOL _ = HOL
   163   | upgrade_lg FOL lg = lg; 
   164 
   165 (* check types *)
   166 fun has_bool (Type("bool",_)) = true
   167   | has_bool (Type(_, Ts)) = exists has_bool Ts
   168   | has_bool _ = false;
   169 
   170 fun has_bool_arg tp = 
   171     let val (targs,tr) = strip_type tp
   172     in
   173 	exists has_bool targs
   174     end;
   175 
   176 fun is_fn_tp (Type("fun",_)) = true
   177   | is_fn_tp _ = false;
   178 
   179 
   180 exception FN_LG of term;
   181 
   182 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   183     if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   184   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   185     if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   186   | fn_lg (t as Var(f,tp)) (lg,seen) =
   187     if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
   188     else (lg,t ins seen)
   189   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
   190   | fn_lg f _ = raise FN_LG(f); 
   191 
   192 
   193 fun term_lg [] (lg,seen) = (lg,seen)
   194   | term_lg (tm::tms) (FOL,seen) =
   195     let val (f,args) = strip_comb tm
   196 	val (lg',seen') = if f mem seen then (FOL,seen) 
   197 			  else fn_lg f (FOL,seen)
   198 
   199 	 in
   200 	     term_lg (args@tms) (lg',seen')
   201     end
   202   | term_lg _ (lg,seen) = (lg,seen)
   203 
   204 exception PRED_LG of term;
   205 
   206 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   207     if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
   208   | pred_lg (t as Free(P,tp)) (lg,seen) =
   209     if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
   210   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
   211   | pred_lg P _ = raise PRED_LG(P);
   212 
   213 
   214 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   215   | lit_lg P (lg,seen) =
   216     let val (pred,args) = strip_comb P
   217 	val (lg',seen') = if pred mem seen then (lg,seen) 
   218 			  else pred_lg pred (lg,seen)
   219     in
   220 	term_lg args (lg',seen')
   221     end;
   222 
   223 fun lits_lg [] (lg,seen) = (lg,seen)
   224   | lits_lg (lit::lits) (FOL,seen) =
   225     lits_lg lits (lit_lg lit (FOL,seen))
   226   | lits_lg lits (lg,seen) = (lg,seen);
   227 
   228 
   229 fun logic_of_clause tm (lg,seen) =
   230     let val tm' = HOLogic.dest_Trueprop tm
   231 	val disjs = HOLogic.dest_disj tm'
   232     in
   233 	lits_lg disjs (lg,seen)
   234     end;
   235 
   236 fun lits_lg [] (lg,seen) = (lg,seen)
   237   | lits_lg (lit::lits) (FOL,seen) =
   238     lits_lg lits (lit_lg lit (FOL,seen))
   239   | lits_lg lits (lg,seen) = (lg,seen);
   240 
   241 
   242 fun logic_of_clause tm (lg,seen) =
   243     let val tm' = HOLogic.dest_Trueprop tm
   244 	val disjs = HOLogic.dest_disj tm'
   245     in
   246 	lits_lg disjs (lg,seen)
   247     end;
   248 
   249 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   250   | logic_of_clauses (cls::clss) (FOL,seen) =
   251     logic_of_clauses clss (logic_of_clause cls (FOL,seen))
   252   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   253 
   254 fun logic_of_nclauses [] (lg,seen) = (lg,seen)
   255   | logic_of_nclauses (cls::clss) (FOL,seen) =
   256     logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
   257   | logic_of_nclauses clss (lg,seen) = (lg,seen);
   258 
   259 
   260 
   261 fun problem_logic (conj_cls,hyp_cls,userR,claR,simpR) =
   262     let val (lg1,seen1) = logic_of_clauses conj_cls (FOL,[])
   263 	val (lg2,seen2) = logic_of_clauses hyp_cls (lg1,seen1)
   264 	val (lg3,seen3) = logic_of_nclauses userR (lg2,seen2)
   265 	val (lg4,seen4) = logic_of_nclauses claR (lg3,seen3)
   266 	val (lg5,seen5) = logic_of_nclauses simpR (lg4,seen4)
   267     in
   268 	lg5
   269     end;
   270 
   271 (***************************************************************)
   272 (* Clauses used by FOL ATPs                                    *)
   273 (***************************************************************)
   274 
   275 datatype clause = FOLClause of ResClause.clause 
   276 		| HOLClause of ResHolClause.clause
   277 
   278 
   279 fun isTaut (FOLClause cls) = ResClause.isTaut cls
   280   | isTaut (HOLClause cls) = ResHolClause.isTaut cls
   281 
   282 
   283 fun clause2tptp (FOLClause cls) = ResClause.clause2tptp cls
   284   | clause2tptp (HOLClause cls) = ResHolClause.clause2tptp cls
   285 
   286 
   287 fun make_clause_fol cls = FOLClause cls
   288 
   289 fun make_clause_hol cls = HOLClause cls
   290 
   291 fun make_conjecture_clauses is_fol terms =
   292     if is_fol then map make_clause_fol (ResClause.make_conjecture_clauses terms)
   293     else
   294 	map make_clause_hol (ResHolClause.make_conjecture_clauses terms)
   295 
   296 (***************************************************************)
   297 (* prover-specific output format:                              *)
   298 (* TPTP                                                        *)
   299 (***************************************************************)
   300 
   301 (**** CNF rules and hypothesis ****)
   302 fun cnf_rules_tms ctxt ths (include_claset,include_simpset) =
   303     let val local_claR = if include_claset then ResAxioms.claset_rules_of_ctxt ctxt else []
   304 	val (local_claR_cls,err1) = ResAxioms.cnf_rules2 local_claR []
   305 	val local_simpR = if include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt else []
   306 	val (local_simpR_cls,err2) = ResAxioms.cnf_rules2 local_simpR []
   307 	val (user_ths_cls,err3) = ResAxioms.cnf_rules2 (map ResAxioms.pairname ths) []
   308 	val errs = err3 @ err2 @ err1
   309     in
   310 	(user_ths_cls,local_simpR_cls,local_claR_cls,errs)
   311     end;
   312 
   313 fun cnf_hyps_thms ctxt = 
   314     let val ths = ProofContext.prems_of ctxt
   315     in
   316 	ResClause.union_all (map ResAxioms.skolem_thm ths)
   317     end;
   318 
   319 (**** clausification ****)
   320 
   321 fun cls_axiom _ _ _ [] = []
   322   | cls_axiom is_fol name i (tm::tms) =
   323     if is_fol then 
   324 	(case ResClause.make_axiom_clause tm (name,i) of 
   325              SOME cls => (FOLClause cls) :: cls_axiom true  name (i+1) tms
   326            | NONE => cls_axiom true name i tms)
   327     else
   328 	HOLClause (ResHolClause.make_axiom_clause tm (name,i)) :: 
   329 	cls_axiom false name (i+1) tms;
   330 
   331 
   332 fun filtered_tptp_axiom is_fol name clss =
   333   (fst
   334    (ListPair.unzip 
   335     (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))),
   336    [])   handle _ => ([],[name]);
   337 
   338 fun tptp_axioms_aux _ [] err = ([],err)
   339   | tptp_axioms_aux is_fol ((name,clss)::nclss) err =
   340     let val (nclss1,err1) = tptp_axioms_aux is_fol nclss err
   341 	val (clsstrs,err_name_list) = filtered_tptp_axiom is_fol name clss
   342     in
   343 	case clsstrs of [] => (nclss1,err_name_list @ err1) 
   344 		      | _ => (clsstrs::nclss1,err1)
   345     end;
   346 
   347 fun tptp_axioms is_fol rules = tptp_axioms_aux is_fol rules [];
   348 
   349 fun atp_axioms is_fol rules file = 
   350     let val out = TextIO.openOut file
   351 	val (clss,errs) = tptp_axioms is_fol rules
   352 	val clss' = ResClause.union_all clss
   353     in
   354 	ResClause.writeln_strs out clss';
   355 	TextIO.closeOut out;
   356 	([file],errs)
   357     end;
   358 
   359 
   360 fun filtered_tptp_conjectures is_fol terms =
   361     let val clss = make_conjecture_clauses is_fol terms
   362 	val clss' = filter (fn c => not (isTaut c)) clss
   363     in
   364 	ListPair.unzip (map clause2tptp clss')
   365     end;
   366 
   367 
   368 fun atp_conjectures_h is_fol hyp_cls =
   369     let val (tptp_h_clss,tfree_litss) = filtered_tptp_conjectures is_fol hyp_cls
   370 	val tfree_lits = ResClause.union_all tfree_litss
   371 	val tfree_clss = map ResClause.tptp_tfree_clause tfree_lits 
   372 	val hypsfile = hyps_file ()
   373         val out = TextIO.openOut(hypsfile)
   374     in
   375         ResClause.writeln_strs out (tfree_clss @ tptp_h_clss);
   376         TextIO.closeOut out; warning hypsfile;
   377         ([hypsfile],tfree_lits)
   378     end;
   379 
   380 
   381 fun atp_conjectures_c is_fol conj_cls n tfrees =
   382     let val (tptp_c_clss,tfree_litss) = filtered_tptp_conjectures is_fol conj_cls
   383 	val tfree_clss = map ResClause.tptp_tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
   384 	val probfile = prob_file n
   385 	val out = TextIO.openOut(probfile)		 	
   386     in
   387 	ResClause.writeln_strs out (tfree_clss @ tptp_c_clss);
   388 	TextIO.closeOut out;
   389 	warning probfile; 
   390 	probfile 
   391     end;
   392 
   393 
   394 fun atp_conjectures is_fol [] conj_cls n =
   395     let val probfile = atp_conjectures_c is_fol conj_cls n []
   396     in
   397 	[probfile]
   398     end
   399   | atp_conjectures is_fol hyp_cls conj_cls n =
   400     let val (hypsfile,tfree_lits) = atp_conjectures_h is_fol hyp_cls
   401 	val probfile = atp_conjectures_c is_fol conj_cls n tfree_lits
   402     in
   403 	(probfile::hypsfile)
   404     end;
   405 
   406 
   407 (**** types and sorts ****)
   408 fun tptp_types_sorts thy = 
   409     let val classrel_clauses = ResClause.classrel_clauses_thy thy
   410 	val arity_clauses = ResClause.arity_clause_thy thy
   411 	val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
   412 	val arity_cls = map ResClause.tptp_arity_clause arity_clauses
   413 	fun write_ts () =
   414 	    let val tsfile = types_sorts_file ()
   415 		val out = TextIO.openOut(tsfile)
   416 	    in
   417 		ResClause.writeln_strs out (classrel_cls @ arity_cls);
   418 		TextIO.closeOut out;
   419 		[tsfile]
   420 	    end
   421     in
   422 	if (List.null arity_cls andalso List.null classrel_cls) then []
   423 	else
   424 	    write_ts ()
   425     end;
   426 
   427 
   428 (******* write to files ******)
   429 
   430 datatype mode = Auto | Fol | Hol;
   431 
   432 fun write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
   433   let val is_fol = is_fol_logic logic
   434       val (files1,err1) = if (null claR) then ([],[]) 
   435                           else (atp_axioms is_fol claR (claset_file()))
   436       val (files2,err2) = if (null simpR) then ([],[]) 
   437                           else (atp_axioms is_fol simpR (simpset_file ()))
   438       val (files3,err3) = if (null userR) then ([],[]) 
   439                           else (atp_axioms is_fol userR (local_lemma_file ()))
   440       val files4 = atp_conjectures is_fol hyp_cls conj_cls n
   441       val errs = err1 @ err2 @ err3 @ err
   442       val logic' = if !include_combS then HOLCS 
   443 		   else 
   444 		       if !include_min_comb then HOLC else logic
   445       val _ = warning ("Problems are " ^ (string_of_logic logic'))
   446       val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
   447       val helpers = case logic' of FOL => []
   448 				 | HOL => [HOL_helper1 ()]
   449 				 | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
   450   in
   451       (helpers,files4 @ files1 @ files2 @ files3)
   452   end;
   453 
   454 
   455 fun write_out_ts is_fol ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
   456     let val ts_file = if ((is_fol andalso (!fol_keep_types)) orelse ((not is_fol) andalso (is_typed_hol ()))) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
   457 	val logic = if is_fol then FOL else HOL
   458 	val (helpers,files) = write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err)
   459     in
   460 	(helpers,files)
   461     end;
   462  
   463 
   464 fun prep_atp_input mode ctxt conjectures user_thms n =
   465     let val conj_cls = map prop_of (make_clauses conjectures) 
   466 	val (userR,simpR,claR,errs) = 
   467 	    cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset) 
   468 	val hyp_cls = map prop_of (cnf_hyps_thms ctxt) 
   469 	val logic = case mode of Auto => problem_logic (conj_cls,hyp_cls,userR,claR,simpR)
   470 			       | Fol => FOL
   471 			       | Hol => HOL
   472     in
   473 	case logic of FOL => write_out_ts true ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
   474 		    | _ => write_out_ts false ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
   475 			   
   476     end;
   477 
   478 
   479 (***************************************************************)
   480 (* setup ATPs as Isabelle methods                              *)
   481 (***************************************************************)
   482 
   483 
   484 fun atp_meth' tac ths ctxt = 
   485     Method.SIMPLE_METHOD' HEADGOAL
   486     (tac ctxt ths);
   487 
   488 fun atp_meth tac ths ctxt = 
   489     let val thy = ProofContext.theory_of ctxt
   490 	val _ = ResClause.init thy
   491 	val _ = ResHolClause.init thy
   492     in
   493 	atp_meth' tac ths ctxt
   494     end;
   495 
   496 
   497 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   498 
   499 
   500 (*************Remove tmp files********************************)
   501 fun rm_tmp_files1 [] = ()
   502   | rm_tmp_files1 (f::fs) =
   503     (OS.FileSys.remove f; rm_tmp_files1 fs);
   504 
   505 fun cond_rm_tmp files = 
   506     if !keep_atp_input then warning "ATP input kept..." 
   507     else if !ResAtp.destdir <> "" then warning ("ATP input kept in directory " ^ (!ResAtp.destdir))
   508     else (warning "deleting ATP inputs..."; rm_tmp_files1 files);
   509 
   510 end