# HG changeset patch # User wenzelm # Date 1464801798 -7200 # Node ID 0bec0d1d9998ed5de189ccc6ac70fea66cc0f1f9 # Parent a0685d2b420b54a361b0f05d5d080760e8c0f764 more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned; diff -r a0685d2b420b -r 0bec0d1d9998 NEWS --- a/NEWS Wed Jun 01 17:46:12 2016 +0200 +++ b/NEWS Wed Jun 01 19:23:18 2016 +0200 @@ -348,7 +348,7 @@ *** ML *** * Ad-hoc overloading for standard operations on type Rat.rat: + - * / = -< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc. +< <= > >= <> ~ abs. INCOMPATIBILITY, need to use + instead of +/ etc. * The ML function "ML" provides easy access to run-time compilation. This is particularly useful for conditional compilation, without diff -r a0685d2b420b -r 0bec0d1d9998 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Jun 01 17:46:12 2016 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Jun 01 19:23:18 2016 +0200 @@ -41,16 +41,12 @@ fun round_rat r = let - val (a,b) = Rat.dest (Rat.abs r) + val (a,b) = Rat.dest (abs r) val d = a div b - val s = if r < @0 then (Rat.neg o Rat.of_int) else Rat.of_int + val s = if r < @0 then ~ o Rat.of_int else Rat.of_int val x2 = 2 * (a - (b * d)) in s (if x2 >= b then d + 1 else d) end -val abs_rat = Rat.abs; -val pow2 = rat_pow @2; -val pow10 = rat_pow @10; - val trace = Attrib.setup_config_bool @{binding sos_trace} (K false); val debug = Attrib.setup_config_bool @{binding sos_debug} (K false); @@ -74,8 +70,8 @@ local fun normalize y = - if abs_rat y < @1/10 then normalize (@10 * y) - 1 - else if abs_rat y >= @1 then normalize (y / @10) + 1 + if abs y < @1/10 then normalize (@10 * y) - 1 + else if abs y >= @1 then normalize (y / @10) + 1 else 0 in @@ -84,10 +80,10 @@ if x = @0 then "0.0" else let - val y = Rat.abs x + val y = abs x val e = normalize y - val z = pow10(~ e) * y + @1 - val k = int_of_rat (round_rat(pow10 d * z)) + val z = rat_pow @10 (~ e) * y + @1 + val k = int_of_rat (round_rat (rat_pow @10 d * z)) in (if x < @0 then "-0." else "0.") ^ implode (tl (raw_explode(string_of_int k))) ^ @@ -182,7 +178,7 @@ if c = @0 then poly_0 else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p; -fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p; +fun poly_neg p = FuncUtil.Monomialfunc.map (K ~) p; fun poly_add p1 p2 = @@ -319,7 +315,7 @@ val numeral = Scan.one isnum val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode) val decimalfrac = Scan.repeat1 numeral - >> (fn s => rat_of_string(implode s) / pow10 (length s)) + >> (fn s => rat_of_string(implode s) / rat_pow @10 (length s)) val decimalsig = decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac) >> (fn (h,NONE) => h | (h,SOME x) => h + x) @@ -333,7 +329,7 @@ val exponent = ($$ "e" || $$ "E") |-- signed decimalint; val decimal = signed decimalsig -- (emptyin @0|| exponent) - >> (fn (h, x) => h * pow10 (int_of_rat x)); + >> (fn (h, x) => h * rat_pow @10 (int_of_rat x)); fun mkparser p s = let val (x,rst) = p (raw_explode s) @@ -359,7 +355,7 @@ fun common_denominator fld amat acc = fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc fun maximal_element fld amat acc = - fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc + fld (fn (_,c) => fn maxa => max_rat maxa (abs c)) amat acc fun float_of_rat x = let val (a,b) = Rat.dest x in Real.fromInt a / Real.fromInt b end; @@ -374,8 +370,8 @@ val obj' = vector_cmul cd2 obj val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0 val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0 - val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0)) - val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) + val scal1 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0)) + val scal2 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats' val obj'' = vector_cmul scal2 obj' in solver obj'' mats'' end @@ -438,7 +434,7 @@ fun elim e = let val b = Inttriplefunc.tryapplyd e v @0 in if b = @0 then e - else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq) + else tri_equation_add e (tri_equation_cmul (~ b / a) eq) end in eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun)) @@ -559,7 +555,7 @@ fun epoly_of_poly p = FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => - FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), Rat.neg c)) a) + FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), ~ c)) a) p FuncUtil.Monomialfunc.empty; (* String for block diagonal matrix numbered k. *) @@ -725,7 +721,7 @@ in (vec, map diag allmats) end val (vec, ratdias) = if null pvs then find_rounding @1 - else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66)) + else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map (rat_pow @2) (5 upto 66)) val newassigs = fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k)) (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1)) diff -r a0685d2b420b -r 0bec0d1d9998 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Wed Jun 01 17:46:12 2016 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Wed Jun 01 19:23:18 2016 +0200 @@ -615,10 +615,10 @@ in if c1 * c2 >= @0 then acc else let - val e1' = linear_cmul (Rat.abs c2) e1 - val e2' = linear_cmul (Rat.abs c1) e2 - val p1' = Product(Rational_lt(Rat.abs c2),p1) - val p2' = Product(Rational_lt(Rat.abs c1),p2) + val e1' = linear_cmul (abs c2) e1 + val e2' = linear_cmul (abs c1) e2 + val p1' = Product(Rational_lt (abs c2), p1) + val p2' = Product(Rational_lt (abs c1), p2) in (linear_add e1' e2',Sum(p1',p2'))::acc end end @@ -653,11 +653,11 @@ let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in if d = @0 then inp else let - val k = (Rat.neg d) * Rat.abs c / c + val k = ~ d * abs c / c val e' = linear_cmul k e - val t' = linear_cmul (Rat.abs c) t + val t' = linear_cmul (abs c) t val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p) - val q' = Product(Rational_lt(Rat.abs c),q) + val q' = Product(Rational_lt (abs c), q) in (linear_add e' t',Sum(p',q')) end end diff -r a0685d2b420b -r 0bec0d1d9998 src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Wed Jun 01 17:46:12 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Jun 01 19:23:18 2016 +0200 @@ -32,7 +32,7 @@ (Thm.dest_arg t) acc | _ => augment_norm true t acc - val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg) + val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~) fun cterm_lincomb_cmul c t = if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r @@ -40,7 +40,7 @@ fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r) (* - val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg) + val int_lincomb_neg = FuncUtil.Intfunc.map (K ~) *) fun int_lincomb_cmul c t = if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t @@ -89,7 +89,7 @@ (* fun flip v eq = if FuncUtil.Ctermfunc.defined eq v - then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq + then FuncUtil.Ctermfunc.update (v, ~ (FuncUtil.Ctermfunc.apply eq v)) eq else eq *) fun allsubsets s = case s of [] => [[]] @@ -109,7 +109,7 @@ then let val c = FuncUtil.Intfunc.apply eq v - val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq + val vdef = int_lincomb_cmul (~ (Rat.inv c)) eq fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn in (case solve (remove (op =) v vs, map eliminate oeqs) of @@ -254,7 +254,7 @@ fun int_flip v eq = if FuncUtil.Intfunc.defined eq v - then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq; + then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq; local val pth_zero = @{thm norm_zero} @@ -283,8 +283,10 @@ let fun coefficients x = let - val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x)) - else FuncUtil.Intfunc.empty + val inp = + if FuncUtil.Ctermfunc.defined d x + then FuncUtil.Intfunc.onefunc (0, ~ (FuncUtil.Ctermfunc.apply d x)) + else FuncUtil.Intfunc.empty in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp end val equations = map coefficients vvs diff -r a0685d2b420b -r 0bec0d1d9998 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Wed Jun 01 17:46:12 2016 +0200 +++ b/src/HOL/Tools/groebner.ML Wed Jun 01 19:23:18 2016 +0200 @@ -32,7 +32,6 @@ if is_binop ct ct' then Thm.dest_binop ct' else raise CTERM ("dest_binary: bad binop", [ct, ct']) -val minus_rat = Rat.neg; val denominator_rat = Rat.dest #> snd #> Rat.of_int; fun int_of_rat a = case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int"; @@ -70,7 +69,7 @@ (* Arithmetic on canonical polynomials. *) -fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l; +fun grob_neg l = map (fn (c,m) => (Rat.neg c,m)) l; fun grob_add l1 l2 = case (l1,l2) of @@ -131,8 +130,8 @@ case pol of [] => error "reduce1" | cm1::cms => ((let val (c,m) = mdiv cm cm1 in - (grob_cmul (minus_rat c,m) cms, - Mmul((minus_rat c,m),hpol)) end) + (grob_cmul (~ c, m) cms, + Mmul ((~ c,m),hpol)) end) handle ERROR _ => error "reduce1"); (* Try this for all polynomials in a basis. *) @@ -169,7 +168,7 @@ (grob_sub (grob_cmul (mdiv cm cm1) ptl1) (grob_cmul (mdiv cm cm2) ptl2), Add(Mmul(mdiv cm cm1,his1), - Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2))); + Mmul(mdiv (~ (fst cm),snd cm) cm2,his2))); (* Make a polynomial monic. *) @@ -711,7 +710,7 @@ in (vars,l,cert,th2) end) val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert - val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m)) + val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (~ c,m)) (filter (fn (c,_) => c < @0) p))) cert val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg diff -r a0685d2b420b -r 0bec0d1d9998 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Jun 01 17:46:12 2016 +0200 +++ b/src/HOL/Tools/lin_arith.ML Wed Jun 01 19:23:18 2016 +0200 @@ -171,7 +171,7 @@ end else (SOME atom, m) (* terms that evaluate to numeric constants *) - | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m) + | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, ~ m) | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0) | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m) (*Warning: in rare cases (neg_)numeral encloses a non-numeral, @@ -200,9 +200,9 @@ fun poly (Const (@{const_name Groups.plus}, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi)) | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) = - if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi)) + if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi)) | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) = - if nT T then add_atom all m pi else poly (t, Rat.neg m, pi) + if nT T then add_atom all m pi else poly (t, ~ m, pi) | poly (Const (@{const_name Groups.zero}, _), _, pi) = pi | poly (Const (@{const_name Groups.one}, _), m, (p, i)) = diff -r a0685d2b420b -r 0bec0d1d9998 src/Pure/General/rat.ML --- a/src/Pure/General/rat.ML Wed Jun 01 17:46:12 2016 +0200 +++ b/src/Pure/General/rat.ML Wed Jun 01 19:23:18 2016 +0200 @@ -13,7 +13,6 @@ val dest: rat -> int * int val string_of_rat: rat -> string val signed_string_of_rat: rat -> string - val eq: rat * rat -> bool val ord: rat * rat -> order val le: rat -> rat -> bool val lt: rat -> rat -> bool @@ -36,7 +35,7 @@ let val m = PolyML.IntInf.lcm (q1, q2) in ((p1 * (m div q1), p2 * (m div q2)), m) end; -fun make (p, 0) = raise Div +fun make (_, 0) = raise Div | make (p, q) = let val m = PolyML.IntInf.gcd (p, q); @@ -53,8 +52,6 @@ fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p | signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q; -fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2); - fun ord (Rat (p1, q1), Rat (p2, q2)) = (case (Integer.sign p1, Integer.sign p2) of (LESS, EQUAL) => LESS @@ -66,12 +63,12 @@ | (GREATER, EQUAL) => GREATER | _ => int_ord (fst (common (p1, q1) (p2, q2)))); -fun le a b = not (ord (a, b) = GREATER); +fun le a b = ord (a, b) <> GREATER; fun lt a b = ord (a, b) = LESS; fun sign (Rat (p, _)) = Integer.sign p; -fun abs (Rat (p, q)) = Rat (Int.abs p, q); +fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r; fun add (Rat (p1, q1)) (Rat (p2, q2)) = let val ((m1, m2), n) = common (p1, q1) (p2, q2) @@ -100,11 +97,11 @@ ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-"; ML_system_overload (uncurry Rat.mult) "*"; ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/"; -ML_system_overload Rat.eq "="; ML_system_overload (uncurry Rat.lt) "<"; ML_system_overload (uncurry Rat.le) "<="; ML_system_overload (fn (a, b) => Rat.lt b a) ">"; ML_system_overload (fn (a, b) => Rat.le b a) ">="; -ML_system_overload (not o Rat.eq) "<>"; +ML_system_overload Rat.neg "~"; +ML_system_overload Rat.abs "abs"; ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));