--- a/src/HOL/Matrix/Compute_Oracle/am.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML Fri Feb 10 22:51:21 2012 +0100
@@ -50,13 +50,13 @@
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
check_freevars 0 t iff t is closed*)
fun check_freevars free (Var x) = x < free
- | check_freevars free (Const c) = true
+ | check_freevars free (Const _) = true
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
| check_freevars free (Abs m) = check_freevars (free+1) m
| check_freevars free (Computed t) = check_freevars free t
fun forall_consts pred (Const c) = pred c
- | forall_consts pred (Var x) = true
+ | forall_consts pred (Var _) = true
| forall_consts pred (App (u,v)) = forall_consts pred u
andalso forall_consts pred v
| forall_consts pred (Abs m) = forall_consts pred m
@@ -70,6 +70,6 @@
exception Run of string;
-fun run p t = raise Run "abstract machine stub"
+fun run _ _ = raise Run "abstract machine stub"
end
--- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Fri Feb 10 22:51:21 2012 +0100
@@ -52,8 +52,7 @@
if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")"
else pattern
- fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
- "Var " ^ str x
+ fun print_term d (Var x) = "Var " ^ str x
| print_term d (Const c) = "c" ^ str c
| print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
| print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
@@ -191,10 +190,10 @@
| SOME r => (compiled_rewriter := NONE; r)
end
-fun compile cache_patterns const_arity eqs =
+fun compile _ _ eqs =
let
- val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
- val eqs = map (fn (a,b,c) => (b,c)) eqs
+ val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
+ val eqs = map (fn (_,b,c) => (b,c)) eqs
fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule")
val _ = map (fn (p, r) =>
(check (p, r);
@@ -205,7 +204,7 @@
fun run prog t = (prog t)
-fun discard p = ()
-
+fun discard _ = ()
+
end
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Fri Feb 10 22:51:21 2012 +0100
@@ -44,7 +44,7 @@
fun arity_of c = the (Inttab.lookup arity c)
fun adjust_pattern PVar = PVar
| adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C
- fun adjust_rule (PVar, t) = raise Compile ("pattern may not be a variable")
+ fun adjust_rule (PVar, _) = raise Compile ("pattern may not be a variable")
| adjust_rule (rule as (p as PConst (c, args),t)) =
let
val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else ()
@@ -211,16 +211,15 @@
end
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
-fun wrap s = "\""^s^"\""
fun writeTextFile name s = File.write (Path.explode name) s
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
-fun compile cache_patterns const_arity eqs =
+fun compile _ _ eqs =
let
- val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
- val eqs = map (fn (a,b,c) => (b,c)) eqs
+ val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
+ val eqs = map (fn (_,b,c) => (b,c)) eqs
val guid = get_guid ()
val module = "AMGHC_Prog_"^guid
val (arity, source) = haskell_prog module eqs
@@ -266,7 +265,7 @@
in
(app_args args (Const c), rest)
end
- | (NONE, rest) => raise Run "parse C")
+ | (NONE, _) => raise Run "parse C")
| parse (#"c"::rest) =
(case parse_int rest of
(SOME c, rest) => (Const c, rest)
@@ -278,7 +277,7 @@
in
(App (a,b), rest)
end
- | parse (#"L"::rest) = raise Run "there may be no abstraction in the result"
+ | parse (#"L"::_) = raise Run "there may be no abstraction in the result"
| parse _ = raise Run "invalid result"
and parse_list n rest =
if n = 0 then
@@ -321,8 +320,7 @@
t'
end
-
fun discard _ = ()
-
+
end
--- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Fri Feb 10 22:51:21 2012 +0100
@@ -32,7 +32,7 @@
| term_of_clos (CConst c) = Const c
| term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
| term_of_clos (CAbs u) = Abs (term_of_clos u)
- | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
+ | term_of_clos (Closure _) = raise (Run "internal error: closure in normalized term found")
| term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found")
fun resolve_closure closures (CVar x) = (case nth closures x of CDummy => CVar x | r => r)
@@ -61,7 +61,7 @@
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
| strip_closure args x = (x, args)
-fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
+fun len_head_of_closure n (CApp (a, _)) = len_head_of_closure (n+1) a
| len_head_of_closure n x = (n, x)
@@ -95,12 +95,12 @@
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
check_freevars 0 t iff t is closed*)
fun check_freevars free (Var x) = x < free
- | check_freevars free (Const c) = true
+ | check_freevars free (Const _) = true
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
| check_freevars free (Abs m) = check_freevars (free+1) m
| check_freevars free (Computed t) = check_freevars free t
-fun compile cache_patterns const_arity eqs =
+fun compile _ _ eqs =
let
fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule")
fun check_guard p (Guard (a,b)) = (check p a; check p b)
@@ -161,13 +161,13 @@
and weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
| weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
| weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case nth e n of CDummy => CVar n | r => r)
- | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
+ | weak_reduce (false, prog, stack, Closure (_, c as CConst _)) = Continue (false, prog, stack, c)
| weak_reduce (false, prog, stack, clos) =
(case match_closure prog clos of
NONE => Continue (true, prog, stack, clos)
| SOME r => Continue (false, prog, stack, r))
| weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
- | weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
+ | weak_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
| weak_reduce (true, prog, stack, c) = Stop (stack, c)
and strong_reduce (false, prog, stack, Closure (e, CAbs m)) =
@@ -178,7 +178,7 @@
SEmpty => Continue (false, prog, SAbs stack, wnf)
| _ => raise (Run "internal error in strong: weak failed")
end handle InterruptedExecution state => raise InterruptedExecution (stack, resolve state))
- | strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u)
+ | strong_reduce (false, prog, stack, CApp (u, v)) = Continue (false, prog, SAppL (v, stack), u)
| strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos)
| strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m)
| strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
@@ -208,6 +208,6 @@
| _ => raise (Run "internal error in run: weak failed")
end handle InterruptedExecution state => term_of_clos (resolve state))
-fun discard p = ()
+fun discard _ = ()
end
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML Fri Feb 10 22:51:21 2012 +0100
@@ -26,7 +26,6 @@
val saved_result = Unsynchronized.ref (NONE:(string*term)option)
fun save_result r = (saved_result := SOME r)
-fun clear_result () = (saved_result := NONE)
val list_nth = List.nth
@@ -102,7 +101,7 @@
let
fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
| term_contains_const c (Abs m) = term_contains_const c m
- | term_contains_const c (Var i) = false
+ | term_contains_const c (Var _) = false
| term_contains_const c (Const c') = (c = c')
fun find_rewrite [] = NONE
| find_rewrite ((prems, PConst (c, []), r) :: _) =
@@ -115,7 +114,7 @@
SOME (c, r)
else raise Compile "unbound variable on right hand side or guards of rule"
| find_rewrite (_ :: rules) = find_rewrite rules
- fun remove_rewrite (c,r) [] = []
+ fun remove_rewrite _ [] = []
| remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) =
(if c = c' then
if null args andalso r = r' andalso null (prems') then
@@ -152,11 +151,10 @@
fun adjust_rules rules =
let
val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty
- val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
+ val toplevel_arity = fold (fn (_, p, _) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
fun arity_of c = the (Inttab.lookup arity c)
- fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c)
fun test_pattern PVar = ()
- | test_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ())
+ | test_pattern (PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ())
fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable")
| adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters")
| adjust_rule (rule as (prems, p as PConst (c, args),t)) =
@@ -492,7 +490,7 @@
fun use_source src = use_text ML_Env.local_context (1, "") false src
-fun compile cache_patterns const_arity eqs =
+fun compile _ _ eqs =
let
val guid = get_guid ()
val code = Real.toString (random ())
@@ -507,29 +505,7 @@
| SOME f => (module, code, arity, toplevel_arity, inlinetab, f)
end
-
-fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t =
- let
- val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
- fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
- | inline (Var i) = Var i
- | inline (App (a, b)) = App (inline a, inline b)
- | inline (Abs m) = Abs (inline m)
- val t = beta (inline t)
- fun arity_of c = Inttab.lookup arity c
- fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
- val term = print_term NONE arity_of toplevel_arity_of 0 0 t
- val source = "local open "^module^" in val _ = export ("^term^") end"
- val _ = writeTextFile "Gencode_call.ML" source
- val _ = clear_result ()
- val _ = use_source source
- in
- case !saved_result of
- NONE => raise Run "broken link to compiled code"
- | SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked")
- end
-
-fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t =
+fun run (_, _, _, _, inlinetab, compiled_fun) t =
let
val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
@@ -541,6 +517,6 @@
compiled_fun (beta (inline t))
end
-fun discard p = ()
-
+fun discard _ = ()
+
end
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Feb 10 22:51:21 2012 +0100
@@ -84,7 +84,7 @@
exception Compute of string;
local
- fun make_constant t ty encoding =
+ fun make_constant t encoding =
let
val (code, encoding) = Encode.insert t encoding
in
@@ -94,10 +94,10 @@
fun remove_types encoding t =
case t of
- Var (_, ty) => make_constant t ty encoding
- | Free (_, ty) => make_constant t ty encoding
- | Const (_, ty) => make_constant t ty encoding
- | Abs (_, ty, t') =>
+ Var _ => make_constant t encoding
+ | Free _ => make_constant t encoding
+ | Const _ => make_constant t encoding
+ | Abs (_, _, t') =>
let val (encoding, t'') = remove_types encoding t' in
(encoding, AbstractMachine.Abs t'')
end
@@ -133,7 +133,7 @@
case aty of
Type ("fun", [dom, range]) => (dom, range)
| _ => raise Fail "infer_types: function type expected"
- val (b, bty) = infer_types level bounds (SOME adom) b
+ val (b, _) = infer_types level bounds (SOME adom) b
in
(a $ b, arange)
end
@@ -143,7 +143,7 @@
in
(Abs (naming level, dom, m), ty)
end
- | infer_types _ _ NONE (AbstractMachine.Abs m) =
+ | infer_types _ _ NONE (AbstractMachine.Abs _) =
raise Fail "infer_types: cannot infer type of abstraction"
fun infer ty term =
@@ -183,10 +183,10 @@
fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
-fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' =
+fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,_,p2,p3,p4,p5,p6)))) encoding' =
(r := SOME (p1,encoding',p2,p3,p4,p5,p6))
fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
-fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'=
+fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,_)))) naming'=
(r := SOME (p1,p2,p3,p4,p5,p6,naming'))
fun ref_of (Computer r) = r
@@ -206,9 +206,9 @@
fun transfer (x:thm) = Thm.transfer thy x
val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
- fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
+ fun make_pattern encoding n vars (AbstractMachine.Abs _) =
raise (Make "no lambda abstractions allowed in pattern")
- | make_pattern encoding n vars (var as AbstractMachine.Var _) =
+ | make_pattern encoding n vars (AbstractMachine.Var _) =
raise (Make "no bound variables allowed in pattern")
| make_pattern encoding n vars (AbstractMachine.Const code) =
(case the (Encode.lookup_term code encoding) of
@@ -299,7 +299,7 @@
val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
- fun arity (Type ("fun", [a,b])) = 1 + arity b
+ fun arity (Type ("fun", [_, b])) = 1 + arity b
| arity _ = 0
fun make_arity (Const (s, _), i) tab =
@@ -456,7 +456,7 @@
(encoding, Symtab.update (s, (x, ty)) tab)
end
val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)
- val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab))
+ val varsubst = Inttab.make (map (fn (_, (x, _)) => (x, NONE)) (Symtab.dest vartab))
(* make the premises and the conclusion *)
fun mk_prem encoding t =
@@ -510,7 +510,6 @@
fun rewrite computer t =
let
- val naming = naming_of computer
val (encoding, t) = remove_types (encoding_of computer) t
val t = runprog (prog_of computer) t
val _ = set_encoding computer encoding
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Fri Feb 10 22:51:21 2012 +0100
@@ -190,12 +190,10 @@
fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
-fun eq_to_meta th = (@{thm HOL.eq_reflection} OF [th] handle THM _ => th)
-
local
-fun collect (Var x) tab = tab
+fun collect (Var _) tab = tab
| collect (Bound _) tab = tab
| collect (a $ b) tab = collect b (collect a tab)
| collect (Abs (_, _, body)) tab = collect body tab
--- a/src/HOL/Matrix/CplexMatrixConverter.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/CplexMatrixConverter.ML Fri Feb 10 22:51:21 2012 +0100
@@ -52,7 +52,7 @@
| neg_term (cplexSum ts) = cplexSum (map neg_term ts)
| neg_term t = cplexNeg t
-fun convert_prog (cplexProg (s, goal, constrs, bounds)) =
+fun convert_prog (cplexProg (_, goal, constrs, bounds)) =
let
fun build_naming index i2s s2i [] = (index, i2s, s2i)
| build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
--- a/src/HOL/Matrix/Cplex_tools.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/Cplex_tools.ML Fri Feb 10 22:51:21 2012 +0100
@@ -108,7 +108,7 @@
fun is_Var (cplexVar _) = true
| is_Var _ = false
-fun is_Neg (cplexNeg x ) = true
+fun is_Neg (cplexNeg _) = true
| is_Neg _ = false
fun is_normed_Prod (cplexProd (t1, t2)) =
@@ -119,7 +119,7 @@
(ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
| is_normed_Sum x = modulo_signed is_normed_Prod x
-fun is_normed_Constr (cplexConstr (c, (t1, t2))) =
+fun is_normed_Constr (cplexConstr (_, (t1, t2))) =
(is_normed_Sum t1) andalso (modulo_signed is_Num t2)
fun is_Num_or_Inf x = is_Inf x orelse is_Num x
@@ -139,7 +139,7 @@
fun term_of_goal (cplexMinimize x) = x
| term_of_goal (cplexMaximize x) = x
-fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) =
+fun is_normed_cplexProg (cplexProg (_, goal, constraints, bounds)) =
is_normed_Sum (term_of_goal goal) andalso
forall (fn (_,x) => is_normed_Constr x) constraints andalso
forall is_normed_Bounds bounds
@@ -244,7 +244,7 @@
(is_delimiter, TOKEN_DELIMITER),
(is_cmp, TOKEN_CMP),
(is_symbol, TOKEN_SYMBOL)]
- fun match_helper [] s = (fn x => false, TOKEN_ERROR)
+ fun match_helper [] s = (fn _ => false, TOKEN_ERROR)
| match_helper (f::fs) s =
if ((fst f) s) then f else match_helper fs s
fun match s = match_helper flist s
@@ -516,9 +516,6 @@
(pushToken (the c); ())
end
- fun is_var (cplexVar _) = true
- | is_var _ = false
-
fun make_bounds c t1 t2 =
cplexBound (t1, c, t2)
@@ -572,7 +569,7 @@
fun readBounds () =
let
- fun makestring b = "?"
+ fun makestring _ = "?"
fun readbody () =
let
val b = readBound ()
@@ -606,7 +603,7 @@
cplexProg (name, result_Goal, result_ST, result_Bounds)
end
-fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
+fun save_cplexFile filename (cplexProg (_, goal, constraints, bounds)) =
let
val f = TextIO.openOut filename
@@ -744,14 +741,14 @@
IF for the input program P holds: is_normed_cplexProg P *)
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
let
- fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
+ fun collect_constr_vars (_, cplexConstr (_, (t1,_))) =
(collect_vars t1)
val cvars = merge (collect_vars (term_of_goal goal))
(mergemap collect_constr_vars constraints)
fun collect_lower_bounded_vars
- (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
+ (cplexBounds (_, _, cplexVar v, _, _)) =
singleton v
| collect_lower_bounded_vars
(cplexBound (_, cplexLe, cplexVar v)) =
@@ -783,7 +780,7 @@
cplexInf)
val pos_constrs = rev (Symtab.fold
- (fn (k, v) => cons (make_pos_constr k))
+ (fn (k, _) => cons (make_pos_constr k))
positive_vars [])
val bound_constrs = map (pair NONE)
(maps bound2constr bounds)
@@ -1170,11 +1167,7 @@
val resultname = tmp_file (name^".txt")
val scriptname = tmp_file (name^".script")
val _ = save_cplexFile lpname prog
- val cplex_path = getenv "CPLEX_PATH"
- val cplex = if cplex_path = "" then "cplex" else cplex_path
val _ = write_script scriptname lpname resultname
- val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
- val answer = "return code " ^ string_of_int (Isabelle_System.bash command)
in
let
val result = load_cplexResult resultname
@@ -1197,27 +1190,3 @@
| SOLVER_GLPK => solve_glpk prog
end;
-
-(*
-val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
-val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
-val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
-
-fun loadcplex () = Cplex.relax_strict_ineqs
- (Cplex.load_cplexFile demofile)
-
-fun writecplex lp = Cplex.save_cplexFile demoout lp
-
-fun test () =
- let
- val lp = loadcplex ()
- val lp2 = Cplex.elim_nonfree_bounds lp
- in
- writecplex lp2
- end
-
-fun loadresult () = Cplex.load_cplexResult demoresult;
-*)
-
-(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt";
-val _ = Cplex.solve prog;*)
--- a/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Fri Feb 10 22:51:21 2012 +0100
@@ -186,7 +186,7 @@
cplex.cplexVar y, cplex.cplexLeq,
cplex.cplexInf)
- val yvars = Inttab.fold (fn (i, y) => fn l => (mk_free y)::l) (!ytable) []
+ val yvars = Inttab.fold (fn (_, y) => fn l => (mk_free y)::l) (!ytable) []
val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
in
@@ -276,8 +276,8 @@
fun indices_of_matrix m = Inttab.keys m
fun delete_vector indices v = fold Inttab.delete indices v
fun delete_matrix indices m = fold Inttab.delete indices m
-fun cut_matrix' indices m = fold (fn i => fn m => (case Inttab.lookup m i of NONE => m | SOME v => Inttab.update (i, v) m)) indices Inttab.empty
-fun cut_vector' indices v = fold (fn i => fn v => (case Inttab.lookup v i of NONE => v | SOME x => Inttab.update (i, x) v)) indices Inttab.empty
+fun cut_matrix' indices _ = fold (fn i => fn m => (case Inttab.lookup m i of NONE => m | SOME v => Inttab.update (i, v) m)) indices Inttab.empty
+fun cut_vector' indices _ = fold (fn i => fn v => (case Inttab.lookup v i of NONE => v | SOME x => Inttab.update (i, x) v)) indices Inttab.empty
--- a/src/HOL/Matrix/matrixlp.ML Sun Feb 12 22:10:33 2012 +0100
+++ b/src/HOL/Matrix/matrixlp.ML Fri Feb 10 22:51:21 2012 +0100
@@ -51,20 +51,6 @@
end
-fun prep ths = ComputeHOL.prep_thms ths
-
-fun inst_tvar ty thm =
- let
- val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
- val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
- val v = TVar (hd (sort ord (Misc_Legacy.term_tvars (prop_of thm))))
- in
- Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
- end
-
-fun inst_tvars [] thms = thms
- | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
-
local
val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"