--- 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;