# HG changeset patch # User mengj # Date 1160049257 -7200 # Node ID 2cfa020109c1958d900b7e0d9656be24b3d1bd44 # Parent bb75b876b2602e49b42f82f7d63c9ae3d157b09b Changed and removed some functions related to combinators, since they are Isabelle constants now. diff -r bb75b876b260 -r 2cfa020109c1 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Thu Oct 05 10:46:26 2006 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Thu Oct 05 13:54:17 2006 +0200 @@ -352,120 +352,8 @@ | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[]) | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]); -fun comb_typ ("COMBI",t) = - let val t' = domain_type t - in - [simp_type_of t'] - end - | comb_typ ("COMBK",t) = - let val a = domain_type t - val b = domain_type (range_type t) - in - map simp_type_of [a,b] - end - | comb_typ ("COMBS",t) = - let val t' = domain_type t - val a = domain_type t' - val b = domain_type (range_type t') - val c = range_type (range_type t') - in - map simp_type_of [a,b,c] - end - | comb_typ ("COMBB",t) = - let val ab = domain_type t - val ca = domain_type (range_type t) - val a = domain_type ab - val b = range_type ab - val c = domain_type ca - in - map simp_type_of [a,b,c] - end - | comb_typ ("COMBC",t) = - let val t1 = domain_type t - val a = domain_type t1 - val b = domain_type (range_type t1) - val c = range_type (range_type t1) - in - map simp_type_of [a,b,c] - end - | comb_typ ("COMBB_e",t) = - let val t1 = domain_type t - val a = domain_type t1 - val b = range_type t1 - val t2 = domain_type (range_type(range_type t)) - val c = domain_type t2 - val d = range_type t2 - in - map simp_type_of [a,b,c,d] - end - | comb_typ ("COMBC_e",t) = - let val t1 = domain_type t - val a = domain_type t1 - val b = domain_type (range_type t1) - val c = range_type (range_type t1) - val d = domain_type (domain_type (range_type t)) - in - map simp_type_of [a,b,c,d] - end - | comb_typ ("COMBS_e",t) = - let val t1 = domain_type t - val a = domain_type t1 - val b = domain_type (range_type t1) - val c = range_type (range_type t1) - val d = domain_type (domain_type (range_type t)) - in - map simp_type_of [a,b,c,d] - end; -fun const_type_of ("COMBI",t) = - let val (tp,ts) = type_of t - val I_var = comb_typ ("COMBI",t) - in - (tp,ts,I_var) - end - | const_type_of ("COMBK",t) = - let val (tp,ts) = type_of t - val K_var = comb_typ ("COMBK",t) - in - (tp,ts,K_var) - end - | const_type_of ("COMBS",t) = - let val (tp,ts) = type_of t - val S_var = comb_typ ("COMBS",t) - in - (tp,ts,S_var) - end - | const_type_of ("COMBB",t) = - let val (tp,ts) = type_of t - val B_var = comb_typ ("COMBB",t) - in - (tp,ts,B_var) - end - | const_type_of ("COMBC",t) = - let val (tp,ts) = type_of t - val C_var = comb_typ ("COMBC",t) - in - (tp,ts,C_var) - end - | const_type_of ("COMBB_e",t) = - let val (tp,ts) = type_of t - val B'_var = comb_typ ("COMBB_e",t) - in - (tp,ts,B'_var) - end - | const_type_of ("COMBC_e",t) = - let val (tp,ts) = type_of t - val C'_var = comb_typ ("COMBC_e",t) - in - (tp,ts,C'_var) - end - | const_type_of ("COMBS_e",t) = - let val (tp,ts) = type_of t - val S'_var = comb_typ ("COMBS_e",t) - in - (tp,ts,S'_var) - end - | const_type_of (c,t) = +fun const_type_of (c,t) = let val (tp,ts) = type_of t val tvars = !const_typargs(c,t) val tvars' = map simp_type_of tvars @@ -791,30 +679,14 @@ in (cls_str, tfree_lits) end; -fun init_combs (comb,funcs) = - case !typ_level of T_CONST => - (case comb of "c_COMBK" => Symtab.update (comb,2) funcs - | "c_COMBS" => Symtab.update (comb,3) funcs - | "c_COMBI" => Symtab.update (comb,1) funcs - | "c_COMBB" => Symtab.update (comb,3) funcs - | "c_COMBC" => Symtab.update (comb,3) funcs - | "c_COMBB_e" => Symtab.update (comb,4) funcs - | "c_COMBC_e" => Symtab.update (comb,4) funcs - | "c_COMBS_e" => Symtab.update (comb,4) funcs - | _ => funcs) - | _ => Symtab.update (comb,0) funcs; - fun init_funcs_tab funcs = let val tp = !typ_level - 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"] - val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0 - | _ => Symtab.update ("hAPP",2) funcs0 + val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs + | _ => Symtab.update ("hAPP",2) funcs val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1 | _ => funcs1 in - case tp of T_CONST => Symtab.update ("c_fequal",1) funcs2 - | _ => Symtab.update ("c_fequal",0) funcs2 + funcs2 end;