Email Gateway (Aug 19 2022 at 14:19): Email Gateway (Aug 19 2022 at 14:19):From: Gottfried Barrow <igbi@gmx.com>
(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.
http://www.polyml.org/docs/Overview.html
THE ZIP FILE
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.
http://www.smlnj.org/doc/smlnj-lib/Manual/toc.html
http://www.cs.nyu.edu/leunga/sml-software.html
Regards
GB
SMLNJ_lib_and_Luengs_RegExp_extension.zip
Email Gateway (Aug 19 2022 at 14:20):From: Lawrence Paulson <lp15@cam.ac.uk>
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
SMLNJ_lib_and_Luengs_RegExp_extension.zip
Email Gateway (Aug 19 2022 at 14:20):From: Gottfried Barrow <igbi@gmx.com>
Larry,
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,
GB
i140417b__ml_lueng.zip
Email Gateway (Aug 19 2022 at 14:20):From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t understand these problems, unless the code somehow breaks the abstraction barriers for the libraries. And that should be impossible.
Type cs is abstract. Structures like Char and String are specified by their signatures. The implementations should not matter at all.
It is possible that Isabelle’s own libraries modify some of these things (Char possibly), creating incompatibilities with the SML Basis Library.
This code is one problem:
fun getArgs text children =
let fun walk (M.Match(SOME{pos,len},children)) =
let val s = String.substring(text,pos,len)
String.substring expects a string and two ints.
fun search regexp text =
StringCvt.scanString (RE.find (compile regexp)) text
Find seems to include type cs in its result.
fun grep regexp text =
case (search regexp text) of
NONE => NONE
| SOME(M.Match(_,children)) => SOME(getArgs text children)
Using getArgs and search together tries to identify types int and cs. But I don’t know how this code ever compiled, unless SML/NJ doesn’t implement signature matching correctly.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:20):From: Gottfried Barrow <igbi@gmx.com>
Larry,
I might finally be understanding what you're saying.
The signature STRING_CVT is the same for both Poly/ML and SML/NJ, which
is where the signatures of cs, reader, and scanstring are defined.
All I know is that I can't experiment with loading a modified SML/NJ
StringCvt because the things it wants to load are at the compiler level.
I need to look at trying to run regexp-lib.sml under SML/NJ. If I can't
get it to run under SML/NJ, it might make sense.
Thanks,
GB
Email Gateway (Aug 19 2022 at 14:20):From: Makarius <makarius@sketis.net>
See also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Systems/proper_int.ML
SML basis with type int representing proper integers, not machine words.
Isabelle/ML is not Standard ML, it is what Standard ML could have been if
that had not been messed up in the late 1990-ies.
If you want to continue this regexp comilation experiment seriously, you
should probably move over to isabelle-dev and do it as a test for the
forthcoming SML IDE, which integrates official SML into the Isabelle
environment.
That might require some further adjustments of these relatively new
things, but that is then part of the continuous development process over
there.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC