Skip to content
This repository


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Original LLF implementation (typechecher + operational semantics) from 1997

branch: master

Fetching latest commit…


Cannot retrieve the latest commit at this time

Octocat-spinner-32 TEST
Octocat-spinner-32 bin
Octocat-spinner-32 examples
Octocat-spinner-32 formatter
Octocat-spinner-32 frontend
Octocat-spinner-32 global
Octocat-spinner-32 index
Octocat-spinner-32 java
Octocat-spinner-32 lambda
Octocat-spinner-32 lex
Octocat-spinner-32 modes
Octocat-spinner-32 names
Octocat-spinner-32 opsem
Octocat-spinner-32 order
Octocat-spinner-32 paths
Octocat-spinner-32 print
Octocat-spinner-32 stream
Octocat-spinner-32 table
Octocat-spinner-32 timing
Octocat-spinner-32 typecheck
Octocat-spinner-32 NOTES
Octocat-spinner-32 README
Octocat-spinner-32 TAGS
Octocat-spinner-32 TODO
Octocat-spinner-32 load.sml
Octocat-spinner-32 main.sml
Copyright (C) 1997, 1998, Iliano Cervesato, Frank Pfenning, and Carsten

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

 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"; --- 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]
    (version 110 or higher)

 MLWorks [commercial, "personal version" free]
Loading LLF:

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

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


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

To define configuration <example>

  use "examples/<example>/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 <example> in
order to conform to the lexical conventions of ML).

  LLF.readConfig <example> ();

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

  LLF.compileConfig <example>
  LLF.readFile "examples/<example>/examples.quy";
Current Examples (see examples/README for information)
  lp-horn (meta-theory only)

Query Format for Files:

  %query <expected> <try> A.

where <expected> is the expected number of answers or * (for infinity),
and <try> 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: ();   (* 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

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

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

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


possibly using -tty option.
Create TAGS file with



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

  cd ..
  tar -cvf llf.tar llf
  gzip llf.tar


  gunzip llf.tar.gz
  tar -xvf llf.tar
  cd llf
  sml-cm  (* requires version 110! *)
  CM.make ();
Something went wrong with that request. Please try again.