Email Gateway (Jul 06 2022 at 13:46): Email Gateway (Jul 06 2022 at 13:46):From: Makarius <makarius@sketis.net>
* ML *
Type Bytes.T supports scalable byte strings, beyond the limit of
String.maxSize (approx. 64 MB on 64_32 architecture).
Operations for XZ compression (via Isabelle/Scala):
XZ.compress: Bytes.T -> Bytes.T
XZ.uncompress: Bytes.T -> Bytes.T
This refers to Isabelle/44815dc2b8f9.
It might be occasionally useful to have XZ (un)compression available in
Isabelle/ML. XZ is the standard compression scheme of Isabelle/Scala.
The main point of the exercise, though, is to show how to implement this my
mostly trivial means, see:
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/xz.ML
and
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/xz.scala
A similar application is Base64 recoding in
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/base64.ML
and
https://isabelle.sketis.net/repos/isabelle/file/44815dc2b8f9/src/Pure/General/base64.scala
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Jul 15 2022 at 23:21 UTC