Grail Tutorial - Command Line Options
Instead of just running Grail with g3
there is a large
number of options which you can specify on the command line. This
section discusses these by theme.
Loading Grammars
-
g3 grammar
File, loads grammar file
File.
Windows
The gv window keeps track of the current state of Grail's partial proofs.
-
gv
, open a ghostview window.
-
nogv
, don't open a ghostview window.
The statistics window keeps track of the number of substitutions
performed and the number of substitutions which have been eliminated
by the different filtering strategies.
-
stats
, open a statistics window.
-
nostats
, don't open a statistics window.
Execution
-
link
Mode, set the link mode for the
substitutions to Mode, which can be one of the following:
auto for automatic linking, partial for automatic
linking of substitutions for which there is a unique possibility,
kbest for automatic linking of the best k
possibilities and manual for manual linking.
-
expr
Term, set k in the kbest term to
Term. Term may contain a single free variable, which will be
instatiated at execution with the number of atomic
formulas. Therefore expr N^2
will perform the best
n2 axiom substitutions for n atomic formulas.
-
par
Mode set the mode for the contractions of
the par links either to auto for automatic contractions or to
manual for manual contractions.
-
regin
, perform Régin's algorithm to eliminate
axiom links which can never contribute to a complete matching (default).
-
noregin
, don't perform Régin's algorithm.
-
zeroheap
, fail whenever an atom has zero linking
possibilities (default).
-
nozeroheap
, don't fail when an atom has zero linking
possibilities. This is useful to identify problems in your grammar
file because of overeager optimization.
Graphviz Output
These options control the way Grail exports its graphs to Graphviz.
-
implicit_modes
, don't portray mode information in
the graphs whenever the grammar contains only a single mode.
-
explicit_modes
, always portray mode information in
the graphs, even when the grammar has a single mode.
-
zero_root
, number the paths from the central node from
1 to n-1, using 0 for the root of a tree.
-
max_root
, number the paths from the central node from
1 to n-1, using n for the root of a tree.
-
tentaclelabels
, label the paths from the central
node of a constructor.
-
notentaclelabels
, don't label the paths from
the central node of a constructor. Note that this can sometimes
produce a misleading visual representation.
LaTeX Output
The following options only affect the LaTeX output produced by Grail.
-
latex
, output LaTeX (default, if LaTeX and a
previewer are installed on your machine)
-
nolatex
, don't output LaTeX files.
-
somebrackets
, don't output brackets (for
formulas and lambda terms) when they can be left implicit because of
the operators and their priorities.
-
allbrackets
, output all brackets for formulas and
lambda terms explicitly.
-
fxy
, output lambda-term applications of the form
((read y) x) as read(x,y) instead.
-
fyx
, keeps lambda term applications of the form
((read y) x) unchanged.
-
alphalex
, sort the lexicon alphabetically for the
LaTeX lexicon file.
-
typelex
, sort the lexicon first by formula, then
alphabetically.
Debugging
The debugger options allow you to lance the Prolog debugger and verify
everything works correctly. This is meant for the use of developpers
and programmers wanting to add new functionality to Grail and not for
the casual user.
-
trace
, follow Grail's execution step by step.
-
spy
Predicate, place a spypoint on
Predicate and enter the debugger when Grail enters this
predicate.
-
guispy
Predicate, as spy
above
this will enter the debugger when Grail enters Predicate, but
using SWI Prolog's graphical debugger environment.
Richard.Moot@labri.fr
Last modified: Tue Feb 10 18:52:15 CET 2009