Sukerujo: syntactic sugar over Dedukti

1 What is Sukerujo?

Sukerujo is an alternative parser for Dedukti bringing the following enhancements:

  • literals for natural numbers in decimal notation
  • literals for characters
  • literals for strings
  • literals for polymorphic lists
  • local (let) definitions
  • recursive records

Sukerujo is developed by Raphaël Cauderlier.

2 Get Sukerujo

Sukerujo source code is distributed as a branch of Dedukti. It can also be installed using the Opam Package Manager.

$ opam repository add deducteam git://scm.gforge.inria.fr/opam-deducteam/opam-deducteam.git
$ opam update
$ opam install sukerujo

3 Usage

Sukerujo is invoked by the command skcheck accepting the same arguments as Dedukti type-checker dkcheck. Sukerujo files typically have the extension .sk. They can be converted to unsugared Dedukti .dk files by the following command:

$ skindent my_file.sk > my_file.dk

If you want to use Sukerujo literals, you need to declare the corresponding types and functions used to build the terms in a regular Dedukti file. This file can have any name but should compile to builtins.dko. Moreover, the .dko file should be readable by skcheck, which in practice means that you should use the version of skcheck corresponding to the version of dkcheck used to compile builtins.dko.

4 Example

File builtins.dk:

#NAME builtins.

nat : Type.
0 : nat.
S : nat -> nat.

list : Type -> Type.
nil : A : Type -> list A.
cons : A : Type -> A -> list A -> list A.

char : Type.
char_of_nat : nat -> char.

string : Type.
string_nil : string.
string_cons : char -> string -> string.

File example.sk:

#NAME example.

def string_length : string -> nat.
[] string_length "" --> 0
[c, s] string_length (string_cons c s) --> S (string_length s).

#CONV string_length "Hello World!", 12.

Compilation and checking:

$ dkcheck -e -coc builtins.dk
SUCCESS File 'builtins.dk' was successfully checked.
$ skcheck example.sk
YES
SUCCESS File 'example.sk' was successfully checked.
logo inrialogo deducteam