src/HOL/Tools/res_clause.ML
changeset 22643 bc3bb8e9594a
parent 22383 01e90256550d
child 22997 d4f3b015b50b
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Apr 12 12:26:19 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Apr 12 13:56:40 2007 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4    type typ_var and type_literal and literal
     1.5    val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list
     1.6    val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
     1.7 -  val arity_clause_thy: theory -> arityClause list 
     1.8    val ascii_of : string -> string
     1.9    val tptp_pack : string list -> string
    1.10 +  val make_arity_clauses: theory -> (class list * arityClause list)
    1.11    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
    1.12    val clause_prefix : string 
    1.13    val clause2tptp : clause -> string * string list
    1.14 @@ -362,31 +362,30 @@
    1.15        (case ord(x,y) of EQUAL => list_ord ord (xs,ys)
    1.16  	 	      | xy_ord => xy_ord);
    1.17  		     
    1.18 -(*Make literals for sorted type variables.  FIXME: can it use map?*) 
    1.19 -fun sorts_on_typs (_, [])   = ([]) 
    1.20 -  | sorts_on_typs (v, "HOL.type" :: s) =
    1.21 -      sorts_on_typs (v,s)                (*IGNORE sort "type"*)
    1.22 -  | sorts_on_typs ((FOLTVar indx), s::ss) =
    1.23 -      LTVar(make_type_class s, make_schematic_type_var indx) :: 
    1.24 -      sorts_on_typs ((FOLTVar indx), ss)
    1.25 -  | sorts_on_typs ((FOLTFree x), s::ss) =
    1.26 -      LTFree(make_type_class s, make_fixed_type_var x) :: 
    1.27 -      sorts_on_typs ((FOLTFree x), ss);
    1.28 -
    1.29 +(*Make literals for sorted type variables*) 
    1.30 +fun sorts_on_typs (_, [])   = []
    1.31 +  | sorts_on_typs (v,  s::ss) = 
    1.32 +      let val sorts = sorts_on_typs (v, ss)
    1.33 +      in
    1.34 +          if s = "HOL.type" then sorts
    1.35 +          else case v of
    1.36 +              FOLTVar indx => LTVar(make_type_class s, make_schematic_type_var indx) :: sorts
    1.37 +            | FOLTFree x => LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    1.38 +      end;
    1.39  
    1.40  fun pred_of_sort (LTVar (s,ty)) = (s,1)
    1.41 -|   pred_of_sort (LTFree (s,ty)) = (s,1)
    1.42 +  | pred_of_sort (LTFree (s,ty)) = (s,1)
    1.43  
    1.44  (*Given a list of sorted type variables, return two separate lists.
    1.45    The first is for TVars, the second for TFrees.*)
    1.46  fun add_typs_aux [] = ([],[])
    1.47 -  | add_typs_aux ((FOLTVar indx,s)::tss) = 
    1.48 +  | add_typs_aux ((FOLTVar indx, s) :: tss) = 
    1.49        let val vs = sorts_on_typs (FOLTVar indx, s)
    1.50  	  val (vss,fss) = add_typs_aux tss
    1.51        in
    1.52  	  (vs union vss, fss)
    1.53        end
    1.54 -  | add_typs_aux ((FOLTFree x,s)::tss) =
    1.55 +  | add_typs_aux ((FOLTFree x, s) :: tss) =
    1.56        let val fs = sorts_on_typs (FOLTFree x, s)
    1.57  	  val (vss,fss) = add_typs_aux tss
    1.58        in
    1.59 @@ -442,8 +441,8 @@
    1.60  type class = string; 
    1.61  type tcons = string; 
    1.62  
    1.63 -datatype arLit = TConsLit of bool * (class * tcons * string list)
    1.64 -               | TVarLit of bool * (class * string);
    1.65 +datatype arLit = TConsLit of class * tcons * string list
    1.66 +               | TVarLit of class * string;
    1.67   
    1.68  datatype arityClause =  
    1.69  	 ArityClause of {axiom_name: axiom_name,
    1.70 @@ -457,21 +456,16 @@
    1.71  
    1.72  fun pack_sort(_,[])  = []
    1.73    | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
    1.74 -  | pack_sort(tvar, cls::srt) =  (make_type_class cls, tvar) :: pack_sort(tvar, srt);
    1.75 +  | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
    1.76      
    1.77 -fun make_TVarLit b (cls,str) = TVarLit(b, (cls,str));
    1.78 -
    1.79 -fun make_TConsLit b (cls,tcons,tvars) = 
    1.80 -      TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars));
    1.81 -
    1.82  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
    1.83 -fun make_axiom_arity_clause (tcons, axiom_name, (res,args)) =
    1.84 +fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
    1.85     let val tvars = gen_TVars (length args)
    1.86         val tvars_srts = ListPair.zip (tvars,args)
    1.87     in
    1.88        ArityClause {axiom_name = axiom_name, kind = Axiom, 
    1.89 -                   conclLit = make_TConsLit true (res,tcons,tvars), 
    1.90 -                   premLits = map (make_TVarLit false) (union_all(map pack_sort tvars_srts))}
    1.91 +                   conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars), 
    1.92 +                   premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
    1.93     end;
    1.94  
    1.95  
    1.96 @@ -515,10 +509,10 @@
    1.97  
    1.98  fun multi_arity_clause [] = []
    1.99    | multi_arity_clause ((tcons,ars) :: tc_arlists) =
   1.100 -      arity_clause [] 1 (tcons, ars)  @  
   1.101 -      multi_arity_clause tc_arlists 
   1.102 +      arity_clause [] 1 (tcons, ars)  @  multi_arity_clause tc_arlists 
   1.103  
   1.104 -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy.*)
   1.105 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   1.106 +  provided its arguments have the corresponding sorts.*)
   1.107  fun type_class_pairs thy tycons classes =
   1.108    let val alg = Sign.classes_of thy
   1.109        fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
   1.110 @@ -528,8 +522,19 @@
   1.111        fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes)
   1.112    in  map try_classes tycons  end;
   1.113  
   1.114 -fun arity_clause_thy thy tycons classes =
   1.115 -  multi_arity_clause (type_class_pairs thy tycons classes);
   1.116 +(*Proving one (tycon, class) membership may require proving others, so iterate.*)
   1.117 +fun iter_type_class_pairs thy tycons [] = ([], [])
   1.118 +  | iter_type_class_pairs thy tycons classes =
   1.119 +      let val cpairs = type_class_pairs thy tycons classes
   1.120 +          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
   1.121 +          val _ = if null newclasses then () 
   1.122 +                  else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
   1.123 +          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses  
   1.124 +      in  (classes' union classes, cpairs' union cpairs)  end;
   1.125 +      
   1.126 +fun make_arity_clauses thy tycons classes =
   1.127 +  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes  
   1.128 +  in  (classes', multi_arity_clause cpairs)  end;
   1.129  
   1.130  
   1.131  (**** Find occurrences of predicates in clauses ****)
   1.132 @@ -557,11 +562,11 @@
   1.133  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
   1.134    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
   1.135  
   1.136 -fun class_of_arityLit (TConsLit(_, (tclass, _, _))) = tclass
   1.137 -  | class_of_arityLit (TVarLit(_, (tclass, _))) = tclass;
   1.138 +fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
   1.139 +  | class_of_arityLit (TVarLit (tclass, _)) = tclass;
   1.140  
   1.141  fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
   1.142 -  let val classes = map class_of_arityLit (conclLit::premLits)
   1.143 +  let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
   1.144        fun upd (class,preds) = Symtab.update (class,1) preds
   1.145    in  foldl upd preds classes  end;
   1.146  
   1.147 @@ -598,7 +603,7 @@
   1.148        Symtab.update (make_fixed_type_var a, 0) funcs
   1.149  
   1.150  fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
   1.151 -  let val TConsLit(_, (_, tcons, tvars)) = conclLit
   1.152 +  let val TConsLit (_, tcons, tvars) = conclLit
   1.153    in  Symtab.update (tcons, length tvars) funcs  end;
   1.154  
   1.155  fun add_clause_funcs (Clause {literals, types_sorts, ...}, funcs) =
   1.156 @@ -708,10 +713,10 @@
   1.157  fun dfg_tfree_clause tfree_lit =
   1.158    "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.159  
   1.160 -fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
   1.161 -      dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.162 -  | dfg_of_arLit (TVarLit(pol,(c,str))) =
   1.163 -      dfg_sign pol (c ^ "(" ^ str ^ ")")
   1.164 +fun dfg_of_arLit (TConsLit (c,t,args)) =
   1.165 +      dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.166 +  | dfg_of_arLit (TVarLit (c,str)) =
   1.167 +      dfg_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.168      
   1.169  fun dfg_classrelLits sub sup =  "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
   1.170  
   1.171 @@ -722,7 +727,7 @@
   1.172  fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   1.173  
   1.174  fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) = 
   1.175 -  let val TConsLit(_, (_,_,tvars)) = conclLit
   1.176 +  let val TConsLit (_,_,tvars) = conclLit
   1.177        val lits = map dfg_of_arLit (conclLit :: premLits)
   1.178    in
   1.179        "clause( %(" ^ name_of_kind kind ^ ")\n" ^ 
   1.180 @@ -800,10 +805,10 @@
   1.181  fun tptp_tfree_clause tfree_lit =
   1.182      "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   1.183      
   1.184 -fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   1.185 -      tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.186 -  | tptp_of_arLit (TVarLit(b,(c,str))) =
   1.187 -      tptp_sign b (c ^ "(" ^ str ^ ")")
   1.188 +fun tptp_of_arLit (TConsLit (c,t,args)) =
   1.189 +      tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.190 +  | tptp_of_arLit (TVarLit (c,str)) =
   1.191 +      tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.192      
   1.193  fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) = 
   1.194    "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^