Changed the DFG format's functions' declaration procedure.
authormengj
Thu May 25 14:08:55 2006 +0200 (2006-05-25)
changeset 19725ada9bb1faba5
parent 19724 20d76a40e362
child 19726 df95778b4c2f
Changed the DFG format's functions' declaration procedure.
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu May 25 11:53:01 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu May 25 14:08:55 2006 +0200
     1.3 @@ -702,10 +702,21 @@
     1.4      in (cls_str, tfree_lits) end;
     1.5  
     1.6  
     1.7 +fun init_combs (comb,funcs) =
     1.8 +    case !typ_level of T_CONST => 
     1.9 +		       (case comb of "c_COMBK" => Symtab.update (comb,2) funcs
    1.10 +				   | "c_COMBS" => Symtab.update (comb,3) funcs
    1.11 +				   | "c_COMBI" => Symtab.update (comb,1) funcs
    1.12 +				   | "c_COMBB" => Symtab.update (comb,3) funcs
    1.13 +				   | "c_COMBC" => Symtab.update (comb,3) funcs
    1.14 +				   | _ => funcs)
    1.15 +		     | _ => Symtab.update (comb,0) funcs;
    1.16 +
    1.17  fun init_funcs_tab funcs = 
    1.18      let val tp = !typ_level
    1.19 -	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs
    1.20 -				      | _ => Symtab.update ("hAPP",2) funcs
    1.21 +	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC"]
    1.22 +	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0
    1.23 +				      | _ => Symtab.update ("hAPP",2) funcs0
    1.24  	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
    1.25  				      | _ => funcs1
    1.26      in
    1.27 @@ -714,9 +725,11 @@
    1.28      end;
    1.29  
    1.30  
    1.31 -fun add_funcs (CombConst(c,_,tvars),funcs) = 
    1.32 -    (case !typ_level of T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
    1.33 -		     | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
    1.34 +fun add_funcs (CombConst(c,_,tvars),funcs) =
    1.35 +    if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
    1.36 +    else
    1.37 +	(case !typ_level of T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
    1.38 +			  | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
    1.39    | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
    1.40    | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs)
    1.41    | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs))