(* Title: Pure/General/integer.ML Author: Florian Haftmann, TU Muenchen
Auxiliary operations on (unbounded) integers.
*)
signature INTEGER = sig val build: (int -> int) -> int val build1: (int -> int) -> int val min: int -> int -> int val max: int -> int -> int val add: int -> int -> int val mult: int -> int -> int val sum: int list -> int val prod: int list -> int val sign: int -> order val div_mod: int -> int -> int * int val quot_rem: int -> int -> int * int val square: int -> int val pow: int -> int -> int (* exponent -> base -> result *) val log2: int -> int val gcd: int -> int -> int val lcm: int -> int -> int val gcds: int list -> int val lcms: int list -> int val radicify: int -> int -> int -> int list(* base -> number of positions -> value -> coefficients *) val eval_radix: int -> int list -> int (* base -> coefficients -> value *) end;
structure Integer : INTEGER = struct
fun build (f: int -> int) = f 0; fun build1 (f: int -> int) = f 1;
fun min x y = Int.min (x, y); fun max x y = Int.max (x, y);
fun add x y = x + y; fun mult x y = x * y;
val sum = build o fold add; val prod = build1 o fold mult;
fun sign x = int_ord (x, 0);
fun div_mod x y = IntInf.divMod (x, y); fun quot_rem x y = IntInf.quotRem (x, y);
fun square x = x * x;
fun pow k l = IntInf.pow (l, k);
val log2 = IntInf.log2;
fun gcd x y = PolyML.IntInf.gcd (x, y); fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
fun radicify base len k = let val _ = if base < 2 then error ("Bad radix base: " ^ string_of_int base) else (); fun shift i = swap (div_mod i base); in funpow_yield len shift k |> fst end;
fun eval_radix base =
build o fold_rev (fn k => fn i => k + i * base);
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
