--- 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) =
--- 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
--- 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")
--- 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
--- 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 |>
--- 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;
--- 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
--- 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 }
--- 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}
--- 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)
--- 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'
--- 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;
--- 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 *********************)
--- 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;
--- 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;
--- 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 =
--- 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 *)
--- 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;
--- 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
--- 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
--- 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) =
--- 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 =
--- 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
--- 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" ^
--- 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 then
- (offset+1, Leaf ((replicate offset False) @ True ::
- (replicate (total-offset-1) False)))
+ fun make_constr [] offset =
+ if offset < total then
+ (Leaf (replicate offset False @ True ::
+ (replicate (total - offset - 1) False)), offset + 1)
else
raise REFUTE ("IDT_constructor_interpreter",
"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 *)
--- 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 =
--- 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, [])
--- 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' *)
--- 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!"))
--- 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 []))
--- 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;
--- 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 =
--- 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;
--- 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 * <split_posns> *)
-
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";
--- 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
--- 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)
--- 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
--- 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 *)