Mentions légales du service

Skip to content

Encode WhyML program into TryWhy3's URL

Guillaume Melquiond requested to merge shortener into master

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.

Edited by Guillaume Melquiond

Merge request reports