Switch branches/tags
Find file
Fetching contributors…
Cannot retrieve contributors at this time
179 lines (124 sloc) 7.14 KB
SML CIDRE (Checker for Intersection and Datasort Refinements)
Author: Rowan Davies (
(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".]
Building and using SML CIDRE
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.
- cd to the directory containing this file.
- type: sml useme.sml
- You can now run sml-cidre via: ./bin/sml-cidre
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 ""; [Replace 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.)
Emacs mode
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.
Syntax for refinement annotations
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.
Files of interest when using SML CIDRE
The following files may be of particular interest to those wanting to use
./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
Files of interest in the source of SML CIDRE
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.
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/ SML/NJ Compilation Manager setup files,
./src/Common/ which contain the names of all the files
./src/Parsing/ needed to build the refinement
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.