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

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
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 (possibly with the `.opt` extension, see the [INSTALL.md](INSTALL.md) file: `acgc` and `acg` (or, instead, their native counterparts: `acgc.opt` and `acg.opt`).
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 12 13


## acgc

`acgc` is a "compiler" of ACG source code, i.e. files containing definitions of signarures 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.

14 15 16 17 18
Run	
```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 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

If the `-nsvg` option is not set when running `acg.opt` or `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:
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 128 129 130 131
$ 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)

## ACG emacs mode 

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 138 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

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
2. then run `M-x compile` (or `C-c C-c`) to call the compiler (`acgc` or `acgc.opt`)
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 185 186 187 188 189 190 191

* 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
  *	`t u v` for application `(equivalent to to `(t u) v`)
  * `t SYM u` if `SYM` is a infix symbol (lowest priority)
  * `SYM t` if `SYM` is a prefix symbol (highest priority)
  *	`BINDER x y z.t` if `BINDER` is a binder

### Lexicons

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
192 193
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
194 195 196 197 198 199 200 201 202 203 204
   	```
	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
205
	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
206 207 208 209

	`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
210

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
211
2. By lexicon composition as in:
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
212 213 214
   ```
   lexicon my_new_lex = lex_2 << lex_1
   ```
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
215