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 on Github. 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 either use the version of skcheck corresponding to the version of dkcheck used to compile builtins.dko or use skcheck in backward-compatibility mode (option -nk) to compile the file declaring the builtins constants.

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.

5. Detailed description

5.1. Grammar

5.1.1. Lexical classes

Tokens are separated by any positive number of whitespace characters (spaces, tabulations, newlines, and carriage return). Comments are delimited by (; and ;); they cannot be nested.

Numbers are written in decimal notation, the first digit must be non-zero.

Character literals are delimited by single quotes (').

String literals are delimited by double quotes (").

The following are reserved keywords: ., , , :, ==, [, ], {, }, (, ), -->, ->, =>, :=, _, Record, Type, def, thm, %typeof, #NAME, #REQUIRE, #EVAL, #INFER, #CHECK, #CHECKNOT, #ASSERT, #ASSERTNOT, #PRINT, #GDT.

The following are builtin constants: nat, 0, S, char, char_of_nat, string, string_cons, list, nil, cons.

Identifiers are any non-empty sequence of ASCII letters (uppercase and lowercase), digits, underscore (_), exclamation mark (!), question mark (?) and apostrophe (') such that the first character is not an apostrophe and which is not one of the reserved keywords nor a builtin constant.

Qualified identifiers are composed of a module name (a non-empty sequence of letters, digits, and underscore) followed by a period (.) and by an identifier. 

<number> :== [1-9][0-9]*
<char> :== ['].[']
<string> :== ["].*["]
<id> :== [_a-zA-Z0-9!?][_a-zA-Z0-9!?']*
<mid> :== [_a-zA-Z0-9]+
<qid> :== <mid>[.]<id>

5.1.2. Grammar rules

This is a slightly simplified and ambiguous presentation of the syntax of Sukerujo. For the exact grammar, see the file parser/menhir_parser.mly. 

term ::= <qid>
      |  <id>
      |  '(' term ')'
      |  'Type'                              // The sort of all types
      |  <number>
      |  <char>
      |  <string>
      |  term+
      |  <id> ':=' term '=>' term            // Local definition
      |  [<id> ':']? term '->' term          // Product
      |  <id> [: ['_' | term]]? '=>' term    // Abstraction
      |  '%typeof' term                      // Type of a term

pattern ::= [<id> | <qid>] pattern*
         |  '_'                              // Universal pattern
         |  '{' term '}'                     // Guard
         |  '(' pattern ')'
         |  <id> '=>' pattern                // Higher-order pattern

param ::= '(' <id> ':' term ')'
       |  '(' <id> ':=' term ')'

eval_config ::= '[' <id> [, <id>]? ']'

decl ::= <id> [':' term]?

def_decl ::= <id> ':' term

rule ::= ['{' <id> | <qid> '}']? '[' [decl [',' decl]*]? ']' [<id> | <qid>] pattern* '-->' term '.'

// An optional name enclosed by '{' and '}', followed by the rule
// context, the left-hand-side pattern and the right-hand-side term

line ::= <id> ['(' <id> ':' term ')']* ':' term '.'                                           // Static declaration
      |  'def' <id> ':' term '.'                                                              // Definable declaration
      |  ['def' | 'thm'] <id> param* [':' term]? ':=' term '.'                                // Definition
      |  'Record' <id> param* ':=' <id> '{' [def_decl [',' def_decl]*]? '}' '.'               // Record type declaration
      |  rule+ '.'                                                                            // Rewrite rule
      |  ['#EVAL' | '#INFER'] eval_config? term '.'
      |  ['#CHECK' | '#CHECKNOT' | '#ASSERT' | '#ASSERTNOT'] term [ ':' | '==' ] term '.'
      |  '#PRINT' <string> '.'
      |  '#GDT' [<id> | <qid>] '.'
      |  ['#NAME' | '#REQUIRE'] <mid> '.'
logo inrialogo deducteam