Resources -- Winter 2008

Twelf

We will be using the Twelf system, which is an implementation of a logical framework (LF), a constraint logic programming language (Elf), and a meta-theorem prover. Below is a quick introduction. For more information see the Twelf home page and the User's Guide for Version 1.3. You may also find the Twelf Wiki useful.

To run Twelf in the SOCS-domain, you need to add the following to your .emacs or .xemacs/init.el file:

;; ============================
;; Twelf
;; ============================

(setq load-path (cons "/usr/share/twelf/emacs/" load-path))

(setq twelf-root "/usr/share/twelf/")


;;; own version of twelf-init

(load "/usr/share/twelf/emacs/twelf-init.el")


Twelf Resources

Twelf Project

Standard ML

Standard ML

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

Programming Contests

Once you have mastered SML, you may be intrigued by the ICFP Programming contest held every year. Check it out here! Note that this contest does not require you to program in a functional language, but nevertheless many people choose a functional language.

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 the lab machines 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 "sources.cm";

If you have started the sml compiler in a different directory than your code, you must change to correct directory. Within sml you can type the following:

• Posix.FileSys.chdir "dirname"; change directory to dirname
• Posix.FileSys.getcwd(); get the name of the current directory

How to change the printing depth in SML 110.55?

If you want to print back the results of some evaluation and you only see # where you expect some expression, then you may want to change the print depth of the sml compiler.

• Control.Print.printDepth controls the printing depth.
  Control.Print.printDepth := 100; will set it to 100.
• Control.Print.printLength controls the printing lenth.
  Control.Print.printLength := 100; will set it to 100.

Alternatively, you can set the depth at startup using the -Cxxx=yyy command line switch:

sml -Cprint.depth=100

Run

sml -H

to see a list of all such options.