Re: [isabelle] Here's 54 ML_file imports from SML/NJ Library; fix regexp-lib.sml if you'd like

On 14-04-16 17:23, Lawrence Paulson wrote:
I made some progress. There were sharing issues, and SML/NJ seems to have some nonstandard extensions that were causing errors.

But I’m still stuck on errors in perl-engine.sml and the discrepancy between the Basis type char and the type R.Char.char.

Debugging ML within PIDE is quite interesting.

Larry Paulson


Thanks a lot for the help. That helped me find one of the problems for sure.

One problem is that the type of StringCvt.cs in Poly/ML is "datatype cs = Index of word". In SML/NJ it's this: "type cs = int".

I include a file, "Lueng_regexp_lib_fun.thy". There's a function "search", which uses "StringCvt.scanString : ((char, cs) reader -> ('a, cs) reader) -> string -> 'a option". So that's where the problem is for that file.

Five of the 11 functions I want now work. There's the statement "StringCvt.scanString (RE.find (compile regexp)) text", and I need to convert "int" to "word" at the return value of "RE.find".

I think the problem with "perl-engine-sig.sml" has to do with the differences between the "Char" structures of Poly/ML and SML/NJ. "Char" is in "String.sml" for Poly/ML, and "char.sml" for SML/NJ. The two different Char structures look substantially different, and they involve "StringCvt.reader", which is related to all this.

In the zip file, I include the SML/NJ files "char.sml" and "string-cvt.sml", along with the .sig files.

Thanks again,

Description: Zip archive

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.