author wenzelm
Sat, 23 Jul 2011 17:22:28 +0200
changeset 43948 8f5add916a99
parent 42017 0d4bedb25fc9
child 45030 9cf265a192f6
permissions -rw-r--r--
explicit structure ML_System; tunned ML bootstrap;

(*  Title:      Pure/ML-Systems/proper_int.ML
    Author:     Makarius

SML basis with type int representing proper integers, not machine

val mk_int = IntInf.fromInt: ->;
val dest_int = IntInf.toInt: ->;

(* Int *)

type int =;

structure IntInf =
  open IntInf;
  fun fromInt (a: int) = a;
  fun toInt (a: int) = a;
  val log2 = mk_int o IntInf.log2;
  val sign = mk_int o IntInf.sign;

structure Int = IntInf;

(* List *)

structure List =
  open List;
  fun length a = mk_int (List.length a);
  fun nth (a, b) = List.nth (a, dest_int b);
  fun take (a, b) = List.take (a, dest_int b);
  fun drop (a, b) = List.drop (a, dest_int b);
  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);

val length = List.length;

(* Array *)

structure Array =
  open Array;
  val maxLen = mk_int Array.maxLen;
  fun array (a, b) = Array.array (dest_int a, b);
  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
  fun length a = mk_int (Array.length a);
  fun sub (a, b) = Array.sub (a, dest_int b);
  fun update (a, b, c) = Array.update (a, dest_int b, c);
  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
  fun findi a b =
    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
      NONE => NONE
    | SOME (c, d) => SOME (mk_int c, d));

(* Vector *)

structure Vector =
  open Vector;
  val maxLen = mk_int Vector.maxLen;
  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
  fun length a = mk_int (Vector.length a);
  fun sub (a, b) = Vector.sub (a, dest_int b);
  fun update (a, b, c) = Vector.update (a, dest_int b, c);
  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
  fun findi a b =
    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
      NONE => NONE
    | SOME (c, d) => SOME (mk_int c, d));

(* Char *)

structure Char =
  open Char;
  val maxOrd = mk_int Char.maxOrd;
  val chr = Char.chr o dest_int;
  val ord = mk_int o Char.ord;

val chr = Char.chr;
val ord = Char.ord;

(* String *)

structure String =
  open String;
  val maxSize = mk_int String.maxSize;
  val size = mk_int o String.size;
  fun sub (a, b) = String.sub (a, dest_int b);
  fun extract (a, b, c) = String.extract (a, dest_int b, dest_int c);
  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);

val size = String.size;
val substring = String.substring;

(* Substring *)

structure Substring =
  open Substring;
  fun sub (a, b) = Substring.sub (a, dest_int b);
  val size = mk_int o Substring.size;
  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
  fun extract (a, b, c) = Substring.extract (a, dest_int b, dest_int c);
  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
  fun triml a b = Substring.triml (dest_int a) b;
  fun trimr a b = Substring.trimr (dest_int a) b;
  fun slice (a, b, c) = Substring.slice (a, dest_int b, dest_int c);
  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);

(* StringCvt *)

structure StringCvt =
  open StringCvt;
  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
  fun realfmt fmt = Real.fmt
    (case fmt of
      EXACT => StringCvt.EXACT
    | FIX NONE => StringCvt.FIX NONE
    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
    | GEN NONE => StringCvt.GEN NONE
    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
    | SCI NONE => StringCvt.SCI NONE
    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));

(* Word *)

structure Word =
  open Word;
  val wordSize = mk_int Word.wordSize;
  val toInt = Word.toLargeInt;
  val toIntX = Word.toLargeIntX;
  val fromInt = Word.fromLargeInt;

structure Word8 =
  open Word8;
  val wordSize = mk_int Word8.wordSize;
  val toInt = Word8.toLargeInt;
  val toIntX = Word8.toLargeIntX;
  val fromInt = Word8.fromLargeInt;

structure Word32 =
  open Word32;
  val wordSize = mk_int Word32.wordSize;
  val toInt = Word32.toLargeInt;
  val toIntX = Word32.toLargeIntX;
  val fromInt = Word32.fromLargeInt;

structure LargeWord =
  open LargeWord;
  val wordSize = mk_int LargeWord.wordSize;
  val toInt = LargeWord.toLargeInt;
  val toIntX = LargeWord.toLargeIntX;
  val fromInt = LargeWord.fromLargeInt;

(* Real *)

structure Real =
  open Real;
  val radix = mk_int Real.radix;
  val precision = mk_int Real.precision;
  fun sign a = mk_int (Real.sign a);
  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
  val ceil = mk_int o Real.ceil;
  val floor = mk_int o Real.floor;
  val real = Real.fromInt o dest_int;
  val round = mk_int o Real.round;
  val trunc = mk_int o Real.trunc;
  fun toInt a b = mk_int (Real.toInt a b);
  fun fromInt a = Real.fromInt (dest_int a);
  val fmt = StringCvt.realfmt;

val ceil = Real.ceil;
val floor = Real.floor;
val real = Real.real;
val round = Real.round;
val trunc = Real.trunc;

(* TextIO *)

structure TextIO =
  open TextIO;
  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
  fun canInput (a, b) = mk_int (TextIO.canInput (a, dest_int b));

(* Time *)

structure Time =
  open Time;
  fun fmt a b = Time.fmt (dest_int a) b;