DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Rank 2 intersection for a simple language of modules (built on a subset of Caml)

This page demonstrates a prototype implementation of a rank 2 intersection type system for a simple language of modules added on top of a core-ML like language. The current version of the prototype (the source code is not availlable):
  • Implements the type system described in [ Damiani, 2003b ] (which adds a simple language of modules with symmetric linking on top of the type system of [ Damiani, 2003 ]).

    The language considered by the implementation is richer than the one considered in the report [ Damiani, 2003 ]. In particular it includes datatype declarations. Symmetric linking in presence of datatype declarations is made possible by suitable constructs for allowing modules to export and import datatype declarations.

  • Is written in O'Caml .

Demonstration of the intrachecking prototype

Type a module in the form below and press the button.

  • Parsing is not particularly smart (for instance, all the infix operators have the same precedence - to avoid problems, it is better to use a lot of parentheses) and the error messages are quite poor.

Here you can find a description of the accepted SYNTAX OF THE LANGUAGE OF MODULES and some EXAMPLES OF MODULES AND INTERFACES that you can copy and paste.



Demonstration of the interchecking prototype

Type a sequence of interfaces terminate by ";;" in the form below and press the button.

Here you can find a description of the SYNTAX OF THE LANGUAGE OF INTERFACES (to supply interfaces in input to the interchecking prototype copy and paste in sequence the interfaces produced as output by the above intrachecking prototype on different modules and terminate the sequence by ";;").



BIBLIOGRAPHY



[On-line tools demonstrations]

Comments to: damiani[at]di[dot]unito[dot]it Last update: Mar 20, 2001