#PTS
A Haskell implementation of the Pure Type System
##Installation
Run the following commands at the top:
cabal install
To proactively avoid dependency hell, consider using cabal-dev or some other tool to sandbox builds.
This repository contains some example programs in the examples folder.
Known public developments using this pts interpreter:
- Toxaris/lift.pts (Constructive lift monad in System Fω)
If you use the pts interpreter and want your use to be mentioned here, sent a pull request for README.md or contact the authors.
We bundle a very simple emacs mode, see emacs/pts-mode.el. To see where the emacs mode has been installed to, run:
pts --locate-emacs-mode
To install the emacs mode, you can add something like this to
your .emacs:
(let ((pts-mode-path (shell-command-to-string "pts --locate-emacs-mode")))
(if (file-exists-p pts-mode-path)
(progn
(add-to-list 'load-path pts-mode-path)
(require 'pts-mode))
(message "Loading PTS returned an invalid path: %s" pts-mode-path)))
This assumes that pts is on your path and calls it to find the
emacs mode. Keybindings in pts-mode:
- C-c C-l check types and assertions in current buffer
If you use exuberant ctags, you can add to your .ctags the following block:
--langdef=LPTS
--langmap=LPTS:.lpts
--regex-LPTS=/^>[ \t]*([^][ \t.:=;()$]+)[ \t]*(\([^()]*\)[ \t]*)*([:=]|$)/\1/v,values/
--regex-LPTS=/^>[ \t]*export ([^][ \t.:=;()$]+)[ \t]*;/\1/e,exports/
--regex-LPTS=/^>[ \t]*module ([^][ \t.:=;()$]+)[ \t]*;/\1/m,modules/
--langdef=PTS
--langmap=PTS:.pts
--regex-PTS=/^[ \t]*([^][ \t.:=;()$]+)[ \t]*(\([^()]*\)[ \t]*)*([:=]|$)/\1/v,values/
--regex-PTS=/^[ \t]*export ([^][ \t.:=;()$]+)[ \t]*;/\1/e,exports/
--regex-PTS=/^[ \t]*module ([^][ \t.:=;()$]+)[ \t]*;/\1/m,modules/
You can then run ctags to produce Emacs tags with a command line similar to the following:
ctags -e $(find . -name '*.pts' -o -name '*.lpts')
I am happy to receive pull requests. Note that I assume that I can publish the code in pull requests under a three-clause BSD license.