get rid of "List.foldl" + add timestamp to SPASS
authorblanchet
Mon Apr 19 09:53:31 2010 +0200 (2010-04-19 ago)
changeset 362180e4a01f3e7d3
parent 36199 4d220994f30b
child 36219 16670b4f0baa
get rid of "List.foldl" + add timestamp to SPASS
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     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  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 07:38:35 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 09:53:31 2010 +0200
     2.3 @@ -174,13 +174,13 @@
     2.4      end;
     2.5  
     2.6  
     2.7 -fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
     2.8 -  let val cls = make_clause dfg thy (id, name, Axiom, th)
     2.9 -  in
    2.10 -      if isTaut cls then pairs else (name,cls)::pairs
    2.11 -  end;
    2.12 +fun add_axiom_clause dfg thy (th, (name, id)) =
    2.13 +  let val cls = make_clause dfg thy (id, name, Axiom, th) in
    2.14 +    not (isTaut cls) ? cons (name, cls)
    2.15 +  end
    2.16  
    2.17 -fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
    2.18 +fun make_axiom_clauses dfg thy clauses =
    2.19 +  fold (add_axiom_clause dfg thy) clauses []
    2.20  
    2.21  fun make_conjecture_clauses_aux _ _ _ [] = []
    2.22    | make_conjecture_clauses_aux dfg thy n (th::ths) =
    2.23 @@ -341,51 +341,51 @@
    2.24  
    2.25  (** For DFG format: accumulate function and predicate declarations **)
    2.26  
    2.27 -fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
    2.28 +fun add_types tvars = fold add_fol_type_funcs tvars
    2.29  
    2.30 -fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) =
    2.31 +fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars))
    2.32 +              (funcs, preds) =
    2.33        if c = "equal" then
    2.34 -        (addtypes tvars funcs, preds)
    2.35 +        (add_types tvars funcs, preds)
    2.36        else
    2.37          let val arity = min_arity_of cma c
    2.38              val ntys = if not full_types then length tvars else 0
    2.39              val addit = Symtab.update(c, arity+ntys)
    2.40          in
    2.41 -            if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
    2.42 -            else (addtypes tvars funcs, addit preds)
    2.43 +            if needs_hBOOL cnh c then (add_types tvars (addit funcs), preds)
    2.44 +            else (add_types tvars funcs, addit preds)
    2.45          end
    2.46 -  | add_decls _ (CombVar (_,ctp), (funcs, preds)) =
    2.47 -      (add_foltype_funcs (ctp,funcs), preds)
    2.48 -  | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
    2.49 +  | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
    2.50 +      (add_fol_type_funcs ctp funcs, preds)
    2.51 +  | add_decls params (CombApp (P, Q)) decls =
    2.52 +      decls |> add_decls params P |> add_decls params Q
    2.53  
    2.54 -fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
    2.55 +fun add_literal_decls params (Literal (_, c)) = add_decls params c
    2.56  
    2.57 -fun add_clause_decls params (HOLClause {literals, ...}, decls) =
    2.58 -    List.foldl (add_literal_decls params) decls literals
    2.59 +fun add_clause_decls params (HOLClause {literals, ...}) decls =
    2.60 +    fold (add_literal_decls params) literals decls
    2.61      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
    2.62  
    2.63  fun decls_of_clauses params clauses arity_clauses =
    2.64 -  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
    2.65 -      val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
    2.66 -      val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
    2.67 -  in
    2.68 -      (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
    2.69 -       Symtab.dest predtab)
    2.70 -  end;
    2.71 +  let val functab = init_functab |> Symtab.update (type_wrapper, 2)
    2.72 +                                 |> Symtab.update ("hAPP", 2)
    2.73 +      val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
    2.74 +      val (functab, predtab) =
    2.75 +        (functab, predtab) |> fold (add_clause_decls params) clauses
    2.76 +                           |>> fold add_arity_clause_funcs arity_clauses
    2.77 +  in (Symtab.dest functab, Symtab.dest predtab) end
    2.78  
    2.79 -fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
    2.80 -  List.foldl add_type_sort_preds preds ctypes_sorts
    2.81 +fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds =
    2.82 +  fold add_type_sort_preds ctypes_sorts preds
    2.83    handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
    2.84  
    2.85  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
    2.86  fun preds_of_clauses clauses clsrel_clauses arity_clauses =
    2.87 -    Symtab.dest
    2.88 -        (List.foldl add_classrel_clause_preds
    2.89 -               (List.foldl add_arity_clause_preds
    2.90 -                      (List.foldl add_clause_preds Symtab.empty clauses)
    2.91 -                      arity_clauses)
    2.92 -               clsrel_clauses)
    2.93 -
    2.94 +  Symtab.empty
    2.95 +  |> fold add_clause_preds clauses
    2.96 +  |> fold add_arity_clause_preds arity_clauses
    2.97 +  |> fold add_classrel_clause_preds clsrel_clauses
    2.98 +  |> Symtab.dest
    2.99  
   2.100  (**********************************************************************)
   2.101  (* write clauses to files                                             *)
   2.102 @@ -395,20 +395,17 @@
   2.103    Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
   2.104                 ("c_COMBS", 0)];
   2.105  
   2.106 -fun count_combterm (CombConst ((c, _), _, _), ct) =
   2.107 -     (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   2.108 -                               | SOME n => Symtab.update (c,n+1) ct)
   2.109 -  | count_combterm (CombVar _, ct) = ct
   2.110 -  | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
   2.111 +fun count_combterm (CombConst ((c, _), _, _)) =
   2.112 +    Symtab.map_entry c (Integer.add 1)
   2.113 +  | count_combterm (CombVar _) = I
   2.114 +  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   2.115  
   2.116 -fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   2.117 +fun count_literal (Literal (_, t)) = count_combterm t
   2.118  
   2.119 -fun count_clause (HOLClause {literals, ...}, ct) =
   2.120 -  List.foldl count_literal ct literals;
   2.121 +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   2.122  
   2.123 -fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
   2.124 -  if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
   2.125 -  else ct;
   2.126 +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
   2.127 +  member (op =) user_lemmas axiom_name ? fold count_literal literals
   2.128  
   2.129  fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
   2.130  
   2.131 @@ -418,8 +415,8 @@
   2.132    else
   2.133      let
   2.134          val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
   2.135 -        val ct0 = List.foldl count_clause init_counters conjectures
   2.136 -        val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
   2.137 +        val ct = init_counters |> fold count_clause conjectures
   2.138 +                               |> fold (count_user_clause user_lemmas) axclauses
   2.139          fun needed c = the (Symtab.lookup ct c) > 0
   2.140          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   2.141                   then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
   2.142 @@ -476,6 +473,10 @@
   2.143       in (const_min_arity, const_needs_hBOOL) end
   2.144    else (Symtab.empty, Symtab.empty);
   2.145  
   2.146 +fun header () =
   2.147 +  "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
   2.148 +  "% " ^ timestamp () ^ "\n"
   2.149 +
   2.150  (* TPTP format *)
   2.151  
   2.152  fun write_tptp_file debug full_types file clauses =
   2.153 @@ -489,7 +490,7 @@
   2.154      val params = (full_types, cma, cnh)
   2.155      val ((conjecture_clss, tfree_litss), pool) =
   2.156        pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   2.157 -    val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   2.158 +    val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
   2.159      val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
   2.160                                     pool
   2.161      val classrel_clss = map tptp_classrel_clause classrel_clauses
   2.162 @@ -498,8 +499,7 @@
   2.163                                         helper_clauses pool
   2.164      val _ =
   2.165        File.write_list file (
   2.166 -        "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
   2.167 -        "% " ^ timestamp () ^ "\n" ::
   2.168 +        header () ::
   2.169          section "Relevant fact" ax_clss @
   2.170          section "Type variable" tfree_clss @
   2.171          section "Conjecture" conjecture_clss @
   2.172 @@ -526,10 +526,11 @@
   2.173      val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
   2.174      val (helper_clauses_strs, pool) =
   2.175        pool_map (apfst fst oo dfg_clause params) helper_clauses pool
   2.176 -    val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   2.177 +    val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   2.178      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   2.179      val _ =
   2.180        File.write_list file (
   2.181 +        header () ::
   2.182          string_of_start probname ::
   2.183          string_of_descrip probname ::
   2.184          string_of_symbols (string_of_funcs funcs)