A Type Error Slicer for MiniML

Welcome user@38.103.63.60!

MiniML is a small sublanguage of Standard ML (SML). It has integers, booleans, lists, tuples, recursive and non-recursive value definitions, and a number of operations from the SML top level environment. The MiniML grammar is shown below. Associativities are as in SML. SML keywords that are not implemented may not be used as identifiers.

Please enter a sequence of MiniML declarations in the text area. Note that you have to enter declarations (members of the syntax class dec below), not expressions. Then click the button labelled "Display any type errors in MiniML code in entry panel". If your program has type errors, then a minimal type error slice will be displayed. Such a slice contains all program points that are relevant for a type error and and masks all irrelevant program points. Moreover, you will see a copy of your declaration sequence, where all relevant program points are highlighted. A declaration sequence may have more than one minimal type error slice. If you want to see another one, click the "Next" link. While our algorithm quickly finds a few minimal type error slices for a given declaration sequence, enumerating all such slices is expensive. For that reason, the enumeration algorithm is interrupted after a certain time limit. After fixing some of the reported errors, the programmer may check the program again to possibly discover further errors.

Note: If your browser does not have good support for CSS, or if it does not allow colors and font changes, pages might not render correctly and some highlight might be missing.
Note: If your browser does not support JavaScript, you can copy an example from this page and paste it into the entry panel.
  
Christian Haack Type Error Slicer Theory and Implementation
Joe Wells Theory and Implementation Consulting and Advice
Sébastien Carlier Web Interface Implementation

MiniML Grammar

op ranges over the following binary infix operators:

  =, <, >, <=, >=, +, -, *, div, mod, @, o, andalso, orelse 
 

Initial environment:

  not, hd, tl, length, rev, map, foldr, foldl
 
decs ::=                        (empty decs) 
       | decs dec

dec ::= val pat = exp

      | val rec x = fn match

exp ::= x
      | b

      | if exp then exp else exp
      | n
      | exp op exp

      | ()
      | (exp1,...,expn)          n >= 1
      | fn match
      | exp exp

      | nil
      | exp :: exp
      | case exp of match
      | let decs in exp end


match ::= mrule
        | mrule | match

mrule ::= pat => exp

        
pat ::= _
      | x
      | b
      | n
      | ()
      | (pat1,...,patn)          n >= 1
      | nil
      | pat :: pat

Syntactic restrictions:


TO DO

This is a work in progress. The following corrections and improvements are under consideration.

We would be delighted to receive bug reports and suggestions. Please send them to Sébastien Carlier and Christian Haack.