Make JonPRL SML '97 Compatible - Githubissues

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]

http://www.jonprl.org

MIT License

109 stars 9 forks source link

Make JonPRL SML '97 Compatible #218

Open jozefg opened 8 years ago

jozefg commented 8 years ago

Making JonPRL fully compliant with '97 has a few nice benefits. We never have to worry about NJ not adapting to a new platform, we can get faster binaries with mlton, we can properly support 64bit (doesn't NJ still have weird issues with it) etc, etc.

As far as making this happen, I can think of three big things off the top of my head

[ ] Make all the satellite projects SML '97 compatible. A few are and most can be with minimal effort
[ ] Stop using #[] vector patterns. They unfortunately aren't standard
[ ] Add .mlb files in addition to .cm files (I really want MLton to work)

There is a potential downside, we can fix the second one by adding a series of utility functions along the lines of

(* ext here being short for "extrude" *)
ext0 : 'a vector -> unit
ext1 : 'a vector -> 'a
ext2 : 'a vector -> 'a * 'a
...

and then use ext* plus a pattern match on a tuple. This is going to be a lot less readable though, particularly in places like src/refiner/extract.fun where all of those pattern matches would grow an extra let-expression to pattern match on the vector. Is there a nicer way that I'm missing? Is it worth the extra ugliness?

jonsterling commented 8 years ago

I think this is worth the pain.

jonsterling commented 8 years ago

one other are of incompatibility may be with structure sharing (which may still occur in a few places?).

jozefg commented 8 years ago

@jonsterling It looks like we're mostly doing sharing type except in one spot in sml-abt-unify, though it's easily fixed. Structure is a mess :/

jonsterling commented 8 years ago

@jozefg Yeah... If they can fix one thing in Successor ML, I hope it's that.

jonsterling commented 8 years ago

So, I think the thing to do is first to make sure all dependencies of JonPRL are compliant; then, we should start making the required changes in JonPRL in earnest.

ghost commented 8 years ago

Regarding MLton, I think there are going to be some problems with unicode, though maybe that's not as big of an issue anymore. But strings in the source will have to be escaped and I think there are some other problems with manipulating the strings even if they are escaped but I don't remember the details.

jonsterling commented 8 years ago

@freebroccolo Oh right, I'd forgotten about that... :(