Programatica Tools

The Programatica tools currently consist of the following programs, which are described in more detail below:

pfe The Preliminary Front-End tool. (Or perhaps the Programatica Front-End tool :-)
pfesetup A front-end to pfe, for simple creation of PFE projects, using a command line interface similar to that of Hugs or GHC.
pfebrowser A Haskell browser tool (runs under the X11 Window system). It also has some support for certificate management.
cert Certificate manipulation tool.

Except for pfebrowser, these are all command-line tools.

We also provide a version of the Haskell 98 Prelude and standard libraries for use with PFE. We also adapted a version of the Haskell Hierarchical Libraries for use with PFE.

Where to get the tools

Binary snapshots and installation instructions are available in the download directory.

If you are a local PacSoft member and you just want to test the tools, they are already installed in

(along with various other Linux tools) so just log in on one of the Linux computers (kokotni, watiya, turing ,...) and add that directory to your path.


Common to all the tools is that they operate on a PFE project, i.e., a collection of files containing Haskell modules. A PFE project is created in a specific directory and the PFE tools operate on the project in the current directory. Except for the source files, which can be located anywhere in the file system, the PFE tools keep all information relating to a project in a subdirectory called hi.


pfesetup creates a new PFE project. Usage:
pfesetup [options] path1 ... pathn

where the paths are Haskell files to include in the project.

pfesetup is designed to ease the transition from other Haskell implementations (hugs, ghc, hbc, nhc) by providing a similar command line interface.


(-P|-I|-i)path1:...:pathn Directories to search for imported modules.
[no]cpp Pass source files through the C preprocessor (or not). The default is nocpp.
[no]prelude All modules implicitly import the Prelude (or not).
[no]plogic Enable (or disable) support for the P-logic extension. When enabled, assert and property are reserved identifiers and text in {-P: comments like this -} is treated as ordinary code
+h|hierarchical Use the Haskell Hierarchical Libraries
-h|nohierarchical Use the plain Haskell 98 Libraries (this is the default)

pfesetup does its work by using the pfe new and pfe chase commands. (pfe chase is the only command that assumes a relationship between file names and module names.)


pfe [options] command

where options include

[no]plogicEnable (or disable) support for the P-logic extension. When enabled, assert and property are reserved identifiers.
[no]cppPass source code through the C preprocessor (or not)
cpp=commandPass source code through a user supplied preprocessor
[no]preludeAll modules implicitly import the Prelude (or not)
(+|-)debugTurn on (or off) verbose debugging info in pretty printed output
(+|-)tinfoInclude (or not) extra type information in pretty printed output
(+|-)utf8Turn on (or off) the use of Unicode symbols and UTF-8 encoding of pretty printed output
layout=layoutChange the pretty printer's layout style to one of PPOffsideRule, PPSemiColon, PPUtrecht, PPInLine, PPNoLayout. (Not all layout styles are implemented)

and where command is one of:

