Levy is a simple implementation of Paul Levy's call-by-push-value language. The implementation contains a parser, type-checker, and an interpreter. It is part of the PL Zoo, see http://math.andrej.com/plzoo/.
The Levy language has the following features:
- integers with arithmetical operations *, +, -
- booleans with conditional statements and comparison =, < of integers
- general recursion (fixpoint operator)
- call-by-push-value features: return, thunk, force, sequence, and let binding
The Levy# language in this branch of the repository is a modification of Levy with user-defined datatypes and match statements. Match statements and user-defined enumerations are discussed in switch.levy, full user-defined datatypes are discussed in datatype.levy. Match statements lead to the possibility of non-exhaustive match exceptions; the possibility of such a runtime error generates a compile-time warning, as discussed in matching.levy.
The language is different enough from standard functional languages that you will not be able to guess how it works without reading about call-by-push-value first. A good place to start is Paul Levy's FAQ at http://www.cs.bham.ac.uk/~pbl/cbpv.html. There is also a blog post about Levy# at http://requestforlogic.blogspot.com/2011/08/embracing-and-extending-levy-language.html aimed at people who may be unfamiliar with call-by-push-value.
The authors of Levy are Matija Pretnar email@example.com, and Andrej Bauer Andrej.Bauer@andrej.com, with modifications by Robert Simmons firstname.lastname@example.org. The adaptation to Levy# is by Robert Simmons. See the file COPYRIGHT.txt for license information.
You need Objective Caml, http://caml.inria.fr/ version 3.10 or higher.
If you have an older version of Objective Caml you can still compile the code by hand.
A simple emacs highlighting mode for Levy is included; you can include it by adding the following text to your .emacs file, changing the levy-root directory to wherever the code for Levy was placed.
;; Setup for levy-mode (setq levy-root "/home/hqbovik/levy/") (load (concat levy-root "levy.el")) (add-to-list 'auto-mode-alist '("\\.levy\\'" . levy-mode))
To compile the program run the command
For the native code version run
If you do not have the make utility, run
First compile the program. You may then run the interpreter with
If you built the native code version, this would be
The file example.levy contains examples that explain the concrete syntax. You can load it and try it as follows:
$ ./levy.byte example.levy