# HG changeset patch # User blanchet # Date 1271663611 -7200 # Node ID 0e4a01f3e7d3210c3577246e37038f29c4d6fd1c # Parent 4d220994f30ba5927dc68598614fb396bf1d66f9 get rid of "List.foldl" + add timestamp to SPASS diff -r 4d220994f30b -r 0e4a01f3e7d3 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Apr 19 07:38:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Apr 19 09:53:31 2010 +0200 @@ -4,7 +4,7 @@ Storing/printing FOL clauses and arity clauses. Typed equality is treated differently. -FIXME: combine with res_hol_clause! +FIXME: combine with sledgehammer_hol_clause! *) signature SLEDGEHAMMER_FOL_CLAUSE = @@ -57,12 +57,14 @@ val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list - val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table - val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table + val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table + val add_classrel_clause_preds : + classrel_clause -> int Symtab.table -> int Symtab.table val class_of_arityLit: arLit -> class - val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table - val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table - val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table + val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table + val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table + val add_arity_clause_funcs: + arity_clause -> int Symtab.table -> int Symtab.table val init_functab: int Symtab.table val dfg_sign: bool -> string -> string val dfg_of_typeLit: bool -> type_literal -> string @@ -102,7 +104,7 @@ val tconst_prefix = "tc_"; val class_prefix = "class_"; -fun union_all xss = List.foldl (uncurry (union (op =))) [] xss; +fun union_all xss = fold (union (op =)) xss [] (* Provide readable names for the more common symbolic functions *) val const_trans_table = @@ -315,7 +317,7 @@ | pred_of_sort (LTFree (s,ty)) = (s,1) (*Given a list of sorted type variables, return a list of type literals.*) -fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts); +fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) [] (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a @@ -373,11 +375,11 @@ (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) fun class_pairs thy [] supers = [] | class_pairs thy subs supers = - let val class_less = Sorts.class_less(Sign.classes_of thy) - fun add_super sub (super,pairs) = - if class_less (sub,super) then (sub,super)::pairs else pairs - fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers - in List.foldl add_supers [] subs end; + let + val class_less = Sorts.class_less (Sign.classes_of thy) + fun add_super sub super = class_less (sub, super) ? cons (sub, super) + fun add_supers sub = fold (add_super sub) supers + in fold add_supers subs [] end fun make_classrel_clause (sub,super) = ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, @@ -402,18 +404,18 @@ arity_clause dfg (class::seen) n (tcons,ars) fun multi_arity_clause dfg [] = [] - | multi_arity_clause dfg ((tcons,ars) :: tc_arlists) = - arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists + | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) = + arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy provided its arguments have the corresponding sorts.*) fun type_class_pairs thy tycons classes = let val alg = Sign.classes_of thy - fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class] - fun add_class tycon (class,pairs) = - (class, domain_sorts(tycon,class))::pairs - handle Sorts.CLASS_ERROR _ => pairs - fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes) + fun domain_sorts tycon = Sorts.mg_domain alg tycon o single + fun add_class tycon class = + cons (class, domain_sorts tycon class) + handle Sorts.CLASS_ERROR _ => I + fun try_classes tycon = (tycon, fold (add_class tycon) classes []) in map try_classes tycons end; (*Proving one (tycon, class) membership may require proving others, so iterate.*) @@ -435,35 +437,35 @@ (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong function (it flags repeated declarations of a function, even with the same arity)*) -fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs; +fun update_many keypairs = fold Symtab.update keypairs -fun add_type_sort_preds (T, preds) = - update_many (preds, map pred_of_sort (sorts_on_typs T)); +val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs -fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) = - Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); +fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) = + Symtab.update (subclass, 1) #> Symtab.update (superclass, 1) fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass | class_of_arityLit (TVarLit (tclass, _)) = tclass; -fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) = - let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits) - fun upd (class,preds) = Symtab.update (class,1) preds - in List.foldl upd preds classes end; +fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) = + let + val classes = map (make_type_class o class_of_arityLit) + (conclLit :: premLits) + in fold (Symtab.update o rpair 1) classes end; (*** Find occurrences of functions in clauses ***) -fun add_foltype_funcs (TyVar _, funcs) = funcs - | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs - | add_foltype_funcs (TyConstr ((s, _), tys), funcs) = - List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys; +fun add_fol_type_funcs (TyVar _) = I + | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0) + | add_fol_type_funcs (TyConstr ((s, _), tys)) = + Symtab.update (s, length tys) #> fold add_fol_type_funcs tys (*TFrees are recorded as constants*) fun add_type_sort_funcs (TVar _, funcs) = funcs | add_type_sort_funcs (TFree (a, _), funcs) = Symtab.update (make_fixed_type_var a, 0) funcs -fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) = +fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs = let val TConsLit (_, tcons, tvars) = conclLit in Symtab.update (tcons, length tvars) funcs end; diff -r 4d220994f30b -r 0e4a01f3e7d3 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 19 07:38:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Apr 19 09:53:31 2010 +0200 @@ -174,13 +174,13 @@ end; -fun add_axiom_clause dfg thy ((th,(name,id)), pairs) = - let val cls = make_clause dfg thy (id, name, Axiom, th) - in - if isTaut cls then pairs else (name,cls)::pairs - end; +fun add_axiom_clause dfg thy (th, (name, id)) = + let val cls = make_clause dfg thy (id, name, Axiom, th) in + not (isTaut cls) ? cons (name, cls) + end -fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) []; +fun make_axiom_clauses dfg thy clauses = + fold (add_axiom_clause dfg thy) clauses [] fun make_conjecture_clauses_aux _ _ _ [] = [] | make_conjecture_clauses_aux dfg thy n (th::ths) = @@ -341,51 +341,51 @@ (** For DFG format: accumulate function and predicate declarations **) -fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars; +fun add_types tvars = fold add_fol_type_funcs tvars -fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) = +fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars)) + (funcs, preds) = if c = "equal" then - (addtypes tvars funcs, preds) + (add_types tvars funcs, preds) else let val arity = min_arity_of cma c val ntys = if not full_types then length tvars else 0 val addit = Symtab.update(c, arity+ntys) in - if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds) - else (addtypes tvars funcs, addit preds) + if needs_hBOOL cnh c then (add_types tvars (addit funcs), preds) + else (add_types tvars funcs, addit preds) end - | add_decls _ (CombVar (_,ctp), (funcs, preds)) = - (add_foltype_funcs (ctp,funcs), preds) - | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); + | add_decls _ (CombVar (_, ctp)) (funcs, preds) = + (add_fol_type_funcs ctp funcs, preds) + | add_decls params (CombApp (P, Q)) decls = + decls |> add_decls params P |> add_decls params Q -fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls); +fun add_literal_decls params (Literal (_, c)) = add_decls params c -fun add_clause_decls params (HOLClause {literals, ...}, decls) = - List.foldl (add_literal_decls params) decls literals +fun add_clause_decls params (HOLClause {literals, ...}) decls = + fold (add_literal_decls params) literals decls handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") fun decls_of_clauses params clauses arity_clauses = - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab) - val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty - val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) - in - (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses), - Symtab.dest predtab) - end; + let val functab = init_functab |> Symtab.update (type_wrapper, 2) + |> Symtab.update ("hAPP", 2) + val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1) + val (functab, predtab) = + (functab, predtab) |> fold (add_clause_decls params) clauses + |>> fold add_arity_clause_funcs arity_clauses + in (Symtab.dest functab, Symtab.dest predtab) end -fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) = - List.foldl add_type_sort_preds preds ctypes_sorts +fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds = + fold add_type_sort_preds ctypes_sorts preds handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") (*Higher-order clauses have only the predicates hBOOL and type classes.*) fun preds_of_clauses clauses clsrel_clauses arity_clauses = - Symtab.dest - (List.foldl add_classrel_clause_preds - (List.foldl add_arity_clause_preds - (List.foldl add_clause_preds Symtab.empty clauses) - arity_clauses) - clsrel_clauses) - + Symtab.empty + |> fold add_clause_preds clauses + |> fold add_arity_clause_preds arity_clauses + |> fold add_classrel_clause_preds clsrel_clauses + |> Symtab.dest (**********************************************************************) (* write clauses to files *) @@ -395,20 +395,17 @@ Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0), ("c_COMBS", 0)]; -fun count_combterm (CombConst ((c, _), _, _), ct) = - (case Symtab.lookup ct c of NONE => ct (*no counter*) - | SOME n => Symtab.update (c,n+1) ct) - | count_combterm (CombVar _, ct) = ct - | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); +fun count_combterm (CombConst ((c, _), _, _)) = + Symtab.map_entry c (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 -fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); +fun count_literal (Literal (_, t)) = count_combterm t -fun count_clause (HOLClause {literals, ...}, ct) = - List.foldl count_literal ct literals; +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) = - if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals - else ct; +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) = + member (op =) user_lemmas axiom_name ? fold count_literal literals fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname @@ -418,8 +415,8 @@ else let val axclauses = map #2 (make_axiom_clauses dfg thy axcls) - val ct0 = List.foldl count_clause init_counters conjectures - val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses + val ct = init_counters |> fold count_clause conjectures + |> fold (count_user_clause user_lemmas) axclauses fun needed c = the (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}] @@ -476,6 +473,10 @@ in (const_min_arity, const_needs_hBOOL) end else (Symtab.empty, Symtab.empty); +fun header () = + "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ + "% " ^ timestamp () ^ "\n" + (* TPTP format *) fun write_tptp_file debug full_types file clauses = @@ -489,7 +490,7 @@ val params = (full_types, cma, cnh) val ((conjecture_clss, tfree_litss), pool) = pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip - val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) + val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss []) val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses pool val classrel_clss = map tptp_classrel_clause classrel_clauses @@ -498,8 +499,7 @@ helper_clauses pool val _ = File.write_list file ( - "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ - "% " ^ timestamp () ^ "\n" :: + header () :: section "Relevant fact" ax_clss @ section "Type variable" tfree_clss @ section "Conjecture" conjecture_clss @ @@ -526,10 +526,11 @@ val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) val (helper_clauses_strs, pool) = pool_map (apfst fst oo dfg_clause params) helper_clauses pool - val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses + val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses val _ = File.write_list file ( + header () :: string_of_start probname :: string_of_descrip probname :: string_of_symbols (string_of_funcs funcs)