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
structure. If you open the
Twelf structure with
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
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
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.
The call to
Twelf.make returns either
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 10.3 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.
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
which is explained in section 5.3 Interactive Queries.
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";
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
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 10.1 Configurations) or
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;
Twelf.doubleCheck := false;
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;
trueit will allow the
%assertdeclaration to assert theorems without proof.
Twelf.Print.implicit := false;
true, implicit arguments (normally elided) are printed. Sometimes this is useful to track particularly baffling errors.
Twelf.Print.depth := NONE;
SOME(d)then terms deeper than level
dare printed as `%%'.
Twelf.Print.length := NONE;
SOME(l)then argument lists longer than
lare truncated with `...'.
Twelf.Print.indent := 3;
Twelf.Print.width := 80;
Twelf.Trace.detail := 1;
Twelf.Prover.strategy := Twelf.Prover.FRS;
S=Splitting. Can also be
Twelf.Prover.maxSplit := 2;
0will prohibit proof by cases.
Twelf.Prover.maxRecurse := 10;
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
second will print the signature interpreted as a logic programming using
<-. 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.
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.
A tracing specification may be associated with constants in a signature.
One can either suspend the execution when a specified clause or predicate is invoked, or simply trace goals
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
Trace.detail := n; to one of
It is possible to examine and reset the state of the currently traced predicates with
Twelf has a few utilities to collect run-time statistics which are
useful mainly for the developers. They are collected in the
Timers. Timing information is cumulative
in an ML session.
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
For reference, here is the ML signature
TWELF of the
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 *) 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 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 after reconstruction *) val unsafe : bool ref (* false, allow %assert without 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 interactive 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 define : string list -> config (* explicitly define configuration *) end val make : string -> Status (* read and load configuration *) val version : string (* Twelf version *) end; (* signature TWELF *)
Go to the first, previous, next, last section, table of contents.