--- a/src/HOL/Nominal/nominal_datatype.ML Tue Oct 27 17:34:00 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Oct 27 22:55:27 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 17:34:00 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Tue Oct 27 22:55:27 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/Tools/Datatype/datatype.ML Tue Oct 27 17:34:00 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Oct 27 22:55:27 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 17:34:00 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 27 22:55:27 2009 +0100
@@ -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 17:34:00 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Tue Oct 27 22:55:27 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 17:34:00 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Oct 27 22:55:27 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/inductive_codegen.ML Tue Oct 27 17:34:00 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Oct 27 22:55:27 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 17:34:00 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Oct 27 22:55:27 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/recfun_codegen.ML Tue Oct 27 17:34:00 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Oct 27 22:55:27 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" ^