[MLton-devel] Porting HOL to MLton

[Joe Hurd]

I've currently involved in porting the HOL theorem prover to MLton,
and I've got a couple of queries about problems that have cropped up.

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?

2. What is the exception raises by TextIO.openIn? 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.

Thanks for any help,

Joe


-------------------------------------------------------
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