[Hol-info] Type definitions: MosML bug?

[Jens B. <br...@in...>]

Due to a bug in Moscow ML 2.00, it seems that new types cannot be created i=
n=20
HOL any more. All definitions throw an overflow exception:

=2D new_type("s",0);
! Uncaught exception:
! Overflow

After a closer look, the error is caused by the function dest_time in
"hol/src/portableML/Portable.sml", which uses toSeconds of the MosML librar=
y.
This function does not work any more, because the value returned by it is=20
greater than the maximum possible integer 2^30-1=3D1073741823.

Moscow ML version 2.00 (June 2000)
Enter `quit();' to quit.
=2D load "Time"; open Time;
> val it =3D () : unit
=2D > type time =3D time
  val fromSeconds =3D fn : int -> time
[...]
  val fromMilliseconds =3D fn : int -> time
=2D toSeconds(now());
! Uncaught exception:
! Overflow
=2D toReal(now());
> val it =3D 1073912178.66 : real

I reported the bug to Peter Sestoft.

Regards,
Jens Brandt

=2D-=20
Jens Brandt
AG Reaktive Systeme, Fachbereich Informatik
Technische Universit=E4t Kaiserslautern
http://rsg.informatik.uni-kl.de