Ari Lamstein and Peter Selinger
The PPL compiler was written by Ari Lamstein under the supervision of Peter Selinger as part of a UROP project in the Winter of 2000, and as part of an REU project in the Spring of 2000, at the University of Michigan.
PPL is an extension of the call-by-name lambda calculus with integers, booleans, let and let rec bindings, products and sum types. The type system of PPL is ML-polymorphism. The syntax of PPL terms M,N is as follows. Here reserved words and symbols are shown in red, n and j are integers, and x is an identifier.
M,N ::= |
x
| n
| true
| false
| ( M)
| \ x. M
| MN
|
| let x= M
in N
| let rec x= M in N
|
|
| ()
| ( M1, ..., Mn)
| pi j/ n M
|
|
| in j/ n M
| case M of in 1/ n x1 -> N1 | ... | in n/ n xn -> Nn
|
plus
, if
etc.
The PPL compiler translates closed PPL terms into an idealized
assembly language. This idealized assembly language differs from
actual assembly language in several respects: it allows for an
infinite number of registers, and it has opcodes for certain
high-level operations, such as allocation and exit, which would
normally be realized as system calls. For reasons of portability, the
``assembly code'' generated by the PPL compiler is actually realized
as a set of pre-processor macros in the C language; thus, the output
of ppl
can be compiled by any
C-compiler on the target machine.
ppl
filename
, where filename
is a file which contains
a PPL program. The compiler will read the program, write its most
general type to the terminal, and write its assembly code translation
to a file.
PPL accepts the following command line options:
--parse, -p | Do not compile; parse and type-check only. |
--step, -s | Print CBN reduction sequence. |
--reduce, -r | Reduce term to CBN normal form. |
--untyped, -u | Omit type-checking. |
--optimize, -z | Create optimized compiled code. |
--typeinfo mode, -i mode |
Print additional type information depending on mode. |
--term term |
Use term as input. |
--stdin | Read input from terminal. |
--stdout | Write output to terminal. |
--output filename, -o filename | Write output to specified file. |
--help, -h | Print help message and exit. |
--version, -v | Print version info and exit. |
--parse
flag will cause the compiler to read and
type-check a PPL program but not compile it. The
--reduce
and --step
flags cause the compiler
to apply CBN reduction to the input term. In --reduce
mode, the final normal form is printed, whereas in --step
mode, the entire reduction sequence is printed, one term per line.
The --typeinfo mode
flag alters the amount of type
information that is displayed to the terminal. mode
must
be one of none
, all
, top
,
let
or an integer nesting depth n. The compiler then
gives type information on, respectively, no variables, all variables,
all variables defined on the top-level, variables defined only by let
and let-rec constructs, and variables defined up to a depth of n.
The --untyped
flag causes the compiler to not type-check
the PPL program. The --optimize
flag will cause the
compiler to beta-reduce certain redexes before compilation, yielding
more efficient assembly code.
The --term
, --stdin
, --stdout
,
and --output filename
flags affect where the compiler
looks for input and where it writes the output. When using the
--term
flag one may find it useful to enclose the term in
quotation marks. This will prevent shell substitutions.
The --help
flag provides a list and brief description of
all PPL options. The --version
flag gives information on
which version of the compiler is in use.
There is also a graphical user interface for PPL called
ppli
. It is written in Tcl/Tk. In Unix, it can be
accessed by typing wish ppli
at the command line.
ppli
provides a window to type a PPL program or load a
program from a file, together with various buttons for compiling,
reducing, and stepping through the reduction sequence of a term.
Theory and Implementation of a Functional Programming Language, Rose-Hulman Institute of Technology Undergraduate Mathematics Journal 1(2), 2000. (DVI, PS, PS 2up, PDF)
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.