src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
author obua
Wed, 13 Jul 2005 09:53:50 +0200
changeset 16784 92ff7c903585
child 16873 9ed940a1bebb
permissions -rw-r--r--
- added cplex package to HOL/Matrix
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     1
(*  Title:      HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     2
    ID:         $Id$
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     3
    Author:     Steven Obua
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     4
*)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     5
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     6
structure FloatSparseMatrixBuilder :
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     7
sig
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     8
    include MATRIX_BUILDER
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     9
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    10
    structure cplex : CPLEX
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    11
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    12
    type float = IntInf.int*IntInf.int
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    13
    type floatfunc = float -> float
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    14
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    15
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    16
    val float2cterm : IntInf.int * IntInf.int -> cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    17
       
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    18
    val approx_value : int -> floatfunc -> string -> cterm * cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    19
    val approx_vector : int -> floatfunc -> vector -> cterm * cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    20
    val approx_matrix : int -> floatfunc -> matrix -> cterm * cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    21
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    22
    val mk_spvec_entry : int -> float -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    23
    val empty_spvec : term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    24
    val cons_spvec : term -> term -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    25
    val empty_spmat : term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    26
    val mk_spmat_entry : int -> term -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    27
    val cons_spmat : term -> term -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    28
    val sign_term : term -> cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    29
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    30
    val v_elem_at : vector -> int -> string option
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    31
    val m_elem_at : matrix -> int -> vector option
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    32
    val v_only_elem : vector -> int option
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    33
    val v_fold : ('a * (int * string) -> 'a) -> 'a -> vector -> 'a
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    34
    val m_fold : ('a * (int * vector) -> 'a) -> 'a -> matrix -> 'a
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    35
				   
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    36
    val transpose_matrix : matrix -> matrix
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    37
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    38
    val cut_vector : int -> vector -> vector
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    39
    val cut_matrix : vector -> (int option) -> matrix -> matrix
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    40
    
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    41
    (* cplexProg c A b *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    42
    val cplexProg : vector -> matrix -> vector -> (cplex.cplexProg * (string -> int))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    43
    (* dual_cplexProg c A b *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    44
    val dual_cplexProg : vector -> matrix -> vector -> (cplex.cplexProg * (string -> int))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    45
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    46
    val real_spmatT : typ
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    47
    val real_spvecT : typ
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    48
end 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    49
= 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    50
struct
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    51
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    52
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    53
structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    54
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    55
type vector = string Inttab.table
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    56
type matrix = vector Inttab.table
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    57
type float = IntInf.int*IntInf.int
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    58
type floatfunc = float -> float
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    59
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    60
val th = theory "FloatSparseMatrix"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    61
val sg = sign_of th
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    62
	 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    63
fun readtype s = Sign.intern_type sg s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    64
fun readterm s = Sign.intern_const sg s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    65
		 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    66
val ty_list = readtype "list"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    67
val term_Nil = readterm "Nil"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    68
val term_Cons = readterm "Cons"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    69
		
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    70
val spvec_elemT = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    71
val spvecT = Type (ty_list, [spvec_elemT])
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    72
val spmat_elemT = HOLogic.mk_prodT (HOLogic.natT, spvecT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    73
val spmatT = Type (ty_list, [spmat_elemT])
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    74
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    75
val real_spmatT = spmatT
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    76
val real_spvecT = spvecT
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    77
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    78
val empty_matrix_const = Const (term_Nil, spmatT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    79
val empty_vector_const = Const (term_Nil, spvecT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    80
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    81
val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    82
val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT) 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    83
			 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    84
val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    85
		  
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    86
val zero = IntInf.fromInt 0
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    87
val minus_one = IntInf.fromInt ~1
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    88
val two = IntInf.fromInt 2
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    89
	  
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    90
fun mk_intinf ty n =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    91
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    92
	fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    93
								 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    94
	fun bin_of n = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    95
	    if n = zero then HOLogic.pls_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    96
	    else if n = minus_one then HOLogic.min_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    97
	    else 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    98
		let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    99
		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   100
	            val q = IntInf.div (n, two)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   101
		    val r = IntInf.mod (n, two)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   102
		in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   103
		    HOLogic.bit_const $ bin_of q $ mk_bit r
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   104
		end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   105
    in 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   106
	HOLogic.number_of_const ty $ (bin_of n)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   107
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   108
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   109
fun mk_float (a,b) = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   110
    float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   111
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   112
fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   113
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   114
fun approx_value_term prec f value = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   115
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   116
	val (flower, fupper) = ExactFloatingPoint.approx_decstr_by_bin prec value
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   117
	val (flower, fupper) = (f flower, f fupper)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   118
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   119
	(mk_float flower, mk_float fupper)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   120
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   121
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   122
fun approx_value prec pprt value = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   123
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   124
	val (flower, fupper) = approx_value_term prec pprt value			       
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   125
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   126
	(cterm_of sg flower, cterm_of sg fupper)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   127
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   128
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   129
fun sign_term t = cterm_of sg t
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   130
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   131
val empty_spvec = empty_vector_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   132
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   133
val empty_spmat = empty_matrix_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   134
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   135
fun mk_spvec_entry i f = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   136
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   137
	val term_i = mk_intinf HOLogic.natT (IntInf.fromInt i)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   138
	val term_f = mk_float f
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   139
    in 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   140
	HOLogic.mk_prod (term_i, term_f)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   141
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   142
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   143
fun mk_spmat_entry i e = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   144
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   145
	val term_i = mk_intinf HOLogic.natT (IntInf.fromInt i)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   146
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   147
	HOLogic.mk_prod (term_i, e)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   148
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   149
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   150
fun cons_spvec h t = Cons_spvec_const $ h $ t
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   151
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   152
fun cons_spmat h t = Cons_spmat_const $ h $ t 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   153
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   154
fun approx_vector_term prec pprt vector = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   155
    let 	 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   156
	fun app ((vlower, vupper), (index, s)) = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   157
	    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   158
		val (flower, fupper) = approx_value_term prec pprt s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   159
		val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   160
		val elower = HOLogic.mk_prod (index, flower)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   161
		val eupper = HOLogic.mk_prod (index, fupper)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   162
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   163
		(Cons_spvec_const $ elower $ vlower,
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   164
		 Cons_spvec_const $ eupper $ vupper)	
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   165
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   166
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   167
	Inttab.foldl app ((empty_vector_const, empty_vector_const), vector)	
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   168
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   169
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   170
fun approx_matrix_term prec pprt matrix =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   171
    let 	 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   172
	fun app ((mlower, mupper), (index, vector)) = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   173
	    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   174
		val (vlower, vupper) = approx_vector_term prec pprt vector  
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   175
		val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   176
		val elower = HOLogic.mk_prod (index, vlower)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   177
		val eupper = HOLogic.mk_prod (index, vupper)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   178
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   179
		(Cons_spmat_const $ elower $ mlower,
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   180
		 Cons_spmat_const $ eupper $ mupper)		
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   181
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   182
		
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   183
	val (mlower, mupper) = Inttab.foldl app ((empty_matrix_const, empty_matrix_const), matrix)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   184
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   185
	Inttab.foldl app ((empty_matrix_const, empty_matrix_const), matrix)	
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   186
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   187
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   188
fun approx_vector prec pprt vector =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   189
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   190
	val (l, u) = approx_vector_term prec pprt vector
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   191
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   192
	(cterm_of sg l, cterm_of sg u)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   193
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   194
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   195
fun approx_matrix prec pprt matrix = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   196
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   197
	val (l, u) = approx_matrix_term prec pprt matrix
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   198
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   199
	(cterm_of sg l, cterm_of sg u)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   200
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   201
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   202
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   203
exception Nat_expected of int;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   204
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   205
val zero_interval = approx_value_term 1 I "0"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   206
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   207
fun set_elem vector index str = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   208
    if index < 0 then 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   209
	raise (Nat_expected index)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   210
    else if (approx_value_term 1 I str) = zero_interval then 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   211
	vector
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   212
    else  
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   213
	Inttab.update ((index, str), vector)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   214
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   215
fun set_vector matrix index vector = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   216
    if index < 0 then
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   217
	raise (Nat_expected index)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   218
    else if Inttab.is_empty vector then
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   219
	matrix
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   220
    else
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   221
	Inttab.update ((index, vector), matrix)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   222
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   223
val empty_matrix = Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   224
val empty_vector = Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   225
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   226
(* dual stuff *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   227
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   228
structure cplex = Cplex
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   229
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   230
fun transpose_matrix matrix = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   231
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   232
	fun upd m j i x =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   233
	    case Inttab.lookup (m, j) of
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   234
		SOME v => Inttab.update ((j, Inttab.update ((i, x), v)), m)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   235
	      | NONE => Inttab.update ((j, Inttab.update ((i, x), Inttab.empty)), m) 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   236
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   237
	fun updv j (m, (i, s)) = upd m i j s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   238
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   239
	fun updm (m, (j, v)) = Inttab.foldl (updv j) (m, v)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   240
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   241
	Inttab.foldl updm (empty_matrix, matrix)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   242
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   243
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   244
exception No_name of string;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   245
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   246
exception Superfluous_constr_right_hand_sides
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   247
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   248
fun cplexProg c A b = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   249
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   250
	val ytable = ref Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   251
	fun indexof s = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   252
	    if String.size s = 0 then raise (No_name s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   253
	    else case Int.fromString (String.extract(s, 1, NONE)) of 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   254
		     SOME i => i | NONE => raise (No_name s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   255
				     
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   256
	fun nameof i = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   257
	    let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   258
		val s = "x"^(Int.toString i)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   259
		val _ = ytable := (Inttab.update ((i, s), !ytable))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   260
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   261
		s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   262
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   263
	    
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   264
	fun split_numstr s = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   265
	    if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   266
	    else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   267
	    else (true, s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   268
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   269
	fun mk_term index s =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   270
	    let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   271
		val (p, s) = split_numstr s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   272
		val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   273
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   274
		if p then prod else cplex.cplexNeg prod
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   275
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   276
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   277
	fun vec2sum vector =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   278
	    cplex.cplexSum (Inttab.foldl (fn (list, (index, s)) => (mk_term index s)::list) ([], vector))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   279
		       		       
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   280
	fun mk_constr index vector c = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   281
	    let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   282
		val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   283
		val (p, s) = split_numstr s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   284
		val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   285
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   286
		(NONE, cplex.cplexConstr (cplex.cplexLeq, (vec2sum vector, num)))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   287
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   288
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   289
	fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   290
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   291
	val (list, b) = Inttab.foldl 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   292
			    (fn ((list, c), (index, v)) => ((mk_constr index v c)::list, delete index c))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   293
			    (([], b), A)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   294
	val _ = if Inttab.is_empty b then () else raise Superfluous_constr_right_hand_sides
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   295
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   296
	fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq, 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   297
					   cplex.cplexVar y, cplex.cplexLeq,
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   298
					   cplex.cplexInf)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   299
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   300
	val yvars = Inttab.foldl (fn (l, (i, y)) => (mk_free y)::l) ([], !ytable)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   301
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   302
	val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   303
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   304
	(prog, indexof)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   305
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   306
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   307
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   308
fun dual_cplexProg c A b = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   309
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   310
	fun indexof s = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   311
	    if String.size s = 0 then raise (No_name s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   312
	    else case Int.fromString (String.extract(s, 1, NONE)) of 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   313
		     SOME i => i | NONE => raise (No_name s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   314
				     
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   315
	fun nameof i = "y"^(Int.toString i)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   316
	    
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   317
	fun split_numstr s = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   318
	    if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   319
	    else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   320
	    else (true, s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   321
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   322
	fun mk_term index s =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   323
	    let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   324
		val (p, s) = split_numstr s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   325
		val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   326
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   327
		if p then prod else cplex.cplexNeg prod
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   328
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   329
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   330
	fun vec2sum vector =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   331
	    cplex.cplexSum (Inttab.foldl (fn (list, (index, s)) => (mk_term index s)::list) ([], vector))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   332
		       		       
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   333
	fun mk_constr index vector c = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   334
	    let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   335
		val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   336
		val (p, s) = split_numstr s
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   337
		val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   338
	    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   339
		(NONE, cplex.cplexConstr (cplex.cplexEq, (vec2sum vector, num)))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   340
	    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   341
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   342
	fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   343
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   344
	val (list, c) = Inttab.foldl 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   345
			    (fn ((list, c), (index, v)) => ((mk_constr index v c)::list, delete index c))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   346
			    (([], c), transpose_matrix A)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   347
	val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   348
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   349
	val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   350
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   351
	(prog, indexof)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   352
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   353
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   354
fun cut_vector size v = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   355
    let
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   356
	val count = ref 0 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   357
	fun app (v, (i, s)) = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   358
	    if (!count < size) then
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   359
		(count := !count +1 ; Inttab.update ((i,s),v))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   360
	    else
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   361
		v
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   362
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   363
	Inttab.foldl app (empty_vector, v)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   364
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   365
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   366
fun cut_matrix vfilter vsize m = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   367
    let 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   368
	fun app (m, (i, v)) = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   369
	    if (Inttab.lookup (vfilter, i) = NONE) then 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   370
		m 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   371
	    else 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   372
		case vsize of
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   373
		    NONE => Inttab.update ((i,v), m)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   374
		  | SOME s => Inttab.update((i, cut_vector s v),m)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   375
    in
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   376
	Inttab.foldl app (empty_matrix, m)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   377
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   378
		 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   379
fun v_elem_at v i = Inttab.lookup (v,i)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   380
fun m_elem_at m i = Inttab.lookup (m,i)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   381
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   382
fun v_only_elem v = 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   383
    case Inttab.min_key v of
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   384
	NONE => NONE
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   385
      | SOME vmin => (case Inttab.max_key v of
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   386
			  NONE => SOME vmin
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   387
			| SOME vmax => if vmin = vmax then SOME vmin else NONE)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   388
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   389
fun v_fold f a v = Inttab.foldl f (a,v) 
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   390
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   391
fun m_fold f a m = Inttab.foldl f (a,m)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   392
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   393
end;