| author | wenzelm |
| Fri, 24 May 2024 16:15:27 +0200 | |
| changeset 80188 | 3956e8b6a9c9 |
| parent 76351 | 2cee31cd92f0 |
| permissions | -rw-r--r-- |
|
76351
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/General/zstd.ML |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
3 |
|
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
4 |
Support for Zstd compression (via Isabelle/Scala). |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
6 |
|
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
7 |
signature Zstd = |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
8 |
sig |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
9 |
val compress: Bytes.T -> Bytes.T |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
10 |
val uncompress: Bytes.T -> Bytes.T |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
11 |
end; |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
12 |
|
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
13 |
structure Zstd: Zstd = |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
14 |
struct |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
15 |
|
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
16 |
val compress = \<^scala>\<open>Zstd.compress\<close>; |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
17 |
val uncompress = \<^scala>\<open>Zstd.uncompress\<close>; |
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
18 |
|
|
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
diff
changeset
|
19 |
end; |