*** 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
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
