README 10.5 KB
Newer Older
1 2 3 4
**************************************************************************
*                                                                        *
*                 ACG development toolkit                                *
*                                                                        *
5
*                  Copyright 2008-2021 INRIA                             *
6
*                                                                        *
7
*  More information on "http://acg.gforge.inria.fr/"                     *
8 9 10 11 12 13 14 15 16 17 18 19
*  License: CeCILL, see the LICENSE file or "http://www.cecill.info"     *
*  Authors: see the AUTHORS file                                         *
*                                                                        *
*                                                                        *
*                                                                        *
*                                                                        *
*  $Rev::                              $:  Revision of last commit       *
*  $Author::                           $:  Author of last commit         *
*  $Date::                             $:  Date of last commit           *
*                                                                        *
**************************************************************************

20
This distribution provides two executables:
21 22 23 24 25 26 27 28 29 30 31

	acgc
and
	acg


************
*** acgc ***
************

acgc is a "compiler" of ACG source code, i.e. files containing
32
definitions of signatures and lexicons. It basically checks whether
33
they are correctly written (syntactically and wrt types and constant
34 35
typing) and outputs a .acgo object file. An interactive mode is
available to parse terms according to signatures.
36 37 38

Run

39
	./acgc --help
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56

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;


POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
57 58
Example files are given in the ./examples directory. Read the
./examples/README file
59

60 61 62 63 64 65 66 67 68 69 70 71 72 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 104 105

***************
* 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.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" is a term of type "NP ->S" 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.

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
106 107 108 109 110 111 112 113 114
Type CTRL-D to exit from the program, or type:

# exit;


**************
* SVG output *
**************

115
If the --nsvg option is not set when running acg, a file
116 117
"realize.svg" (default name) is generated in the current directory
whenever a 'realize' command is invoked. In order to set another file
118
name, use the option --svg other_filename.
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154

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.

4 rendering engines are available 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 characters

The association between the name of a signature and a rendering engine
is declared in a configuration file that can be loaded through the
155
'--realize' option and that looks like:
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178

$ 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
179

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
180 181 182 183 184 185
********************
** ACG emacs mode **
********************

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

186 187 188
Look at the INSTALL file to see how to install it and where you can
find the acg.el file if automatically installed (in particular using
opam).
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
189 190 191 192 193 194 195 196 197 198

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

199
2. then run "M-x compile" (or C-cC-c) to call the compiler (acgc)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
200 201 202 203

3. then run "M-x next-error" (or C-x`) to search for the next error
(if any) and highlights it

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
204 205


206 207 208
************************
* Syntax of signatures *
************************
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237

(see the examples/tag.acg file for an example)

Signatures are defined by:

signature my_sig_name=
	sig_entries
end

Sig_entries always ends with a ; and can be:
+ type declaration as in
	NP,S : type;

+ type definition as in
	o :type;
	string = o -> o;

Note that type constructors are -> and => for the linear and
intuitionnistic arrow respectively.

+ 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 and prefix are keywords to introduce symbols (of
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
238
length 1. This probably will change).
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
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 abstraction

	Lambda x y z.t
for non-linear abstraction

	t u v
256
for application (equal to (t u) v)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
257 258

	t SYM u
259 260 261 262 263 264

if SYM is a infix symbol (lowest priority). It is equal to

        ((SYM) t) u

where SYM is used as a usual constant, with the priority of application.
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
265 266 267 268 269 270 271

	SYM t
if SYM is a prefic symbol (highest priority)

	BINDER x y z.t
if BINDER is a binder

272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
+ 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.

306 307 308 309 310
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

311 312
See examples/infix-examples and examples/infix-examples-script for examples.

313 314 315
***********************
* Syntax of  lexicons *
***********************
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
316

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
317 318
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
319

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
320
```
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
321 322 323
lexicon my_lex_name(abstract_sig_name) : object_sig_name =
	lex_entries
end
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
324 325
```
or
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
326

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
327 328 329 330 331
```
nl_lexicon my_lex_name(abstract_sig_name) : object_sig_name =
	lex_entries
end
```
332

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
333 334 335
Lex_entries always ends with a ; and have the following form:
	abstract_atomic_type1, abstract_atomic_type2 := object_type;
	abstract_const1, abstract_const2 := object_term;
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
336 337 338 339


With the `lexicon` keyword, `lambda` (resp. `->`) is interpreted as
`lambda` (resp. `->`), whereas with `nl_lexicon`, `lambda`
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
340 341 342 343
(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
344 345 346 347 348

2. By lexicon composition as in:
```
lexicon my_new_lex = lex_2 << lex_1

349 350
3. Keywords

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
351 352
The keywords are `signature`, `lexicon`, `nl_lexicon`, `end`, `type`,
`prefix`, `infix`, `binder`, `lambda`, and `Lambda`.
353
	
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
354 355
The reserved symbols are `=`, `<<`, `;`, `:`, `,`, `(`, `)`, `.`,
`->`, `=>`, and `:=`.
356
	
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
357 358
Inside a signature or a lexicon, `signature`, `lexicon` and
`nl_lexicon` are not considered as keywords and can be used as
359 360
identifier.
	
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
361 362
Other keywords can be used as identifier when escaped with `\` (e.g.,
`\end`).