[MLton-devel] Porting HOL to MLton

[Stephen Weeks]

> 1. HOL uses mosmllex to generate a lexer. However, the generated lexer
> files use low-level primitive operations, specifically casting from
> one type to another:
> 
> Obj.magic : 'a -> 'b
> 
> [Casting is used to make the generated lexer more efficient, and there
> are additional checks made to ensure that everything is typesafe.]
> 
> Is there such a casting function in MLton?

No.  I don't know enough about mosmllex to know how easy these are to
workaround.  Can you give us an idea of the casts used?

> 2. What is the exception raises by TextIO.openIn?

IO.Io

> From using -show-basis true it seems that IO.Io would be the right
> one, but MLton complains about this ("longid in var pat"). I'm using
> -basis 1997.

Hmm.  I don't see what's wrong.  The following transcript demonstrates
that IO.Io works with mlton -basis 1997.

% mlton
MLton 20030716 (built Wed Jul 16 10:23:10 2003 on redhat71)
% cat z.sml
val _ =
   (TextIO.openIn "/foo"; ())
   handle IO.Io _ => print "ok\n"
% mlton -basis 1997 z.sml
% z
ok



-------------------------------------------------------
This SF.net email is sponsored by: SF.net Giveback Program.
SourceForge.net hosts over 70,000 Open Source Projects.
See the people who have HELPED US provide better services:
Click here: http://sourceforge.net/supporters.php
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel