12. ML Interface

The Twelf implementation defines a number of ML functions embedded in structures which can be called to load files, execute queries, and set environment parameters such as the verbosity level of the interaction. These functions and parameters are available in the Twelf structure. If you open the Twelf structure with

open Twelf

after compiling and loading Twelf, you do not have to type the `Twelf.' to the functions shown below.

Previous implementations of Elf offered a stand-alone command interpreter but this has not yet been ported. To exit Twelf and ML call Twelf.OS.exit ();.

12.1 Configurations

Groups of Twelf files are managed in configurations. A configuration is defined by a file, by convention called `sources.cfg', which resides in the same directory as the Twelf source files. The configuration file must contain at most one Twelf source file per line, and the files must be listed in dependency order. A configuration config can then be defined from the file by the ML declaration

val config = Twelf.Config.read "sources.cfg";

By convention, the filenames end in the extensions

`.elf'

for constant declarations and definitions or mixed files,

`.quy'

for files which contain query declarations,

`.thm'

for files which contain %theorem and %proof declarations.

File names may not contain whitespace. They are interpreted relative to the current working directory of ML, but resolved into absolute path names when the configuration file is read. To change the current working directory call

Twelf.OS.getDir ();               (* get working directory *)
Twelf.OS.chDir "directory"; (* change working directory *)

As an example, we show how the Mini-ML configuration is defined and loaded, assuming your current working directory is the root directory of Twelf.

Twelf.make "examples/mini-ml/sources.cfg";

The call to Twelf.make returns either Twelf.OK or Twelf.ABORT. It reads each file in turn, starting from an empty signature, printing the results of type reconstruction and search based on the value of the Twelf.chatter variable (see section Environment Parameters). If another configuration or file has previously been read, all the declarations will first be deleted so that Twelf.make always starts from the same state.

To load a configuration, use Twelf.Config.load config. This is will first reset the state and then load config. In order to avoid resetting the state, use Twelf.Config.append config instead.

Loading a configuration will stop at the first error encountered, issue an appropriate message and return Twelf.ABORT. If there is an unexpected internal error (which indicates a bug in the Twelf implementation), it raises an uncaught exception instead and returns to the ML top-level.

To explore the behavior of programs interactively, you may call the Twelf top-level with

Twelf.top ();

which is explained in Interactive Queries.

The default suffix for configuration files is `cfg'; it can be changed with

Twelf.Config.suffix := "suffix";

although this may confuse the Twelf server.

Twelf configurations can also be defined explicitly from a list of file names with

Twelf.Config.define ["file1, …, filen"];

12.2 Loading Files

Twelf also allows direct management of the signature by loading individual files. This is generally not recommended because successive declarations simply accumulate in the global signature which may lead to unexpected behavior. The relevant function calls are

Twelf.reset ();
Twelf.loadFile "file";

where Twelf.reset () resets the current global signature to be empty and Twelf.readFile "file" loads the given file whose name is interpreted relative to the current working directory.

Caution: Reading a file twice will not replace the declarations of the first pass by the second, but simply add them to the current signature. If names are reused, old declarations will be shadowed, but they are still in the global signature and might be used in the search for a solution to a query or in theorem proving, leading to unexpected behavior. When in doubt, use configurations (see section Configurations) or call Twelf.reset ().

12.3 Environment Parameters

Various flags and parameters can be used to modify the behavior of Twelf and the messages it issues. They are given below with the assignment of the default value.

Twelf.chatter := 3;

Controls the detail of the information which is printed when signatures are read.

0

Nothing.

1

Just file names.

2

File names and number of query solutions.

3

Each declarations after type reconstruction.

4

Debug information.

5

More debug information.

6

Even more debug information.

Twelf.doubleCheck := false;

If true, each declaration is checked again for type correctness after type reconstruction. This is expensive and useful only for your peace of mind, since type checking is significantly simpler than type reconstruction.

Twelf.unsafe := false;

If true it will allow the %assert declaration to assert theorems without proof.

Twelf.Print.implicit := false;

If true, implicit arguments (normally elided) are printed. Sometimes this is useful to track particularly baffling errors.

