src/HOL/Tools/res_hol_clause.ML
changeset 20865 2cfa020109c1
parent 20864 bb75b876b260
child 20953 1ea394dc2a0f
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Oct 05 10:46:26 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Oct 05 13:54:17 2006 +0200
     1.3 @@ -352,120 +352,8 @@
     1.4    | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[])
     1.5    | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]);
     1.6  
     1.7 -fun comb_typ ("COMBI",t) = 
     1.8 -    let val t' = domain_type t
     1.9 -    in
    1.10 -	[simp_type_of t']
    1.11 -    end
    1.12 -  | comb_typ ("COMBK",t) = 
    1.13 -    let val a = domain_type t
    1.14 -	val b = domain_type (range_type t)
    1.15 -    in
    1.16 -	map simp_type_of [a,b]
    1.17 -    end
    1.18 -  | comb_typ ("COMBS",t) = 
    1.19 -    let val t' = domain_type t
    1.20 -	val a = domain_type t'
    1.21 -	val b = domain_type (range_type t')
    1.22 -	val c = range_type (range_type t')
    1.23 -    in 
    1.24 -	map simp_type_of [a,b,c]
    1.25 -    end
    1.26 -  | comb_typ ("COMBB",t) = 
    1.27 -    let val ab = domain_type t
    1.28 -	val ca = domain_type (range_type t)
    1.29 -	val a = domain_type ab
    1.30 -	val b = range_type ab
    1.31 -	val c = domain_type ca
    1.32 -    in
    1.33 -	map simp_type_of [a,b,c]
    1.34 -    end
    1.35 -  | comb_typ ("COMBC",t) =
    1.36 -    let val t1 = domain_type t
    1.37 -	val a = domain_type t1
    1.38 -	val b = domain_type (range_type t1)
    1.39 -	val c = range_type (range_type t1)
    1.40 -    in
    1.41 -	map simp_type_of [a,b,c]
    1.42 -    end
    1.43 -  | comb_typ ("COMBB_e",t) =
    1.44 -    let val t1 = domain_type t
    1.45 -	val a = domain_type t1
    1.46 -	val b = range_type t1
    1.47 -	val t2 = domain_type (range_type(range_type t))
    1.48 -	val c = domain_type t2
    1.49 -	val d = range_type t2
    1.50 -    in
    1.51 -	map simp_type_of [a,b,c,d]
    1.52 -    end
    1.53 -  | comb_typ ("COMBC_e",t) =
    1.54 -    let val t1 = domain_type t
    1.55 -	val a = domain_type t1
    1.56 -	val b = domain_type (range_type t1)
    1.57 -	val c = range_type (range_type t1)
    1.58 -	val d = domain_type (domain_type (range_type t))
    1.59 -    in
    1.60 -	map simp_type_of [a,b,c,d]
    1.61 -    end
    1.62 -  | comb_typ ("COMBS_e",t) = 
    1.63 -    let val t1 = domain_type t
    1.64 -	val a = domain_type t1
    1.65 -	val b = domain_type (range_type t1)
    1.66 -	val c = range_type (range_type t1)
    1.67 -	val d = domain_type (domain_type (range_type t))
    1.68 -    in
    1.69 -	map simp_type_of [a,b,c,d]
    1.70 -    end;
    1.71  
    1.72 -fun const_type_of ("COMBI",t) = 
    1.73 -    let val (tp,ts) = type_of t
    1.74 -	val I_var = comb_typ ("COMBI",t)
    1.75 -    in
    1.76 -	(tp,ts,I_var)
    1.77 -    end
    1.78 -  | const_type_of ("COMBK",t) =
    1.79 -    let val (tp,ts) = type_of t
    1.80 -	val K_var = comb_typ ("COMBK",t)
    1.81 -    in
    1.82 -	(tp,ts,K_var)
    1.83 -    end
    1.84 -  | const_type_of ("COMBS",t) =
    1.85 -    let val (tp,ts) = type_of t
    1.86 -	val S_var = comb_typ ("COMBS",t)
    1.87 -    in
    1.88 -	(tp,ts,S_var)
    1.89 -    end
    1.90 -  | const_type_of ("COMBB",t) =
    1.91 -    let val (tp,ts) = type_of t
    1.92 -	val B_var = comb_typ ("COMBB",t)
    1.93 -    in
    1.94 -	(tp,ts,B_var)
    1.95 -    end
    1.96 -  | const_type_of ("COMBC",t) =
    1.97 -    let val (tp,ts) = type_of t
    1.98 -	val C_var = comb_typ ("COMBC",t)
    1.99 -    in
   1.100 -	(tp,ts,C_var)
   1.101 -    end
   1.102 -  | const_type_of ("COMBB_e",t) =
   1.103 -    let val (tp,ts) = type_of t
   1.104 -	val B'_var = comb_typ ("COMBB_e",t)
   1.105 -    in
   1.106 -	(tp,ts,B'_var)
   1.107 -    end
   1.108 -  | const_type_of ("COMBC_e",t) =
   1.109 -    let val (tp,ts) = type_of t
   1.110 -	val C'_var = comb_typ ("COMBC_e",t)
   1.111 -    in
   1.112 -	(tp,ts,C'_var)
   1.113 -    end
   1.114 -  | const_type_of ("COMBS_e",t) =
   1.115 -    let val (tp,ts) = type_of t
   1.116 -	val S'_var = comb_typ ("COMBS_e",t)
   1.117 -    in
   1.118 -	(tp,ts,S'_var)
   1.119 -    end
   1.120 -  | const_type_of (c,t) =
   1.121 +fun const_type_of (c,t) =
   1.122      let val (tp,ts) = type_of t
   1.123  	val tvars = !const_typargs(c,t)
   1.124  	val tvars' = map simp_type_of tvars
   1.125 @@ -791,30 +679,14 @@
   1.126      in (cls_str, tfree_lits) end;
   1.127  
   1.128  
   1.129 -fun init_combs (comb,funcs) =
   1.130 -    case !typ_level of T_CONST => 
   1.131 -	    (case comb of "c_COMBK" => Symtab.update (comb,2) funcs
   1.132 -			| "c_COMBS" => Symtab.update (comb,3) funcs
   1.133 -			| "c_COMBI" => Symtab.update (comb,1) funcs
   1.134 -			| "c_COMBB" => Symtab.update (comb,3) funcs
   1.135 -			| "c_COMBC" => Symtab.update (comb,3) funcs
   1.136 -			| "c_COMBB_e" => Symtab.update (comb,4) funcs
   1.137 -			| "c_COMBC_e" => Symtab.update (comb,4) funcs
   1.138 -			| "c_COMBS_e" => Symtab.update (comb,4) funcs
   1.139 -			| _ => funcs)
   1.140 -	  | _ => Symtab.update (comb,0) funcs;
   1.141 -
   1.142  fun init_funcs_tab funcs = 
   1.143      let val tp = !typ_level
   1.144 -	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC",
   1.145 -	                                     "c_COMBB__e","c_COMBC__e","c_COMBS__e"]
   1.146 -	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0
   1.147 -				      | _ => Symtab.update ("hAPP",2) funcs0
   1.148 +	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   1.149 +				      | _ => Symtab.update ("hAPP",2) funcs
   1.150  	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
   1.151  				      | _ => funcs1
   1.152      in
   1.153 -	case tp of T_CONST => Symtab.update ("c_fequal",1) funcs2
   1.154 -			 | _ => Symtab.update ("c_fequal",0) funcs2
   1.155 +	funcs2
   1.156      end;
   1.157  
   1.158