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

(At the bottom, I talk about how I have Lueng's extension of SML/NJ RegExp all imported, with only errors in two files, in particular "regexp-fn.sml". What I really want is his functions in "regexp-lib.sml", such as grep, findall, subst, substAll, replace, replaceAll, and 5 more. )

Consider me the unofficial marketing guy, like the unofficial mascot, in the stands, for a pro sports team. The management tolerates him, but it's inevitable he'll eventually be asked to leave, since he, at times, tarnishes the team image, a prestigious one, acquired over many years.

A professional programmer will have a different perspective about ML than myself. Only doing ML programming for 3 weeks or so, I see that it has its own special attributes. It seems streamlined in some ways, though anything with enough nested levels gets complex.

Signatures give a high-level overview, and by necessity separate values and functions from their details. Looking at signatures helps me find a lot of what I need. The syntax is not as streamlined as Haskell, but most syntax isn't, though Isar and Isabelle/HOL are very competitive.

But in the end, ML is the only language a person can do native programming inside Isabelle/HOL, though I suspect that will change with an official SC{*...*} command, someday, which will allow Scala to easily interact globally with a ML{*...*}.

*There's Isabelle/ML and Poly/ML Library Support Already*

First, it is as Makarius Wenzel said. There is actually already a lot of ML library support in Isabelle/ML, such as in file.ML, library.ML, path.ML, with even the ability to create squiggly lines with the messages in output.ML. Squiggly lines. Graphics. Modern computing. Yea. Yes. Si, senior. Ja, mate.

There also are some extra functions in David Mathews Poly/ML Basis, such as HashArray, and after searching to make sure its special, Google took me to Poly/ML's web page. There is "polyml-5.5.1-1\src\mlsource", which contains some Windows libraries, so I'll have to check that out.



I attach a zip file, SMLNJ_lib_and_Luengs_RegExp_extension.zip.

In that file, there is one main file, NJlib.thy. That theory imports 54 SML/NJ files without errors, for me. After learning some ML, the files only required a minimal amount of edits, to add fully qualified names for functions, like "ord", "chr", "ref", etc. I tested a few things, but not much.

There are URLs in the file to the SML/NJ Library page, and I only imported what was potentially useful to me, among which are an Awk RegExp engine (though lacking in easy functions to use it), iteraters, random generators (one taken from Larry Paulson's book), hash tables, atoms, arrays, and a fifo.

*What I Really Want In the Big Ocean of Life Here on the Terrestrial Inhabitating Location*

I couldn't get Lueng's RegExp library working. I document the basic problems in "ml_lueng/Lueng.thy". What I really want is his high-level functions for regex use, not so much his Perl extension.

These functions are in "ml_lueng/RegExp/regexp-lib.sml", which I put in "ml_lueng/Lueng_regexp_lib_sig_and_sml.thy".

Lueng extended "match", which may not be the problem, but it's related to that.

All of Lueng's code in include, but I only include the RegExp and Util folders from SML/NJ Library.



Attachment: SMLNJ_lib_and_Luengs_RegExp_extension.zip
Description: Binary data

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