Author: Rowan Davies (rowan@csse.uwa.edu.au) (Built using the ML Kit: see the file COPYING.)
Version: 0.99999 (supports CM&MLB files, and the standard basis is pretty complete) Date: 2011 October 18
This directory contains SML CIDRE, a "Checker for Intersection and Datasort REfinements" for Standard ML. SML CIDRE checks properties of programs following modest programmer supplied annotations, and is intended to be used similarly to a type checker. However, it includes features specifically for capturing program properties, in particular intersection and datasort refinements.
[Note: "CIDRE" is pronounced like "cider".]
This version of SML CIDRE is intended to be used while developing SML programs using SML/NJ as the main development environment. Any version of SML/NJ after 110.0.7 (from 2000) should be suitable, and recent SML CIDRE development has used version 110.73, so that definitely works.
sml-cidre includes all of SML/NJ, so use it in place of the normal "sml", and maybe put it on your path or point emacs at it.
The simplest way to sort check and make an SML program from sml-cidre is:
Cidre.make "filepath.cm"; [Replace filepath.cm with the actual path]This will sort check the SML files in an appropriate order, and if there are no errors or pattern coverage warnings it automatically calls CM.make to compile the program.
If you want to sort check without compiling, use Cidre.check instead. Both commands will also accept the name of an MLB file instead of a CM file. This allows more control over exactly how the files are sort checked. Note that CM files are actually translated to default MLB files "on-the-fly". (See src/Cidre/Cidre.sml.)
An extension of the emacs sml-mode is included that highlights sort annotations differently to comments. It seems to work with sml-mode 4.1.
SML CIDRE annotations appear in "psuedo comments" enclosed by ([ and ]). The following are some examples.
(Note that refinement-types are also called "sorts".)
datatype 'a stream = Stream of unit -> 'a front
and 'a front = Empty | Cons of 'a * 'a stream
(*[ datasort 'a infStream = Stream of unit -> 'a infFront
and 'a infFront = Cons of 'a * 'a infStream ]*)
(*[ sortdef intInfStream = int infStream
and intInfFront = int infFront ]*)
(*[ val delay <: (unit -> 'a front) -> 'a stream
& (unit -> 'a infFront) -> 'a infStream ]*)
fun delay d = Stream(d)
(*[ map <: ('a -> 'b) -> 'a stream -> 'b stream
& ('a -> 'b) -> 'a infStream -> 'b infStream ]*)
(*[ map' <: ('a -> 'b) -> 'a front -> 'b front
& ('a -> 'b) -> 'a infFront -> 'b infFront ]*)
fun map f s = delay (fn () => map' f (expose s))
and map' f Empty = Empty
| map' f (Cons(x,s)) = Cons (f(x), map f s)Here the "val" keyword has been omitted from the annotations for map and map'. It is optional for annotations containing only a sort annotation for a single variable - this allows the name to line up nicely in the same column as in the actual "fun" or "val" definition.
An older syntax used ":>" and ":" instead of "<:". These are depreciated, but there may still be some code around which uses them.
Refinement annotation declarations (datasort, val and sortdef) may appear anywhere that an SML declaration (like datatype, val, type) is allowed. Similar specifications in signatures are supported.
See my PhD disseration "Practical Refinement-Type Checking" for more details, including a grammar that describes the language of annotations more precisely.
The following files may be of particular interest to those wanting to use SML CIDRE.
./test-examples/ A directory containing some test files, which may be useful as examples of the use of sorts.
./emacs/sml-refinements.el Extends the emacs sml-mode with fonts for refinement annotations, so that they can be easily distinguished from ordinary comments
The following files and directories may be of particular interest to those wanting to browse the source code of SML CIDRE.
./src/ Contains all the source code for the checker.
./src/Cidre/ Contains the top-level of CIDRE, including processing of MLB files - partly based on the ML Kit version 4.3.2.
./src/Common/ These two directories contain most of the ./src/Parsing/ source files for the ML Kit front end. Many of these files have been modified to support refinement checking, and many new files have been added.
./src/Common/RefObject.sml Low-level code for representations of sorts, sort schemes, sort functions, realisations, etc.
./src/Common/RefinedEnvironments.sml Representations of environments, and related functions, including calculation of lattices of refinements.
./src/Common/RefDec.sml High-level code for refinement checking of core declarations and expressions.
./src/Common/ElabDec.sml High-level code for elaboration of core declarations and expressions.
./src/Common/ElabTopdec.sml High-level code for elaboration of modules. Refinement checking for module-level constructs is built directly into this module.
./src/Common/Elaboration.sml Contains most of the functor applications that build the front end.
./src/Manager/ParseElab.sml Contains top-level functions for checking files, reporting errors, managing the current basis.
./src/Common/RefineCheck.sml The top-level module in the refinement checker.
./src/sources.cm SML/NJ Compilation Manager setup files, ./src/Common/common.cm which contain the names of all the files ./src/Parsing/parsing.cm needed to build the refinement checker.
SML CIDRE is built on top of parts of the ML Kit - mostly version 3, but also versions 1.5 and 4.0. Warning: currently some of the unused ML Kit files are still in place, which could potentially lead to confusion when browsing the source code.