=============================================================
SML CIDRE (Checker for Intersection and Datasort Refinements)
=============================================================

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


Introduction
------------

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 "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.)

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 
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


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.

 ./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.