Twelf.Print.depth := NONE;

If SOME(d) then terms deeper than level d are printed as `%%'.

Twelf.Print.length := NONE;

If SOME(l) then argument lists longer than l are truncated with `...'.

Twelf.Print.indent := 3;

Controls the amount of indentation for printing nested terms.

Twelf.Print.width := 80;

The value used to decide when to break lines during printing of terms.

Twelf.Trace.detail := 1;

Controls the detail in information during tracing. See Tracing and Breakpoints

Twelf.Compile.optimize := true;

Determines whether a minimal amount of optimization during translation from signature to program is carried out. If set to false, unification can be traced in more detail.

Twelf.Prover.strategy := Twelf.Prover.FRS;

Determines the strategy, where F=Filling, R=Recursion, and S=Splitting. Can also be Twelf.Prover.RFS.

Twelf.Prover.maxSplit := 2;

The maximal number of generations of a variable introduced by splitting. Setting is to 0 will prohibit proof by cases.

Twelf.Prover.maxRecurse := 10;

The maximal number of appeals to the induction hypothesis in any case during a proof.

Twelf.Table.strategy := Twelf.Table.Variant;

Determines the subsumption strategy for tabled logic programming which is either Twelf.Table.Variant or Twelf.Table.Subsumption.

Twelf.Table.strengthen := false;

Determines whether table entry lookup takes subordination into account or not.

12.4 Signature Printing

Twelf provides two ways to print the current global signature.

Twelf.Print.sgn ();
Twelf.Print.prog ();

The first prints the signature, using only forward arrows ->, the second will print the signature interpreted as a logic programming using backward arrows <-. Depending on your goals, one or the other might be easier to use.

