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



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


On 17 Apr 2014, at 07:53, Gottfried Barrow <igbi at gmx.com> wrote:

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





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