src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36218 0e4a01f3e7d3
parent 36170 0cdb76723c88
child 36221 3abbae8a10cd
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 07:38:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 09:53:31 2010 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  Storing/printing FOL clauses and arity clauses.  Typed equality is
     1.5  treated differently.
     1.6  
     1.7 -FIXME: combine with res_hol_clause!
     1.8 +FIXME: combine with sledgehammer_hol_clause!
     1.9  *)
    1.10  
    1.11  signature SLEDGEHAMMER_FOL_CLAUSE =
    1.12 @@ -57,12 +57,14 @@
    1.13    val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    1.14    val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
    1.15    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    1.16 -  val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
    1.17 -  val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table
    1.18 +  val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table
    1.19 +  val add_classrel_clause_preds :
    1.20 +    classrel_clause -> int Symtab.table -> int Symtab.table
    1.21    val class_of_arityLit: arLit -> class
    1.22 -  val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table
    1.23 -  val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
    1.24 -  val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table
    1.25 +  val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table
    1.26 +  val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table
    1.27 +  val add_arity_clause_funcs:
    1.28 +    arity_clause -> int Symtab.table -> int Symtab.table
    1.29    val init_functab: int Symtab.table
    1.30    val dfg_sign: bool -> string -> string
    1.31    val dfg_of_typeLit: bool -> type_literal -> string
    1.32 @@ -102,7 +104,7 @@
    1.33  val tconst_prefix = "tc_";
    1.34  val class_prefix = "class_";
    1.35  
    1.36 -fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
    1.37 +fun union_all xss = fold (union (op =)) xss []
    1.38  
    1.39  (* Provide readable names for the more common symbolic functions *)
    1.40  val const_trans_table =
    1.41 @@ -315,7 +317,7 @@
    1.42    | pred_of_sort (LTFree (s,ty)) = (s,1)
    1.43  
    1.44  (*Given a list of sorted type variables, return a list of type literals.*)
    1.45 -fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts);
    1.46 +fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) []
    1.47  
    1.48  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
    1.49    * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
    1.50 @@ -373,11 +375,11 @@
    1.51  (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
    1.52  fun class_pairs thy [] supers = []
    1.53    | class_pairs thy subs supers =
    1.54 -      let val class_less = Sorts.class_less(Sign.classes_of thy)
    1.55 -          fun add_super sub (super,pairs) =
    1.56 -                if class_less (sub,super) then (sub,super)::pairs else pairs
    1.57 -          fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
    1.58 -      in  List.foldl add_supers [] subs  end;
    1.59 +      let
    1.60 +        val class_less = Sorts.class_less (Sign.classes_of thy)
    1.61 +        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
    1.62 +        fun add_supers sub = fold (add_super sub) supers
    1.63 +      in fold add_supers subs [] end
    1.64  
    1.65  fun make_classrel_clause (sub,super) =
    1.66    ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
    1.67 @@ -402,18 +404,18 @@
    1.68            arity_clause dfg (class::seen) n (tcons,ars)
    1.69  
    1.70  fun multi_arity_clause dfg [] = []
    1.71 -  | multi_arity_clause dfg ((tcons,ars) :: tc_arlists) =
    1.72 -      arity_clause dfg [] 1 (tcons, ars)  @  multi_arity_clause dfg tc_arlists
    1.73 +  | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) =
    1.74 +      arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists
    1.75  
    1.76  (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
    1.77    provided its arguments have the corresponding sorts.*)
    1.78  fun type_class_pairs thy tycons classes =
    1.79    let val alg = Sign.classes_of thy
    1.80 -      fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
    1.81 -      fun add_class tycon (class,pairs) =
    1.82 -            (class, domain_sorts(tycon,class))::pairs
    1.83 -            handle Sorts.CLASS_ERROR _ => pairs
    1.84 -      fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes)
    1.85 +      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
    1.86 +      fun add_class tycon class =
    1.87 +        cons (class, domain_sorts tycon class)
    1.88 +        handle Sorts.CLASS_ERROR _ => I
    1.89 +      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
    1.90    in  map try_classes tycons  end;
    1.91  
    1.92  (*Proving one (tycon, class) membership may require proving others, so iterate.*)
    1.93 @@ -435,35 +437,35 @@
    1.94  (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
    1.95    function (it flags repeated declarations of a function, even with the same arity)*)
    1.96  
    1.97 -fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs;
    1.98 +fun update_many keypairs = fold Symtab.update keypairs
    1.99  
   1.100 -fun add_type_sort_preds (T, preds) =
   1.101 -      update_many (preds, map pred_of_sort (sorts_on_typs T));
   1.102 +val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs
   1.103  
   1.104 -fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) =
   1.105 -  Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
   1.106 +fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) =
   1.107 +  Symtab.update (subclass, 1) #> Symtab.update (superclass, 1)
   1.108  
   1.109  fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
   1.110    | class_of_arityLit (TVarLit (tclass, _)) = tclass;
   1.111  
   1.112 -fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) =
   1.113 -  let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
   1.114 -      fun upd (class,preds) = Symtab.update (class,1) preds
   1.115 -  in  List.foldl upd preds classes  end;
   1.116 +fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) =
   1.117 +  let
   1.118 +    val classes = map (make_type_class o class_of_arityLit)
   1.119 +                      (conclLit :: premLits)
   1.120 +  in fold (Symtab.update o rpair 1) classes end;
   1.121  
   1.122  (*** Find occurrences of functions in clauses ***)
   1.123  
   1.124 -fun add_foltype_funcs (TyVar _, funcs) = funcs
   1.125 -  | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs
   1.126 -  | add_foltype_funcs (TyConstr ((s, _), tys), funcs) =
   1.127 -      List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys;
   1.128 +fun add_fol_type_funcs (TyVar _) = I
   1.129 +  | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0)
   1.130 +  | add_fol_type_funcs (TyConstr ((s, _), tys)) =
   1.131 +    Symtab.update (s, length tys) #> fold add_fol_type_funcs tys
   1.132  
   1.133  (*TFrees are recorded as constants*)
   1.134  fun add_type_sort_funcs (TVar _, funcs) = funcs
   1.135    | add_type_sort_funcs (TFree (a, _), funcs) =
   1.136        Symtab.update (make_fixed_type_var a, 0) funcs
   1.137  
   1.138 -fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) =
   1.139 +fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs =
   1.140    let val TConsLit (_, tcons, tvars) = conclLit
   1.141    in  Symtab.update (tcons, length tvars) funcs  end;
   1.142