Merged HOL and FOL clauses and combined some functions.
authormengj
Wed Mar 01 06:05:25 2006 +0100 (2006-03-01)
changeset 19160c1b3aa0a6827
parent 19159 f737ecbad1c4
child 19161 b395f586633f
Merged HOL and FOL clauses and combined some functions.
src/HOL/Tools/res_atp_setup.ML
     1.1 --- a/src/HOL/Tools/res_atp_setup.ML	Wed Mar 01 05:56:53 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp_setup.ML	Wed Mar 01 06:05:25 2006 +0100
     1.3 @@ -151,6 +151,11 @@
     1.4    | string_of_logic HOLC = "HOLC"
     1.5    | string_of_logic HOLCS = "HOLCS";
     1.6  
     1.7 +
     1.8 +fun is_fol_logic FOL = true
     1.9 +  | is_fol_logic  _ = false
    1.10 +
    1.11 +
    1.12  (*HOLCS will not occur here*)
    1.13  fun upgrade_lg HOLC _ = HOLC
    1.14    | upgrade_lg HOL HOLC = HOLC
    1.15 @@ -263,7 +268,30 @@
    1.16  	lg5
    1.17      end;
    1.18  
    1.19 +(***************************************************************)
    1.20 +(* Clauses used by FOL ATPs                                    *)
    1.21 +(***************************************************************)
    1.22  
    1.23 +datatype clause = FOLClause of ResClause.clause 
    1.24 +		| HOLClause of ResHolClause.clause
    1.25 +
    1.26 +
    1.27 +fun isTaut (FOLClause cls) = ResClause.isTaut cls
    1.28 +  | isTaut (HOLClause cls) = ResHolClause.isTaut cls
    1.29 +
    1.30 +
    1.31 +fun clause2tptp (FOLClause cls) = ResClause.clause2tptp cls
    1.32 +  | clause2tptp (HOLClause cls) = ResHolClause.clause2tptp cls
    1.33 +
    1.34 +
    1.35 +fun make_clause_fol cls = FOLClause cls
    1.36 +
    1.37 +fun make_clause_hol cls = HOLClause cls
    1.38 +
    1.39 +fun make_conjecture_clauses is_fol terms =
    1.40 +    if is_fol then map make_clause_fol (ResClause.make_conjecture_clauses terms)
    1.41 +    else
    1.42 +	map make_clause_hol (ResHolClause.make_conjecture_clauses terms)
    1.43  
    1.44  (***************************************************************)
    1.45  (* prover-specific output format:                              *)
    1.46 @@ -289,42 +317,35 @@
    1.47      end;
    1.48  
    1.49  (**** clausification ****)
    1.50 -fun cls_axiom_fol _ _ [] = []
    1.51 -  | cls_axiom_fol name i (tm::tms) =
    1.52 -      case ResClause.make_axiom_clause tm (name,i) of 
    1.53 -          SOME cls => cls :: cls_axiom_fol name (i+1) tms
    1.54 -        | NONE => cls_axiom_fol name i tms;
    1.55  
    1.56 -fun cls_axiom_hol  _ _ [] = []
    1.57 -  | cls_axiom_hol name i (tm::tms) =
    1.58 -   (ResHolClause.make_axiom_clause tm (name,i)) :: (cls_axiom_hol name (i+1) tms);
    1.59 +fun cls_axiom _ _ _ [] = []
    1.60 +  | cls_axiom is_fol name i (tm::tms) =
    1.61 +    if is_fol then 
    1.62 +	(case ResClause.make_axiom_clause tm (name,i) of 
    1.63 +             SOME cls => (FOLClause cls) :: cls_axiom true  name (i+1) tms
    1.64 +           | NONE => cls_axiom true name i tms)
    1.65 +    else
    1.66 +	(HOLClause (ResHolClause.make_axiom_clause tm (name,i))) :: (cls_axiom false name (i+1) tms);
    1.67  
    1.68  
    1.69 -fun filtered_tptp_axiom_fol name clss =
    1.70 -    (fst(ListPair.unzip (map ResClause.clause2tptp (filter (fn c => not (ResClause.isTaut c)) (cls_axiom_fol name 0 clss)))),[])
    1.71 +fun filtered_tptp_axiom is_fol name clss =
    1.72 +    (fst(ListPair.unzip (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))),[])
    1.73      handle _ => ([],[name]);
    1.74  
    1.75 -fun filtered_tptp_axiom_hol name clss =
    1.76 -    (fst(ListPair.unzip (map ResHolClause.clause2tptp (filter (fn c => not (ResHolClause.isTaut c)) (cls_axiom_hol name 0 clss)))),[])
    1.77 -    handle _ => ([],[name]);
    1.78 -
    1.79 -fun tptp_axioms_g filt_ax_fn [] err = ([],err)
    1.80 -  | tptp_axioms_g filt_ax_fn ((name,clss)::nclss) err =
    1.81 -    let val (nclss1,err1) = tptp_axioms_g filt_ax_fn nclss err
    1.82 -	val (clsstrs,err_name_list) = filt_ax_fn name clss
    1.83 +fun tptp_axioms_aux _ [] err = ([],err)
    1.84 +  | tptp_axioms_aux is_fol ((name,clss)::nclss) err =
    1.85 +    let val (nclss1,err1) = tptp_axioms_aux is_fol nclss err
    1.86 +	val (clsstrs,err_name_list) = filtered_tptp_axiom is_fol name clss
    1.87      in
    1.88  	case clsstrs of [] => (nclss1,err_name_list @ err1) 
    1.89  		      | _ => (clsstrs::nclss1,err1)
    1.90      end;
    1.91 -		
    1.92 -fun tptp_axioms_fol rules = tptp_axioms_g filtered_tptp_axiom_fol rules [];
    1.93  
    1.94 -fun tptp_axioms_hol rules = tptp_axioms_g filtered_tptp_axiom_hol rules [];
    1.95 +fun tptp_axioms is_fol rules = tptp_axioms_aux is_fol rules [];
    1.96  
    1.97 -
    1.98 -fun atp_axioms_g tptp_ax_fn rules file =
    1.99 +fun atp_axioms is_fol rules file = 
   1.100      let val out = TextIO.openOut file
   1.101 -	val (clss,errs) = tptp_ax_fn rules
   1.102 +	val (clss,errs) = tptp_axioms is_fol rules
   1.103  	val clss' = ResClause.union_all clss
   1.104      in
   1.105  	ResClause.writeln_strs out clss';
   1.106 @@ -333,27 +354,16 @@
   1.107      end;
   1.108  
   1.109  
   1.110 -fun atp_axioms_fol rules file = atp_axioms_g tptp_axioms_fol rules file;
   1.111 -
   1.112 -fun atp_axioms_hol rules file = atp_axioms_g tptp_axioms_hol rules file;
   1.113 +fun filtered_tptp_conjectures is_fol terms =
   1.114 +    let val clss = make_conjecture_clauses is_fol terms
   1.115 +	val clss' = filter (fn c => not (isTaut c)) clss
   1.116 +    in
   1.117 +	ListPair.unzip (map clause2tptp clss')
   1.118 +    end;
   1.119  
   1.120  
   1.121 -fun filtered_tptp_conjectures_fol terms =
   1.122 -    let val clss = ResClause.make_conjecture_clauses terms
   1.123 -	val clss' = filter (fn c => not (ResClause.isTaut c)) clss
   1.124 -    in
   1.125 -	ListPair.unzip (map ResClause.clause2tptp clss')
   1.126 -    end;
   1.127 -
   1.128 -fun filtered_tptp_conjectures_hol terms =
   1.129 -    let val clss = ResHolClause.make_conjecture_clauses terms
   1.130 -	val clss' = filter (fn c => not (ResHolClause.isTaut c)) clss
   1.131 -    in
   1.132 -	ListPair.unzip (map ResHolClause.clause2tptp clss')
   1.133 -    end;
   1.134 -
   1.135 -fun atp_conjectures_h_g filt_conj_fn hyp_cls =
   1.136 -    let val (tptp_h_clss,tfree_litss) = filt_conj_fn hyp_cls
   1.137 +fun atp_conjectures_h is_fol hyp_cls =
   1.138 +    let val (tptp_h_clss,tfree_litss) = filtered_tptp_conjectures is_fol hyp_cls
   1.139  	val tfree_lits = ResClause.union_all tfree_litss
   1.140  	val tfree_clss = map ResClause.tptp_tfree_clause tfree_lits 
   1.141  	val hypsfile = hyps_file ()
   1.142 @@ -364,12 +374,9 @@
   1.143          ([hypsfile],tfree_lits)
   1.144      end;
   1.145  
   1.146 -fun atp_conjectures_h_fol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_fol hyp_cls;
   1.147  
   1.148 -fun atp_conjectures_h_hol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_hol hyp_cls;
   1.149 -
   1.150 -fun atp_conjectures_c_g filt_conj_fn conj_cls n tfrees =
   1.151 -    let val (tptp_c_clss,tfree_litss) = filt_conj_fn conj_cls
   1.152 +fun atp_conjectures_c is_fol conj_cls n tfrees =
   1.153 +    let val (tptp_c_clss,tfree_litss) = filtered_tptp_conjectures is_fol conj_cls
   1.154  	val tfree_clss = map ResClause.tptp_tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
   1.155  	val probfile = prob_file n
   1.156  	val out = TextIO.openOut(probfile)		 	
   1.157 @@ -380,27 +387,19 @@
   1.158  	probfile 
   1.159      end;
   1.160  
   1.161 -fun atp_conjectures_c_fol conj_cls n tfrees = atp_conjectures_c_g filtered_tptp_conjectures_fol conj_cls n tfrees;
   1.162  
   1.163 -fun atp_conjectures_c_hol conj_cls n tfrees = atp_conjectures_c_g filtered_tptp_conjectures_hol conj_cls n tfrees;
   1.164 -
   1.165 -
   1.166 -fun atp_conjectures_g atp_conj_h_fn atp_conj_c_fn [] conj_cls n =
   1.167 -    let val probfile = atp_conj_c_fn conj_cls n []
   1.168 +fun atp_conjectures is_fol [] conj_cls n =
   1.169 +    let val probfile = atp_conjectures_c is_fol conj_cls n []
   1.170      in
   1.171  	[probfile]
   1.172      end
   1.173 -  | atp_conjectures_g atp_conj_h_fn atp_conj_c_fn hyp_cls conj_cls n =
   1.174 -    let val (hypsfile,tfree_lits) = atp_conj_h_fn hyp_cls
   1.175 -	val probfile = atp_conj_c_fn conj_cls n tfree_lits
   1.176 +  | atp_conjectures is_fol hyp_cls conj_cls n =
   1.177 +    let val (hypsfile,tfree_lits) = atp_conjectures_h is_fol hyp_cls
   1.178 +	val probfile = atp_conjectures_c is_fol conj_cls n tfree_lits
   1.179      in
   1.180  	(probfile::hypsfile)
   1.181      end;
   1.182  
   1.183 -fun atp_conjectures_fol hyp_cls conj_cls n = atp_conjectures_g atp_conjectures_h_fol atp_conjectures_c_fol hyp_cls conj_cls n;
   1.184 -
   1.185 -fun atp_conjectures_hol hyp_cls conj_cls n = atp_conjectures_g atp_conjectures_h_hol atp_conjectures_c_hol hyp_cls conj_cls n;
   1.186 -
   1.187  
   1.188  (**** types and sorts ****)
   1.189  fun tptp_types_sorts thy = 
   1.190 @@ -427,11 +426,12 @@
   1.191  
   1.192  datatype mode = Auto | Fol | Hol;
   1.193  
   1.194 -fun write_out_g logic atp_ax_fn atp_conj_fn (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
   1.195 -    let val (files1,err1) = if (null claR) then ([],[]) else (atp_ax_fn claR (claset_file()))
   1.196 -	val (files2,err2) = if (null simpR) then ([],[]) else (atp_ax_fn simpR (simpset_file ()))
   1.197 -	val (files3,err3) = if (null userR) then ([],[]) else (atp_ax_fn userR (local_lemma_file ()))
   1.198 -	val files4 = atp_conj_fn hyp_cls conj_cls n
   1.199 +fun write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
   1.200 +    let val is_fol = is_fol_logic logic
   1.201 +	val (files1,err1) = if (null claR) then ([],[]) else (atp_axioms is_fol claR (claset_file()))
   1.202 +	val (files2,err2) = if (null simpR) then ([],[]) else (atp_axioms is_fol simpR (simpset_file ()))
   1.203 +	val (files3,err3) = if (null userR) then ([],[]) else (atp_axioms is_fol userR (local_lemma_file ()))
   1.204 +	val files4 = atp_conjectures is_fol hyp_cls conj_cls n
   1.205  	val errs = err1 @ err2 @ err3 @ err
   1.206  	val logic' = if !include_combS then HOLCS 
   1.207  		     else 
   1.208 @@ -445,24 +445,15 @@
   1.209  	(helpers,files4 @ files1 @ files2 @ files3)
   1.210      end;
   1.211  
   1.212 -fun write_out_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err) = write_out_g FOL atp_axioms_fol atp_conjectures_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err);
   1.213  
   1.214 -fun write_out_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err) = write_out_g HOL atp_axioms_hol atp_conjectures_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err);
   1.215 -
   1.216 -fun write_out_fol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =  
   1.217 -    let val ts_file = if (!fol_keep_types) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
   1.218 -	val (helpers,files) = write_out_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err) 
   1.219 +fun write_out_ts is_fol ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
   1.220 +    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 []
   1.221 +	val logic = if is_fol then FOL else HOL
   1.222 +	val (helpers,files) = write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err)
   1.223      in
   1.224 -	(helpers,files@ts_file)
   1.225 +	(helpers,files)
   1.226      end;
   1.227 -
   1.228 -fun write_out_hol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =  
   1.229 -    let val ts_file = if (is_typed_hol()) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
   1.230 -	val (helpers,files) = write_out_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err)
   1.231 -    in
   1.232 -	(helpers,files@ts_file)
   1.233 -    end;
   1.234 -
   1.235 + 
   1.236  
   1.237  fun prep_atp_input mode ctxt conjectures user_thms n =
   1.238      let val conj_cls = map prop_of (make_clauses conjectures) 
   1.239 @@ -472,8 +463,8 @@
   1.240  			       | Fol => FOL
   1.241  			       | Hol => HOL
   1.242      in
   1.243 -	case logic of FOL => write_out_fol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
   1.244 -		    | _ => write_out_hol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
   1.245 +	case logic of FOL => write_out_ts true ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
   1.246 +		    | _ => write_out_ts false ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
   1.247  			   
   1.248      end;
   1.249