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

/home/projects/pacsoft/tools/bin

(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.

Usage

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

pfesetup creates a new PFE project. Usage:

pfesetup [options] path₁ ... path_n

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.

Options:

(-P\|-I\|-i)`path₁`:...:`path_n`	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

Usage:

pfe [options] command

where options include

[no]plogic	Enable (or disable) support for the P-logic extension. When enabled, `assert` and `property` are reserved identifiers.
[no]cpp	Pass source code through the C preprocessor (or not)
cpp=`command`	Pass source code through a user supplied preprocessor
[no]prelude	All modules implicitly import the Prelude (or not)
(+\|-)debug	Turn on (or off) verbose debugging info in pretty printed output
(+\|-)tinfo	Include (or not) extra type information in pretty printed output
(+\|-)utf8	Turn on (or off) the use of Unicode symbols and UTF-8 encoding of pretty printed output
layout=`layout`	Change 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
files	list files in the project
options	show options in effect
modules `modules`	list modules in the project
Module graph queries
graph [-rev] [-dot] [-dir] `modules`	show module dependecy (sub)graph
unused `modules`	show unimported and unreachable modules
prune `modules`	remove unreachable modules from the project
file `modules`	which file is the module in
module `files`	which module does the file contain
Import chasing
chase `files`	look for imported modules in given files/directories
Level 1: simple, local module queries
defined `modules`	list entities defined in the module
free `modules`	list names referenced but not defined in the module
pragmas `modules`	extract pragmas from modules
lex `files`	show 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 `modules`	list entities exported by the modules
find `identifiers`	find exported entities with the given names
inscope `modules`	list entities in modules' top-level environment
Level 3: proper parsing (and name resolution)
pp `modules`	parse and pretty-print modules
parse `modules`	parse and show abstract syntax
HTML
htmlfiles `modules`	generate HTML files for modules (to be used with pfe.cgi for dynamically generated web pages)
webpages `modules`	generate static web pages for modules
Program transformation
rmpatbind `modules`	remove pattern bindings
patmatch `modules`	simplify pattern matches
funbind `modules`	simplify function bindings
Level 4: type checking
tc [-pm] [-pb] [-lc] `modules`	type check and display decorated modules
types `modules`	show 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 `modules`	list instances defined in a module
iface `modules`	show the interfaces of modules
usedtypes `modules`	show 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.xn`	needed definitions
neededmodules [-untyped] `M1.x1 ... Mn.xn`	names of modules containing needed values
dead [-untyped] `M1.x1 ... Mn.xn`	dead code (default: Main.main)
uses [type\|class\|value\|con] `M.x`	find all uses of an entity
Metrics
loc `modules`	number of lines of code
sizemetrics	number of lines per module metrics
locmetrics	number of lines of code per module metrics
importmetrics	number of imports per module metrics
exportmetrics	number of exports (importers) per module metrics
classmetrics	number of instances per class metrics
Commands to support certificate servers
assertions `modules`	list names of named assertion
asig `M.x`	write an assertion signature to stdout
tasig `M.x`	write an assertion signature to stdout
adiff `M.x`	compare an assertion signature with stdin
tadiff `M.x`	compare an assertion signature with stdin
qc `modules`	translate to QuickCheck
slice `M.x`	extract a slice (needed part) of the program
pqc `M.x`	pruned translation to QuickCheck
qcslice `M.x`	translate a slice to QuickCheck
stratego `modules`	simple translation of one module to Stratego
strategoslice `modules`	translate a slice to Stratego
alfa [-simplepats] `modules`	translate modules to Alfa
Cleaning
clean	remove cache files
Interactive/server mode
interactive	read pfe commands from stdin
server	start a PFE server
Documentation
help	list available commands
version	display version number

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

cert

Usage:

cert command

where the command is one of

types	list supported certificate types
ls	list certificates
dotgraph	output dot format certificate dependency graph
todo	list uncertified assertions
new `type` `M/c` `conc` ...	create a new certificate
info `M/c`	show certificate details
validate `M/c`	validate a certificate
validate -all	validate all certificates
sign `M/c`	add a PGP signature to a certifiacte
verify `M/c`	verify the PGP signature of a certificate
rm `M/c`	remove a certificate
recreate	generate a list of `cert new` commands to recreate all certificates

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

pfebrowser

Usage:

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.

Browsing

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.)