--- a/NEWS Thu Oct 19 12:08:27 2006 +0200
+++ b/NEWS Fri Oct 20 10:44:33 2006 +0200
@@ -584,7 +584,7 @@
* Linear arithmetic now splits certain operators (e.g. min, max, abs)
also when invoked by the simplifier. This results in the simplifier
-being more powerful on arithmetic goals. INCOMPATIBILTY. Set
+being more powerful on arithmetic goals. INCOMPATIBILITY. Set
fast_arith_split_limit to 0 to obtain the old behavior.
* Support for hex (0x20) and binary (0b1001) numerals.
@@ -632,9 +632,14 @@
*** ML ***
+* Pure/table:
+
+Function `...tab.foldl` removed.
+INCOMPATIBILITY: use `...tabfold` instead
+
* Pure/library:
-gen_rem(s) abandoned in favour of remove / subtract.
+`gen_rem(s)` abandoned in favour of `remove` / `subtract`.
INCOMPATIBILITY:
rewrite "gen_rem eq (xs, x)" to "remove (eq o swap) x xs"
rewrite "gen_rems eq (xs, ys)" to "subtract (eq o swap) ys xs"
@@ -642,7 +647,7 @@
* Pure/library:
-infixes ins ins_string ins_int have been abandoned in favour of insert.
+infixes `ins` `ins_string` `ins_int` have been abandoned in favour of `insert`.
INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs"
* Pure/General/susp.ML:
--- a/src/HOL/Import/hol4rews.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Oct 20 10:44:33 2006 +0200
@@ -21,7 +21,7 @@
val extend = I
fun merge _ (NoImport,NoImport) = NoImport
| merge _ _ = (warning "Import status set during merge"; NoImport)
-fun print sg import_status =
+fun print _ import_status =
Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
end;
@@ -40,7 +40,7 @@
if s1 = s2
then s1
else error "Trying to merge two different import segments"
-fun print sg import_segment =
+fun print _ import_segment =
Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))
end;
@@ -58,7 +58,7 @@
val extend = I
fun merge _ ([],[]) = []
| merge _ _ = error "Used names not empty during merge"
-fun print sg used_names =
+fun print _ used_names =
Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
end;
@@ -73,7 +73,7 @@
val extend = I
fun merge _ (("","",[]),("","",[])) = ("","",[])
| merge _ _ = error "Dump data not empty during merge"
-fun print sg dump_data =
+fun print _ dump_data =
Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
end;
@@ -87,9 +87,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 moves:"
- (Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 moves:"
+ (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
end;
structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);
@@ -102,9 +102,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 imports:"
- (Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 imports:"
+ (Symtab.fold (fn (thyname, segname) => fn xl => (Pretty.str (thyname ^ " imported from segment " ^ segname) :: xl)) tab []))
end;
structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
@@ -128,9 +128,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
- (Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
+ (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
end;
structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);
@@ -143,9 +143,10 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 mappings:"
- (StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 mappings:"
+ (StringPair.fold (fn ((bthy, bthm), isathm) => fn xl =>
+ (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED")) :: xl)) tab []))
end;
structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);
@@ -158,9 +159,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 mappings:"
- (StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 mappings:"
+ (StringPair.fold (fn ((bthy, bthm), (_, thm)) => fn xl => (Pretty.str (bthy ^ "." ^ bthm ^ ":") :: Display.pretty_thm thm :: xl)) tab []))
end;
structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);
@@ -173,9 +174,10 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
- (StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
+ (StringPair.fold (fn ((bthy, bconst), (internal, isaconst, _)) => fn xl =>
+ (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
end;
structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);
@@ -188,9 +190,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
- (StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
+ (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) tab []))
end;
structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);
@@ -203,9 +205,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
- (StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
+ (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) tab []))
end;
structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);
@@ -218,9 +220,10 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
- Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
- (StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
+fun print _ tab =
+ Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
+ (StringPair.fold (fn ((bthy, bconst), (internal, isaconst)) => fn xl =>
+ (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
end;
structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);
@@ -233,9 +236,9 @@
val copy = I
val extend = I
fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print sg tab =
+fun print _ tab =
Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
- (StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))
+ (StringPair.fold (fn ((bthy,bthm),(_,th)) => fn xl => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) tab []))
end;
structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);
@@ -248,7 +251,7 @@
val copy = I
val extend = I
fun merge _ = Library.gen_union Thm.eq_thm
-fun print sg thms =
+fun print _ thms =
Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
(map Display.pretty_thm thms))
end;
@@ -261,14 +264,14 @@
fun add_hol4_rewrite (Context.Theory thy, th) =
let
val _ = message "Adding HOL4 rewrite"
- val th1 = th RS eq_reflection
+ val th1 = th RS HOL.eq_reflection
val current_rews = HOL4Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
in
(Context.Theory updated_thy,th1)
end
- | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
+ | add_hol4_rewrite (context, th) = (context, th RS HOL.eq_reflection);
fun ignore_hol4 bthy bthm thy =
let
@@ -449,43 +452,38 @@
end;
fun get_hol4_theorem thyname thmname thy =
- let
- val isathms = HOL4Thms.get thy
- in
- StringPair.lookup isathms (thyname,thmname)
- end
+ let
+ val isathms = HOL4Thms.get thy
+ in
+ StringPair.lookup isathms (thyname,thmname)
+ end;
-fun add_hol4_theorem thyname thmname hth thy =
- let
- val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
- val isathms = HOL4Thms.get thy
- val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms
- val thy' = HOL4Thms.put isathms' thy
- in
- thy'
- end
+fun add_hol4_theorem thyname thmname hth =
+ let
+ val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
+ in
+ HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
+ end;
fun export_hol4_pending thy =
- let
- val rews = HOL4Rewrites.get thy
- val outthy = get_output_thy thy
- fun process (thy,((bthy,bthm),hth as (_,thm))) =
- let
- val sg = sign_of thy
- val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm)
- val thm2 = standard thm1
- val thy2 = PureThy.store_thm ((bthm, thm2), []) thy |> snd
- val thy5 = add_hol4_theorem bthy bthm hth thy2
- in
- thy5
- end
-
- val pending = HOL4Pending.get thy
- val thy1 = StringPair.foldl process (thy,pending)
- val thy2 = HOL4Pending.put (StringPair.empty) thy1
- in
- thy2
- end;
+ let
+ val rews = HOL4Rewrites.get thy;
+ val pending = HOL4Pending.get thy;
+ fun process ((bthy,bthm), hth as (_,thm)) thy =
+ let
+ val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
+ val thm2 = standard thm1;
+ in
+ thy
+ |> PureThy.store_thm ((bthm, thm2), [])
+ |> snd
+ |> add_hol4_theorem bthy bthm hth
+ end;
+ in
+ thy
+ |> StringPair.fold process pending
+ |> HOL4Pending.put StringPair.empty
+ end;
fun setup_dump (dir,thyname) thy =
HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
@@ -562,46 +560,22 @@
val output_thy = get_output_thy thy
val input_thy = Context.theory_name thy
val import_segment = get_import_segment thy
- val sg = sign_of thy
val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
file=thyname ^ ".imp"})
fun out s = TextIO.output(os,s)
- val (ignored,mapped) =
- StringPair.foldl (fn ((ign,map),((bthy,bthm),v)) =>
- if bthy = thyname
- then (case v of
- NONE => (bthm::ign,map)
- | SOME w => (ign,(bthm,w)::map))
- else (ign,map))
- (([],[]),HOL4Maps.get thy)
- val constmaps =
- StringPair.foldl (fn (map,((bthy,bthm),v)) =>
- if bthy = thyname
- then (bthm,v)::map
- else map)
- ([],HOL4ConstMaps.get thy)
-
- val constrenames =
- StringPair.foldl (fn (map,((bthy,bthm),v)) =>
- if bthy = thyname
- then (bthm,v)::map
- else map)
- ([],HOL4Rename.get thy)
-
- val typemaps =
- StringPair.foldl (fn (map,((bthy,bthm),v)) =>
- if bthy = thyname
- then (bthm,v)::map
- else map)
- ([],HOL4TypeMaps.get thy)
-
- val defmaps =
- StringPair.foldl (fn (map,((bthy,bthm),v)) =>
- if bthy = thyname
- then (bthm,v)::map
- else map)
- ([],HOL4DefMaps.get thy)
-
+ val (ignored, mapped) = StringPair.fold
+ (fn ((bthy, bthm), v) => fn (ign, map) =>
+ if bthy = thyname
+ then case v
+ of NONE => (bthm :: ign, map)
+ | SOME w => (ign, (bthm, w) :: map)
+ else (ign, map)) (HOL4Maps.get thy) ([],[]);
+ fun mk init = StringPair.fold
+ (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
+ val constmaps = mk (HOL4ConstMaps.get thy);
+ val constrenames = mk (HOL4Rename.get thy);
+ val typemaps = mk (HOL4TypeMaps.get thy);
+ val defmaps = mk (HOL4DefMaps.get thy);
fun new_name internal isa =
if internal
then
@@ -643,7 +617,7 @@
val _ = app (fn (hol,(internal,isa,opt_ty)) =>
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
case opt_ty of
- SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")
+ SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of thy ty)) ^ "\"")
| NONE => ())) constmaps
val _ = if null constmaps
then ()
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Fri Oct 20 10:44:33 2006 +0200
@@ -729,13 +729,11 @@
fun merge a b = Symtab.merge (op =) (a, b)
-fun mergemap f ts = Library.foldl
- (fn (table, x) => merge table (f x))
- (Symtab.empty, ts)
+fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
-fun diff a b = Symtab.foldl (fn (a, (k,v)) =>
+fun diff a b = Symtab.fold (fn (k, v) => fn a =>
(Symtab.delete k a) handle UNDEF => a)
- (a, b)
+ b a
fun collect_vars (cplexVar v) = singleton v
| collect_vars (cplexNeg t) = collect_vars t
@@ -787,15 +785,13 @@
cplexVar v, cplexLeq,
cplexInf)
- val pos_constrs = rev(Symtab.foldl
- (fn (l, (k,v)) => (make_pos_constr k) :: l)
- ([], positive_vars))
- val bound_constrs = map (fn x => (NONE, x))
- (Library.flat (map bound2constr bounds))
- val constraints' = constraints @ pos_constrs @ bound_constrs
- val bounds' = rev(Symtab.foldl (fn (l, (v,_)) =>
- (make_free_bound v)::l)
- ([], cvars))
+ val pos_constrs = rev (Symtab.fold
+ (fn (k, v) => cons (make_pos_constr k))
+ positive_vars [])
+ val bound_constrs = map (pair NONE)
+ (maps bound2constr bounds)
+ val constraints' = constraints @ pos_constrs @ bound_constrs
+ val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
in
cplexProg (name, goal, constraints', bounds')
end
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Oct 20 10:44:33 2006 +0200
@@ -30,8 +30,8 @@
val v_elem_at : vector -> int -> string option
val m_elem_at : matrix -> int -> vector option
val v_only_elem : vector -> int option
- val v_fold : ('a * (int * string) -> 'a) -> 'a -> vector -> 'a
- val m_fold : ('a * (int * vector) -> 'a) -> 'a -> matrix -> 'a
+ val v_fold : (int * string -> 'a -> 'a) -> vector -> 'a -> 'a
+ val m_fold : (int * vector -> 'a -> 'a) -> matrix -> 'a -> 'a
val transpose_matrix : matrix -> matrix
@@ -129,7 +129,7 @@
fun approx_vector_term prec pprt vector =
let
- fun app ((vlower, vupper), (index, s)) =
+ fun app (index, s) (vlower, vupper) =
let
val (flower, fupper) = approx_value_term prec pprt s
val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
@@ -140,26 +140,22 @@
Cons_spvec_const $ eupper $ vupper)
end
in
- Inttab.foldl app ((empty_vector_const, empty_vector_const), vector)
+ Inttab.fold app vector (empty_vector_const, empty_vector_const)
end
fun approx_matrix_term prec pprt matrix =
- let
- fun app ((mlower, mupper), (index, vector)) =
- let
- val (vlower, vupper) = approx_vector_term prec pprt vector
- val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
- val elower = HOLogic.mk_prod (index, vlower)
- val eupper = HOLogic.mk_prod (index, vupper)
- in
- (Cons_spmat_const $ elower $ mlower,
- Cons_spmat_const $ eupper $ mupper)
- end
-
- val (mlower, mupper) = Inttab.foldl app ((empty_matrix_const, empty_matrix_const), matrix)
- in
- Inttab.foldl app ((empty_matrix_const, empty_matrix_const), matrix)
- end
+ let
+ fun app (index, vector) (mlower, mupper) =
+ let
+ val (vlower, vupper) = approx_vector_term prec pprt vector
+ val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
+ val elower = HOLogic.mk_prod (index, vlower)
+ val eupper = HOLogic.mk_prod (index, vupper)
+ in
+ (Cons_spmat_const $ elower $ mlower, Cons_spmat_const $ eupper $ mupper)
+ end
+ val (mlower, mupper) = Inttab.fold app matrix (empty_matrix_const, empty_matrix_const)
+ in Inttab.fold app matrix (empty_matrix_const, empty_matrix_const) end;
fun approx_vector prec pprt vector =
let
@@ -204,18 +200,11 @@
structure cplex = Cplex
fun transpose_matrix matrix =
- let
- fun upd m j i x =
- case Inttab.lookup m j of
- SOME v => Inttab.update (j, Inttab.update (i, x) v) m
- | NONE => Inttab.update (j, Inttab.update (i, x) Inttab.empty) m
-
- fun updv j (m, (i, s)) = upd m i j s
-
- fun updm (m, (j, v)) = Inttab.foldl (updv j) (m, v)
- in
- Inttab.foldl updm (empty_matrix, matrix)
- end
+ let
+ fun upd j (i, s) =
+ Inttab.map_default (i, Inttab.empty) (Inttab.update (j, s));
+ fun updm (j, v) = Inttab.fold (upd j) v;
+ in Inttab.fold updm matrix empty_matrix end;
exception No_name of string;
@@ -251,7 +240,7 @@
end
fun vec2sum vector =
- cplex.cplexSum (Inttab.foldl (fn (list, (index, s)) => (mk_term index s)::list) ([], vector))
+ cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s) :: list) vector [])
fun mk_constr index vector c =
let
@@ -264,16 +253,16 @@
fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
- val (list, b) = Inttab.foldl
- (fn ((list, c), (index, v)) => ((mk_constr index v c)::list, delete index c))
- (([], b), A)
+ val (list, b) = Inttab.fold
+ (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
+ A ([], b)
val _ = if Inttab.is_empty b then () else raise Superfluous_constr_right_hand_sides
fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq,
cplex.cplexVar y, cplex.cplexLeq,
cplex.cplexInf)
- val yvars = Inttab.foldl (fn (l, (i, y)) => (mk_free y)::l) ([], !ytable)
+ val yvars = Inttab.fold (fn (i, y) => fn l => (mk_free y)::l) (!ytable) []
val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
in
@@ -304,7 +293,7 @@
end
fun vec2sum vector =
- cplex.cplexSum (Inttab.foldl (fn (list, (index, s)) => (mk_term index s)::list) ([], vector))
+ cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s)::list) vector [])
fun mk_constr index vector c =
let
@@ -317,9 +306,9 @@
fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
- val (list, c) = Inttab.foldl
- (fn ((list, c), (index, v)) => ((mk_constr index v c)::list, delete index c))
- (([], c), transpose_matrix A)
+ val (list, c) = Inttab.fold
+ (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
+ (transpose_matrix A) ([], c)
val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
@@ -328,30 +317,24 @@
end
fun cut_vector size v =
- let
- val count = ref 0
- fun app (v, (i, s)) =
- if (!count < size) then
- (count := !count +1 ; Inttab.update (i,s) v)
- else
- v
- in
- Inttab.foldl app (empty_vector, v)
- end
+ let
+ val count = ref 0;
+ fun app (i, s) = if (!count < size) then
+ (count := !count +1 ; Inttab.update (i, s))
+ else I
+ in
+ Inttab.fold app v empty_vector
+ end
fun cut_matrix vfilter vsize m =
- let
- fun app (m, (i, v)) =
- if Inttab.lookup vfilter i = NONE then
- m
- else
- case vsize of
- NONE => Inttab.update (i,v) m
- | SOME s => Inttab.update (i, cut_vector s v) m
- in
- Inttab.foldl app (empty_matrix, m)
- end
-
+ let
+ fun app (i, v) =
+ if is_none (Inttab.lookup vfilter i) then I
+ else case vsize
+ of NONE => Inttab.update (i, v)
+ | SOME s => Inttab.update (i, cut_vector s v)
+ in Inttab.fold app m empty_matrix end
+
fun v_elem_at v i = Inttab.lookup v i
fun m_elem_at m i = Inttab.lookup m i
@@ -362,8 +345,7 @@
NONE => SOME vmin
| SOME vmax => if vmin = vmax then SOME vmin else NONE)
-fun v_fold f a v = Inttab.foldl f (a,v)
-
-fun m_fold f a m = Inttab.foldl f (a,m)
+fun v_fold f = Inttab.fold f;
+fun m_fold f = Inttab.fold f;
end;
--- a/src/HOL/Matrix/cplex/fspmlp.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML Fri Oct 20 10:44:33 2006 +0200
@@ -107,24 +107,15 @@
VarGraph.update (dest_key, (sure_bound, Inttab.update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
fun split_graph g =
- let
- fun split ((r1, r2), (key, (sure_bound, _))) =
- case sure_bound of
- NONE => (r1, r2)
- | SOME bound =>
- (case key of
- (u, UPPER) => (r1, Inttab.update (u, bound) r2)
- | (u, LOWER) => (Inttab.update (u, bound) r1, r2))
- in
- VarGraph.foldl split ((Inttab.empty, Inttab.empty), g)
- end
+ let
+ fun split (key, (sure_bound, _)) (r1, r2) = case sure_bound
+ of NONE => (r1, r2)
+ | SOME bound => (case key
+ of (u, UPPER) => (r1, Inttab.update (u, bound) r2)
+ | (u, LOWER) => (Inttab.update (u, bound) r1, r2))
+ in VarGraph.fold split g (Inttab.empty, Inttab.empty) end
-fun it2list t =
- let
- fun tolist (l, a) = a::l
- in
- Inttab.foldl tolist ([], t)
- end
+fun it2list t = Inttab.fold cons t [];
(* If safe is true, termination is guaranteed, but the sure bounds may be not optimal (relative to the algorithm).
If safe is false, termination is not guaranteed, but on termination the sure bounds are optimal (relative to the algorithm) *)
@@ -147,9 +138,9 @@
val mult_btype = case btype of UPPER => mult_upper | LOWER => mult_lower
- fun calc_sure_bound (sure_bound, (row_index, (row_bound, sources))) =
+ fun calc_sure_bound (row_index, (row_bound, sources)) sure_bound =
let
- fun add_src_bound (sum, (coeff, src_key)) =
+ fun add_src_bound (coeff, src_key) sum =
case sum of
NONE => NONE
| SOME x =>
@@ -157,7 +148,7 @@
NONE => NONE
| SOME src_sure_bound => SOME (FloatArith.add x (mult_btype src_sure_bound coeff)))
in
- case Library.foldl add_src_bound (SOME row_bound, sources) of
+ case fold add_src_bound sources (SOME row_bound) of
NONE => sure_bound
| new_sure_bound as (SOME new_bound) =>
(case sure_bound of
@@ -172,13 +163,13 @@
NONE => NONE
| SOME (sure_bound, f) =>
let
- val x = Inttab.foldl calc_sure_bound (sure_bound, f)
+ val x = Inttab.fold calc_sure_bound f sure_bound
in
if x = sure_bound then NONE else x
end
end
- fun propagate ((g, b), (key, _)) =
+ fun propagate (key, _) (g, b) =
case calc_sure_bound_from_sources g key of
NONE => (g,b)
| SOME bound => (update_sure_bound g key bound,
@@ -189,7 +180,7 @@
else
true)
- val (g, b) = VarGraph.foldl propagate ((g, false), g)
+ val (g, b) = VarGraph.fold propagate g (g, false)
in
if b then propagate_sure_bounds safe names g else g
end
@@ -212,15 +203,15 @@
else 0)
else 0
- fun calcr (g, (row_index, a)) =
- let
+ fun calcr (row_index, a) g =
+ let
val b = FloatSparseMatrixBuilder.v_elem_at b row_index
val (_, b2) = ExactFloatingPoint.approx_decstr_by_bin prec (case b of NONE => "0" | SOME b => b)
- val approx_a = FloatSparseMatrixBuilder.v_fold (fn (l, (i,s)) =>
- (i, ExactFloatingPoint.approx_decstr_by_bin prec s)::l) [] a
+ val approx_a = FloatSparseMatrixBuilder.v_fold (fn (i, s) => fn l =>
+ (i, ExactFloatingPoint.approx_decstr_by_bin prec s)::l) a []
- fun fold_dest_nodes (g, (dest_index, dest_value)) =
- let
+ fun fold_dest_nodes (dest_index, dest_value) g =
+ let
val dest_test = test_1 dest_value
in
if dest_test = 0 then
@@ -232,7 +223,7 @@
else
((dest_index, UPPER), b2)
- fun fold_src_nodes (g, (src_index, src_value as (src_lower, src_upper))) =
+ fun fold_src_nodes (src_index, src_value as (src_lower, src_upper)) g =
if src_index = dest_index then g
else
let
@@ -246,7 +237,7 @@
add_edge g (src_index, LOWER) dest_key row_index coeff
end
in
- Library.foldl fold_src_nodes ((add_row_bound g dest_key row_index row_bound), approx_a)
+ fold fold_src_nodes approx_a (add_row_bound g dest_key row_index row_bound)
end
end
in
@@ -263,10 +254,10 @@
else
g
end
- | _ => Library.foldl fold_dest_nodes (g, approx_a)
+ | _ => fold fold_dest_nodes approx_a g
end
- val g = FloatSparseMatrixBuilder.m_fold calcr VarGraph.empty A
+ val g = FloatSparseMatrixBuilder.m_fold calcr A VarGraph.empty
val g = propagate_sure_bounds safe_propagation names g
val (r1, r2) = split_graph g
--- a/src/HOL/Tools/refute.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/HOL/Tools/refute.ML Fri Oct 20 10:44:33 2006 +0200
@@ -421,10 +421,10 @@
(* (string * Term.term) list *)
val axioms = Theory.all_axioms_of thy;
(* string list *)
- val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
- #rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
+ val rec_names = Symtab.fold (fn (_, info) => fn acc =>
+ #rec_names info @ acc) (DatatypePackage.get_datatypes thy) []
(* string list *)
- val const_of_class_names = map Logic.const_of_class (Sign.classes (sign_of thy))
+ val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
(* given a constant 's' of type 'T', which is a subterm of 't', where *)
(* 't' has a (possibly) more general type, the schematic type *)
(* variables in 't' are instantiated to match the type 'T' (may raise *)
@@ -1891,12 +1891,12 @@
(* terms has had a chance to look at 't' *)
(Const (s, T), params) =>
(* iterate over all datatypes in 'thy' *)
- Symtab.foldl (fn (result, (_, info)) =>
+ Symtab.fold (fn (_, info) => fn result =>
case result of
SOME _ =>
result (* just keep 'result' *)
| NONE =>
- if s mem (#rec_names info) then
+ if member (op =) (#rec_names info) s then
(* we do have a recursion operator of the datatype given by 'info', *)
(* or of a mutually recursive datatype *)
let
@@ -2069,7 +2069,7 @@
end
else
NONE (* not a recursion operator of this datatype *)
- ) (NONE, DatatypePackage.get_datatypes thy)
+ ) (DatatypePackage.get_datatypes thy) NONE
| _ => (* head of term is not a constant *)
NONE;
--- a/src/Pure/Proof/proof_syntax.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Oct 20 10:44:33 2006 +0200
@@ -96,13 +96,13 @@
val thms = thms_of_proof prf Symtab.empty;
val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy);
- val tab = Symtab.foldl (fn (tab, (key, ps)) =>
+ val tab = Symtab.fold (fn (key, ps) => fn tab =>
let val prop = the_default (Bound 0) (AList.lookup (op =) thms' key)
- in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
+ in fst (fold_rev (fn (prop', prf) => fn x as (tab, i) =>
if prop <> prop' then
(Symtab.update (key ^ "_" ^ string_of_int i, prf) tab, i+1)
- else x) (tab, 1) ps)
- end) (Symtab.empty, thms);
+ else x) ps (tab, 1))
+ end) thms Symtab.empty;
fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
| rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
--- a/src/Pure/codegen.ML Thu Oct 19 12:08:27 2006 +0200
+++ b/src/Pure/codegen.ML Fri Oct 20 10:44:33 2006 +0200
@@ -561,7 +561,7 @@
fun is_instance thy T1 T2 =
Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
-fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) =>
+fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
fun get_aux_code xs = map_filter (fn (m, code) =>
@@ -581,16 +581,14 @@
val (s, T) = dest_Const c
in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
end handle TERM _ => NONE;
- fun add_def thyname (defs, (name, t)) = (case dest t of
- NONE => defs
+ fun add_def thyname (name, t) = (case dest t of
+ NONE => I
| SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of
- NONE => defs
- | SOME (s, (T, (args, rhs))) => Symtab.update
- (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
- the_default [] (Symtab.lookup defs s)) defs))
+ NONE => I
+ | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, [])
+ (cons (T, (thyname, split_last (rename_terms (args @ [rhs])))))))
in
- foldl (fn ((thyname, axms), defs) =>
- Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
+ fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
end;
fun get_defn thy defs s T = (case Symtab.lookup defs s of
@@ -848,7 +846,7 @@
fun string_of_cycle (a :: b :: cs) =
let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
if a = a' then Option.map (pair x)
- (Library.find_first (equal b o #2 o Graph.get_node gr)
+ (find_first (equal b o #2 o Graph.get_node gr)
(Graph.imm_succs gr x))
else NONE) code
in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
@@ -987,7 +985,7 @@
Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" ::
flat (separate [Pretty.str ",", Pretty.brk 1]
(map (fn ((s, T), s') => [Pretty.block
- [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
+ [Pretty.str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
mk_app false (mk_term_of gr "Generated" false T)
[Pretty.str s'], Pretty.str ")"]]) frees')) @
[Pretty.str "]"])]],