[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / Skil / Reference / Skil-ref
Printer-friendly
The Language Skil
 Skil ,  Research ,  Lehrstuhl für Informatik II ,  Department of Computer Science RWTH

Description of the Language Skil (1.00)

General:

Skil is an imperative (C-based) language enhanced with a series of functional features. It aims to provide a high programming level, which allows the integration of algorithmic skeletons (Skil stands for Skeleton Imperative Language). At the same time, due to the fact that the base language is imperative and due to the instantiation technique used in the Skil compiler to translate the functional features, Skil programs reach a higher performance than their functional counterparts, while approaching the efficiency of direct C implementations.

The main goals in the design of Skil were on the one hand to provide it with constructs supporting polymorphism, the definition and use of distributed data structures and higher-order functions, and on the other hand to simplify the base language (C) by eliminating some of its redundancies and some of its features of lesser importance. The enhancements, restrictions and grammar of Skil are given below.


Enhancements:

Five kinds of features were added to the language: firstly, type variables to support polymorphism, secondly a construct that supports the definition and use of distributed data types (pardata), thirdly higher-order functions and partial function applications, fourthly the conversion of infix operators (and of two prefix ones) to function calls by enclosing them between brackets, and finally, two predefined test functions, which check if a data structure is dynamic, respectively distributed.
  • Type variables have the form $id, where id is a legal identifier (i.e. it begins with a letter). They can be instantiated with any type, except void and functional types. In addition, type variables which occur inside other types may not be instantiated with pardatas (i.e. pardatas may not `be part of' other types, in particular pardatas may not be nested). Some examples of using type variables are given below.
            $t x ;                              /* variable declaration           */
    
            $t id ($t x)                        /* function definition            */
              { return (x) ; }
    
    Apart from these cases, type variables may appear as arguments of structs and unions, as well as of typedef- and pardata-defined types. These arguments must be enclosed between angle brackets (<>), as shown in the examples below.
            typedef struct _list <$elem_t> {    /* definition of polymorphic list */
              $elem_t                 elem ;
              struct _list <$elem_t> *next ;
            }
            * list <$elem_t> ;
    
            pardata matrix <$item_t> ;          /* `pardata' declaration          */
    
                                                /* header of polymorphic `map'    */
            list <$t1> map ($t1 f ($t2), list <$t1> l) ;
    
    Apart from type variables, which play the role of formal parameters, struct, union, typedef and pardata types may also have (monomorphic) types as arguments. This allows the explicit instantiation of previously defined polymorphic types. For instance one can derive from the above polymorphic list type the type `list of integers' using the following declaration:
            typedef list <int> intlist ;        /* instantiation to integer list  */
    
    Since polymorphism is unsound in the presence of side effects, we have the following restrictions in the use of polymorphic variables:
    • the expressions on both sides of the assignment operator (=) must have the same type, in particular the same polymorphic type
    • polymorphic variables may not be used on the left hand side of all other assignment operators (i.e. +=, *=, ..., ++, --)
    • global variables must be monomorphic
  • The "pardata" construct serves for the declaration of distributed (`parallel') data types. The construct is similar to typedef, with a `reversed' syntax (see grammar). pardatas can have type variables as arguments. Other than typedefs, pardata declarations may lack the `body', i.e. the type specification. This enables their use in header files, similarly to function prototypes. The main difference to typedefs, however, lies in the fact the pardatas may denote only distributed data types. Moreover, pardatas may not occur inside other types, i.e. they are always `top-level'.
  • Higher-order functions and partial applications. Similarly to functional languages, Skil allows the definition and use of functions having other functions as arguments or as return values, i.e. higher-order functions. Nevertheless, unlike in functional languages, where an arbitrary expression may be used on the left side of a function application, here e(e') is only a valid application if e is a function name, a functional argument or another valid application (in the case of curried applications). Moreover, functional expressions are not allowed as arguments of the following operators: assignment (=), conditional (?:), sequence (,), cast, sizeof, as well as in the for statement and as expression statements.
  • Conversion of operators to functions. The conversion of infix operators (and of two prefix ones) to function calls was enabled by enclosing these operators between brackets (like in Haskell). For instance, (+) is thus a function that can be called by a fold skeleton, e.g. fold ((+), data_struct). This allows passing operators as functional parameters to higher-order functions, as well as partial application of operators. The operators for which this conversion can be applied are: ||, &&, |, ^, &, ==, !=, <, >, <=, >=, <<, >>, +, -, *, /, %, ~ and !.
  • Type test functions. Two test functions for types are internally defined: $$dyn tests, if a data type is dynamic, and $$par tests, if a data structure is distributed (i.e. a pardata).


Restrictions:

  • no `wide chars/strings' are supported
  • only `new style' function definitions, in which the types of the arguments are given in the argument list, are supported. For instance
            int main (int argc, char **argv)
            { ... }
    
    is legal, while
            int main (argc, argv)
            int    argc ;
            char **argv ;
            { ... }
    
    is not allowed.
  • only `pedantic' initializations of arrays and structures are allowed. For instance
            struct key {
               char *word  ;
               int   count ;
            } keytab[] = {
               {"auto", 0},
               {"break", 0},
               /* ... */
            } ;
    
    is legal, while
            struct key {
               char *word  ;
               int   count ;
            } keytab[] = {
               "auto", 0,
               "break", 0,
               /* ... */
            } ;
    
    (i.e. without the inner braces) is not. Unions may not be initialized.
  • passing pointers to functions as arguments requires the explicit use of the address (`&') operator, unlike in C, where, if this operator is missing, it is automatically supplied by the compiler (see K&R'88, pp. 119).

  • Obsolete features:

    These features of C are still available in Skil, however they have become obsolete due to the integration of the functional features. They have been kept in the language for compatibility reasons, but users are encouraged to use the new Skil constructs instead. The obsolete features are:
    • pointers to functions as arguments/result of functions. This feature is handled in Skil by higher-order functions.
    • void * are no longer needed as `universal pointers'. This can be achieved by using for example $t *.
    • casts are no longer needed.


    Grammar:

    The grammar is given in EBNF-like notation. Each production has the form:
                nonterm :  alt_1
                        |  ...
                        |  alt_n
    
    Moreover, the following notations are employed:
                [ exp ]         optional expression
                { exp }         the expression is repeated 0 or more times
                ( exp )         grouping
                exp_1 | exp_2   alternative
                "int"           terminal symbols are included between double
                                quotation marks (these do not appear as terminal
                                symbols or as part of terminal symbols themselves)
    
    The following symbols denote classes of terminals recognized by the scanner:
                identifier    - the scanner makes the distinction based on the
                typedef_name    symbol table
                pardata_name
    
                typevar_name  - these names always begin with a `$'. Note, however,
                                that the `$' sign must always be followed by a
                                legal identifier (which must begin with a letter).
                                Thus `$', `$$', `$1' etc. are not legal type
                                variable names.
    
                integer       - constants returned by the scanner (all integer
                character       constants are converted to decimal and double
                string          precision values are distinguished internally)
                real
    
     	    inline        - pass 'C-Code' through the compiler, there are two
    		            possibilities:
    			    %inline ......    /* at the beginning of a line */
    				 		 and
    			    %{ .....%}        /* both at the beginning of a 
                                                     line */
    

    
    /*--------  DECLARATIONS  --------*/
    
    transl_unit            :  ext_decl  { ext_decl }
    
    ext_decl               :  fundef
                           |  decl
                           |  inline
    
    fundef                 :  decl_spec  declarator  comp_stmt
    
    decl                   :  decl_spec  [ init_declarator
                                           { ","  init_declarator } ]  ";"
                           |  "typedef"  decl_spec  declarator  [ typeargs ]  ";"
                           |  "pardata"  identifier  [ typeargs ]  [ type_name ] ";"
    
    
    decl_spec              :  [ storage_class ]  [ type_spec ] [ type_qual ]
    
    storage_class          :  "auto"  |  "register"  |  "static"  |  "extern"
    
    type_qual              :  "const"  |  "volatile"
    
    type_spec              :  "void"  |  "char"  |  "short"  |  "int"  |  "long"
                           |  "float"  |  "double"  |  "signed"  |  "unsigned"
                           |  typedef_name  [ typeargs ]
                           |  typevar_name
                           |  struct_union_spec
                           |  enum_spec
    
    struct_union_spec      :  struct_union  identifier  [ typeargs ]
                              [ "{"  struct_decl  { struct_decl }  "}" ]
    
    struct_union           :  "struct"  |  "union"
    
    enum_spec              :  "enum"  [ identifier ]  [ "{" enum_list "}" ]
    
    enum_list              :  enumerator  { "," enum_list }
    
    enumerator             :  identifier [ "=" const_expr ]
    
    typeargs               :  "<"  [ type_name  { ","  type_name } ]  ">"
    
    init_declarator        :  declarator  [ "="  init ]
    
    spec_qual_list         :  type_qual {  spec_qual_list }
                           |  type_spec {  spec_qual_list }
    
    struct_decl            :  spec_qual_list  struct_declarator
                              { ","  struct_declarator }  ";"
    
    struct_declarator      :  declarator
                           |  declarator  ":"  const_expr
    
    declarator             :  [ pointer ]  direct_declarator
    
    direct_declarator      :  identifier
                           |  "("  declarator  ")"
                           |  direct_declarator  "["  [ const_expr ]  "]"
                           |  direct_declarator  "("  [ params_ell ]  ")"
    
    type_qual_list         :  type_qual  { type_qual_list }
    
    pointer                :  "*"  [ pointer ]
    
    params_ell             :  param_decl  { ","  param_decl }  [ ","  "..." ]
    
    param_decl             :  decl_spec  [ declarator  |  abstr_declarator ]
    
    init                   :  assign_expr
                           |  "{"  init  { ","  init }  [ "," ]  "}"
    
    type_name              :  spec_qual_list  [ abstr_declarator ]
    
    abstr_declarator       :  pointer
                           |  [ pointer ]  direct_abstr_declarator
    
    direct_abstr_declarator:  "("  abstr_declarator  ")"
                           |  [ direct_abstr_declarator ]  "["  [ const_expr ]  "]"
                           |  [ direct_abstr_declarator ]  "("  [ params_ell ]  ")"
    
    
    /*--------  STATEMENTS  --------*/
    
    stmt                   :  lab_stmt
                           |  expr_stmt
                           |  comp_stmt
                           |  sel_stmt
                           |  iter_stmt
                           |  jmp_stmt
    
    lab_stmt               :  identifier  ":"  stmt
                           |  "case"  const_expr ":"  stmt
                           |  "default"  ":"  stmt
    
    expr_stmt              :  inline
                           |  [ expr ]  ";"
    
    comp_stmt              :  "{"  { decl }  { stmts }  "}"
    
    sel_stmt               :  "if"  "("  expr  ")"  stmt  [ "else"  stmt ]
                           |  "switch"  "("  expr  ")"  stmt
    
    iter_stmt              : "while"  "("  expr  ")"  stmt
                           |  "do"  stmt  "while"  "("  expr  ")"  ";"
                           |  "for"  "("  [ expr ]  ";"  [ expr ]  ";"  [ expr ]
                                     ")"  stmt
    
    jmp_stmt               :  "goto"  identifier  ";"
                           |  "continue"  ";"
                           |  "break"  ";"
                           |  "return"  [ expr ]  ";"
    
    
    /*--------  EXPRESSIONS  --------*/
    
    expr                   :  [ expr  "," ]  assign_expr
    
    assign_expr            :  cond_expr
                           |  unary_expr  ass_op  assign_expr
    
    ass_op                 :  "="  |  "*="  |  "/="  |  "%="  |  "+="  |  "-="
                           |  "<<="  |  ">>="  |  "&="  |  "^="  |  "|="
    
    cond_expr              :  logic_or_expr  [ "?"  expr  ":"  cond_expr ]
    
    const_expr             :  cond_expr
    
    logic_or_expr          :  [ logic_or_expr  "||" ]  logic_and_expr
    
    logic_and_expr         :  [ logic_and_expr  "&&" ]  incl_or_expr
    
    incl_or_expr           :  [ incl_or_expr  "|" ]  excl_or_expr
    
    excl_or_expr           :  [ excl_or_expr  "^" ]  and_expr
    
    and_expr               :  [ and_expr  "&" ]  equal_expr
    
    equal_expr             :  [ equal_expr  ( "=="  |  "!=" ) ]  rel_expr
    
    rel_expr               :  [ rel_expr  ( "<"  |  ">"  |  "<="  |  ">=" ) ]
                              shift_expr
    
    shift_expr             :  [ shift_expr  ( "<<"  |  ">>" ) ]  add_expr
    
    add_expr               :  [ add_expr  ( "+"  |  "-" ) ]  mult_expr
    
    mult_expr              :  [ mult_expr  ( "*"  | "/"  | "%" ) ]  cast_expr
    
    cast_expr              :  unary_expr
                           |  "("  type_name  ")"  cast_expr
    
    unary_expr             :  postfix_expr
                           |  ( "++"  |  "--" )  unary_expr
                           |  unary_op  cast_expr
                           |  "sizeof"  unary_expr
                           |  "sizeof"  "("  type_name  ")"
    
    unary_op               :  "&"  |  "*"  |  "+"  |  "-"  |  "~"  |  "!"
    
    postfix_expr           :  prim_expr
                           |  postfix_expr  "["  expr  "]"
                           |  postfix_expr  "("  [ arg_exprs ]  ")"
                           |  postfix_expr  ( "."  |  "->" )  identifier
                           |  postfix_expr  ( "++"  |  "--" )
    
    prim_expr              :  identifier
                           |  constant
                           |  ( "$$dyn"  |  "$$par" )  "("  type  ")"
                           |  "("  expr  ")"
                           |  "("  funop  ")"
    
    funop                  :  "||"  |  "&&"  |  "|"  |  "^"  |  "&"
                           |  "=="  |  "!="  |  "<"  |  ">"  |  "<="  |  ">="
                           |  "<<"  |  ">>"
                           |  "+"  |  "-"  |  "*"  |  "/"  |  "%"
                           |  "~"  |  "!"
    
    arg_exprs              :  [ arg_exprs  "," ]  assign_expr
    
    constant               :  integer  |  character  |  string  |  real
    
    

    Thomas Richert , 3.11.99
    Valid HTML 4.01 Strict! Valid CSS!