LLF Copyright (C) 1997, 1998, Iliano Cervesato, Frank Pfenning, and Carsten Schuermann

Authors: Frank Pfenning Iliano Cervesato Carsten Schuermann Jeff Polakow

LLF is an implementation of

• the LLF linear logical framework, including type reconstruction
• the LLF constraint linear logic programming language

====================================================================== Files: NOTES --- remarks and todo list, most recent notes are at the top README --- this file, including some instructions for compilation TAGS --- tags file, for use in Emacs TEST/ --- test files, try use "TEST/all.sml"; sources.cm --- enables CM.make (); load.sml --- enables use "load.sml"; ( especially for MLWorks ) bin/ --- utility scripts java/ --- postprocessing Java modules

Standard ML, Revision of 1997:

If it is not installed already, please check

SML of New Jersey [free] http://cm.bell-labs.com/cm/cs/what/smlnj/index.html (version 110 or higher)

MLWorks [commercial, "personal version" free] http://www.harlequin.com/products/ads/ml/

Loading LLF:

Connect to LLF root directory Start SML/NJ 110 or MLWorks

CM.make (); ( in SML/NJ 110, sml-cm )

OR

use "load.sml"; ( in SML/NJ 110, sml or MLWorks )

To define configuration

use "examples//config.sml"; ( define configuration )

To load files and start top-level for queries (note that you have to replace -' (dash) by_' (underscore) in the name of the in order to conform to the lexical conventions of ML).

LLF.readConfig LLF.top ();

To compile files and read queries (see below for format)

LLF.compileConfig LLF.readFile "examples//examples.quy";

Current Examples (see examples/README for information) ccc church-rosser compile cut-elim lp lp-horn (meta-theory only) mini-ml polylam prop-calc units

Query Format for Files:

%query A.

where is the expected number of answers or (for infinity), and is the bound on the number of tries or (for infinity), and A is the goal type.

Formats M : A or c = M : A are currently not supported for queries.

Flags (with defaults):

Global.chatter := 3; ( chatter levels: 0 = nothing, 1 = files, 2 = number of query solutions, 3 = entries in external form, 4 = entries in internal form, 5 = debugging I, 6 = debugging II ) TpRecon.doubleCheck := false; ( re-check entries after reconstruction )

( for external format printing ) EPrint.printDepth := NONE; ( SOME(d): replace level n expressions by '%%' ) EPrint.printLength := NONE; ( SOME(l): replace lists longer than l by '...' )

( for internal format printing ) IPrint.printDepth := NONE; ( SOME(d): replace level n expressions by '%%' ) IPrint.printLength := NONE; ( SOME(l): replace lists longer than l by '...' )

Formatter.Indent := 3; ( number of spaces for indentation level ) Formatter.PageWidth := 80; ( default page width for formatting ) ( see formatter/formatter.sig for more )

Timing:

Timers.show (); ( show internal timers and reset )

Timers.reset (); ( reset internal timers ) Timers.check (); ( check internal timers, but do not reset )

Currently, the timing information for the solver includes the time taken by the success continuation. This is non-trivial if the success continuation prints the answer substitution, but negligible otherwise.

Generate the file load.sml for MLWorks or SML w/o the Compilation Manager with

CM.mkusefile "load.sml"; ( for core and meta-prover ) CM.mkusefile' ("meta.cm", "load-meta.sml"); ( for core ) CM.mkusefile' ("core.cm", "load-core.sml"); ( for meta-prover )

Make sure the current working directory is the root file of the implementation.

To run MLWorks, use Andrew SparcStation (telnet sun4.andrew) and invoke

/afs/andrew/scs/cs/mlworks/ultra/bin/mlworks-basis

possibly using -tty option.

Create TAGS file with

bin/tag-twelf

In SMLofNJ:

SMLofNJ.Internals.GC.messages

Compiler.Control.Print.printDepth := 100; ( default: 5 ) Compiler.Control.Print.printLength := 80; ( default: 12 ) Compiler.Control.Print.signatures := 1; ( default: 2 ) Compiler.Control.Print.linewidth := 79; Compiler.Control.Print.stringDepth := 200; ( default: 70 )

OS.FileSys.chDir "directory"; OS.FileSys.getDir ();

Profiling (under MLWorks):

In each examples directory there is a file config.sml, defining a configuration with the name of the example (where hyphens are replaced by underscore). Typical session:

use "examples/church-rosser/config.sml"; LLF.readConfig church_rosser;

For the last expression, hit the "Profile" button in the interactive system. Also, don't forget to set Preferences>Compilers> so that profiling is enabled BEFORE using "load.sml";

For "release":

( Compiler.Control.indexing := true; ) ( doesn't work right now )

bin/clean bin/clean-cm bin/tag-twelf cd .. tar -cvf llf.tar llf gzip llf.tar

Installation:

gunzip llf.tar.gz tar -xvf llf.tar cd llf sml-cm ( requires version 110! ) CM.make ();