Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-1-RC5: Outdated information about...


view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC