src/HOL/Tools/res_hol_clause.ML
changeset 20953 1ea394dc2a0f
parent 20865 2cfa020109c1
child 20997 4b500d78cb4f
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 10 13:59:16 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 10 15:30:48 2006 +0200
     1.3 @@ -48,12 +48,20 @@
     1.4  
     1.5  
     1.6  exception DECRE_COMB of string;
     1.7 -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.8 +fun decreB count_comb n = 
     1.9 +  if count_comb then 
    1.10 +    if !combB_count >= n then combB_count := !combB_count - n else raise DECRE_COMB "COMBB"
    1.11 +  else ();
    1.12  
    1.13 -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.14 +fun decreC count_comb n =
    1.15 +  if count_comb then 
    1.16 +    if !combC_count >= n then combC_count := !combC_count - n else raise DECRE_COMB "COMBC"
    1.17 +  else ();
    1.18  
    1.19 -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.20 -
    1.21 +fun decreS count_comb n = 
    1.22 +  if count_comb then 
    1.23 +    if !combS_count >= n then combS_count := !combS_count - n else raise DECRE_COMB "COMBS"
    1.24 +  else ();
    1.25  
    1.26  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.27  
    1.28 @@ -82,7 +90,7 @@
    1.29  
    1.30  
    1.31  (*******************************************)
    1.32 -fun mk_compact_comb (tm as (Const("COMBB",_)$p) $ (Const("COMBB",_)$q$r)) Bnds count_comb =
    1.33 +fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)$p) $ (Const("Reconstruction.COMBB",_)$q$r)) Bnds count_comb =
    1.34      let val tp_p = Term.type_of1(Bnds,p)
    1.35  	val tp_q = Term.type_of1(Bnds,q)
    1.36  	val tp_r = Term.type_of1(Bnds,r)
    1.37 @@ -91,9 +99,9 @@
    1.38  	val _ = increB' count_comb
    1.39  	val _ = decreB count_comb 2
    1.40      in
    1.41 -	Const("COMBB_e",typ_B') $ p $ q $ r
    1.42 +	Const("Reconstruction.COMBB'",typ_B') $ p $ q $ r
    1.43      end
    1.44 -  | mk_compact_comb (tm as (Const("COMBC",_) $ (Const("COMBB",_)$p$q) $ r)) Bnds count_comb =
    1.45 +  | mk_compact_comb (tm as (Const("Reconstruction.COMBC",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb =
    1.46      let val tp_p = Term.type_of1(Bnds,p)
    1.47  	val tp_q = Term.type_of1(Bnds,q)
    1.48  	val tp_r = Term.type_of1(Bnds,r)
    1.49 @@ -103,9 +111,9 @@
    1.50  	val _ = decreC count_comb 1
    1.51  	val _ = decreB count_comb 1
    1.52      in
    1.53 -	Const("COMBC_e",typ_C') $ p $ q $ r
    1.54 +	Const("Reconstruction.COMBC'",typ_C') $ p $ q $ r
    1.55      end
    1.56 -  | mk_compact_comb (tm as (Const("COMBS",_) $ (Const("COMBB",_)$p$q) $ r)) Bnds count_comb =
    1.57 +  | mk_compact_comb (tm as (Const("Reconstruction.COMBS",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb =
    1.58      let val tp_p = Term.type_of1(Bnds,p)
    1.59  	val tp_q = Term.type_of1(Bnds,q)
    1.60  	val tp_r = Term.type_of1(Bnds,r)
    1.61 @@ -115,7 +123,7 @@
    1.62  	val _ = decreS count_comb 1
    1.63  	val _ = decreB count_comb 1
    1.64      in
    1.65 -	Const("COMBS_e",typ_S') $ p $ q $ r
    1.66 +	Const("Reconstruction.COMBS'",typ_S') $ p $ q $ r
    1.67      end
    1.68    | mk_compact_comb tm _ _ = tm;
    1.69  
    1.70 @@ -125,7 +133,7 @@
    1.71      let val tpI = Type("fun",[tp,tp])
    1.72  	val _ = increI count_comb
    1.73      in 
    1.74 -	Const("COMBI",tpI) 
    1.75 +	Const("Reconstruction.COMBI",tpI) 
    1.76      end
    1.77    | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = 
    1.78      let val (Bound n') = decre_bndVar (Bound n)
    1.79 @@ -133,25 +141,25 @@
    1.80  	val tK = Type("fun",[tb,Type("fun",[tp,tb])])
    1.81  	val _ = increK count_comb 
    1.82      in
    1.83 -	Const("COMBK",tK) $ (Bound n')
    1.84 +	Const("Reconstruction.COMBK",tK) $ (Bound n')
    1.85      end
    1.86    | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
    1.87      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.88  	val _ = increK count_comb 
    1.89      in 
    1.90 -	Const("COMBK",tK) $ Const(c,t2) 
    1.91 +	Const("Reconstruction.COMBK",tK) $ Const(c,t2) 
    1.92      end
    1.93    | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
    1.94      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
    1.95  	val _ = increK count_comb
    1.96      in
    1.97 -	Const("COMBK",tK) $ Free(v,t2)
    1.98 +	Const("Reconstruction.COMBK",tK) $ Free(v,t2)
    1.99      end
   1.100    | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
   1.101      let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
   1.102  	val _ = increK count_comb 
   1.103      in
   1.104 -	Const("COMBK",tK) $ Var(ind,t2)
   1.105 +	Const("Reconstruction.COMBK",tK) $ Var(ind,t2)
   1.106      end
   1.107    | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
   1.108      let val nfreeP = not(is_free P 0)
   1.109 @@ -166,7 +174,7 @@
   1.110  		  val _ = increI count_comb
   1.111  		  val _ = increS count_comb
   1.112  	      in
   1.113 -		  compact_comb (Const("COMBS",tS) $ P' $ Const("COMBI",tI)) Bnds count_comb
   1.114 +		  compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Const("Reconstruction.COMBI",tI)) Bnds count_comb
   1.115  	      end)
   1.116      end
   1.117  	    
   1.118 @@ -179,7 +187,7 @@
   1.119  		val PQ' = decre_bndVar(P $ Q)
   1.120  		val _ = increK count_comb
   1.121  	    in 
   1.122 -		Const("COMBK",tK) $ PQ'
   1.123 +		Const("Reconstruction.COMBK",tK) $ PQ'
   1.124  	    end)
   1.125  	else (
   1.126  	      if nfreeP then (
   1.127 @@ -190,7 +198,7 @@
   1.128  				   val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.129  				   val _ = increB count_comb
   1.130  			       in
   1.131 -				   compact_comb (Const("COMBB",tB) $ P' $ Q') Bnds count_comb 
   1.132 +				   compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
   1.133  			       end)
   1.134  	      else (
   1.135  		    if nfreeQ then (
   1.136 @@ -201,7 +209,7 @@
   1.137  					val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
   1.138  					val _ = increC count_comb
   1.139  				    in
   1.140 -					compact_comb (Const("COMBC",tC) $ P' $ Q') Bnds count_comb
   1.141 +					compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
   1.142  				    end)
   1.143  		    else(
   1.144  			 let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   1.145 @@ -211,7 +219,7 @@
   1.146  			     val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
   1.147  			     val _ = increS count_comb
   1.148  			 in
   1.149 -			     compact_comb (Const("COMBS",tS) $ P' $ Q') Bnds count_comb
   1.150 +			     compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
   1.151  			 end)))
   1.152      end
   1.153    | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
   1.154 @@ -795,7 +803,10 @@
   1.155  	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   1.156  	ResClause.writeln_strs out tfree_clss;
   1.157  	ResClause.writeln_strs out dfg_clss;
   1.158 -	TextIO.output (out, "end_of_list.\n\nend_problem.\n");
   1.159 +	TextIO.output (out, "end_of_list.\n\n");
   1.160 +	(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   1.161 +	TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   1.162 +	TextIO.output (out, "end_problem.\n");
   1.163  	TextIO.closeOut out;
   1.164  	clnames
   1.165      end;