Introduced combinators B', C' and S'.
authormengj
Wed Sep 20 13:54:03 2006 +0200 (2006-09-20 ago)
changeset 20644ff938c7b15e8
parent 20643 267f30cbe2cb
child 20645 5e28b8f2cb52
Introduced combinators B', C' and S'.
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Sep 20 13:53:03 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Sep 20 13:54:03 2006 +0200
     1.3 @@ -9,17 +9,41 @@
     1.4  
     1.5  struct
     1.6  
     1.7 +(* a flag to set if we use extra combinators B',C',S' *)
     1.8 +val use_combB'C'S' = ref true;
     1.9  
    1.10 -val include_combS = ref false;
    1.11 -val include_min_comb = ref false;
    1.12 +val combI_count = ref 0;
    1.13 +val combK_count = ref 0;
    1.14 +val combB_count = ref 0;
    1.15 +val combC_count = ref 0;
    1.16 +val combS_count = ref 0;
    1.17 +
    1.18 +val combB'_count = ref 0;
    1.19 +val combC'_count = ref 0;
    1.20 +val combS'_count = ref 0; 
    1.21 +
    1.22  
    1.23 -fun in_min_comb count_comb = if count_comb then include_min_comb:=true else ();
    1.24 - 
    1.25 -fun in_combS count_comb = if count_comb then include_combS:=true else (); 
    1.26 +fun increI count_comb =  if count_comb then combI_count := !combI_count + 1 else ();
    1.27 +fun increK count_comb =  if count_comb then combK_count := !combK_count + 1 else ();
    1.28 +fun increB count_comb =  if count_comb then combB_count := !combB_count + 1 else ();
    1.29 +fun increC count_comb =  if count_comb then combC_count := !combC_count + 1 else ();
    1.30 +fun increS count_comb =  if count_comb then combS_count := !combS_count + 1 else (); 
    1.31 +fun increB' count_comb =  if count_comb then combB'_count := !combB'_count + 1 else (); 
    1.32 +fun increC' count_comb =  if count_comb then combC'_count := !combC'_count + 1 else ();
    1.33 +fun increS' count_comb =  if count_comb then combS'_count := !combS'_count + 1 else (); 
    1.34 +
    1.35 +
    1.36 +exception DECRE_COMB of string;
    1.37 +fun decreB count_comb n = if count_comb then (if !combB_count >= n then combB_count := !combB_count - n else raise (DECRE_COMB "COMBB")) else ();
    1.38 +
    1.39 +fun decreC count_comb n = if count_comb then (if !combC_count >= n then combC_count := !combC_count - n else raise (DECRE_COMB "COMBC")) else ();
    1.40 +
    1.41 +fun decreS count_comb n = if count_comb then (if !combS_count >= n then combS_count := !combS_count - n else raise (DECRE_COMB "COMBS")) else ();
    1.42 +
    1.43  
    1.44  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.45  
    1.46 -fun init thy = (include_combS:=false; include_min_comb:=false;
    1.47 +fun init thy = (combI_count:=0; combK_count:=0;combB_count:=0;combC_count:=0;combS_count:=0;combB'_count:=0;combC'_count:=0;combS'_count:=0;
    1.48                  const_typargs := Sign.const_typargs thy);
    1.49  
    1.50  (**********************************************************************)
    1.51 @@ -46,9 +70,48 @@
    1.52  
    1.53  
    1.54  (*******************************************)
    1.55 +fun mk_compact_comb (tm as (Const("COMBB",_)$p) $ (Const("COMBB",_)$q$r)) Bnds count_comb =
    1.56 +    let val tp_p = Term.type_of1(Bnds,p)
    1.57 +	val tp_q = Term.type_of1(Bnds,q)
    1.58 +	val tp_r = Term.type_of1(Bnds,r)
    1.59 +	val typ = Term.type_of1(Bnds,tm)
    1.60 +	val typ_B' = [tp_p,tp_q,tp_r] ---> typ
    1.61 +	val _ = increB' count_comb
    1.62 +	val _ = decreB count_comb 2
    1.63 +    in
    1.64 +	Const("COMBB_e",typ_B') $ p $ q $ r
    1.65 +    end
    1.66 +  | mk_compact_comb (tm as (Const("COMBC",_) $ (Const("COMBB",_)$p$q) $ r)) Bnds count_comb =
    1.67 +    let val tp_p = Term.type_of1(Bnds,p)
    1.68 +	val tp_q = Term.type_of1(Bnds,q)
    1.69 +	val tp_r = Term.type_of1(Bnds,r)
    1.70 +	val typ = Term.type_of1(Bnds,tm)
    1.71 +	val typ_C' = [tp_p,tp_q,tp_r] ---> typ
    1.72 +	val _ = increC' count_comb
    1.73 +	val _ = decreC count_comb 1
    1.74 +	val _ = decreB count_comb 1
    1.75 +    in
    1.76 +	Const("COMBC_e",typ_C') $ p $ q $ r
    1.77 +    end
    1.78 +  | mk_compact_comb (tm as (Const("COMBS",_) $ (Const("COMBB",_)$p$q) $ r)) Bnds count_comb =
    1.79 +    let val tp_p = Term.type_of1(Bnds,p)
    1.80 +	val tp_q = Term.type_of1(Bnds,q)
    1.81 +	val tp_r = Term.type_of1(Bnds,r)
    1.82 +	val typ = Term.type_of1(Bnds,tm)
    1.83 +	val typ_S' = [tp_p,tp_q,tp_r] ---> typ
    1.84 +	val _ = increS' count_comb
    1.85 +	val _ = decreS count_comb 1
    1.86 +	val _ = decreB count_comb 1
    1.87 +    in
    1.88 +	Const("COMBS_e",typ_S') $ p $ q $ r
    1.89 +    end
    1.90 +  | mk_compact_comb tm _ _ = tm;
    1.91 +
    1.92 +fun compact_comb t Bnds count_comb = if !use_combB'C'S' then mk_compact_comb t Bnds count_comb else t;
    1.93 +
    1.94  fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = 
    1.95      let val tpI = Type("fun",[tp,tp])
    1.96 -	val _ = in_min_comb count_comb
    1.97 +	val _ = increI count_comb
    1.98      in 
    1.99  	Const("COMBI",tpI) 
   1.100      end
   1.101 @@ -56,25 +119,25 @@
   1.102      let val (Bound n') = decre_bndVar (Bound n)
   1.103  	val tb = List.nth(Bnds,n')
   1.104  	val tK = Type("fun",[tb,Type("fun",[tp,tb])])
   1.105 -	val _ = in_min_comb count_comb 
   1.106 +	val _ = increK count_comb 
   1.107      in
   1.108  	Const("COMBK",tK) $ (Bound n')
   1.109      end
   1.110    | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
   1.111      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
   1.112 -	val _ = in_min_comb count_comb 
   1.113 +	val _ = increK count_comb 
   1.114      in 
   1.115  	Const("COMBK",tK) $ Const(c,t2) 
   1.116      end
   1.117    | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
   1.118      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
   1.119 -	val _ = in_min_comb count_comb
   1.120 +	val _ = increK count_comb
   1.121      in
   1.122  	Const("COMBK",tK) $ Free(v,t2)
   1.123      end
   1.124    | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
   1.125      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
   1.126 -	val _ = in_min_comb count_comb 
   1.127 +	val _ = increK count_comb 
   1.128      in
   1.129  	Const("COMBK",tK) $ Var(ind,t2)
   1.130      end
   1.131 @@ -88,10 +151,10 @@
   1.132  		  val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.133  		  val tp' = Term.type_of1(Bnds,P')
   1.134  		  val tS = Type("fun",[tp',Type("fun",[tI,tr])])
   1.135 -		  val _ = in_min_comb count_comb
   1.136 -		  val _ = in_combS count_comb
   1.137 +		  val _ = increI count_comb
   1.138 +		  val _ = increS count_comb
   1.139  	      in
   1.140 -		  Const("COMBS",tS) $ P' $ Const("COMBI",tI)
   1.141 +		  compact_comb (Const("COMBS",tS) $ P' $ Const("COMBI",tI)) Bnds count_comb
   1.142  	      end)
   1.143      end
   1.144  	    
   1.145 @@ -102,7 +165,7 @@
   1.146  	if(nfreeP andalso nfreeQ) then (
   1.147  	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
   1.148  		val PQ' = decre_bndVar(P $ Q)
   1.149 -		val _ = in_min_comb count_comb
   1.150 +		val _ = increK count_comb
   1.151  	    in 
   1.152  		Const("COMBK",tK) $ PQ'
   1.153  	    end)
   1.154 @@ -113,9 +176,9 @@
   1.155  				   val tp = Term.type_of1(Bnds,P')
   1.156  				   val tq' = Term.type_of1(Bnds, Q')
   1.157  				   val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.158 -				   val _ = in_min_comb count_comb
   1.159 +				   val _ = increB count_comb
   1.160  			       in
   1.161 -				   Const("COMBB",tB) $ P' $ Q' 
   1.162 +				   compact_comb (Const("COMBB",tB) $ P' $ Q') Bnds count_comb 
   1.163  			       end)
   1.164  	      else (
   1.165  		    if nfreeQ then (
   1.166 @@ -124,9 +187,9 @@
   1.167  					val tq = Term.type_of1(Bnds,Q')
   1.168  					val tp' = Term.type_of1(Bnds, P')
   1.169  					val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
   1.170 -					val _ = in_min_comb count_comb
   1.171 +					val _ = increC count_comb
   1.172  				    in
   1.173 -					Const("COMBC",tC) $ P' $ Q'
   1.174 +					compact_comb (Const("COMBC",tC) $ P' $ Q') Bnds count_comb
   1.175  				    end)
   1.176  		    else(
   1.177  			 let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.178 @@ -134,10 +197,9 @@
   1.179  			     val tp' = Term.type_of1(Bnds,P')
   1.180  			     val tq' = Term.type_of1(Bnds,Q')
   1.181  			     val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.182 -			     val _ = in_min_comb count_comb
   1.183 -			     val _ = in_combS count_comb
   1.184 +			     val _ = increS count_comb
   1.185  			 in
   1.186 -			     Const("COMBS",tS) $ P' $ Q'
   1.187 +			     compact_comb (Const("COMBS",tS) $ P' $ Q') Bnds count_comb
   1.188  			 end)))
   1.189      end
   1.190    | lam2comb (t as (Abs(x,t1,_))) _ _ = raise LAM2COMB (t);
   1.191 @@ -150,9 +212,9 @@
   1.192    | to_comb (P $ Q) Bnds count_comb = ((to_comb P Bnds count_comb) $ (to_comb Q Bnds count_comb))
   1.193    | to_comb t _ _ = t;
   1.194   
   1.195 -    
   1.196 +   
   1.197  fun comb_of t count_comb = to_comb t [] count_comb;
   1.198 -
   1.199 + 
   1.200  (* print a term containing combinators, used for debugging *)
   1.201  exception TERM_COMB of term;
   1.202  
   1.203 @@ -313,6 +375,34 @@
   1.204  	val c = range_type (range_type t1)
   1.205      in
   1.206  	map simp_type_of [a,b,c]
   1.207 +    end
   1.208 +  | comb_typ ("COMBB_e",t) =
   1.209 +    let val t1 = domain_type t
   1.210 +	val a = domain_type t1
   1.211 +	val b = range_type t1
   1.212 +	val t2 = domain_type (range_type(range_type t))
   1.213 +	val c = domain_type t2
   1.214 +	val d = range_type t2
   1.215 +    in
   1.216 +	map simp_type_of [a,b,c,d]
   1.217 +    end
   1.218 +  | comb_typ ("COMBC_e",t) =
   1.219 +    let val t1 = domain_type t
   1.220 +	val a = domain_type t1
   1.221 +	val b = domain_type (range_type t1)
   1.222 +	val c = range_type (range_type t1)
   1.223 +	val d = domain_type (domain_type (range_type t))
   1.224 +    in
   1.225 +	map simp_type_of [a,b,c,d]
   1.226 +    end
   1.227 +  | comb_typ ("COMBS_e",t) = 
   1.228 +    let val t1 = domain_type t
   1.229 +	val a = domain_type t1
   1.230 +	val b = domain_type (range_type t1)
   1.231 +	val c = range_type (range_type t1)
   1.232 +	val d = domain_type (domain_type (range_type t))
   1.233 +    in
   1.234 +	map simp_type_of [a,b,c,d]
   1.235      end;
   1.236  
   1.237  fun const_type_of ("COMBI",t) = 
   1.238 @@ -345,6 +435,24 @@
   1.239      in
   1.240  	(tp,ts,C_var)
   1.241      end
   1.242 +  | const_type_of ("COMBB_e",t) =
   1.243 +    let val (tp,ts) = type_of t
   1.244 +	val B'_var = comb_typ ("COMBB_e",t)
   1.245 +    in
   1.246 +	(tp,ts,B'_var)
   1.247 +    end
   1.248 +  | const_type_of ("COMBC_e",t) =
   1.249 +    let val (tp,ts) = type_of t
   1.250 +	val C'_var = comb_typ ("COMBC_e",t)
   1.251 +    in
   1.252 +	(tp,ts,C'_var)
   1.253 +    end
   1.254 +  | const_type_of ("COMBS_e",t) =
   1.255 +    let val (tp,ts) = type_of t
   1.256 +	val S'_var = comb_typ ("COMBS_e",t)
   1.257 +    in
   1.258 +	(tp,ts,S'_var)
   1.259 +    end
   1.260    | const_type_of (c,t) =
   1.261      let val (tp,ts) = type_of t
   1.262  	val tvars = !const_typargs(c,t)
   1.263 @@ -353,6 +461,7 @@
   1.264  	(tp,ts,tvars')
   1.265      end;
   1.266  
   1.267 +
   1.268  fun is_bool_type (Type("bool",[])) = true
   1.269    | is_bool_type _ = false;
   1.270  
   1.271 @@ -677,12 +786,15 @@
   1.272  			| "c_COMBI" => Symtab.update (comb,1) funcs
   1.273  			| "c_COMBB" => Symtab.update (comb,3) funcs
   1.274  			| "c_COMBC" => Symtab.update (comb,3) funcs
   1.275 +			| "c_COMBB_e" => Symtab.update (comb,4) funcs
   1.276 +			| "c_COMBC_e" => Symtab.update (comb,4) funcs
   1.277 +			| "c_COMBS_e" => Symtab.update (comb,4) funcs
   1.278  			| _ => funcs)
   1.279  	  | _ => Symtab.update (comb,0) funcs;
   1.280  
   1.281  fun init_funcs_tab funcs = 
   1.282      let val tp = !typ_level
   1.283 -	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC"]
   1.284 +	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC","c_COMBB_e","c_COMBC_e","c_COMBS_e"]
   1.285  	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0
   1.286  				      | _ => Symtab.update ("hAPP",2) funcs0
   1.287  	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
   1.288 @@ -732,6 +844,17 @@
   1.289  
   1.290  fun read_in fs = map (File.read o File.unpack_platform_path) fs; 
   1.291  
   1.292 +fun get_helper_tptp () =
   1.293 +    let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.tptp"]) else []
   1.294 +	val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.tptp"]) else []
   1.295 +	val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.tptp"]) else []
   1.296 +	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.tptp"]) else []
   1.297 +	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.tptp"]) else []
   1.298 +    in
   1.299 +	("helper1.tptp") :: (IK @ BC @ S @ B'C' @ S')
   1.300 +    end;
   1.301 +
   1.302 +
   1.303  fun get_helper_clauses_tptp () =
   1.304    let val tlevel = case !typ_level of 
   1.305  		       T_FULL => (Output.debug "Fully-typed HOL"; 
   1.306 @@ -742,13 +865,7 @@
   1.307  				   "~~/src/HOL/Tools/atp-inputs/const_")
   1.308  		     | T_NONE => (Output.debug "Untyped HOL"; 
   1.309  				  "~~/src/HOL/Tools/atp-inputs/u_")
   1.310 -      val helpers = if !include_combS 
   1.311 -                    then (Output.debug "Include combinator S"; 
   1.312 -                          ["helper1.tptp","comb_inclS.tptp"]) 
   1.313 -                    else if !include_min_comb 
   1.314 -                    then (Output.debug "Include min combinators"; 
   1.315 -                          ["helper1.tptp","comb_noS.tptp"])
   1.316 -		    else (Output.debug "No combinator is used"; ["helper1.tptp"])
   1.317 +      val helpers = get_helper_tptp ()
   1.318        val t_helpers = map (curry (op ^) tlevel) helpers
   1.319    in
   1.320        read_in t_helpers
   1.321 @@ -776,6 +893,17 @@
   1.322      end;
   1.323  
   1.324  
   1.325 +fun get_helper_dfg () =
   1.326 +    let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K";["combIK.dfg"]) else []
   1.327 +	val BC = if !combB_count > 0 orelse !combC_count > 0 then (Output.debug "Include combinator B C";["combBC.dfg"]) else []
   1.328 +	val S = if !combS_count > 0 then (Output.debug "Include combinator S";["combS.dfg"]) else []
   1.329 +	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 then (Output.debug "Include combinator B' C'"; ["combBC_e.dfg"]) else []
   1.330 +	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'";["combS_e.dfg"]) else []
   1.331 +    in
   1.332 +	("helper1.dfg") :: (IK @ BC @ S @ B'C' @ S')
   1.333 +    end;
   1.334 +
   1.335 +
   1.336  (* dfg format *)
   1.337  fun get_helper_clauses_dfg () = 
   1.338   let val tlevel = case !typ_level of 
   1.339 @@ -787,13 +915,7 @@
   1.340  		                  "~~/src/HOL/Tools/atp-inputs/const_")
   1.341  		    | T_NONE => (Output.debug "Untyped HOL"; 
   1.342  		                 "~~/src/HOL/Tools/atp-inputs/u_")
   1.343 -     val helpers = if !include_combS 
   1.344 -                   then (Output.debug "Include combinator S"; 
   1.345 -                         ["helper1.dfg","comb_inclS.dfg"]) else
   1.346 -		   if !include_min_comb 
   1.347 -		   then (Output.debug "Include min combinators"; 
   1.348 -		         ["helper1.dfg","comb_noS.dfg"])
   1.349 -		   else (Output.debug "No combinator is used"; ["helper1.dfg"])
   1.350 +     val helpers = get_helper_dfg ()
   1.351       val t_helpers = map (curry (op ^) tlevel) helpers
   1.352   in
   1.353       read_in t_helpers