Output can also be generated in TeX format. The necessary library files can be found in the `tex/' subdirectory of the distribution. To print the current signature using TeX format, use

Twelf.Print.TeX.sgn ();
Twelf.Print.TeX.prog ();

with the same interpretation as the plain text printing commands above.

12.5 Tracing and Breakpoints

Twelf no incorporates some rudimentary tracing facilities for the logic programming interpreter of signatures. This is best used within the Emacs server, but it is also available within the ML Interface. It is not available with the tabled logic programming interpreter. Also, when optimizations are enabled (Twelf.Compile.optimize is true), unification can not be traced.

A tracing specification may be associated with constants in a signature.

Twelf.Trace.None

Do not trace.

Twelf.Trace.Some ["c1",...,"cn"]

Trace clauses (object-level constants) or predicates (type families) named c1 through cn.

Twelf.Trace.All

Trace all clauses and predicates.

One can either suspend the execution when a specified clause or predicate is invoked, or simply trace goals

Twelf.Trace.trace spec

Twelf.Trace.break spec

When a breakpoint is set, execution will halt and ask for an action from the user. This consists of a (possible empty) line of input followed by RET. Current, the following actions are available.

<newline> - continue --- execute with current settings
n - next --- take a single step
r - run --- remove all breakpoints and continue
s - skip --- skip until current subgoals succeeds, is retried, or fails
s n - skip to n --- skip until goal (n) is considered
t - trace --- trace all events
u - untrace --- trace no events
d n - detail --- set trace detail to n (0, 1, or 2)
h - hypotheses --- show current hypotheses
g - goal --- show current goal
i - instantiation --- show instantiation of variables in current goal
v X1 ... Xn - variables --- show instantiation of X1 ... Xn
? for help 

The detail of the trace information can be set with the variable Trace.detail := n; to one of

0

print no information

1

print standard information

2

print details of unification

Note that if Twelf.Compile.optimize is true, then details of unification cannot be shown. It is possible to examine and reset the state of the currently traced predicates with

Twelf.Trace.show ();

Twelf.Trace.reset ();

12.6 Timing Statistics

Twelf has a few utilities to collect run-time statistics which are useful mainly for the developers. They are collected in the structure Timers. Timing information is cumulative in an ML session.

Twelf.Timers.show ();

Show the value of timers and reset them to zero.

Twelf.Timers.reset ();

Simply reset all timers to zero.

Twelf.Timers.check ();

Display the value of timers, but do not reset them.

Caution: Normally, the various times are exclusive, except that the runtime includes the garbage collection time which is shown separately. However, there is a problem the time for printing the answer substitution to a query is charged both to Printing and Solving.

12.7 Twelf Signature

For reference, here is the ML signature TWELF of the Twelf structure which defines most functions and flags relevant to loading and executing Twelf programs.

signature TWELF =
sig
structure Print :
sig
  val implicit : bool ref           (* false, print implicit args *)
  val depth : int option ref        (* NONE, limit print depth *)
  val length : int option ref       (* NONE, limit argument length *)
  val indent : int ref              (* 3, indentation of subterms *)
  val width : int ref               (* 80, line width *)

  val sgn : unit -> unit            (* print signature *)
  val prog : unit -> unit           (* print signature as program *)
  val subord : unit -> unit         (* print subordination relation *)
  val domains : unit -> unit        (* list constraint domains *)

  structure TeX :                   (* print in TeX format *)
  sig
    val sgn : unit -> unit          (* print signature *)
    val prog : unit -> unit         (* print signature as program *)
  end
end

structure Trace :
sig 
  datatype 'a Spec =                (* trace and breakpoint spec *)
    None                            (* no tracing, default *)
  | Some of 'a list                 (* list of clauses and families *)
  | All                             (* trace all clauses and families *)

  val trace : string Spec -> unit   (* trace clauses and families *)
  val break : string Spec -> unit   (* break at clauses and families *)
  val detail : int ref              (* 0=none, 1=default, 2=unify *)

  val show : unit -> unit           (* show trace, break, and detail *)
  val reset : unit -> unit          (* reset trace, break, and detail *)
end

structure Timers :
sig
  val show : unit -> unit           (* show and reset timers *)
  val reset : unit -> unit          (* reset timers *)
  val check : unit -> unit          (* display, but not no reset *)
end

structure OS :
sig
  val chDir : string -> unit        (* change working directory *)
  val getDir : unit -> string       (* get working directory *)
  val exit : unit -> unit           (* exit Twelf and ML *)
end

structure Compile :
sig
  val optimize : bool ref          (* true, optimize clauses *)
end

structure Table : 
sig 
  datatype Strategy = Variant | Subsumption

  val strategy : Strategy ref      (* Variant, tabling strategy *)
  val strengthen : bool ref        (* false, tabling optimization *)

  val top : unit -> unit           (* top-level for tabled queries *)
end 

structure Recon :
sig
  datatype TraceMode = Progressive | Omniscient
  val trace : bool ref		   (* false, trace term reconstruction *)
  val traceMode : TraceMode ref	   (* Omniscient, trace mode *)
end

structure Prover :
sig
  datatype Strategy = RFS | FRS    (* F=Fill, R=Recurse, S=Split *)
  val strategy : Strategy ref      (* FRS, strategy used for %prove *)
  val maxSplit : int ref           (* 2, bound on splitting  *)
  val maxRecurse : int ref         (* 10, bound on recursion *)
end

val chatter : int ref               (* 3, chatter level *)
val doubleCheck : bool ref          (* false, check internal types *)
val unsafe : bool ref               (* false, allow %assert w/o proof *)

datatype Status = OK | ABORT        (* return status *)

val reset : unit -> unit            (* reset global signature *)
val loadFile : string -> Status     (* load file *)
val readDecl : unit -> Status       (* read declaration interactively *)
val decl : string -> Status         (* print declaration of constant *)

val top : unit -> unit              (* top-level for queries *)

structure Config :
sig
  type config                       (* configuration *)
  val suffix : string ref           (* suffix of configuration files *)
  val read : string -> config       (* read config file *)
  val load : config -> Status       (* reset and load configuration *)
  val append : config -> Status     (* load configuration (w/o reset) *)
  val define : string list -> config (* define configuration *)
end

val make : string -> Status         (* read and load configuration *)

val version : string                (* Twelf version *)
end;  (* signature TWELF *)

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.