tidied code
authorpaulson
Mon Nov 27 18:18:05 2006 +0100 (2006-11-27)
changeset 21560d92389321fa7
parent 21559 d24fb16e1a1d
child 21561 cfd2258f0b23
tidied code
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Nov 27 17:35:50 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Nov 27 18:18:05 2006 +0100
     1.3 @@ -477,21 +477,19 @@
     1.4    | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
     1.5    | pack_sort(tvar, cls::srt) =  (make_type_class cls, tvar) :: pack_sort(tvar, srt);
     1.6      
     1.7 -fun make_TVarLit (b, (cls,str)) = TVarLit(b, (cls,str));
     1.8 -fun make_TConsLit (b, (cls,tcons,tvars)) = 
     1.9 +fun make_TVarLit b (cls,str) = TVarLit(b, (cls,str));
    1.10 +
    1.11 +fun make_TConsLit b (cls,tcons,tvars) = 
    1.12        TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars));
    1.13  
    1.14  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
    1.15  fun make_axiom_arity_clause (tcons, axiom_name, (res,args)) =
    1.16 -   let val nargs = length args
    1.17 -       val tvars = gen_TVars nargs
    1.18 +   let val tvars = gen_TVars (length args)
    1.19         val tvars_srts = ListPair.zip (tvars,args)
    1.20 -       val tvars_srts' = union_all(map pack_sort tvars_srts)
    1.21 -       val false_tvars_srts' = map (pair false) tvars_srts'
    1.22     in
    1.23        ArityClause {axiom_name = axiom_name, kind = Axiom, 
    1.24 -                   conclLit = make_TConsLit(true, (res,tcons,tvars)), 
    1.25 -                   premLits = map make_TVarLit false_tvars_srts'}
    1.26 +                   conclLit = make_TConsLit true (res,tcons,tvars), 
    1.27 +                   premLits = map (make_TVarLit false) (union_all(map pack_sort tvars_srts))}
    1.28     end;
    1.29  
    1.30  
    1.31 @@ -577,7 +575,6 @@
    1.32  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
    1.33    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
    1.34  
    1.35 -(*Not sure the TVar case is ever used*)
    1.36  fun class_of_arityLit (TConsLit(_, (tclass, _, _))) = tclass
    1.37    | class_of_arityLit (TVarLit(_, (tclass, _))) = tclass;
    1.38  
    1.39 @@ -734,9 +731,6 @@
    1.40  fun dfg_tfree_clause tfree_lit =
    1.41    "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
    1.42  
    1.43 -fun string_of_arClauseID (ArityClause {axiom_name,...}) =
    1.44 -    arclause_prefix ^ ascii_of axiom_name;
    1.45 -
    1.46  fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
    1.47        dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")
    1.48    | dfg_of_arLit (TVarLit(pol,(c,str))) =
    1.49 @@ -748,15 +742,15 @@
    1.50    "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
    1.51    axiom_name ^ ").\n\n";
    1.52        
    1.53 -fun dfg_arity_clause (arcls as ArityClause{kind,conclLit,premLits,...}) = 
    1.54 -  let val arcls_id = string_of_arClauseID arcls
    1.55 -      val knd = name_of_kind kind
    1.56 -      val TConsLit(_, (_,_,tvars)) = conclLit
    1.57 +fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
    1.58 +
    1.59 +fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) = 
    1.60 +  let val TConsLit(_, (_,_,tvars)) = conclLit
    1.61        val lits = map dfg_of_arLit (conclLit :: premLits)
    1.62    in
    1.63 -      "clause( %(" ^ knd ^ ")\n" ^ 
    1.64 +      "clause( %(" ^ name_of_kind kind ^ ")\n" ^ 
    1.65        dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
    1.66 -      arcls_id ^ ").\n\n"
    1.67 +      string_of_ar axiom_name ^ ").\n\n"
    1.68    end;
    1.69  
    1.70  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.71 @@ -838,13 +832,9 @@
    1.72    | tptp_of_arLit (TVarLit(b,(c,str))) =
    1.73        tptp_sign b (c ^ "(" ^ str ^ ")")
    1.74      
    1.75 -fun tptp_arity_clause (arcls as ArityClause{kind,conclLit,premLits,...}) = 
    1.76 -  let val arcls_id = string_of_arClauseID arcls
    1.77 -      val knd = name_of_kind kind
    1.78 -      val lits = map tptp_of_arLit (conclLit :: premLits)
    1.79 -  in
    1.80 -    "cnf(" ^ arcls_id ^ "," ^ knd ^ "," ^ tptp_pack lits ^ ").\n"
    1.81 -  end;
    1.82 +fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) = 
    1.83 +  "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^ 
    1.84 +  tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
    1.85  
    1.86  fun tptp_classrelLits sub sup = 
    1.87    let val tvar = "(T)"