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
let. With seeding, the compressed text would be twice as small.