README 10.6 KB
Newer Older
1 2 3 4
**************************************************************************
*                                                                        *
*                 ACG development toolkit                                *
*                                                                        *
5
*                  Copyright 2008-2018 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 21 22 23 24 25 26 27 28 29 30 31 32
This distribution provides two executables (possibly with the .opt
extension, see the INSTALL file):

	acgc
and
	acg


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

acgc is a "compiler" of ACG source code, i.e. files containing
33
definitions of signatures and lexicons. It basically checks whether
34
they are correctly written (syntactically and wrt types and constant
35 36
typing) and outputs a .acgo object file. An interactive mode is
available to parse terms according to signatures.
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57

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;


58 59
Example files are given in the ./examples directory. Read the
./examples/README file
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 106

***************
* 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.

107 108 109 110 111 112 113 114 115 116
Type CTRL-D to exit from the program, or type:

# exit;


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

If the -nsvg option is not set when running acg.opt/acg, a file
117 118 119
"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.
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 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179

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
'-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
180

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

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

187 188 189
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
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205

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

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
206 207


208 209 210
************************
* Syntax of signatures *
************************
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
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 238 239

(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
240
length 1. This probably will change).
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
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
258
for application (equal to (t u) v)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
259 260

	t SYM u
261 262 263 264 265 266

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
267 268 269 270 271 272 273

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

	BINDER x y z.t
if BINDER is a binder

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 306 307
+ 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.

308 309 310 311 312
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

313 314
See examples/infix-examples and examples/infix-examples-script for examples.

315 316 317
***********************
* Syntax of  lexicons *
***********************
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
318

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
319 320
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
321

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

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

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
335 336 337
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
338 339 340 341


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

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

351 352 353 354 355 356 357 358 359 360 361 362 363 364
3. 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").