Encode WhyML program into TryWhy3's URL
This started as a small experiment on the compression of text and ended up as something potentially useful.
Accessing the URL trywhy3.html?code=A1use1int7tA1IntNN1let1foozx7yHs7qz1N
fills the editor with
use int.Int
let foo x =
x + 1
The compression algorithm was tested on the whole set of .mlw
files present in Why3. The compression ratio is about 3 with respect to plain Base64. Compressed code is about 60% larger than if compressed with gzip -9 | base64 -w0
. But it is almost readable; and on small files, it actually beats gzip
flat out. For example, on the example above, the compressed text is twice as small.
The compression format is agnostic to the programming language. There is nothing specific about WhyML in it. Compressed text could be made even smaller by seeding the compression algorithm with words commonly found in WhyML code. For example, in the above example, the search fragment shows the words use
, int
, Int
, let
. With seeding, the compressed text would be twice as small.