src/Pure/ML-Systems/proper_int.ML
changeset 41619 6cac9f48f96a
parent 40747 889b7545a408
child 42017 0d4bedb25fc9
equal deleted inserted replaced
41618:79dae6b7857d 41619:6cac9f48f96a
   139 (* StringCvt *)
   139 (* StringCvt *)
   140 
   140 
   141 structure StringCvt =
   141 structure StringCvt =
   142 struct
   142 struct
   143   open StringCvt;
   143   open StringCvt;
   144   datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
   144   datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
   145   fun realfmt fmt = Real.fmt
   145   fun realfmt fmt = Real.fmt
   146     (case fmt of
   146     (case fmt of
   147       EXACT => StringCvt.EXACT
   147       EXACT => StringCvt.EXACT
   148     | FIX NONE => StringCvt.FIX NONE
   148     | FIX NONE => StringCvt.FIX NONE
   149     | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
   149     | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
   158 
   158 
   159 structure Word =
   159 structure Word =
   160 struct
   160 struct
   161   open Word;
   161   open Word;
   162   val wordSize = mk_int Word.wordSize;
   162   val wordSize = mk_int Word.wordSize;
   163   val toInt = mk_int o Word.toInt;
   163   val toInt = Word.toLargeInt;
   164   val toIntX = mk_int o Word.toIntX;
   164   val toIntX = Word.toLargeIntX;
   165   val fromInt = Word.fromInt o dest_int;
   165   val fromInt = Word.fromLargeInt;
   166 end;
   166 end;
   167 
   167 
   168 structure Word8 =
   168 structure Word8 =
   169 struct
   169 struct
   170   open Word8;
   170   open Word8;
   171   val wordSize = mk_int Word8.wordSize;
   171   val wordSize = mk_int Word8.wordSize;
   172   val toInt = mk_int o Word8.toInt;
   172   val toInt = Word8.toLargeInt;
   173   val toIntX = mk_int o Word8.toIntX;
   173   val toIntX = Word8.toLargeIntX;
   174   val fromInt = Word8.fromInt o dest_int;
   174   val fromInt = Word8.fromLargeInt;
   175 end;
   175 end;
   176 
   176 
   177 structure Word32 =
   177 structure Word32 =
   178 struct
   178 struct
   179   open Word32;
   179   open Word32;
   180   val wordSize = mk_int Word32.wordSize;
   180   val wordSize = mk_int Word32.wordSize;
   181   val toInt = mk_int o Word32.toInt;
   181   val toInt = Word32.toLargeInt;
   182   val toIntX = mk_int o Word32.toIntX;
   182   val toIntX = Word32.toLargeIntX;
   183   val fromInt = Word32.fromInt o dest_int;
   183   val fromInt = Word32.fromLargeInt;
   184 end;
   184 end;
   185 
   185 
   186 structure LargeWord =
   186 structure LargeWord =
   187 struct
   187 struct
   188   open LargeWord;
   188   open LargeWord;
   189   val wordSize = mk_int LargeWord.wordSize;
   189   val wordSize = mk_int LargeWord.wordSize;
   190   val toInt = mk_int o LargeWord.toInt;
   190   val toInt = LargeWord.toLargeInt;
   191   val toIntX = mk_int o LargeWord.toIntX;
   191   val toIntX = LargeWord.toLargeIntX;
   192   val fromInt = LargeWord.fromInt o dest_int;
   192   val fromInt = LargeWord.fromLargeInt;
   193 end;
   193 end;
   194 
   194 
   195 
   195 
   196 (* Real *)
   196 (* Real *)
   197 
   197