POGODALLA Sylvain committed Oct 21, 2008 1 2 3 4 ************************************************************************** * * * ACG development toolkit * * *  5 * Copyright 2008-2021 INRIA *  POGODALLA Sylvain committed Oct 21, 2008 6 * *  POGODALLA Sylvain committed Nov 25, 2013 7 * More information on "http://acg.gforge.inria.fr/" *  POGODALLA Sylvain committed Oct 21, 2008 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:  POGODALLA Sylvain committed Oct 17, 2008 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  POGODALLA Sylvain committed Oct 03, 2018 32 definitions of signatures and lexicons. It basically checks whether  POGODALLA Sylvain committed Oct 17, 2008 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.  POGODALLA Sylvain committed Oct 17, 2008 36 37 38  Run  39  ./acgc --help  POGODALLA Sylvain committed Oct 17, 2008 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 committed Oct 17, 2008 57 58 Example files are given in the ./examples directory. Read the ./examples/README file  POGODALLA Sylvain committed Oct 17, 2008 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 committed Nov 30, 2015 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  POGODALLA Sylvain committed Mar 03, 2017 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 committed Nov 30, 2015 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 committed Nov 30, 2015 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 committed Nov 20, 2008 180 181 182 183 184 185 ******************** ** ACG emacs mode ** ******************** There is an ACG emacs mode (acg.el) in the emacs directory.  POGODALLA Sylvain committed Feb 09, 2014 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 committed Nov 20, 2008 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 committed Nov 20, 2008 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 committed Oct 24, 2008 204 205   POGODALLA Sylvain committed Oct 08, 2018 206 207 208 ************************ * Syntax of signatures * ************************  POGODALLA Sylvain committed Oct 24, 2008 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 committed Nov 30, 2015 238 length 1. This probably will change).  POGODALLA Sylvain committed Oct 24, 2008 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 committed Oct 24, 2008 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 committed Oct 24, 2008 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  POGODALLA Sylvain committed Oct 08, 2018 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  POGODALLA Sylvain committed Oct 15, 2018 311 312 See examples/infix-examples and examples/infix-examples-script for examples.  POGODALLA Sylvain committed Oct 08, 2018 313 314 315 *********************** * Syntax of lexicons * ***********************  POGODALLA Sylvain committed Oct 24, 2008 316   POGODALLA Sylvain committed May 29, 2018 317 318 There are two ways to define a lexicon: 1. By using the keyword lexicon or nl_lexicon as in :  POGODALLA Sylvain committed May 29, 2018 319   POGODALLA Sylvain committed May 29, 2018 320   POGODALLA Sylvain committed Oct 24, 2008 321 322 323 lexicon my_lex_name(abstract_sig_name) : object_sig_name = lex_entries end  POGODALLA Sylvain committed May 29, 2018 324 325  or  POGODALLA Sylvain committed Oct 24, 2008 326   POGODALLA Sylvain committed May 29, 2018 327 328 329 330 331  nl_lexicon my_lex_name(abstract_sig_name) : object_sig_name = lex_entries end   332   POGODALLA Sylvain committed Oct 24, 2008 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 committed May 29, 2018 336 337 338 339  With the lexicon keyword, lambda (resp. ->) is interpreted as lambda (resp. ->), whereas with nl_lexicon, lambda  POGODALLA Sylvain committed May 29, 2018 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 committed May 29, 2018 344 345 346 347 348  2. By lexicon composition as in:  lexicon my_new_lex = lex_2 << lex_1  POGODALLA Sylvain committed Oct 03, 2018 349 350 3. Keywords  POGODALLA Sylvain committed Oct 22, 2020 351 352 The keywords are signature, lexicon, nl_lexicon, end, type, prefix, infix, binder, lambda, and Lambda.  POGODALLA Sylvain committed Oct 03, 2018 353   POGODALLA Sylvain committed Oct 22, 2020 354 355 The reserved symbols are =, <<, ;, :, ,, (, ), ., ->, =>, and :=.  POGODALLA Sylvain committed Oct 03, 2018 356   POGODALLA Sylvain committed Oct 22, 2020 357 358 Inside a signature or a lexicon, signature, lexicon and nl_lexicon are not considered as keywords and can be used as  POGODALLA Sylvain committed Oct 03, 2018 359 360 identifier.  POGODALLA Sylvain committed Oct 22, 2020 361 362 Other keywords can be used as identifier when escaped with \ (e.g., \end).