Purely cosmetic
authorpaulson
Mon Oct 30 16:42:46 2006 +0100 (2006-10-30)
changeset 2110804d8e6eb9a2e
parent 21107 e69c0e82955a
child 21109 f8f89be75e81
Purely cosmetic
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Mon Oct 30 13:07:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Mon Oct 30 16:42:46 2006 +0100
     1.3 @@ -23,10 +23,12 @@
     1.4  val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
     1.5  
     1.6  
     1.7 -(*A flag to set if we use extra combinators B',C',S', currently FALSE as the 5 standard
     1.8 +(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
     1.9    combinators appear to work best.*)
    1.10 -val use_combB'C'S' = ref false;
    1.11 +val use_Turner = ref false;
    1.12  
    1.13 +(*FIXME: these refs should probaby replaced by code to count the combinators in the 
    1.14 +  translated form of the term.*)
    1.15  val combI_count = ref 0;
    1.16  val combK_count = ref 0;
    1.17  val combB_count = ref 0;
    1.18 @@ -128,101 +130,102 @@
    1.19      end
    1.20    | mk_compact_comb tm _ _ = tm;
    1.21  
    1.22 -fun compact_comb t Bnds count_comb = if !use_combB'C'S' then mk_compact_comb t Bnds count_comb else t;
    1.23 +fun compact_comb t Bnds count_comb = 
    1.24 +  if !use_Turner then mk_compact_comb t Bnds count_comb else t;
    1.25  
    1.26  fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = 
    1.27 -    let val tpI = Type("fun",[tp,tp])
    1.28 -	val _ = increI count_comb
    1.29 -    in 
    1.30 -	Const("Reconstruction.COMBI",tpI) 
    1.31 -    end
    1.32 +      let val tpI = Type("fun",[tp,tp])
    1.33 +	  val _ = increI count_comb
    1.34 +      in 
    1.35 +	  Const("Reconstruction.COMBI",tpI) 
    1.36 +      end
    1.37    | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = 
    1.38 -    let val (Bound n') = decre_bndVar (Bound n)
    1.39 -	val tb = List.nth(Bnds,n')
    1.40 -	val tK = Type("fun",[tb,Type("fun",[tp,tb])])
    1.41 -	val _ = increK count_comb 
    1.42 -    in
    1.43 -	Const("Reconstruction.COMBK",tK) $ (Bound n')
    1.44 -    end
    1.45 +      let val (Bound n') = decre_bndVar (Bound n)
    1.46 +	  val tb = List.nth(Bnds,n')
    1.47 +	  val tK = Type("fun",[tb,Type("fun",[tp,tb])])
    1.48 +	  val _ = increK count_comb 
    1.49 +      in
    1.50 +	  Const("Reconstruction.COMBK",tK) $ (Bound n')
    1.51 +      end
    1.52    | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
    1.53 -    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.54 -	val _ = increK count_comb 
    1.55 -    in 
    1.56 -	Const("Reconstruction.COMBK",tK) $ Const(c,t2) 
    1.57 -    end
    1.58 +      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.59 +	  val _ = increK count_comb 
    1.60 +      in 
    1.61 +	  Const("Reconstruction.COMBK",tK) $ Const(c,t2) 
    1.62 +      end
    1.63    | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
    1.64 -    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.65 -	val _ = increK count_comb
    1.66 -    in
    1.67 -	Const("Reconstruction.COMBK",tK) $ Free(v,t2)
    1.68 -    end
    1.69 +      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.70 +	  val _ = increK count_comb
    1.71 +      in
    1.72 +	  Const("Reconstruction.COMBK",tK) $ Free(v,t2)
    1.73 +      end
    1.74    | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
    1.75 -    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.76 -	val _ = increK count_comb 
    1.77 -    in
    1.78 -	Const("Reconstruction.COMBK",tK) $ Var(ind,t2)
    1.79 -    end
    1.80 +      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.81 +	  val _ = increK count_comb 
    1.82 +      in
    1.83 +	  Const("Reconstruction.COMBK",tK) $ Var(ind,t2)
    1.84 +      end
    1.85    | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
    1.86 -    let val nfreeP = not(is_free P 0)
    1.87 -	val tr = Term.type_of1(t1::Bnds,P)
    1.88 -    in
    1.89 -	if nfreeP then (decre_bndVar P)
    1.90 -	else (
    1.91 -	      let val tI = Type("fun",[t1,t1])
    1.92 -		  val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
    1.93 -		  val tp' = Term.type_of1(Bnds,P')
    1.94 -		  val tS = Type("fun",[tp',Type("fun",[tI,tr])])
    1.95 -		  val _ = increI count_comb
    1.96 -		  val _ = increS count_comb
    1.97 -	      in
    1.98 -		  compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb
    1.99 -	      end)
   1.100 -    end
   1.101 +      let val nfreeP = not(is_free P 0)
   1.102 +	  val tr = Term.type_of1(t1::Bnds,P)
   1.103 +      in
   1.104 +	  if nfreeP then (decre_bndVar P)
   1.105 +	  else 
   1.106 +	  let val tI = Type("fun",[t1,t1])
   1.107 +	      val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.108 +	      val tp' = Term.type_of1(Bnds,P')
   1.109 +	      val tS = Type("fun",[tp',Type("fun",[tI,tr])])
   1.110 +	      val _ = increI count_comb
   1.111 +	      val _ = increS count_comb
   1.112 +	  in
   1.113 +	      compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb
   1.114 +	  end
   1.115 +      end
   1.116  	    
   1.117    | lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb =
   1.118 -    let val (nfreeP,nfreeQ) = (not(is_free P 0),not(is_free Q 0))
   1.119 -	val tpq = Term.type_of1(t1::Bnds, P$Q) 
   1.120 -    in
   1.121 -	if(nfreeP andalso nfreeQ) then (
   1.122 +      let val nfreeP = not(is_free P 0)
   1.123 +	  and nfreeQ = not(is_free Q 0)
   1.124 +	  val tpq = Term.type_of1(t1::Bnds, P$Q) 
   1.125 +      in
   1.126 +	  if nfreeP andalso nfreeQ 
   1.127 +	  then 
   1.128  	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
   1.129  		val PQ' = decre_bndVar(P $ Q)
   1.130  		val _ = increK count_comb
   1.131  	    in 
   1.132  		Const("Reconstruction.COMBK",tK) $ PQ'
   1.133 -	    end)
   1.134 -	else (
   1.135 -	      if nfreeP then (
   1.136 -			       let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
   1.137 -				   val P' = decre_bndVar P
   1.138 -				   val tp = Term.type_of1(Bnds,P')
   1.139 -				   val tq' = Term.type_of1(Bnds, Q')
   1.140 -				   val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.141 -				   val _ = increB count_comb
   1.142 -			       in
   1.143 -				   compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
   1.144 -			       end)
   1.145 -	      else (
   1.146 -		    if nfreeQ then (
   1.147 -				    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.148 -					val Q' = decre_bndVar Q
   1.149 -					val tq = Term.type_of1(Bnds,Q')
   1.150 -					val tp' = Term.type_of1(Bnds, P')
   1.151 -					val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
   1.152 -					val _ = increC count_comb
   1.153 -				    in
   1.154 -					compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
   1.155 -				    end)
   1.156 -		    else(
   1.157 -			 let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.158 -			     val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb 
   1.159 -			     val tp' = Term.type_of1(Bnds,P')
   1.160 -			     val tq' = Term.type_of1(Bnds,Q')
   1.161 -			     val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.162 -			     val _ = increS count_comb
   1.163 -			 in
   1.164 -			     compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
   1.165 -			 end)))
   1.166 -    end
   1.167 +	    end
   1.168 +	  else if nfreeP then 
   1.169 +	    let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
   1.170 +		val P' = decre_bndVar P
   1.171 +		val tp = Term.type_of1(Bnds,P')
   1.172 +		val tq' = Term.type_of1(Bnds, Q')
   1.173 +		val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.174 +		val _ = increB count_comb
   1.175 +	    in
   1.176 +		compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
   1.177 +	    end
   1.178 +	  else if nfreeQ then 
   1.179 +	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.180 +		val Q' = decre_bndVar Q
   1.181 +		val tq = Term.type_of1(Bnds,Q')
   1.182 +		val tp' = Term.type_of1(Bnds, P')
   1.183 +		val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
   1.184 +		val _ = increC count_comb
   1.185 +	    in
   1.186 +		compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
   1.187 +	    end
   1.188 +          else
   1.189 +	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.190 +		val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb 
   1.191 +		val tp' = Term.type_of1(Bnds,P')
   1.192 +		val tq' = Term.type_of1(Bnds,Q')
   1.193 +		val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.194 +		val _ = increS count_comb
   1.195 +	    in
   1.196 +		compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
   1.197 +	    end
   1.198 +      end
   1.199    | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
   1.200  
   1.201  (*********************)