Email Gateway (Dec 07 2021 at 10:01): Email Gateway (Dec 07 2021 at 10:01):From: Dominique Unruh <unruh@ut.ee>
Hi,
system.pdf says in Section 5.3.1: /A Scala functions of type String =>
String may be wrapped as isabelle.Scala.Fun and collected via an
instance of the class isabelle.Scala.Functions./
If I understand things right, a "String => String" function should
inherit from Scala.Fun_String, and a "List[String] => List[String]"
function from Scala.Fun_Strings.
Related, in Section 5.3.2, it is said the type of Scala-functions in ML
is "string -> string". This is only correct if they inherit from
Scala.Fun_String. Otherwise it is "string list -> string list".
Best wishes,
Dominique.
Email Gateway (Dec 07 2021 at 21:18):From: Makarius <makarius@sketis.net>
On 07/12/2021 11:00, Dominique Unruh wrote:
Hi,
system.pdf says in Section 5.3.1: /A Scala functions of type String => String
may be wrapped as isabelle.Scala.Fun and collected via an instance of the
class isabelle.Scala.Functions./If I understand things right, a "String => String" function should inherit
from Scala.Fun_String, and a "List[String] => List[String]" function from
Scala.Fun_Strings.
OK, I have refined that here
https://isabelle.sketis.net/repos/isabelle-release/rev/74a800810bde
The basic form is actually List[Bytes] => List[Bytes] which is e.g. relevant
for decode_base64 / decode_base64 (presently unused).
At a later stage, SHA1 or SHA2 will follow: Then we will also discontinue the
SHA1 C module for Poly/ML.
Related, in Section 5.3.2, it is said the type of Scala-functions in ML is
"string -> string". This is only correct if they inherit from
Scala.Fun_String. Otherwise it is "string list -> string list".
I have refined it here: c49362e85f5a.
The type is determined by the definition in Isabelle/Scala ("multi"), and
automatically propagated to Isabelle/ML.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC