# HG changeset patch # User wenzelm # Date 1256681530 -3600 # Node ID 03c08ce703bf891dcbaa6a7358f9050a283be17f # Parent b8d3b7196fe748724f5123c38e6a9f2458395464# Parent 46e47aa1558fe213b8bffde467ea89985cb6852c merged diff -r b8d3b7196fe7 -r 03c08ce703bf src/FOLP/simp.ML --- a/src/FOLP/simp.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/FOLP/simp.ML Tue Oct 27 23:12:10 2009 +0100 @@ -254,13 +254,13 @@ val insert_thms = fold_rev insert_thm_warn; -fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = +fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let val thms = mk_simps thm in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} end; -val op addrews = Library.foldl addrew; +fun ss addrews thms = fold addrew thms ss; fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = let val congs' = thms @ congs; @@ -287,7 +287,7 @@ mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} end; -fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = +fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let fun find((p as (th,ths))::ps',ps) = if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) | find([],simps') = @@ -298,7 +298,7 @@ simps = simps', simp_net = delete_thms thms simp_net } end; -val op delrews = Library.foldl delrew; +fun ss delrews thms = fold delrew thms ss; fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Import/shuffler.ML Tue Oct 27 23:12:10 2009 +0100 @@ -248,16 +248,16 @@ val tvars = OldTerm.term_tvars t val tfree_names = OldTerm.add_term_tfree_names(t,[]) val (type_inst,_) = - Library.foldl (fn ((inst,used),(w as (v,_),S)) => + fold (fn (w as (v,_), S) => fn (inst, used) => let val v' = Name.variant used v in ((w,TFree(v',S))::inst,v'::used) end) - (([],tfree_names),tvars) + tvars ([], tfree_names) val t' = subst_TVars type_inst t in - (t',map (fn (w,TFree(v,S)) => (v,TVar(w,S)) + (t', map (fn (w,TFree(v,S)) => (v,TVar(w,S)) | _ => error "Internal error in Shuffler.freeze_thaw") type_inst) end diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Matrix/cplex/CplexMatrixConverter.ML --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Tue Oct 27 23:12:10 2009 +0100 @@ -75,7 +75,7 @@ set_elem vec (s2i v) (if positive then num else "-"^num) | setprod _ _ _ = raise (Converter "term is not a normed product") - fun sum2vec (cplexSum ts) = Library.foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts) + fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector | sum2vec t = setprod empty_vector true t fun constrs2Ab j A b [] = (A, b) @@ -100,9 +100,9 @@ fun convert_results (cplex.Optimal (opt, entries)) name2index = let - fun setv (v, (name, value)) = (matrix_builder.set_elem v (name2index name) value) + fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value in - (opt, Library.foldl setv (matrix_builder.empty_vector, entries)) + (opt, fold setv entries (matrix_builder.empty_vector)) end | convert_results _ _ = raise (Converter "No optimal result") diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Tue Oct 27 23:12:10 2009 +0100 @@ -28,8 +28,8 @@ val goal_thm_of : Proof.state -> thm val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool - val theorems_in_proof_term : Thm.thm -> Thm.thm list - val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list + val theorems_in_proof_term : thm -> thm list + val theorems_of_sucessful_proof : Toplevel.state option -> thm list val get_setting : (string * string) list -> string * string -> string val get_int_setting : (string * string) list -> string * int -> int val cpu_time : ('a -> 'b) -> 'a -> 'b * int diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Tue Oct 27 23:12:10 2009 +0100 @@ -202,15 +202,15 @@ val atoms = atoms_of thy; - fun prep_constr ((constrs, sorts), (cname, cargs, mx)) = - let val (cargs', sorts') = Library.foldl (prep_typ tmp_thy) (([], sorts), cargs) + fun prep_constr (cname, cargs, mx) (constrs, sorts) = + let val (cargs', sorts') = fold_map (prep_typ tmp_thy) cargs sorts in (constrs @ [(cname, cargs', mx)], sorts') end - fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) = - let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs) + fun prep_dt_spec (tvs, tname, mx, constrs) (dts, sorts) = + let val (constrs', sorts') = fold prep_constr constrs ([], sorts) in (dts @ [(tvs, tname, mx, constrs')], sorts') end - val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts); + val (dts', sorts) = fold prep_dt_spec dts ([], []); val tyvars = map (map (fn s => (s, the (AList.lookup (op =) sorts s))) o #1) dts'; @@ -770,8 +770,8 @@ val full_new_type_names = map (Sign.full_bname thy) new_type_names; - fun make_constr_def tname T T' ((thy, defs, eqns), - (((cname_rep, _), (cname, cargs)), (cname', mx))) = + fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx)) + (thy, defs, eqns) = let fun constr_arg ((dts, dt), (j, l_args, r_args)) = let @@ -805,22 +805,24 @@ (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] in (thy', defs @ [def_thm], eqns @ [eqn]) end; - fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)), - (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) = + fun dt_constr_defs ((((((_, (_, _, constrs)), + (_, (_, _, constrs'))), tname), T), T'), constr_syntax) (thy, defs, eqns, dist_lemmas) = let val rep_const = cterm_of thy (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T')); - val dist = Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); - val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T') - ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax) + val dist = + Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); + val (thy', defs', eqns') = fold (make_constr_def tname T T') + (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, []) in (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) end; - val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs - ((thy7, [], [], []), List.take (descr, length new_type_names) ~~ + val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs + (List.take (descr, length new_type_names) ~~ List.take (pdescr, length new_type_names) ~~ - new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax); + new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax) + (thy7, [], [], []); val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs val rep_inject_thms = map (#Rep_inject o fst) typedefs @@ -1031,7 +1033,7 @@ (**** weak induction theorem ****) - fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) = + fun mk_indrule_lemma (((i, _), T), U) (prems, concls) = let val Rep_t = Const (List.nth (rep_names, i), T --> U) $ mk_Free "x" T i; @@ -1045,7 +1047,7 @@ end; val (indrule_lemma_prems, indrule_lemma_concls) = - Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs')); + fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []); val indrule_lemma = Goal.prove_global thy8 [] [] (Logic.mk_implies @@ -1455,8 +1457,8 @@ (* FIXME: avoid collisions with other variable names? *) val rec_ctxt = Free ("z", fsT'); - fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems', - rec_eq_prems, l), ((cname, cargs), idxs)) = + fun make_rec_intr T p rec_set ((cname, cargs), idxs) + (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) = let val Ts = map (typ_of_dtyp descr'' sorts) cargs; val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts; @@ -1500,9 +1502,10 @@ end; val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) = - Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) => - Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d')) - (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets'); + fold (fn ((((d, d'), T), p), rec_set) => + fold (make_rec_intr T p rec_set) (#3 (snd d) ~~ snd d')) + (descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets') + ([], [], [], [], 0); val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = thy10 |> diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Tue Oct 27 23:12:10 2009 +0100 @@ -301,9 +301,9 @@ val ps = Logic.strip_params (term_of goal); val Ts = rev (map snd ps); val vs = collect_vars 0 x []; - val s = Library.foldr (fn (v, s) => + val s = fold_rev (fn v => fn s => HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) - (vs, HOLogic.unit); + vs HOLogic.unit; val s' = list_abs (ps, Const ("Nominal.supp", fastype_of1 (Ts, s) --> snd (split_last (binder_types T)) --> HOLogic.boolT) $ s); @@ -343,9 +343,9 @@ val ps = Logic.strip_params (term_of goal); val Ts = rev (map snd ps); val vs = collect_vars 0 t []; - val s = Library.foldr (fn (v, s) => + val s = fold_rev (fn v => fn s => HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) - (vs, HOLogic.unit); + vs HOLogic.unit; val s' = list_abs (ps, Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s); val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/SMT/Tools/smt_normalize.ML --- a/src/HOL/SMT/Tools/smt_normalize.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Tue Oct 27 23:12:10 2009 +0100 @@ -14,8 +14,8 @@ signature SMT_NORMALIZE = sig val normalize_rule: Proof.context -> thm -> thm - val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm - val discharge_definition: Thm.cterm -> thm -> thm + val instantiate_free: cterm * cterm -> thm -> thm + val discharge_definition: cterm -> thm -> thm val trivial_let: Proof.context -> thm list -> thm list val positive_numerals: Proof.context -> thm list -> thm list @@ -33,8 +33,7 @@ AddFunUpdRules | AddAbsMinMaxRules - val normalize: config list -> Proof.context -> thm list -> - Thm.cterm list * thm list + val normalize: config list -> Proof.context -> thm list -> cterm list * thm list val setup: theory -> theory end diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/SMT/Tools/z3_proof.ML --- a/src/HOL/SMT/Tools/z3_proof.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/SMT/Tools/z3_proof.ML Tue Oct 27 23:12:10 2009 +0100 @@ -48,7 +48,7 @@ datatype context = Context of { Ttab: typ Symtab.table, - ttab: Thm.cterm Symtab.table, + ttab: cterm Symtab.table, etab: T.preterm Inttab.table, ptab: R.proof Inttab.table, nctxt: Name.context } diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/SMT/Tools/z3_proof_rules.ML --- a/src/HOL/SMT/Tools/z3_proof_rules.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Tue Oct 27 23:12:10 2009 +0100 @@ -13,7 +13,7 @@ (*proof reconstruction*) type proof - val make_proof: rule -> int list -> Thm.cterm * Thm.cterm list -> proof + val make_proof: rule -> int list -> cterm * cterm list -> proof val prove: Proof.context -> thm list option -> proof Inttab.table -> int -> thm @@ -103,11 +103,11 @@ Unproved of { rule: rule, subs: int list, - prop: Thm.cterm, - vars: Thm.cterm list } | + prop: cterm, + vars: cterm list } | Sequent of { - hyps: Thm.cterm list, - vars: Thm.cterm list, + hyps: cterm list, + vars: cterm list, thm: theorem } fun make_proof r ps (ct, cvs) = Unproved {rule=r, subs=ps, prop=ct, vars=cvs} diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/SMT/Tools/z3_proof_terms.ML --- a/src/HOL/SMT/Tools/z3_proof_terms.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/SMT/Tools/z3_proof_terms.ML Tue Oct 27 23:12:10 2009 +0100 @@ -6,15 +6,15 @@ signature Z3_PROOF_TERMS = sig - val mk_prop: Thm.cterm -> Thm.cterm - val mk_meta_eq: Thm.cterm -> Thm.cterm -> Thm.cterm + val mk_prop: cterm -> cterm + val mk_meta_eq: cterm -> cterm -> cterm type preterm - val compile: theory -> Name.context -> preterm -> Thm.cterm * Thm.cterm list + val compile: theory -> Name.context -> preterm -> cterm * cterm list val mk_bound: theory -> int -> typ -> preterm - val mk_fun: Thm.cterm -> preterm list -> preterm + val mk_fun: cterm -> preterm list -> preterm val mk_forall: theory -> string * typ -> preterm -> preterm val mk_exists: theory -> string * typ -> preterm -> preterm @@ -73,8 +73,8 @@ datatype preterm = Preterm of { - cterm: Thm.cterm, - vars: (int * Thm.cterm) list } + cterm: cterm, + vars: (int * cterm) list } fun mk_preterm (ct, vs) = Preterm {cterm=ct, vars=vs} fun dest_preterm (Preterm {cterm, vars}) = (cterm, vars) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Oct 27 23:12:10 2009 +0100 @@ -29,8 +29,7 @@ val make_case : Proof.context -> DatatypeCase.config -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option - val read_typ: theory -> - (typ list * (string * sort) list) * string -> typ list * (string * sort) list + val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list val setup: theory -> theory end; @@ -160,23 +159,24 @@ (* prepare datatype specifications *) -fun read_typ thy ((Ts, sorts), str) = +fun read_typ thy str sorts = let val ctxt = ProofContext.init thy |> fold (Variable.declare_typ o TFree) sorts; val T = Syntax.read_typ ctxt str; - in (Ts @ [T], Term.add_tfreesT T sorts) end; + in (T, Term.add_tfreesT T sorts) end; -fun cert_typ sign ((Ts, sorts), raw_T) = +fun cert_typ sign raw_T sorts = let - val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle - TYPE (msg, _, _) => error msg; + val T = Type.no_tvars (Sign.certify_typ sign raw_T) + handle TYPE (msg, _, _) => error msg; val sorts' = Term.add_tfreesT T sorts; - in (Ts @ [T], + val _ = case duplicates (op =) (map fst sorts') of - [] => sorts' - | dups => error ("Inconsistent sort constraints for " ^ commas dups)) - end; + [] => () + | dups => error ("Inconsistent sort constraints for " ^ commas dups) + in (T, sorts') end; + (* case names *) @@ -460,8 +460,9 @@ let fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') = let - val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs); - val _ = (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of + val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts'; + val _ = + (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of [] => () | vs => error ("Extra type variables on rhs: " ^ commas vs)) in (constrs @ [(Sign.full_name_path tmp_thy tname' diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 27 23:12:10 2009 +0100 @@ -74,7 +74,7 @@ val get_rec_types : descr -> (string * sort) list -> typ list val interpret_construction : descr -> (string * sort) list -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a } - -> ((string * Term.typ list) * (string * 'a list) list) list + -> ((string * typ list) * (string * 'a list) list) list val check_nonempty : descr list -> unit val unfold_datatypes : theory -> descr -> (string * sort) list -> info Symtab.table -> @@ -255,9 +255,8 @@ (* find all non-recursive types in datatype description *) fun get_nonrec_types descr sorts = - map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) => - Library.foldl (fn (Ts', (_, cargs)) => - union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr)); + map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) => + fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []); (* get all recursive types in datatype description *) @@ -335,7 +334,7 @@ (* unfold a single constructor argument *) - fun unfold_arg ((i, Ts, descrs), T) = + fun unfold_arg T (i, Ts, descrs) = if is_rec_type T then let val (Us, U) = strip_dtyp T in if exists is_rec_type Us then @@ -353,19 +352,17 @@ (* unfold a constructor *) - fun unfold_constr ((i, constrs, descrs), (cname, cargs)) = - let val (i', cargs', descrs') = Library.foldl unfold_arg ((i, [], descrs), cargs) + fun unfold_constr (cname, cargs) (i, constrs, descrs) = + let val (i', cargs', descrs') = fold unfold_arg cargs (i, [], descrs) in (i', constrs @ [(cname, cargs')], descrs') end; (* unfold a single datatype *) - fun unfold_datatype ((i, dtypes, descrs), (j, (tname, tvars, constrs))) = - let val (i', constrs', descrs') = - Library.foldl unfold_constr ((i, [], descrs), constrs) - in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs') - end; + fun unfold_datatype (j, (tname, tvars, constrs)) (i, dtypes, descrs) = + let val (i', constrs', descrs') = fold unfold_constr constrs (i, [], descrs) + in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs') end; - val (i', descr', descrs) = Library.foldl unfold_datatype ((i, [],[]), descr); + val (i', descr', descrs) = fold unfold_datatype descr (i, [], []); in (descr' :: descrs, i') end; diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Tue Oct 27 23:12:10 2009 +0100 @@ -221,7 +221,7 @@ (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns)) (reccomb_names ~~ recTs ~~ rec_result_Ts); - fun make_primrec T comb_t ((ts, f::fs), (cname, cargs)) = + fun make_primrec T comb_t (cname, cargs) (ts, f::fs) = let val recs = List.filter is_rec_type cargs; val Ts = map (typ_of_dtyp descr' sorts) cargs; @@ -242,11 +242,12 @@ in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees), list_comb (f, frees @ reccombs')))], fs) - end + end; - in fst (Library.foldl (fn (x, ((dt, T), comb_t)) => - Library.foldl (make_primrec T comb_t) (x, #3 (snd dt))) - (([], rec_fns), descr' ~~ recTs ~~ reccombs)) + in + fold (fn ((dt, T), comb_t) => fold (make_primrec T comb_t) (#3 (snd dt))) + (descr' ~~ recTs ~~ reccombs) ([], rec_fns) + |> fst end; (****************** make terms of form t_case f1 ... fn *********************) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Oct 27 23:12:10 2009 +0100 @@ -207,7 +207,7 @@ (* constructor definitions *) - fun make_constr_def tname T n ((thy, defs, eqns, i), ((cname, cargs), (cname', mx))) = + fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) = let fun constr_arg (dt, (j, l_args, r_args)) = let val T = typ_of_dtyp descr' sorts dt; @@ -238,8 +238,8 @@ (* constructor definitions for datatype *) - fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas), - ((((_, (_, _, constrs)), tname), T), constr_syntax)) = + fun dt_constr_defs ((((_, (_, _, constrs)), tname), T), constr_syntax) + (thy, defs, eqns, rep_congs, dist_lemmas) = let val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong; val rep_const = cterm_of thy @@ -248,16 +248,18 @@ Drule.standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong); val dist = Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); - val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs)) - ((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax) + val (thy', defs', eqns', _) = fold ((make_constr_def tname T) (length constrs)) + (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1); in (Sign.parent_path thy', defs', eqns @ [eqns'], rep_congs @ [cong'], dist_lemmas @ [dist]) end; - val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs - ((thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []), - hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); + val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = + fold dt_constr_defs + (hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax) + (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []); + (*********** isomorphisms for new types (introduced by typedef) ***********) @@ -283,7 +285,7 @@ (* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *) (*---------------------------------------------------------------------*) - fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) = + fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) = let val argTs = map (typ_of_dtyp descr' sorts) cargs; val T = nth recTs k; @@ -291,7 +293,7 @@ val rep_const = Const (rep_name, T --> Univ_elT); val constr = Const (cname, argTs ---> T); - fun process_arg ks' ((i2, i2', ts, Ts), dt) = + fun process_arg ks' dt (i2, i2', ts, Ts) = let val T' = typ_of_dtyp descr' sorts dt; val (Us, U) = strip_type T' @@ -307,12 +309,12 @@ | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts)) end; - val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs); + val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []); val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1))); val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1))); val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i); - val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs); + val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []); val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) @@ -320,20 +322,20 @@ (* define isomorphisms for all mutually recursive datatypes in list ds *) - fun make_iso_defs (ds, (thy, char_thms)) = + fun make_iso_defs ds (thy, char_thms) = let val ks = map fst ds; val (_, (tname, _, _)) = hd ds; val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname); - fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = + fun process_dt (k, (tname, _, constrs)) (fs, eqns, isos) = let - val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs)) - ((fs, eqns, 1), constrs); + val (fs', eqns', _) = + fold (make_iso_def k ks (length constrs)) constrs (fs, eqns, 1); val iso = (nth recTs k, nth all_rep_names k) in (fs', eqns', isos @ [iso]) end; - val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); + val (fs, eqns, isos) = fold process_dt ds ([], [], []); val fTs = map fastype_of fs; val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"), Logic.mk_equals (Const (iso_name, T --> Univ_elT), @@ -349,8 +351,8 @@ in (thy', char_thms' @ char_thms) end; - val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs - (Sign.add_path big_name thy4, []) (tl descr)); + val (thy5, iso_char_thms) = apfst Theory.checkpoint (fold_rev make_iso_defs + (tl descr) (Sign.add_path big_name thy4, [])); (* prove isomorphism properties *) @@ -563,7 +565,7 @@ (map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded); val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded; - fun mk_indrule_lemma ((prems, concls), ((i, _), T)) = + fun mk_indrule_lemma ((i, _), T) (prems, concls) = let val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $ mk_Free "x" T i; @@ -582,7 +584,7 @@ end; val (indrule_lemma_prems, indrule_lemma_concls) = - Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); + fold mk_indrule_lemma (descr' ~~ recTs) ([], []); val cert = cterm_of thy6; diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Tue Oct 27 23:12:10 2009 +0100 @@ -189,12 +189,11 @@ in fun derive_init_eqs sgn rules eqs = let - val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) - eqs - fun countlist l = - (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l) + val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) eqs + fun countlist l = + rev (snd (fold (fn e => fn (i, L) => (i + 1, (e, i) :: L)) l (0, []))) in - maps (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths) + maps (fn (e, i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths) end; end; diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/choice_specification.ML Tue Oct 27 23:12:10 2009 +0100 @@ -165,7 +165,7 @@ val cnames = map (fst o dest_Const) proc_consts fun post_process (arg as (thy,thm)) = let - fun inst_all thy (thm,v) = + fun inst_all thy v thm = let val cv = cterm_of thy v val cT = ctyp_of_term cv @@ -174,7 +174,7 @@ thm RS spec' end fun remove_alls frees thm = - Library.foldl (inst_all (Thm.theory_of_thm thm)) (thm,frees) + fold (inst_all (Thm.theory_of_thm thm)) frees thm fun process_single ((name,atts),rew_imp,frees) args = let fun undo_imps thm = diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/hologic.ML Tue Oct 27 23:12:10 2009 +0100 @@ -638,8 +638,8 @@ val Ts = map snd vs; val t = Const (c, Ts ---> T); val tt = mk_prod (t, Abs ("u", unitT, reflect_term t)); - fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T); - in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end; + fun app (fT, (v, T)) t = valapp T fT $ t $ Free (v, termifyT T); + in fold app (mk_fTs Ts T ~~ vs) tt end; (* open state monads *) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Tue Oct 27 23:12:10 2009 +0100 @@ -41,7 +41,7 @@ fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ Display.string_of_thm_without_context thm); -fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g; +fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g; fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy => let @@ -72,7 +72,7 @@ Symtab.update (s, (AList.update Thm.eq_thm_prop (thm, (thyname_of s, nparms)) rules)), graph = List.foldr (uncurry (Graph.add_edge o pair s)) - (Library.foldl add_node (graph, s :: cs)) cs, + (fold add_node (s :: cs) graph) cs, eqns = eqns} thy end | _ => (warn thm; thy)) @@ -266,19 +266,22 @@ flat (separate [str ",", Pretty.brk 1] (map single xs)) @ [str ")"]); -fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of - NONE => ((names, (s, [s])::vs), s) - | SOME xs => let val s' = Name.variant names s in - ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end); +fun mk_v s (names, vs) = + (case AList.lookup (op =) vs s of + NONE => (s, (names, (s, [s])::vs)) + | SOME xs => + let val s' = Name.variant names s + in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end); -fun distinct_v (nvs, Var ((s, 0), T)) = - apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s)) - | distinct_v (nvs, t $ u) = +fun distinct_v (Var ((s, 0), T)) nvs = + let val (s', nvs') = mk_v s nvs + in (Var ((s', 0), T), nvs') end + | distinct_v (t $ u) nvs = let - val (nvs', t') = distinct_v (nvs, t); - val (nvs'', u') = distinct_v (nvs', u); - in (nvs'', t' $ u') end - | distinct_v x = x; + val (t', nvs') = distinct_v t nvs; + val (u', nvs'') = distinct_v u nvs'; + in (t' $ u', nvs'') end + | distinct_v t nvs = (t, nvs); fun is_exhaustive (Var _) = true | is_exhaustive (Const ("Pair", _) $ t $ u) = @@ -346,30 +349,29 @@ (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) (arg_vs ~~ iss); - fun check_constrt ((names, eqs), t) = - if is_constrt thy t then ((names, eqs), t) else + fun check_constrt t (names, eqs) = + if is_constrt thy t then (t, (names, eqs)) + else let val s = Name.variant names "x"; - in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end; + in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end; fun compile_eq (s, t) gr = apfst (Pretty.block o cons (str (s ^ " = ")) o single) (invoke_codegen thy defs dep module false t gr); val (in_ts, out_ts) = get_args is 1 ts; - val ((all_vs', eqs), in_ts') = - Library.foldl_map check_constrt ((all_vs, []), in_ts); + val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []); fun compile_prems out_ts' vs names [] gr = let - val (out_ps, gr2) = fold_map - (invoke_codegen thy defs dep module false) out_ts gr; + val (out_ps, gr2) = + fold_map (invoke_codegen thy defs dep module false) out_ts gr; val (eq_ps, gr3) = fold_map compile_eq eqs gr2; - val ((names', eqs'), out_ts'') = - Library.foldl_map check_constrt ((names, []), out_ts'); - val (nvs, out_ts''') = Library.foldl_map distinct_v - ((names', map (fn x => (x, [x])) vs), out_ts''); - val (out_ps', gr4) = fold_map - (invoke_codegen thy defs dep module false) (out_ts''') gr3; + val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []); + val (out_ts''', nvs) = + fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs); + val (out_ps', gr4) = + fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3; val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; in (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' @@ -379,15 +381,11 @@ | compile_prems out_ts vs names ps gr = let val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); - val SOME (p, mode as SOME (Mode (_, js, _))) = - select_mode_prem thy modes' vs' ps; + val SOME (p, mode as SOME (Mode (_, js, _))) = select_mode_prem thy modes' vs' ps; val ps' = filter_out (equal p) ps; - val ((names', eqs), out_ts') = - Library.foldl_map check_constrt ((names, []), out_ts); - val (nvs, out_ts'') = Library.foldl_map distinct_v - ((names', map (fn x => (x, [x])) vs), out_ts'); - val (out_ps, gr0) = fold_map - (invoke_codegen thy defs dep module false) out_ts'' gr; + val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []); + val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs); + val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr; val (eq_ps, gr1) = fold_map compile_eq eqs gr0; in (case p of @@ -480,19 +478,22 @@ fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs; fun constrain cs [] = [] - | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of - NONE => xs - | SOME xs' => inter (op =) xs' xs) :: constrain cs ys; + | constrain cs ((s, xs) :: ys) = + (s, + case AList.lookup (op =) cs (s : string) of + NONE => xs + | SOME xs' => inter (op =) xs' xs) :: constrain cs ys; fun mk_extra_defs thy defs gr dep names module ts = - Library.foldl (fn (gr, name) => + fold (fn name => fn gr => if name mem names then gr - else (case get_clauses thy name of + else + (case get_clauses thy name of NONE => gr | SOME (names, thyname, nparms, intrs) => mk_ind_def thy defs gr dep names (if_library thyname module) [] (prep_intrs intrs) nparms)) - (gr, fold Term.add_const_names ts []) + (fold Term.add_const_names ts []) gr and mk_ind_def thy defs gr dep names module modecs intrs nparms = add_edge_acyclic (hd names, dep) gr handle @@ -562,17 +563,16 @@ val (ts1, ts2) = chop k ts; val u = list_comb (Const (s, T), ts1); - fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) = - ((ts, mode), i+1) - | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1); + fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1) + | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1); val module' = if_library thyname module; val gr1 = mk_extra_defs thy defs (mk_ind_def thy defs gr dep names module' [] (prep_intrs intrs) k) dep names module' [u]; val (modes, _) = lookup_modes gr1 dep; - val (ts', is) = if is_query then - fst (Library.foldl mk_mode ((([], []), 1), ts2)) + val (ts', is) = + if is_query then fst (fold mk_mode ts2 (([], []), 1)) else (ts2, 1 upto length (binder_types T) - k); val mode = find_mode gr1 dep s u modes is; val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1; @@ -697,8 +697,9 @@ val setup = add_codegen "inductive" inductive_codegen #> - Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- - Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add)) + Attrib.setup @{binding code_ind} + (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- + Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add)) "introduction rules for executable predicates"; end; diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Oct 27 23:12:10 2009 +0100 @@ -271,7 +271,7 @@ fun rename tab = map (fn x => the_default x (AList.lookup op = tab x)); -fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) = +fun add_ind_realizer rsets intrs induct raw_induct elims vs thy = let val qualifier = Long_Name.qualifier (name_of_thm induct); val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts"); @@ -367,7 +367,7 @@ SOME (fst (fst (dest_Var (head_of P)))) else NONE) (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); - fun add_ind_realizer (thy, Ps) = + fun add_ind_realizer Ps thy = let val vs' = rename (map (pairself (fst o fst o dest_Var)) (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop @@ -426,13 +426,12 @@ let val (prem :: prems) = prems_of elim; fun reorder1 (p, (_, intr)) = - Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t) - (strip_all p, subtract (op =) params' (Term.add_vars (prop_of intr) [])); + fold (fn ((s, _), T) => Logic.all (Free (s, T))) + (subtract (op =) params' (Term.add_vars (prop_of intr) [])) + (strip_all p); fun reorder2 ((ivs, intr), i) = let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) []) - in Library.foldl (fn (t, x) => lambda (Var x) t) - (list_comb (Bound (i + length ivs), ivs), fs) - end; + in fold (lambda o Var) fs (list_comb (Bound (i + length ivs), ivs)) end; val p = Logic.list_implies (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim); val T' = Extraction.etype_of thy (vs @ Ps) [] p; @@ -465,7 +464,7 @@ (** add realizers to theory **) - val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps); + val thy4 = fold add_ind_realizer (subsets Ps) thy3; val thy5 = Extraction.add_realizers_i (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) => (name_of_thm rule, rule, rrule, rlz, @@ -474,10 +473,11 @@ val elimps = map_filter (fn ((s, intrs), p) => if s mem rsets then SOME (p, intrs) else NONE) (rss' ~~ (elims ~~ #elims ind_info)); - val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |> - add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var - (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, - elimps ~~ case_thms ~~ case_names ~~ dummies) + val thy6 = + fold (fn p as (((((elim, _), _), _), _), _) => + add_elim_realizer [] p #> + add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p) + (elimps ~~ case_thms ~~ case_names ~~ dummies) thy5; in Sign.restore_naming thy thy6 end; @@ -488,7 +488,7 @@ val vss = sort (int_ord o pairself length) (subsets (map fst (relevant_vars (concl_of (hd intrs))))) in - Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss) + fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy end fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/meson.ML Tue Oct 27 23:12:10 2009 +0100 @@ -462,14 +462,13 @@ (** Detecting repeated assumptions in a subgoal **) (*The stringtree detects repeated assumptions.*) -fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net; +fun ins_term t net = Net.insert_term (op aconv) (t, t) net; (*detects repetitions in a list of terms*) fun has_reps [] = false | has_reps [_] = false | has_reps [t,u] = (t aconv u) - | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) - handle Net.INSERT => true; + | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true; (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) fun TRYING_eq_assume_tac 0 st = Seq.single st diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/metis_tools.ML Tue Oct 27 23:12:10 2009 +0100 @@ -21,8 +21,6 @@ val trace = Unsynchronized.ref false; fun trace_msg msg = if ! trace then tracing (msg ()) else (); -structure Recon = ResReconstruct; - val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; datatype mode = FO | HO | FT (*first-order, higher-order, fully-typed*) @@ -211,14 +209,14 @@ | strip_happ args x = (x, args); fun fol_type_to_isa _ (Metis.Term.Var v) = - (case Recon.strip_prefix ResClause.tvar_prefix v of - SOME w => Recon.make_tvar w - | NONE => Recon.make_tvar v) + (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of + SOME w => ResReconstruct.make_tvar w + | NONE => ResReconstruct.make_tvar v) | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = - (case Recon.strip_prefix ResClause.tconst_prefix x of - SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys) + (case ResReconstruct.strip_prefix ResClause.tconst_prefix x of + SOME tc => Term.Type (ResReconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys) | NONE => - case Recon.strip_prefix ResClause.tfree_prefix x of + case ResReconstruct.strip_prefix ResClause.tfree_prefix x of SOME tf => mk_tfree ctxt tf | NONE => error ("fol_type_to_isa: " ^ x)); @@ -227,10 +225,10 @@ let val thy = ProofContext.theory_of ctxt val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case Recon.strip_prefix ResClause.tvar_prefix v of - SOME w => Type (Recon.make_tvar w) + (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of + SOME w => Type (ResReconstruct.make_tvar w) | NONE => - case Recon.strip_prefix ResClause.schematic_var_prefix v of + case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of SOME w => Term (mk_var (w, HOLogic.typeT)) | NONE => Term (mk_var (v, HOLogic.typeT)) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -247,14 +245,14 @@ and applic_to_tt ("=",ts) = Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case Recon.strip_prefix ResClause.const_prefix a of + case ResReconstruct.strip_prefix ResClause.const_prefix a of SOME b => - let val c = Recon.invert_const b - val ntypes = Recon.num_typargs thy c + let val c = ResReconstruct.invert_const b + val ntypes = ResReconstruct.num_typargs thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts val tys = types_of (List.take(tts,ntypes)) - val ntyargs = Recon.num_typargs thy c + val ntyargs = ResReconstruct.num_typargs thy c in if length tys = ntyargs then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ @@ -265,13 +263,14 @@ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case Recon.strip_prefix ResClause.tconst_prefix a of - SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts))) + case ResReconstruct.strip_prefix ResClause.tconst_prefix a of + SOME b => + Type (Term.Type (ResReconstruct.invert_type_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case Recon.strip_prefix ResClause.tfree_prefix a of + case ResReconstruct.strip_prefix ResClause.tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case Recon.strip_prefix ResClause.fixed_var_prefix a of + case ResReconstruct.strip_prefix ResClause.fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -282,16 +281,16 @@ fun fol_term_to_hol_FT ctxt fol_tm = let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = - (case Recon.strip_prefix ResClause.schematic_var_prefix v of + (case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = - (case Recon.strip_prefix ResClause.const_prefix x of - SOME c => Const (Recon.invert_const c, dummyT) + (case ResReconstruct.strip_prefix ResClause.const_prefix x of + SOME c => Const (ResReconstruct.invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case Recon.strip_prefix ResClause.fixed_var_prefix x of + case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of SOME v => Free (v, fol_type_to_isa ctxt ty) | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = @@ -302,13 +301,15 @@ | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = - (case Recon.strip_prefix ResClause.const_prefix x of - SOME c => Const (Recon.invert_const c, dummyT) + (case ResReconstruct.strip_prefix ResClause.const_prefix x of + SOME c => Const (ResReconstruct.invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case Recon.strip_prefix ResClause.fixed_var_prefix x of + case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t)) - | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t) + | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); + fol_term_to_hol_RAW ctxt t)) + | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); + fol_term_to_hol_RAW ctxt t) in cvt fol_tm end; fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt @@ -382,9 +383,9 @@ " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = - case Recon.strip_prefix ResClause.schematic_var_prefix a of + case ResReconstruct.strip_prefix ResClause.schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case Recon.strip_prefix ResClause.tvar_prefix a of + | NONE => case ResReconstruct.strip_prefix ResClause.tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) @@ -451,7 +452,7 @@ in cterm_instantiate [(refl_x, c_t)] REFL_THM end; fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size thy (Const (c, _)) = (ResReconstruct.num_typargs thy c handle TYPE _ => 0) | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) @@ -522,7 +523,7 @@ val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) - (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) + (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' end; val factor = Seq.hd o distinct_subgoals_tac; @@ -588,7 +589,7 @@ (* ------------------------------------------------------------------------- *) type logic_map = - {axioms : (Metis.Thm.thm * Thm.thm) list, + {axioms : (Metis.Thm.thm * thm) list, tfrees : ResClause.type_literal list}; fun const_in_metis c (pred, tm_list) = diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/prop_logic.ML Tue Oct 27 23:12:10 2009 +0100 @@ -37,9 +37,9 @@ val eval : (int -> bool) -> prop_formula -> bool (* semantics *) (* propositional representation of HOL terms *) - val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table + val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table (* HOL term representation of propositional formulae *) - val term_of_prop_formula : prop_formula -> Term.term + val term_of_prop_formula : prop_formula -> term end; structure PropLogic : PROP_LOGIC = diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/quickcheck_generators.ML Tue Oct 27 23:12:10 2009 +0100 @@ -8,7 +8,7 @@ type seed = Random_Engine.seed val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) - -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed + -> seed -> (('a -> 'b) * (unit -> term)) * seed val ensure_random_typecopy: string -> theory -> theory val random_aux_specification: string -> string -> term list -> local_theory -> local_theory val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Oct 27 23:12:10 2009 +0100 @@ -65,9 +65,9 @@ exception EQN of string * typ * string; -fun cycle g (xs, x : string) = +fun cycle g x xs = if member (op =) xs x then xs - else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x))); + else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs); fun add_rec_funs thy defs dep module eqs gr = let @@ -107,7 +107,7 @@ val gr1 = add_edge (dname, dep) (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ; - val xs = cycle gr2 ([], dname); + val xs = cycle gr2 dname []; val cs = map (fn x => case get_node gr2 x of (SOME (EQN (s, T, _)), _, _) => (s, T) | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/refute.ML Tue Oct 27 23:12:10 2009 +0100 @@ -25,16 +25,15 @@ exception MAXVARS_EXCEEDED - val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> + val add_interpreter : string -> (theory -> model -> arguments -> term -> (interpretation * model * arguments) option) -> theory -> theory - val add_printer : string -> (theory -> model -> Term.typ -> - interpretation -> (int -> bool) -> Term.term option) -> theory -> theory + val add_printer : string -> (theory -> model -> typ -> + interpretation -> (int -> bool) -> term option) -> theory -> theory - val interpret : theory -> model -> arguments -> Term.term -> + val interpret : theory -> model -> arguments -> term -> (interpretation * model * arguments) - val print : theory -> model -> Term.typ -> interpretation -> - (int -> bool) -> Term.term + val print : theory -> model -> typ -> interpretation -> (int -> bool) -> term val print_model : theory -> model -> (int -> bool) -> string (* ------------------------------------------------------------------------- *) @@ -46,10 +45,10 @@ val get_default_params : theory -> (string * string) list val actual_params : theory -> (string * string) list -> params - val find_model : theory -> params -> Term.term -> bool -> unit + val find_model : theory -> params -> term -> bool -> unit (* tries to find a model for a formula: *) - val satisfy_term : theory -> (string * string) list -> Term.term -> unit + val satisfy_term : theory -> (string * string) list -> term -> unit (* tries to find a model that refutes a formula: *) val refute_term : theory -> (string * string) list -> term -> unit val refute_goal : theory -> (string * string) list -> thm -> int -> unit @@ -60,20 +59,18 @@ (* Additional functions used by Nitpick (to be factored out) *) (* ------------------------------------------------------------------------- *) - val close_form : Term.term -> Term.term - val get_classdef : theory -> string -> (string * Term.term) option - val norm_rhs : Term.term -> Term.term - val get_def : theory -> string * Term.typ -> (string * Term.term) option - val get_typedef : theory -> Term.typ -> (string * Term.term) option - val is_IDT_constructor : theory -> string * Term.typ -> bool - val is_IDT_recursor : theory -> string * Term.typ -> bool - val is_const_of_class: theory -> string * Term.typ -> bool - val monomorphic_term : Type.tyenv -> Term.term -> Term.term - val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term - val string_of_typ : Term.typ -> string - val typ_of_dtyp : - Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp - -> Term.typ + val close_form : term -> term + val get_classdef : theory -> string -> (string * term) option + val norm_rhs : term -> term + val get_def : theory -> string * typ -> (string * term) option + val get_typedef : theory -> typ -> (string * term) option + val is_IDT_constructor : theory -> string * typ -> bool + val is_IDT_recursor : theory -> string * typ -> bool + val is_const_of_class: theory -> string * typ -> bool + val monomorphic_term : Type.tyenv -> term -> term + val specialize_type : theory -> (string * typ) -> term -> term + val string_of_typ : typ -> string + val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ end; (* signature REFUTE *) structure Refute : REFUTE = @@ -185,7 +182,7 @@ (* ------------------------------------------------------------------------- *) type model = - (Term.typ * int) list * (Term.term * interpretation) list; + (typ * int) list * (term * interpretation) list; (* ------------------------------------------------------------------------- *) (* arguments: additional arguments required during interpretation of terms *) @@ -207,10 +204,10 @@ structure RefuteData = TheoryDataFun ( type T = - {interpreters: (string * (theory -> model -> arguments -> Term.term -> + {interpreters: (string * (theory -> model -> arguments -> term -> (interpretation * model * arguments) option)) list, - printers: (string * (theory -> model -> Term.typ -> interpretation -> - (int -> bool) -> Term.term option)) list, + printers: (string * (theory -> model -> typ -> interpretation -> + (int -> bool) -> term option)) list, parameters: string Symtab.table}; val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; val copy = I; @@ -433,9 +430,8 @@ (* (Term.indexname * Term.typ) list *) val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t)) in - Library.foldl (fn (t', ((x, i), T)) => - (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) - (t, vars) + fold (fn ((x, i), T) => fn t' => + Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t end; (* ------------------------------------------------------------------------- *) @@ -768,60 +764,55 @@ val _ = tracing "Adding axioms..." val axioms = Theory.all_axioms_of thy fun collect_this_axiom (axname, ax) axs = - let - val ax' = unfold_defs thy ax - in - if member (op aconv) axs ax' then axs - else (tracing axname; collect_term_axioms (ax' :: axs, ax')) - end - (* Term.term list * Term.typ -> Term.term list *) - and collect_sort_axioms (axs, T) = - let - (* string list *) - val sort = (case T of - TFree (_, sort) => sort - | TVar (_, sort) => sort - | _ => raise REFUTE ("collect_axioms", "type " ^ - Syntax.string_of_typ_global thy T ^ " is not a variable")) - (* obtain axioms for all superclasses *) - val superclasses = sort @ (maps (Sign.super_classes thy) sort) - (* merely an optimization, because 'collect_this_axiom' disallows *) - (* duplicate axioms anyway: *) - val superclasses = distinct (op =) superclasses - val class_axioms = maps (fn class => map (fn ax => - ("<" ^ class ^ ">", Thm.prop_of ax)) - (#axioms (AxClass.get_info thy class) handle ERROR _ => [])) - superclasses - (* replace the (at most one) schematic type variable in each axiom *) - (* by the actual type 'T' *) - val monomorphic_class_axioms = map (fn (axname, ax) => - (case Term.add_tvars ax [] of - [] => - (axname, ax) - | [(idx, S)] => - (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) - | _ => - raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ - Syntax.string_of_term_global thy ax ^ - ") contains more than one type variable"))) - class_axioms - in - fold collect_this_axiom monomorphic_class_axioms axs - end - (* Term.term list * Term.typ -> Term.term list *) - and collect_type_axioms (axs, T) = + let + val ax' = unfold_defs thy ax + in + if member (op aconv) axs ax' then axs + else (tracing axname; collect_term_axioms ax' (ax' :: axs)) + end + and collect_sort_axioms T axs = + let + val sort = + (case T of + TFree (_, sort) => sort + | TVar (_, sort) => sort + | _ => raise REFUTE ("collect_axioms", + "type " ^ Syntax.string_of_typ_global thy T ^ " is not a variable")) + (* obtain axioms for all superclasses *) + val superclasses = sort @ maps (Sign.super_classes thy) sort + (* merely an optimization, because 'collect_this_axiom' disallows *) + (* duplicate axioms anyway: *) + val superclasses = distinct (op =) superclasses + val class_axioms = maps (fn class => map (fn ax => + ("<" ^ class ^ ">", Thm.prop_of ax)) + (#axioms (AxClass.get_info thy class) handle ERROR _ => [])) + superclasses + (* replace the (at most one) schematic type variable in each axiom *) + (* by the actual type 'T' *) + val monomorphic_class_axioms = map (fn (axname, ax) => + (case Term.add_tvars ax [] of + [] => (axname, ax) + | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) + | _ => + raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ + Syntax.string_of_term_global thy ax ^ + ") contains more than one type variable"))) + class_axioms + in + fold collect_this_axiom monomorphic_class_axioms axs + end + and collect_type_axioms T axs = case T of (* simple types *) - Type ("prop", []) => axs - | Type ("fun", [T1, T2]) => collect_type_axioms - (collect_type_axioms (axs, T1), T2) + Type ("prop", []) => axs + | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) (* axiomatic type classes *) - | Type ("itself", [T1]) => collect_type_axioms (axs, T1) - | Type (s, Ts) => + | Type ("itself", [T1]) => collect_type_axioms T1 axs + | Type (s, Ts) => (case Datatype.get_info thy s of SOME info => (* inductive datatype *) (* only collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts) + fold collect_type_axioms Ts axs | NONE => (case get_typedef thy T of SOME (axname, ax) => @@ -829,20 +820,19 @@ | NONE => (* unspecified type, perhaps introduced with "typedecl" *) (* at least collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts))) - (* axiomatic type classes *) - | TFree _ => collect_sort_axioms (axs, T) + fold collect_type_axioms Ts axs)) (* axiomatic type classes *) - | TVar _ => collect_sort_axioms (axs, T) - (* Term.term list * Term.term -> Term.term list *) - and collect_term_axioms (axs, t) = + | TFree _ => collect_sort_axioms T axs + (* axiomatic type classes *) + | TVar _ => collect_sort_axioms T axs + and collect_term_axioms t axs = case t of (* Pure *) Const (@{const_name all}, _) => axs | Const (@{const_name "=="}, _) => axs | Const (@{const_name "==>"}, _) => axs (* axiomatic type classes *) - | Const (@{const_name TYPE}, T) => collect_type_axioms (axs, T) + | Const (@{const_name TYPE}, T) => collect_type_axioms T axs (* HOL *) | Const (@{const_name Trueprop}, _) => axs | Const (@{const_name Not}, _) => axs @@ -850,7 +840,7 @@ | Const (@{const_name True}, _) => axs (* redundant, since 'False' is also an IDT constructor *) | Const (@{const_name False}, _) => axs - | Const (@{const_name undefined}, T) => collect_type_axioms (axs, T) + | Const (@{const_name undefined}, T) => collect_type_axioms T axs | Const (@{const_name The}, T) => let val ax = specialize_type thy (@{const_name The}, T) @@ -865,74 +855,68 @@ in collect_this_axiom ("Hilbert_Choice.someI", ax) axs end - | Const (@{const_name All}, T) => collect_type_axioms (axs, T) - | Const (@{const_name Ex}, T) => collect_type_axioms (axs, T) - | Const (@{const_name "op ="}, T) => collect_type_axioms (axs, T) + | Const (@{const_name All}, T) => collect_type_axioms T axs + | Const (@{const_name Ex}, T) => collect_type_axioms T axs + | Const (@{const_name "op ="}, T) => collect_type_axioms T axs | Const (@{const_name "op &"}, _) => axs | Const (@{const_name "op |"}, _) => axs | Const (@{const_name "op -->"}, _) => axs (* sets *) - | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T) - | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T) + | Const (@{const_name Collect}, T) => collect_type_axioms T axs + | Const (@{const_name "op :"}, T) => collect_type_axioms T axs (* other optimizations *) - | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms (axs, T) + | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs | Const (@{const_name Finite_Set.finite}, T) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) + collect_type_axioms T axs | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => - collect_type_axioms (axs, T) - | Const (@{const_name List.append}, T) => collect_type_axioms (axs, T) - | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T) - | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T) - | Const (@{const_name fst}, T) => collect_type_axioms (axs, T) - | Const (@{const_name snd}, T) => collect_type_axioms (axs, T) + collect_type_axioms T axs + | Const (@{const_name List.append}, T) => collect_type_axioms T axs + | Const (@{const_name lfp}, T) => collect_type_axioms T axs + | Const (@{const_name gfp}, T) => collect_type_axioms T axs + | Const (@{const_name fst}, T) => collect_type_axioms T axs + | Const (@{const_name snd}, T) => collect_type_axioms T axs (* simply-typed lambda calculus *) | Const (s, T) => if is_const_of_class thy (s, T) then (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) (* and the class definition *) let - val class = Logic.class_of_const s + val class = Logic.class_of_const s val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) - val ax_in = SOME (specialize_type thy (s, T) of_class) + val ax_in = SOME (specialize_type thy (s, T) of_class) (* type match may fail due to sort constraints *) handle Type.TYPE_MATCH => NONE - val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) - ax_in - val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) - (get_classdef thy class) + val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in + val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) in - collect_type_axioms (fold collect_this_axiom - (map_filter I [ax_1, ax_2]) axs, T) + collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs) end else if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then (* only collect relevant type axioms *) - collect_type_axioms (axs, T) + collect_type_axioms T axs else (* other constants should have been unfolded, with some *) (* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) (* typedefs, or type-class related constants *) (* only collect relevant type axioms *) - collect_type_axioms (axs, T) - | Free (_, T) => collect_type_axioms (axs, T) - | Var (_, T) => collect_type_axioms (axs, T) - | Bound i => axs - | Abs (_, T, body) => collect_term_axioms - (collect_type_axioms (axs, T), body) - | t1 $ t2 => collect_term_axioms - (collect_term_axioms (axs, t1), t2) - (* Term.term list *) - val result = map close_form (collect_term_axioms ([], t)) + collect_type_axioms T axs + | Free (_, T) => collect_type_axioms T axs + | Var (_, T) => collect_type_axioms T axs + | Bound _ => axs + | Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs) + | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs) + val result = map close_form (collect_term_axioms t []) val _ = tracing " ...done." in result @@ -1040,7 +1024,7 @@ fun size_of_typ T = case AList.lookup (op =) sizes (string_of_typ T) of SOME n => n - | NONE => minsize + | NONE => minsize in map (fn T => (T, size_of_typ T)) xs end; @@ -1094,13 +1078,13 @@ case next (maxsize-minsize) 0 0 diffs of SOME diffs' => (* merge with those types for which the size is fixed *) - SOME (snd (Library.foldl_map (fn (ds, (T, _)) => + SOME (fst (fold_map (fn (T, _) => fn ds => case AList.lookup (op =) sizes (string_of_typ T) of (* return the fixed size *) - SOME n => (ds, (T, n)) + SOME n => ((T, n), ds) (* consume the head of 'ds', add 'minsize' *) - | NONE => (tl ds, (T, minsize + hd ds))) - (diffs', xs))) + | NONE => ((T, minsize + hd ds), tl ds)) + xs diffs')) | NONE => NONE end; @@ -1157,8 +1141,7 @@ val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) val axioms = collect_axioms thy u (* Term.typ list *) - val types = Library.foldl (fn (acc, t') => - uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms) + val types = fold (union (op =) o ground_types thy) (u :: axioms) [] val _ = tracing ("Ground types: " ^ (if null types then "none." else commas (map (Syntax.string_of_typ_global thy) types))) @@ -1197,15 +1180,15 @@ val _ = tracing ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") (* translate 'u' and all axioms *) - val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') => + val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => let val (i, m', a') = interpret thy m a t' in (* set 'def_eq' to 'true' *) - ((m', {maxvars = #maxvars a', def_eq = true, + (i, (m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', - wellformed = #wellformed a'}), i) - end) ((init_model, init_args), u :: axioms) + wellformed = #wellformed a'})) + end) (u :: axioms) (init_model, init_args) (* make 'u' either true or false, and make all axioms true, and *) (* add the well-formedness side condition *) val fm_u = (if negate then toFalse else toTrue) (hd intrs) @@ -1309,10 +1292,9 @@ (* (Term.indexname * Term.typ) list *) val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t)) (* Term.term *) - val ex_closure = Library.foldl (fn (t', ((x, i), T)) => - (HOLogic.exists_const T) $ - Abs (x, T, abstract_over (Var ((x, i), T), t'))) - (t, vars) + val ex_closure = fold (fn ((x, i), T) => fn t' => + HOLogic.exists_const T $ + Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) (* 'HOLogic.exists_const' is not type-correct. However, this is not *) (* really a problem as long as 'find_model' still interprets the *) @@ -1733,8 +1715,8 @@ (* create all constants of type 'T' *) val constants = make_constants thy model T (* interpret the 'body' separately for each constant *) - val ((model', args'), bodies) = Library.foldl_map - (fn ((m, a), c) => + val (bodies, (model', args')) = fold_map + (fn c => fn (m, a) => let (* add 'c' to 'bounds' *) val (i', m', a') = interpret thy m {maxvars = #maxvars a, @@ -1743,15 +1725,15 @@ in (* keep the new model m' and 'next_idx' and 'wellformed', *) (* but use old 'bounds' *) - ((m', {maxvars = maxvars, def_eq = def_eq, + (i', (m', {maxvars = maxvars, def_eq = def_eq, next_idx = #next_idx a', bounds = bounds, - wellformed = #wellformed a'}), i') + wellformed = #wellformed a'})) end) - ((model, args), constants) + constants (model, args) in SOME (Node bodies, model', args') end - | t1 $ t2 => + | t1 $ t2 => let (* interpret 't1' and 't2' separately *) val (intr1, model1, args1) = interpret thy model args t1 @@ -2212,14 +2194,14 @@ Node (replicate size (make_undef ds)) end (* returns the interpretation for a constructor *) - fun make_constr (offset, []) = - if offset= total") - | make_constr (offset, d::ds) = + | make_constr (d::ds) offset = let (* Term.typ *) val dT = typ_of_dtyp descr typ_assoc d @@ -2228,8 +2210,8 @@ (* for the IDT) *) val terms' = canonical_terms typs' dT (* sanity check *) - val _ = if length terms' <> - size_of_type thy (typs', []) dT + val _ = + if length terms' <> size_of_type thy (typs', []) dT then raise REFUTE ("IDT_constructor_interpreter", "length of terms' is not equal to old size") @@ -2239,46 +2221,52 @@ (* for the IDT) *) val terms = canonical_terms typs dT (* sanity check *) - val _ = if length terms <> size_of_type thy (typs, []) dT + val _ = + if length terms <> size_of_type thy (typs, []) dT then raise REFUTE ("IDT_constructor_interpreter", "length of terms is not equal to current size") else () (* sanity check *) - val _ = if length terms < length terms' then + val _ = + if length terms < length terms' then raise REFUTE ("IDT_constructor_interpreter", "current size is less than old size") else () (* sanity check: every element of terms' must also be *) (* present in terms *) - val _ = if List.all (member op= terms) terms' then () + val _ = + if List.all (member (op =) terms) terms' then () else raise REFUTE ("IDT_constructor_interpreter", "element has disappeared") (* sanity check: the order on elements of terms' is *) (* the same in terms, for those elements *) - val _ = let + val _ = + let fun search (x::xs) (y::ys) = - if x = y then search xs ys else search (x::xs) ys + if x = y then search xs ys else search (x::xs) ys | search (x::xs) [] = - raise REFUTE ("IDT_constructor_interpreter", - "element order not preserved") + raise REFUTE ("IDT_constructor_interpreter", + "element order not preserved") | search [] _ = () in search terms' terms end (* int * interpretation list *) - val (new_offset, intrs) = Library.foldl_map (fn (off, t_elem) => - (* if 't_elem' existed at the previous depth, *) - (* proceed recursively, otherwise map the entire *) - (* subtree to "undefined" *) - if t_elem mem terms' then - make_constr (off, ds) - else - (off, make_undef ds)) (offset, terms) + val (intrs, new_offset) = + fold_map (fn t_elem => fn off => + (* if 't_elem' existed at the previous depth, *) + (* proceed recursively, otherwise map the entire *) + (* subtree to "undefined" *) + if t_elem mem terms' then + make_constr ds off + else + (make_undef ds, off)) + terms offset in - (new_offset, Node intrs) + (Node intrs, new_offset) end in - SOME (snd (make_constr (offset, ctypes)), model, args) + SOME (fst (make_constr ctypes offset), model, args) end end | NONE => (* body type is not an inductive datatype *) @@ -2332,12 +2320,12 @@ else (* mconstrs_count = length params *) let (* interpret each parameter separately *) - val ((model', args'), p_intrs) = Library.foldl_map (fn ((m, a), p) => + val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => let val (i, m', a') = interpret thy m a p in - ((m', a'), i) - end) ((model, args), params) + (i, (m', a')) + end) params (model, args) val (typs, _) = model' (* 'index' is /not/ necessarily the index of the IDT that *) (* the recursion operator is associated with, but merely *) @@ -2440,14 +2428,14 @@ end) descr (* associate constructors with corresponding parameters *) (* (int * (interpretation * interpretation) list) list *) - val (p_intrs', mc_p_intrs) = Library.foldl_map - (fn (p_intrs', (idx, c_intrs)) => + val (mc_p_intrs, p_intrs') = fold_map + (fn (idx, c_intrs) => fn p_intrs' => let val len = length c_intrs in - (List.drop (p_intrs', len), - (idx, c_intrs ~~ List.take (p_intrs', len))) - end) (p_intrs, mc_intrs) + ((idx, c_intrs ~~ List.take (p_intrs', len)), + List.drop (p_intrs', len)) + end) mc_intrs p_intrs (* sanity check: no 'p_intr' may be left afterwards *) val _ = if p_intrs' <> [] then raise REFUTE ("IDT_recursion_interpreter", @@ -2672,15 +2660,15 @@ let (* interpretation -> int *) fun number_of_elements (Node xs) = - Library.foldl (fn (n, x) => - if x=TT then - n+1 - else if x=FF then - n - else - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type does not yield a Boolean")) - (0, xs) + fold (fn x => fn n => + if x = TT then + n + 1 + else if x = FF then + n + else + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type does not yield a Boolean")) + xs 0 | number_of_elements (Leaf _) = raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf") @@ -2885,7 +2873,7 @@ (* of width 'size_elem' and depth 'length_list' (with 'size_list' *) (* nodes total) *) (* (int * (int * int)) list *) - val (_, lenoff_lists) = Library.foldl_map (fn ((offsets, off), elem) => + val (lenoff_lists, _) = fold_map (fn elem => fn (offsets, off) => (* corresponds to a pre-order traversal of the tree *) let val len = length offsets @@ -2894,10 +2882,10 @@ in if len < list_length then (* go to first child node *) - ((off :: offsets, off * size_elem), assoc) + (assoc, (off :: offsets, off * size_elem)) else if off mod size_elem < size_elem - 1 then (* go to next sibling node *) - ((offsets, off + 1), assoc) + (assoc, (offsets, off + 1)) else (* go back up the stack until we find a level where we can go *) (* to the next sibling node *) @@ -2909,12 +2897,12 @@ [] => (* we're at the last node in the tree; the next value *) (* won't be used anyway *) - (([], 0), assoc) + (assoc, ([], 0)) | off'::offs' => (* go to next sibling node *) - ((offs', off' + 1), assoc) + (assoc, (offs', off' + 1)) end - end) (([], 0), elements) + end) elements ([], 0) (* we also need the reverse association (from length/offset to *) (* index) *) val lenoff'_lists = map Library.swap lenoff_lists @@ -3251,7 +3239,7 @@ print thy (typs, []) dT (List.nth (consts, n)) assignment end) (cargs ~~ args) in - SOME (Library.foldl op$ (cTerm, argsTerms)) + SOME (list_comb (cTerm, argsTerms)) end end | NONE => (* not an inductive datatype *) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Oct 27 23:12:10 2009 +0100 @@ -10,17 +10,17 @@ val fix_sorts: sort Vartab.table -> term -> term val invert_const: string -> string val invert_type_const: string -> string - val num_typargs: Context.theory -> string -> int + val num_typargs: theory -> string -> int val make_tvar: string -> typ val strip_prefix: string -> string -> string option - val setup: Context.theory -> Context.theory + val setup: theory -> theory (* extracting lemma list*) val find_failure: string -> string option val lemma_list: bool -> string -> - string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list + string * string vector * (int * int) * Proof.context * thm * int -> string * string list (* structured proofs *) val structured_proof: string -> - string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list + string * string vector * (int * int) * Proof.context * thm * int -> string * string list end; structure ResReconstruct : RES_RECONSTRUCT = diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Tue Oct 27 23:12:10 2009 +0100 @@ -92,8 +92,8 @@ (* ------------------------------------------------------------------------- *) datatype CLAUSE = NO_CLAUSE - | ORIG_CLAUSE of Thm.thm - | RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list; + | ORIG_CLAUSE of thm + | RAW_CLAUSE of thm * (int * cterm) list; (* ------------------------------------------------------------------------- *) (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) @@ -346,11 +346,16 @@ fold Thm.weaken (rev sorted_clauses) False_thm end in - case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of + case + let val the_solver = ! solver + in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end + of SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( if !trace_sat then tracing ("Proof trace from SAT solver:\n" ^ - "clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^ + "clauses: " ^ ML_Syntax.print_list + (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) + (Inttab.dest clause_table) ^ "\n" ^ "empty clause: " ^ Int.toString empty_id) else (); if !quick_and_dirty then @@ -388,8 +393,9 @@ val msg = "SAT solver found a countermodel:\n" ^ (commas o map (fn (term, idx) => - Syntax.string_of_term_global @{theory} term ^ ": " - ^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false"))) + Syntax.string_of_term_global @{theory} term ^ ": " ^ + (case assignment idx of NONE => "arbitrary" + | SOME true => "true" | SOME false => "false"))) (Termtab.dest atom_table) in raise THM (msg, 0, []) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOL/Tools/sat_solver.ML Tue Oct 27 23:12:10 2009 +0100 @@ -370,13 +370,13 @@ (* string * solver -> unit *) - fun add_solver (name, new_solver) = + fun add_solver (name, new_solver) = CRITICAL (fn () => let val the_solvers = !solvers; val _ = if AList.defined (op =) the_solvers name then warning ("SAT solver " ^ quote name ^ " was defined before") else (); - in solvers := AList.update (op =) (name, new_solver) the_solvers end; + in solvers := AList.update (op =) (name, new_solver) the_solvers end); (* ------------------------------------------------------------------------- *) (* invoke_solver: returns the solver associated with the given 'name' *) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOLCF/IOA/ABP/Check.ML --- a/src/HOLCF/IOA/ABP/Check.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOLCF/IOA/ABP/Check.ML Tue Oct 27 23:12:10 2009 +0100 @@ -15,8 +15,8 @@ fun check(extacts,intacts,string_of_a,startsI,string_of_s, nexts,hom,transA,startsS) = let fun check_s(s,unchecked,checked) = - let fun check_sa(unchecked,a) = - let fun check_sas(unchecked,t) = + let fun check_sa a unchecked = + let fun check_sas t unchecked = (if a mem extacts then (if transA(hom s,a,hom t) then ( ) else (writeln("Error: Mapping of Externals!"); @@ -29,8 +29,8 @@ string_of_a a; writeln""; string_of_s t;writeln"";writeln"" )); if t mem checked then unchecked else insert (op =) t unchecked) - in Library.foldl check_sas (unchecked,nexts s a) end; - val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts) + in fold check_sas (nexts s a) unchecked end; + val unchecked' = fold check_sa (extacts @ intacts) unchecked in (if s mem startsI then (if hom(s) mem startsS then () else writeln("Error: At start states!")) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Oct 27 23:12:10 2009 +0100 @@ -17,7 +17,7 @@ end; -structure Domain_Axioms :> DOMAIN_AXIOMS = +structure Domain_Axioms : DOMAIN_AXIOMS = struct open Domain_Library; @@ -218,13 +218,13 @@ ("bisim_def", %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); - fun add_one (thy,(dnam,axs,dfs)) = - thy |> Sign.add_path dnam - |> add_defs_infer dfs - |> add_axioms_infer axs - |> Sign.parent_path; + fun add_one (dnam, axs, dfs) = + Sign.add_path dnam + #> add_defs_infer dfs + #> add_axioms_infer axs + #> Sign.parent_path; - val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); + val thy = fold add_one (mapn (calc_axioms comp_dname eqs) 0 eqs) thy'; in thy |> Sign.add_path comp_dnam |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) diff -r b8d3b7196fe7 -r 03c08ce703bf src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/HOLCF/Tools/cont_consts.ML Tue Oct 27 23:12:10 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOLCF/Tools/cont_consts.ML - ID: $Id$ Author: Tobias Mayr, David von Oheimb, and Markus Wenzel HOLCF version of consts: handle continuous function types in mixfix @@ -12,7 +11,7 @@ val add_consts_i: (binding * typ * mixfix) list -> theory -> theory end; -structure ContConsts :> CONT_CONSTS = +structure ContConsts: CONT_CONSTS = struct @@ -29,18 +28,23 @@ | change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T]) | change_arrow _ _ = sys_error "cont_consts: change_arrow"; -fun trans_rules name2 name1 n mx = let - fun argnames _ 0 = [] - | argnames c n = chr c::argnames (c+1) (n-1); - val vnames = argnames (ord "A") n; - val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); - in [Syntax.ParsePrintRule (Syntax.mk_appl (Constant name2) (map Variable vnames), - Library.foldl (fn (t,arg) => (Syntax.mk_appl (Constant "Rep_CFun") - [t,Variable arg])) - (Constant name1,vnames))] - @(case mx of InfixName _ => [extra_parse_rule] - | InfixlName _ => [extra_parse_rule] - | InfixrName _ => [extra_parse_rule] | _ => []) end; +fun trans_rules name2 name1 n mx = + let + fun argnames _ 0 = [] + | argnames c n = chr c::argnames (c+1) (n-1); + val vnames = argnames (ord "A") n; + val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); + in + [Syntax.ParsePrintRule + (Syntax.mk_appl (Constant name2) (map Variable vnames), + fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg]) + vnames (Constant name1))] @ + (case mx of + InfixName _ => [extra_parse_rule] + | InfixlName _ => [extra_parse_rule] + | InfixrName _ => [extra_parse_rule] + | _ => []) + end; (* transforming infix/mixfix declarations of constants with type ...->... @@ -59,7 +63,8 @@ (const_binding mx syn, T, InfixrName (Binding.name_of syn, p)) | fix_mixfix decl = decl; -fun transform decl = let +fun transform decl = + let val (c, T, mx) = fix_mixfix decl; val c1 = Binding.name_of c; val c2 = "_cont_" ^ c1; diff -r b8d3b7196fe7 -r 03c08ce703bf src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 27 23:12:10 2009 +0100 @@ -702,12 +702,11 @@ result end; -fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) : - (bool * term) list = +fun add_datoms ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _) (dats : (bool * term) list) = union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); fun discr (initems : (LA_Data.decomp * int) list) : bool list = - map fst (Library.foldl add_datoms ([],initems)); + map fst (fold add_datoms initems []); fun refutes ctxt params show_ex : (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option = diff -r b8d3b7196fe7 -r 03c08ce703bf src/Provers/order.ML --- a/src/Provers/order.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Provers/order.ML Tue Oct 27 23:12:10 2009 +0100 @@ -697,9 +697,9 @@ dfs_visit along with u form a connected component. We collect all the connected components together in a list, which is what is returned. *) - Library.foldl (fn (comps,u) => + fold (fn u => fn comps => if been_visited u then comps - else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps)) ([],(!finish)) + else (u :: dfs_visit (transpose (op aconv) G) u) :: comps) (!finish) [] end; diff -r b8d3b7196fe7 -r 03c08ce703bf src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Provers/splitter.ML Tue Oct 27 23:12:10 2009 +0100 @@ -26,9 +26,10 @@ signature SPLITTER = sig (* somewhat more internal functions *) - val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list - val split_posns : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term -> - (thm * (typ * typ * int list) list * int list * typ * term) list (* first argument is a "cmap", returns a list of "split packs" *) + val cmap_of_split_thms: thm list -> (string * (typ * term * thm * typ * int) list) list + val split_posns: (string * (typ * term * thm * typ * int) list) list -> + theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list + (* first argument is a "cmap", returns a list of "split packs" *) (* the "real" interface, providing a number of tactics *) val split_tac : thm list -> int -> tactic val split_inside_tac: thm list -> int -> tactic @@ -57,37 +58,33 @@ fun split_format_err () = error "Wrong format for split rule"; -(* thm -> (string * typ) * bool *) fun split_thm_info thm = case concl_of (Data.mk_eq thm) of Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false) | _ => split_format_err ()) | _ => split_format_err (); -(* thm list -> (string * (typ * term * thm * typ * int) list) list *) fun cmap_of_split_thms thms = let val splits = map Data.mk_eq thms - fun add_thm (cmap, thm) = - (case concl_of thm of _$(t as _$lhs)$_ => - (case strip_comb lhs of (Const(a,aT),args) => - let val info = (aT,lhs,thm,fastype_of t,length args) - in case AList.lookup (op =) cmap a of - SOME infos => AList.update (op =) (a, info::infos) cmap - | NONE => (a,[info])::cmap - end - | _ => split_format_err()) - | _ => split_format_err()) + fun add_thm thm cmap = + (case concl_of thm of _ $ (t as _ $ lhs) $ _ => + (case strip_comb lhs of (Const(a,aT),args) => + let val info = (aT,lhs,thm,fastype_of t,length args) + in case AList.lookup (op =) cmap a of + SOME infos => AList.update (op =) (a, info::infos) cmap + | NONE => (a,[info])::cmap + end + | _ => split_format_err()) + | _ => split_format_err()) in - Library.foldl add_thm ([], splits) + fold add_thm splits [] end; (* ------------------------------------------------------------------------- *) (* mk_case_split_tac *) (* ------------------------------------------------------------------------- *) -(* (int * int -> order) -> thm list -> int -> tactic * *) - fun mk_case_split_tac order = let @@ -154,7 +151,7 @@ (* add all loose bound variables in t to list is *) -fun add_lbnos (is,t) = add_loose_bnos (t,0,is); +fun add_lbnos t is = add_loose_bnos (t, 0, is); (* check if the innermost abstraction that needs to be removed has a body of type T; otherwise the expansion thm will fail later on @@ -194,7 +191,7 @@ fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) = if n > length ts then [] else let val lev = length apsns - val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts)) + val lbnos = fold add_lbnos (Library.take (n, ts)) [] val flbnos = List.filter (fn i => i < lev) lbnos val tt = incr_boundvars (~lev) t in if null flbnos then @@ -225,13 +222,11 @@ local exception MATCH in - (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *) fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv) handle Type.TYPE_MATCH => raise MATCH - (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *) + fun fomatch sg args = let - (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *) fun mtch tyinsts = fn (Ts, Var(_,T), t) => typ_match sg (tyinsts, (T, fastype_of1(Ts,t))) @@ -247,10 +242,8 @@ mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u) | _ => raise MATCH in (mtch Vartab.empty args; true) handle MATCH => false end; -end (* local *) +end; -(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term -> - (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *) fun split_posns (cmap : (string * (typ * term * thm * typ * int) list) list) sg Ts t = let val T' = fastype_of1 (Ts, t); @@ -260,20 +253,21 @@ | posns Ts pos apsns t = let val (h, ts) = strip_comb t - fun iter((i, a), t) = (i+1, (posns Ts (i::pos) apsns t) @ a); - val a = case h of - Const(c, cT) => - let fun find [] = [] - | find ((gcT, pat, thm, T, n)::tups) = - let val t2 = list_comb (h, Library.take (n, ts)) - in if Sign.typ_instance sg (cT, gcT) - andalso fomatch sg (Ts,pat,t2) - then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2) - else find tups - end - in find (these (AList.lookup (op =) cmap c)) end - | _ => [] - in snd(Library.foldl iter ((0, a), ts)) end + fun iter t (i, a) = (i+1, (posns Ts (i::pos) apsns t) @ a); + val a = + case h of + Const(c, cT) => + let fun find [] = [] + | find ((gcT, pat, thm, T, n)::tups) = + let val t2 = list_comb (h, Library.take (n, ts)) + in if Sign.typ_instance sg (cT, gcT) + andalso fomatch sg (Ts,pat,t2) + then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2) + else find tups + end + in find (these (AList.lookup (op =) cmap c)) end + | _ => [] + in snd (fold iter ts (0, a)) end in posns Ts [] [] t end; fun nth_subgoal i thm = List.nth (prems_of thm, i-1); @@ -343,8 +337,8 @@ (Logic.strip_assums_concl (Thm.prop_of thm')))); val cert = cterm_of (Thm.theory_of_thm state); val cntxt = mk_cntxt_splitthm t tt TB; - val abss = Library.foldl (fn (t, T) => Abs ("", T, t)); - in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm' + val abss = fold (fn T => fn t => Abs ("", T, t)); + in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm' end; @@ -355,8 +349,6 @@ i : number of subgoal the tactic should be applied to *****************************************************************************) -(* thm list -> int -> tactic *) - fun split_tac [] i = no_tac | split_tac splits i = let val cmap = cmap_of_split_thms splits @@ -379,9 +371,9 @@ in (split_tac, exported_split_posns) end; (* mk_case_split_tac *) -val (split_tac, split_posns) = mk_case_split_tac int_ord; +val (split_tac, split_posns) = mk_case_split_tac int_ord; -val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord); +val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord); (***************************************************************************** @@ -389,7 +381,7 @@ splits : list of split-theorems to be tried ****************************************************************************) -fun split_asm_tac [] = K no_tac +fun split_asm_tac [] = K no_tac | split_asm_tac splits = let val cname_list = map (fst o fst o split_thm_info) splits; @@ -431,25 +423,28 @@ (* addsplits / delsplits *) -fun string_of_typ (Type (s, Ts)) = (if null Ts then "" - else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s +fun string_of_typ (Type (s, Ts)) = + (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s | string_of_typ _ = "_"; fun split_name (name, T) asm = "split " ^ (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T; fun ss addsplits splits = - let fun addsplit (ss,split) = - let val (name,asm) = split_thm_info split - in Simplifier.addloop (ss, (split_name name asm, - (if asm then split_asm_tac else split_tac) [split])) end - in Library.foldl addsplit (ss,splits) end; + let + fun addsplit split ss = + let + val (name, asm) = split_thm_info split + val tac = (if asm then split_asm_tac else split_tac) [split] + in Simplifier.addloop (ss, (split_name name asm, tac)) end + in fold addsplit splits ss end; fun ss delsplits splits = - let fun delsplit(ss,split) = - let val (name,asm) = split_thm_info split - in Simplifier.delloop (ss, split_name name asm) - end in Library.foldl delsplit (ss,splits) end; + let + fun delsplit split ss = + let val (name, asm) = split_thm_info split + in Simplifier.delloop (ss, split_name name asm) end + in fold delsplit splits ss end; (* attributes *) @@ -471,7 +466,8 @@ (* theory setup *) val setup = - Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #> + Attrib.setup @{binding split} + (Attrib.add_del split_add split_del) "declare case split rule" #> Method.setup @{binding split} (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) "apply case split rule"; diff -r b8d3b7196fe7 -r 03c08ce703bf src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Tue Oct 27 23:12:10 2009 +0100 @@ -716,8 +716,9 @@ quote name ^ " has no computational content") in (Reconstruct.reconstruct_proof thy prop prf, vs) end; - val defs = Library.foldl (fn (defs, (prf, vs)) => - fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms); + val defs = + fold (fn (prf, vs) => fn defs => fst (extr 0 defs vs [] [] [] prf)) + (map prep_thm thms) []; fun add_def (s, (vs, ((t, u), (prf, _)))) thy = (case Sign.const_type thy (extr_name s vs) of diff -r b8d3b7196fe7 -r 03c08ce703bf src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Pure/Proof/reconstruct.ML Tue Oct 27 23:12:10 2009 +0100 @@ -40,11 +40,11 @@ fun mk_var env Ts T = let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) - in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end; + in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end; -fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) = - (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, - TVar (("'t", maxidx + 1), s)); +fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) = + (TVar (("'t", maxidx + 1), S), + Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}); val mk_abs = fold (fn T => fn u => Abs ("", T, u)); @@ -73,14 +73,14 @@ | infer_type thy env Ts vTs (t as Free (s, T)) = if T = dummyT then (case Symtab.lookup vTs s of NONE => - let val (env', T) = mk_tvar (env, []) + let val (T, env') = mk_tvar [] env in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end | SOME T => (Free (s, T), T, vTs, env)) else (t, T, vTs, env) | infer_type thy env Ts vTs (Var _) = error "reconstruct_proof: internal error" | infer_type thy env Ts vTs (Abs (s, T, t)) = let - val (env', T') = if T = dummyT then mk_tvar (env, []) else (env, T); + val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t in (Abs (s, T', t'), T' --> U, vTs', env'') end | infer_type thy env Ts vTs (t $ u) = @@ -90,7 +90,7 @@ in (case chaseT env2 T of Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') | _ => - let val (env3, V) = mk_tvar (env2, []) + let val (V, env3) = mk_tvar [] env2 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) end | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) @@ -99,21 +99,24 @@ fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); -fun decompose thy Ts (env, p as (t, u)) = - let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p - else apsnd flat (Library.foldl_map (decompose thy Ts) (uT env T U, ts ~~ us)) - in case pairself (strip_comb o Envir.head_norm env) p of +fun decompose thy Ts (p as (t, u)) env = + let + fun rigrig (a, T) (b, U) uT ts us = + if a <> b then cantunify thy p + else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) + in + case pairself (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us | ((Bound i, ts), (Bound j, us)) => rigrig (i, dummyT) (j, dummyT) (K o K) ts us | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => - decompose thy (T::Ts) (unifyT thy env T U, (t, u)) + decompose thy (T::Ts) (t, u) (unifyT thy env T U) | ((Abs (_, T, t), []), _) => - decompose thy (T::Ts) (env, (t, incr_boundvars 1 u $ Bound 0)) + decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env | (_, (Abs (_, T, u), [])) => - decompose thy (T::Ts) (env, (incr_boundvars 1 t $ Bound 0, u)) - | _ => (env, [(mk_abs Ts t, mk_abs Ts u)]) + decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env + | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) end; fun make_constraints_cprf thy env cprf = @@ -125,7 +128,7 @@ in (prop, prf, cs, Pattern.unify thy (t', u') env, vTs) handle Pattern.Pattern => - let val (env', cs') = decompose thy [] (env, (t', u')) + let val (cs', env') = decompose thy [] (t', u') env in (prop, prf, cs @ cs', env', vTs) end | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u') @@ -135,10 +138,10 @@ let val tvars = OldTerm.term_tvars prop; val tfrees = OldTerm.term_tfrees prop; - val (env', Ts) = + val (Ts, env') = (case opTs of - NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) - | SOME Ts => (env, Ts)); + NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env + | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) (forall_intr_vfs prop) handle Library.UnequalLengths => error ("Wrong number of type arguments for " ^ @@ -152,8 +155,10 @@ handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = let - val (env', T) = (case opT of - NONE => mk_tvar (env, []) | SOME T => (env, T)); + val (T, env') = + (case opT of + NONE => mk_tvar [] env + | SOME T => (T, env)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), @@ -167,7 +172,7 @@ end | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = let - val (env', t) = mk_var env Ts propT; + val (t, env') = mk_var env Ts propT; val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') end @@ -178,7 +183,7 @@ add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) env'' vTs'' (u, u') | (t, prf1, cnstrts', env'', vTs'') => - let val (env''', v) = mk_var env'' Ts propT + let val (v, env''') = mk_var env'' Ts propT in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) env''' vTs'' (t, Logic.mk_implies (u, v)) end) @@ -192,7 +197,7 @@ in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) end | (u, prf, cnstrts, env2, vTs2) => - let val (env3, v) = mk_var env2 Ts (U --> propT); + let val (v, env3) = mk_var env2 Ts (U --> propT); in add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 (u, Const ("all", (U --> propT) --> propT) $ v) @@ -202,14 +207,14 @@ (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env', vTs') => - let val (env'', t) = mk_var env' Ts T + let val (t, env'') = mk_var env' Ts T in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') end | (u, prf, cnstrts, env', vTs') => let - val (env1, T) = mk_tvar (env', []); - val (env2, v) = mk_var env1 Ts (T --> propT); - val (env3, t) = mk_var env2 Ts T + val (T, env1) = mk_tvar [] env'; + val (v, env2) = mk_var env1 Ts (T --> propT); + val (t, env3) = mk_var env2 Ts T in add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' (u, Const ("all", (T --> propT) --> propT) $ v) @@ -267,7 +272,7 @@ (Pattern.unify thy (tn1, tn2) env, ps) handle Pattern.Unif => cantunify thy (tn1, tn2) else - let val (env', cs') = decompose thy [] (env, (tn1, tn2)) + let val (cs', env') = decompose thy [] (tn1, tn2) env in if cs' = [(tn1, tn2)] then apsnd (cons (false, (tn1, tn2), vs)) (search env ps) else search env' (map (fn q => (true, q, vs)) cs' @ ps) diff -r b8d3b7196fe7 -r 03c08ce703bf src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Tue Oct 27 23:12:10 2009 +0100 @@ -1139,8 +1139,8 @@ end and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = - transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1 - (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems')) + transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 + (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) (if changed > 0 then mut_impc (rev prems') concl (rev rrss') (rev asms') [] [] [] [] ss ~1 changed diff -r b8d3b7196fe7 -r 03c08ce703bf src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Tue Oct 27 19:03:59 2009 +0100 +++ b/src/Tools/eqsubst.ML Tue Oct 27 23:12:10 2009 +0100 @@ -269,7 +269,7 @@ (* FOR DEBUGGING... type trace_subst_errT = int (* subgoal *) * thm (* thm with all goals *) - * (Thm.cterm list (* certified free var placeholders for vars *) + * (cterm list (* certified free var placeholders for vars *) * thm) (* trivial thm of goal concl *) (* possible matches/unifiers *) * thm (* rule *)