README.md 9.79 KB
Newer Older
1 2
# ACGtk: an ACG development toolkit

3
**ACGtk** is a software package ([2008-2017 INRIA](http://www.inria.fr)©) for the development of abstract categorial grammars. This distribution provides two executables file: `acgc` and `acg`.
4

5
It is distributed with the *CeCILL* license (see the [LICENSE](LICENSE.en) file or http://www.cecill.info). Contributors are listed in the [AUTHORS.md](AUTHORS.md) file.
6 7

A list of related publications is available at the [ACG web page](http://calligramme.loria.fr/acg).
8 9 10 11


## acgc

12
`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.
13

14
Run
15 16 17 18
```bash
./acgc -help
```
to get help.
19 20 21 22

## acg

`acg` is an interpreter of command meant to be useful when using ACGs. To get a list of command, run
23 24
```bash
./acg
25
```
26
then, on the prompt, type
27 28 29 30
```
	help;
```

31
Example files are given in the [examples directory](examples). Read the [README.md file](examples/README.md).
32 33 34 35

### 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:
36
```bash
37 38 39 40 41
$ 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 :
42
```bash
43 44 45
$ acg
```
will open a prompt in which you can type:
46
```ocaml
47 48 49
# 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:
50
```ocaml
51 52 53 54 55
# 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:
56
```ocaml
57 58 59 60 61
# 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:
62
```ocaml
63 64 65 66 67
# 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:
68
```ocaml
69 70 71
# exit;
```

72
### SVG output
73

74
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`.
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103

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:
104
```bash
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
$ 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](examples/config.json)

128
## ACG emacs mode
129 130 131

There is an ACG emacs mode `acg.el` in the [emacs](emacs) directory.

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
132
Look at the [INSTALL.md](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).
133 134 135 136 137

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.
1. First load an acg file
138
2. then run `M-x compile` (or `C-c C-c`) to call the compiler (`acgc`)
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
3. then run `M-x next-error` (or ``C-x` `) to search for the next error (if any) and highlights it

## Syntax of signature and lexicons

(See the [examples/tag.acg](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*)
  ```
173
  Note that `infix` and `prefix` are keywords to introduce symbols (of **length 1**. This probably will change). Also notes that comments are surrounded by `(*` and `*)`.
174 175 176 177 178 179 180 181 182 183 184

* 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 abstraction
  *	`Lambda x y z.t` for non-linear abstraction
185 186
  *	`t u v` for application (equivalent to to `(t u) v`)
  * `t SYM u` if `SYM` is a infix symbol (lowest priority). It is equal to `((SYM) t) u` where `SYM` is used as usual constant, with the priority of application
187 188 189
  * `SYM t` if `SYM` is a prefix symbol (highest priority)
  *	`BINDER x y z.t` if `BINDER` is a binder

190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
* 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`, or `NonAssoc`. If not present, left associativity is set by default to infix operators

  + an (optional) precedence declaration (if not present, the highest precedence over all the infix operators defined so far is given). It is defined as `< SYM` (where `SYM` is a symbol). It assigns to the operator being declared or defined the greates precedence *below* the precedence of `SYM`.

212
  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`
213

214
  See [examples/infix-examples](examples/infix-examples) and [examples/infix-examples-script](examples/infix-examples) for examples.
215

216 217
### Lexicons

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
218 219
There are two ways to define a lexicon:
1. By using the keyword `lexicon` or `nl_lexicon` as in :
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
220 221 222 223 224 225 226 227 228 229 230
   	```
	lexicon my_lex_name(abstract_sig_name) : object_sig_name =
		lex_entries
	end
	```
	or
	```
	nl_lexicon my_lex_name(abstract_sig_name) : object_sig_name =
		lex_entries
	end
	```
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
231
	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).
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
232 233 234 235

	`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;`
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
236

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
237
2. By lexicon composition as in:
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
238 239 240
   ```
   lexicon my_new_lex = lex_2 << lex_1
   ```
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
241

242 243 244
## Keywords

	The keywords are "signature, "lexicon, "nl_lexicon", "end", "type", "prefix", "infix", "binder", "lambda", and "Lambda".
245

246
	The reserved symbols are '=', '<<', ';', ':', ',', '('), ')', '.', '->', '=>', and ':='.
247

248 249
	Inside a signature or a lexicon, "signature", "lexicon" and "nl_lexicon" are not considered as keywords and can be used as identifier.

250
	Other keywords can be used as identifier when escaped with '\' (e.g., "\end").