# HG changeset patch # User haftmann # Date 1328910681 -3600 # Node ID eff798e48efc0214aad86da3605f8bd451c91a25 # Parent d5d14046686f2c07f2d2fc76dfe4d86e9db64393 dropped dead code diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/am.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/am_compiler.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/am_ghc.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/am_interpreter.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/am_sml.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/compute.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Compute_Oracle/linker.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/CplexMatrixConverter.ML --- 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) diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/Cplex_tools.ML --- 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;*) diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/FloatSparseMatrixBuilder.ML --- 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 diff -r d5d14046686f -r eff798e48efc src/HOL/Matrix/matrixlp.ML --- 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"