COMP 426 Automated Reasoning
Software

Standard ML is a safe, modular, strict, functional, polymorphic programming language with compile-time type checking and type inference, garbage collection, exception handling, immutable data types and updatable references, abstract data types, and parametric modules. It has efficient implementations and a formal definition with a proof of soundness. For more information:

• What is SML?
• User's guide to SML , including information on downloading SML.
• The Standard ML Basis Library

Recommended gentle introductions:

• A Gentle Introduction to ML, by Andrew Cumming, Computer Studies, Napier University, Edinburgh
• Tips for Computer Scientists on Standard ML, by Mads Tofte, Department of Computer Science, University of Copenhagen (20 pages)

Recommended books and other documents:

• Programming in Standard ML, Robert Harper
• ML for the Working Programmer (2nd edition), Larry Paulson, Cambridge University Press,1996, ISBN (hardback):0-521-57050-6, ISBN (paperback):0-521-56543-X
• Information on SML including tutorials

Using SML in emacs or xemacs:

• Documentation for sml-mode
• Files for sml-mode (sml-mode)
• Usage of sml-mode:
  1. Copy the files for sml-mode into your load-path /home/user/yourname/yourdir/
  2. Add the following into your emacs or xemacs init.el file
     

     ;; SML Mode 
     ;; ============================
     
     (setq load-path (cons  "/home/user/yourname/yourdir" load-path))
     (autoload 'sml-mode "sml-mode" "Major mode for editing SML." t)
     (setq sml-mode-info "~/yourdir/sml-mode/sml-mode.info")
     
     (setq auto-mode-alist
                (append '(("\\.cm$" . sml-mode)
                          ("\\.fun$" . sml-mode)
                          ("\\.sml$" . sml-mode)
                          ("\\.sig$" . sml-mode)
                          ("\\.ML$"  . sml-mode)) auto-mode-alist))
     
     (add-hook 'sml-load-hook '(lambda () (require 'sml-font)))
     
     (defun delete-gc-message ()
       (beginning-of-line 0)
       (if (looking-at ".*\\(GC #[0-9]+[\.[0-9]+]*: *([0-9]* ms)\C-m*\n\\)")
           (delete-region (match-beginning 1) (match-end 1))))
     
     (defun comint-filter-sml-gc-messages (foo)
       (save-excursion
         (goto-char comint-last-output-start)
         (delete-gc-message)))
     
     (add-hook 'inferior-sml-mode-hook
               (lambda ()
                 (add-to-list 'comint-output-filter-functions
                              'comint-filter-sml-gc-messages)))
     
             

• How to use SML within emacs or xemacs:
  1. Start emacs or xemacs (ideally in the directory where your sml-code resides)
  2. Load a sml-file.
  3. Type M-sml. This will start a "sml" process in the background.
  4. Switch to buffer *sml*. Now you can start programming within emacs or xemacs.

Basics on how to use SML within SOCS McGill

SML has been installed on some of the lab machines (lab7-1 to lab7-16) and you should be able to start the SML compiler by logging into one of these machines and then typing sml in a shell.

To run the code provided, you should first change to the directory where your sml code resides. Then you can start the sml compiler by typing sml. To compile the code provided, just type CM.make();