package acgtk
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2743321ae4cc97400856eb503a876cbcbd08435ebc750276399a97481d001d41
md5=04c1e14f98e2c8fd966ef7ef30b38323
Description
This toolkit provides a compiler and an interpreter for Abstract Categorial Grammars (ACGs). Grammars can be compiled and then used by the interpreter to parse (if the grammar is at most second-order) or to generate terms. See http://acg.loria.fr for more details and bibliographic references.
Published: 07 Sep 2021
README
ACGtk: an ACG development toolkit
ACGtk is a software package (2008-2021 INRIA©) for the development of abstract categorial grammars. This distribution provides two executables file: acgc
and acg
.
It is distributed with the CeCILL license (see the LICENSE file or http://www.cecill.info). Contributors are listed in the AUTHORS.md file.
A list of related publications is available at the ACG web page.
acgc
acgc
is a "compiler" of ACG source code, i.e. files containing definitions of signatures and lexicons. It basically checks whether they are correctly written (syntactically and wrt types and constant typing) and outputs a .acgo
object file. An interactive mode is available to parse terms according to signatures.
Run
./acgc --help
to get help.
acg
acg
is an interpreter of command meant to be useful when using ACGs. To get a list of command, run
./acg
then, on the prompt, type
help;
Example files are given in the examples directory. Read the README.md file.
Basic usage
Let's assume you defined a file my_acg.acg
in directory my_dir
. A basic usage of the acgc
and acg
commands could be:
$ acgc -o my_acg.acgo my_acg.acg
This will produce a my_acg.acgo
file (note that this is the default name and location if the -o
option is not provided).
Then, running :
$ acg
will open a prompt in which you can type:
# load o my_acg.acgo;
to load the data contained in the my_acg.acg
file. Assuming you have defined the signature Sig
and the lexicon Lex
, you can then run the following commands:
# Sig check lambda x.some_cst x: NP ->S;
to check whether lambda x.some_cst x
is a term of type NP ->S
according to Sig
.
You can type:
# Lex realize lambda x.cst x: NP ->S;
to compute the image of lambda x.cst x
by Lex
(assuming this term and this type are correct according to the abstract signature of Lex
).
You can type:
# Lex parse John+loves+Mary: S;
to check whether the term John+loves+Mary
has an antecend of type S
by Lex
, assuming that John+loves+Mary
is a term of type Lex (S)
in the object signature of Lex
.
Type CTRL-D
to exit from the program, or type:
# exit;
SVG output
If the --nsvg
option is not set when running acg
, a file realize.svg
(default name) is generated in the current directory whenever a realize
command is invoked. In order to set another file name, use the option --svg other_filename
.
This files contains a representation as a tree of the operations described by the term to realize (applications, abstractions). Each node contains the abstract term and its realizations by each of the lexicons specified on the command line. The graphic file can for instance been observed through a web browser.
Four rendering engines are available so far to render the terms in each node:
the default engine: just generates a lambda-term following the signature/lexicon syntax
the "logic" engine: formulas are rendered as logical formulas: non logical constants are in bold font, logical connectives are rendered using utf-8 if their names are as follows:
"Ex" -> "∃"
"ExUni" -> "∃!"
"Ex_l" -> "∃ₗ"
"Ex_t" -> "∃ₜ"
"All" -> "∀"
"All_t" -> "∀ₜ"
"TOP" -> "⊤"
"The" -> "ι"
"&" -> "∧"
">" -> "⇒"
"~" -> "¬"
the "trees" engine: terms are rendered as trees (e.g., derivation trees)
the "unranked trees": terms are rendered as trees, but if a non-terminal is defined as
[a-zA-Z]+[0-9]*
, it is rendered only using the[a-zA-Z]
part.
The association between the name of a signature and a rendering engine is declared in a configuration file that can be loaded through the --realize
option and that looks like:
$ cat config.json
{
"signatures": [
{ "name": "TAG", "engine": "trees" },
{ "name": "DSTAG", "engine": "trees" },
{ "name": "CoTAG", "engine": "trees" },
{ "name": "derivations", "engine": "trees" },
{ "name": "strings", "engine" : "strings"},
{ "name": "Strings", "engine" : "strings"},
{ "name": "logic", "engine" : "logic"},
{ "name": "low_logic", "engine" : "logic"},
{ "name": "derived_trees", "engine" : "unranked trees"},
{ "name": "Derived_trees", "engine" : "unranked trees"},
{ "name": "trees", "engine" : "unranked trees"}
],
"colors": {
"node-background": (239, 239, 239),
"background": (255,255,255)
}
}
An example file is given in examples/config.json
ACG emacs mode
There is an ACG emacs mode acg.el
in the emacs directory.
Look at the INSTALL.md file to see how to install it and where you can find the acg.el
file if automatically installed (in particular using opam).
It's main feature is to be loaded when editing an acg data file (with signatures and lexicons). It is automatically loaded for files with a .acg
extension
It basically contains compilation directives and next-error searching.
First load an acg file
then run
M-x compile
(orC-c C-c
) to call the compiler (acgc
)then run
M-x next-error
(or ``C-x
Syntax of signature and lexicons
(See the examples/tag.acg file for an example).
Signatures are defined by:
signature my_sig_name=
sig_entries
end
sig_entries
is a list of sig_entry
, separated with a ;
. A sig_entry
can be:
a type declaration as in
NP,S : type;
a type definition as in
o :type; string = o -> o;
Note that type constructors are
->
and=>
for the linear and intuitionistic arrows respectively.a constant declarations as in
foo:NP; bar,dummy:NP -> S; infix + : string -> string -> string; prefix - : bool -> bool; binder All : (e =>t) -> t; infix > : bool -> bool -> bool; (*This means implication*)
Note that
infix
andprefix
are keywords to introduce symbols (of length 1. This probably will change). Also notes that comments are surrounded by(*
and*)
.constant definitions as in
n = lambda n. bar n : NP -> S; infix + = lambda x y z.x(y z): string -> string -> string; prefix - = lambda p.not p:bool -> bool; everyone = lambda P. All x. (human x) > (P x) ;
Note the syntax for binders (
All
in the last example). Available construction for terms are:lambda x y z.t
for linear abstractionmbda x y z.t` for non-linear abstraction
u v
for application (equivalent to to
(t u) v`)t SYM u
ifSYM
is a infix symbol (lowest priority). It is equal to((SYM) t) u
whereSYM
is used as usual constant, with the priority of applicationSYM t
ifSYM
is a prefix symbol (highest priority)NDER x y z.t
if
BINDER` is a binder
About associativity and precedence of operators
Prefix operators have precedence over application, and application has precedence over infix operators. Relative precedence among infix operators can be defined.
When no associativity specification is set, the default is left associative.
When no precedece definition is given, the default is higher precedence over any infix operator defined so far.
When declaring or defining an infix operator with the keyword 'infix', the optional specification for the associativity and the relative precedence can be set.
A specification is given between square brackets. The syntax is as follows:
infix [specification] SYM …
(the remaining part of the declaration is the same as without the specification)
A specification is non-empty comma-separated list of:
an (optional) associativity specification, given by one of the keywords
Left
,Right
, orNonAssoc
. If not present, left associativity is set by default to infix operatorsan (optional) precedence declaration (if not present, the highest precedence over all the infix operators defined so far is given). It is defined as
< SYM
(whereSYM
is a symbol). It assigns to the operator being declared or defined the greates precedence below the precedence ofSYM
.
It is possible to use an infix symbol as a normal constant by surrounding it with left and right parenthesis, so that
t SYM u = (SYM) t u
See examples/infix-examples and examples/infix-examples-script for examples.
Lexicons
There are two ways to define a lexicon:
By using the keyword
lexicon
ornl_lexicon
as in : ``` lexicon my_lex_name(abstract_sig_name) : object_sig_name = lex_entries endor
nl_lexicon my_lex_name(abstract_sig_name) : object_sig_name = lex_entries end
With the `lexicon` keyword, `lambda` (resp. `->`) is interpreted as `lambda` (resp. `->`), whereas with `nl_lexicon`, `lambda` (resp. `->`) is interpreted as `Lambda` (resp. `=>`). I.e., everything is interpreted non linearly. It is useful when not interested in linear constraints in the object signature (as, for instance, in the context-free lambda grammars). `Lex_entries` is a list of `lex_entry`, separated with a `;`. A `lex_entry` can be of the following forms: * `abstract_atomic_type1, abstract_atomic_type2 := object_type;` * `abstract_const1, abstract_const2 := object_term;`
By lexicon composition as in:
lexicon my_new_lex = lex_2 << lex_1
Keywords
The keywords are signature
, lexicon
, nl_lexicon
, end
, type
, prefix
, infix
, binder
, lambda
, and Lambda
.
The reserved symbols are =
, <<
, ;
, :
, ,
, (
, )
, .
, ->
, =>
, and :=
.
Inside a signature or a lexicon, signature
, lexicon
and nl_lexicon
are not considered as keywords and can be used as identifier.
Other keywords can be used as identifier when escaped with \
(e.g., \end
).
Dependencies (14)
- easy-format
-
yojson
>= "1.6.0"
- cairo2
- conf-cairo
- conf-pkg-config
- conf-freetype
-
cmdliner
>= "1.0.0" & < "1.1.0"
-
mtime
>= "1.0.0" & < "2.0.0"
- logs
- fmt
- ANSITerminal
-
menhir
>= "20181113"
-
dune
>= "1.4"
-
ocaml
>= "4.05.0"
Dev Dependencies
None
Used by
None
Conflicts
None