Level 0: basic project management
new [-quiet] files create a new project containing (zero or more) files
add [-quiet] files add files to the project
remove [-quiet] files remove files from the project
fileslist files in the project
optionsshow options in effect
modules moduleslist modules in the project
Module graph queries
graph [-rev] [-dot] [-dir] modules show module dependecy (sub)graph
unused modulesshow unimported and unreachable modules
prune modulesremove unreachable modules from the project
file moduleswhich file is the module in
module fileswhich module does the file contain
Import chasing
chase fileslook for imported modules in given files/directories
Level 1: simple, local module queries
defined moduleslist entities defined in the module
free moduleslist names referenced but not defined in the module
pragmas modulesextract pragmas from modules
lex filesshow the result of lexical analysis
lexl files show the result of lexical analysis + layout preprocessing
preparse files preparse and show abstract syntax
Level 2: module system queries (import/export, top level environment)
exports moduleslist entities exported by the modules
find identifiersfind exported entities with the given names
inscope moduleslist entities in modules' top-level environment
Level 3: proper parsing (and name resolution)
pp modulesparse and pretty-print modules
parse modulesparse and show abstract syntax
htmlfiles modulesgenerate HTML files for modules (to be used with pfe.cgi for dynamically generated web pages)
webpages modulesgenerate static web pages for modules
Program transformation
rmpatbind modulesremove pattern bindings
patmatch modulessimplify pattern matches
funbind modulessimplify function bindings
Level 4: type checking
tc [-pm] [-pb] [-lc] modules type check and display decorated modules
types modulesshow types/kinds of top-level entities
typeof M1.x1 ... Mn.xn show types of named top-level entities
kindof M1.x1 ... Mn.xn show kinds of named top-level entities
instances moduleslist instances defined in a module
iface modulesshow the interfaces of modules
usedtypes modulesshow what types identifers are used at
Level 5: function level dependencies
deps [-dot] [-untyped] modules compute dependency graph for definitions
needed [-untyped] M1.x1 ... Mn.xnneeded definitions
neededmodules [-untyped] M1.x1 ... Mn.xnnames of modules containing needed values
dead [-untyped] M1.x1 ... Mn.xndead code (default: Main.main)
uses [type|class|value|con] M.x find all uses of an entity
loc modulesnumber of lines of code
sizemetricsnumber of lines per module metrics
locmetricsnumber of lines of code per module metrics
importmetricsnumber of imports per module metrics
exportmetricsnumber of exports (importers) per module metrics
classmetricsnumber of instances per class metrics
Commands to support certificate servers
assertions moduleslist names of named assertion
asig M.xwrite an assertion signature to stdout
tasig M.xwrite an assertion signature to stdout
adiff M.xcompare an assertion signature with stdin
tadiff M.xcompare an assertion signature with stdin
qc modulestranslate to QuickCheck
slice M.xextract a slice (needed part) of the program
pqc M.xpruned translation to QuickCheck
qcslice M.xtranslate a slice to QuickCheck
stratego modulessimple translation of one module to Stratego
strategoslice modulestranslate a slice to Stratego
alfa [-simplepats] modulestranslate modules to Alfa
cleanremove cache files
Interactive/server mode
interactiveread pfe commands from stdin
serverstart a PFE server
helplist available commands
versiondisplay version number

(TODO: many commands need to be explained in more detailed. Some related commands should be combined into one command with options.)


cert command
where the command is one of

typeslist supported certificate types
lslist certificates
dotgraphoutput dot format certificate dependency graph
todolist uncertified assertions
new type M/c conc ... create a new certificate
info M/cshow certificate details
validate M/cvalidate a certificate
validate -allvalidate all certificates
sign M/cadd a PGP signature to a certifiacte
verify M/cverify the PGP signature of a certificate
rm M/cremove a certificate
recreategenerate a list of cert new commands to recreate all certificates

(TODO: describe commands in more detail. Add more functionality.)


pfebrowser [options]
where the options are the same as for pfe.

Since pfebrowser currently doesn't provide any project management functionality, before you start pfebrowser, you should create a PFE project with the pfesetup or pfe command. Also, if files are added or removed from the project, you need to restart pfebrowser.


In the source display area, clicking on identifiers have the following effect:

Button 1 (Left) Jumps to the definition
Button 2 (Middle) Displays information about the identifier, such as where it was originally defined and what type of entity it represents.
If type checking is turned on, pfebrowser also displays the type of the identifier, both it's general type scheme and the instance it is used at. For an identifier denoting a type or a class, its kind is shown.
Button 3 (Right) Highlight all references to the same entity in the current module.

Type checking

Type checking is turned off by default. To turn it on, select Type Info in the View menu. Type checking is turned off when a type error is encountered.

Auxiliary windows

The Windows menu lists the following windows that display additional views of the current module.

CertInfo Details about the currently selected certificates. (Opens automatically when clicking on a certificate icons.)
CertTypes Lists known certificate types.
Evidence List assertions and certificates in the current module
Exports Lists entities exported from the current module
Interface Lists types/kinds of entities exported from the current module, provided type checking is turned on.
Pretty Displays a pretty printed view of the current module.

Certificate management

(TODO: document how to manipulate certificates with pfebrowser...)

(TODO: there is probably more functionality in pfebrowser that needs to be documented.)