wenzelm@23339: (*  Title:      Pure/ML-Systems/proper_int.ML
wenzelm@23339:     ID:         $Id$
wenzelm@23339:     Author:     Makarius
wenzelm@23339: 
wenzelm@23339: SML basis with type int representing proper integers, not machine
wenzelm@23339: words.
wenzelm@23339: *)
wenzelm@23339: 
wenzelm@23339: local
wenzelm@23339: 
wenzelm@23339: val mk = IntInf.fromInt: Int.int -> IntInf.int;
wenzelm@23339: val dest = IntInf.toInt: IntInf.int -> Int.int;
wenzelm@23339: 
wenzelm@23339: in
wenzelm@23339: 
wenzelm@23339: (* Int *)
wenzelm@23339: 
wenzelm@23339: structure OrigInt = Int;
wenzelm@23339: structure OrigIntInf = IntInf;
wenzelm@23339: type int = IntInf.int;
wenzelm@23339: 
wenzelm@23339: structure IntInf =
wenzelm@23339: struct
wenzelm@23339:   open IntInf;
wenzelm@23339:   fun fromInt (a: int) = a;
wenzelm@23339:   fun toInt (a: int) = a;
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: structure Int = IntInf;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* List *)
wenzelm@23339: 
wenzelm@23339: structure List =
wenzelm@23339: struct
wenzelm@23339:   open List;
wenzelm@23339:   fun length a = mk (List.length a);
wenzelm@23339:   fun nth (a, b) = List.nth (a, dest b);
wenzelm@23339:   fun take (a, b) = List.take (a, dest b);
wenzelm@23339:   fun drop (a, b) = List.drop (a, dest b);
wenzelm@23339:   fun tabulate (a, b) = List.tabulate (dest a, b o mk);
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: val length = List.length;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Array *)
wenzelm@23339: 
wenzelm@23339: structure Array =
wenzelm@23339: struct
wenzelm@23339:   open Array;
wenzelm@23339:   val maxLen = mk Array.maxLen;
wenzelm@23339:   fun array (a, b) = Array.array (dest a, b);
wenzelm@23339:   fun tabulate (a, b) = Array.tabulate (dest a, b o mk);
wenzelm@23339:   fun length a = mk (Array.length a);
wenzelm@23339:   fun sub (a, b) = Array.sub (a, dest b);
wenzelm@23339:   fun update (a, b, c) = Array.update (a, dest b, c);
wenzelm@23339:   fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest di};
wenzelm@23339:   fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest di};
wenzelm@23339:   fun appi a b = Array.appi (fn (x, y) => a (mk x, y)) b;
wenzelm@23339:   fun modifyi a b = Array.modifyi (fn (x, y) => a (mk x, y)) b;
wenzelm@23339:   fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
wenzelm@23339:   fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
wenzelm@23339:   fun findi a b =
wenzelm@23339:     (case Array.findi (fn (x, y) => a (mk x, y)) b of
wenzelm@23339:       NONE => NONE
wenzelm@23339:     | SOME (c, d) => SOME (mk c, d));
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Vector *)
wenzelm@23339: 
wenzelm@23339: structure Vector =
wenzelm@23339: struct
wenzelm@23339:   open Vector;
wenzelm@23339:   val maxLen = mk Vector.maxLen;
wenzelm@23339:   fun tabulate (a, b) = Vector.tabulate (dest a, b o mk);
wenzelm@23339:   fun length a = mk (Vector.length a);
wenzelm@23339:   fun sub (a, b) = Vector.sub (a, dest b);
wenzelm@23339:   fun update (a, b, c) = Vector.update (a, dest b, c);
wenzelm@23339:   fun appi a b = Vector.appi (fn (x, y) => a (mk x, y)) b;
wenzelm@23339:   fun mapi a b = Vector.mapi (fn (x, y) => a (mk x, y)) b;
wenzelm@23339:   fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk x, y, z)) b c;
wenzelm@23339:   fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk x, y, z)) b c;
wenzelm@23339:   fun findi a b =
wenzelm@23339:     (case Vector.findi (fn (x, y) => a (mk x, y)) b of
wenzelm@23339:       NONE => NONE
wenzelm@23339:     | SOME (c, d) => SOME (mk c, d));
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Char *)
wenzelm@23339: 
wenzelm@23339: structure Char =
wenzelm@23339: struct
wenzelm@23339:   open Char;
wenzelm@23339:   val maxOrd = mk Char.maxOrd;
wenzelm@23339:   val chr = Char.chr o dest;
wenzelm@23339:   val ord = mk o Char.ord;
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: val chr = Char.chr;
wenzelm@23339: val ord = Char.ord;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* String *)
wenzelm@23339: 
wenzelm@23339: structure String =
wenzelm@23339: struct
wenzelm@23339:   open String;
wenzelm@23339:   val maxSize = mk String.maxSize;
wenzelm@23339:   val size = mk o String.size;
wenzelm@23339:   fun sub (a, b) = String.sub (a, dest b);
wenzelm@23339:   fun extract (a, b, c) = String.extract (a, dest b, Option.map dest c);
wenzelm@23339:   fun substring (a, b, c) = String.substring (a, dest b, dest c);
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: val size = String.size;
wenzelm@23339: val substring = String.substring;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Substring *)
wenzelm@23339: 
wenzelm@23339: structure Substring =
wenzelm@23339: struct
wenzelm@23339:   open Substring;
wenzelm@23339:   fun sub (a, b) = Substring.sub (a, dest b);
wenzelm@23339:   val size = mk o Substring.size;
wenzelm@23339:   fun base a = let val (b, c, d) = Substring.base a in (b, mk c, mk d) end;
wenzelm@23339:   fun extract (a, b, c) = Substring.extract (a, dest b, Option.map dest c);
wenzelm@23339:   fun substring (a, b, c) = Substring.substring (a, dest b, dest c);
wenzelm@23339:   fun triml a b = Substring.triml (dest a) b;
wenzelm@23339:   fun trimr a b = Substring.trimr (dest a) b;
wenzelm@23339:   fun slice (a, b, c) = Substring.slice (a, dest b, Option.map dest c);
wenzelm@23339:   fun splitAt (a, b) = Substring.splitAt (a, dest b);
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Word *)
wenzelm@23339: 
wenzelm@23339: structure Word =
wenzelm@23339: struct
wenzelm@23339:   open Word;
wenzelm@23339:   val wordSize = mk Word.wordSize;
wenzelm@23339:   val toInt = mk o Word.toInt;
wenzelm@23339:   val toIntX = mk o Word.toIntX;
wenzelm@23339:   val fromInt = Word.fromInt o dest;
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Real *)
wenzelm@23339: 
wenzelm@23339: structure Real =
wenzelm@23339: struct
wenzelm@23339:   open Real;
wenzelm@23339:   val radix = mk Real.radix;
wenzelm@23339:   val precision = mk Real.precision;
wenzelm@23339:   fun sign a = mk (Real.sign a);
wenzelm@23339:   fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk exp} end;
wenzelm@23339:   fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest exp};
wenzelm@23339:   val ceil = mk o Real.ceil;
wenzelm@23339:   val floor = mk o Real.floor;
wenzelm@23339:   val real = Real.fromInt o dest;
wenzelm@23339:   val round = mk o Real.round;
wenzelm@23339:   val trunc = mk o Real.trunc;
wenzelm@23339:   fun toInt a b = mk (Real.toInt a b);
wenzelm@23339:   fun fromInt a = Real.fromInt (dest a);
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: val ceil = Real.ceil;
wenzelm@23339: val floor = Real.floor;
wenzelm@23339: val real = Real.real;
wenzelm@23339: val round = Real.round;
wenzelm@23339: val trunc = Real.trunc;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* TextIO *)
wenzelm@23339: 
wenzelm@23339: structure TextIO =
wenzelm@23339: struct
wenzelm@23339:   open TextIO;
wenzelm@23339:   fun inputN (a, b) = TextIO.inputN (a, dest b);
wenzelm@23339:   fun canInput (a, b) = Option.map mk (TextIO.canInput (a, dest b));
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: 
wenzelm@23339: (* Time *)
wenzelm@23339: 
wenzelm@23339: structure Time =
wenzelm@23339: struct
wenzelm@23339:   open Time;
wenzelm@23339:   fun fmt a b = Time.fmt (dest a) b;
wenzelm@23339: end;
wenzelm@23339: 
wenzelm@23339: end;