POGODALLA Sylvain committed Nov 15, 2017 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.  POGODALLA Sylvain committed Nov 15, 2017 4   POGODALLA Sylvain committed Nov 15, 2017 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.  POGODALLA Sylvain committed Nov 15, 2017 6 7  A list of related publications is available at the [ACG web page](http://calligramme.loria.fr/acg).  POGODALLA Sylvain committed Nov 15, 2017 8 9 10 11  ## acgc  POGODALLA Sylvain committed Oct 03, 2018 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.  POGODALLA Sylvain committed Nov 15, 2017 13   14 Run  POGODALLA Sylvain committed Nov 15, 2017 15 16 17 18 bash ./acgc -help  to get help.  POGODALLA Sylvain committed Nov 15, 2017 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  POGODALLA Sylvain committed Nov 15, 2017 23 24 bash ./acg  POGODALLA Sylvain committed Nov 15, 2017 25   POGODALLA Sylvain committed Nov 15, 2017 26 then, on the prompt, type  POGODALLA Sylvain committed Nov 15, 2017 27 28 29 30  help;   POGODALLA Sylvain committed Nov 15, 2017 31 Example files are given in the [examples directory](examples). Read the [README.md file](examples/README.md).  POGODALLA Sylvain committed Nov 15, 2017 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:  POGODALLA Sylvain committed Nov 15, 2017 36 bash  POGODALLA Sylvain committed Nov 15, 2017 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 :  POGODALLA Sylvain committed Nov 15, 2017 42 bash  POGODALLA Sylvain committed Nov 15, 2017 43 44 45 $ acg  will open a prompt in which you can type:  POGODALLA Sylvain committed Nov 15, 2017 46 ocaml  POGODALLA Sylvain committed Nov 15, 2017 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:  POGODALLA Sylvain committed Nov 15, 2017 50 ocaml  POGODALLA Sylvain committed Nov 15, 2017 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:  POGODALLA Sylvain committed Nov 15, 2017 56 ocaml  POGODALLA Sylvain committed Nov 15, 2017 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:  POGODALLA Sylvain committed Nov 15, 2017 62 ocaml  POGODALLA Sylvain committed Nov 15, 2017 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:  POGODALLA Sylvain committed Nov 15, 2017 68 ocaml  POGODALLA Sylvain committed Nov 15, 2017 69 70 71 # exit;   POGODALLA Sylvain committed Nov 15, 2017 72 ### SVG output  POGODALLA Sylvain committed Nov 15, 2017 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.  POGODALLA Sylvain committed Nov 15, 2017 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:  POGODALLA Sylvain committed Nov 15, 2017 104 bash  POGODALLA Sylvain committed Nov 15, 2017 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  POGODALLA Sylvain committed Nov 15, 2017 129 130 131  There is an ACG emacs mode acg.el in the [emacs](emacs) directory.  POGODALLA Sylvain committed Nov 23, 2017 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).  POGODALLA Sylvain committed Nov 15, 2017 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)  POGODALLA Sylvain committed Nov 15, 2017 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*)   POGODALLA Sylvain committed Nov 15, 2017 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 *).  POGODALLA Sylvain committed Nov 15, 2017 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  POGODALLA Sylvain committed Nov 15, 2017 187 188 189  * SYM t if SYM is a prefix symbol (highest priority) * BINDER x y z.t if BINDER is a binder  POGODALLA Sylvain committed Oct 08, 2018 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   POGODALLA Sylvain committed Oct 15, 2018 214  See [examples/infix-examples](examples/infix-examples) and [examples/infix-examples-script](examples/infix-examples) for examples.  POGODALLA Sylvain committed Oct 03, 2018 215   POGODALLA Sylvain committed Nov 15, 2017 216 217 ### Lexicons  POGODALLA Sylvain committed May 29, 2018 218 219 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 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 committed May 29, 2018 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 committed May 29, 2018 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 committed May 29, 2018 236   POGODALLA Sylvain committed May 29, 2018 237 2. By lexicon composition as in:  POGODALLA Sylvain committed May 29, 2018 238 239 240   lexicon my_new_lex = lex_2 << lex_1   POGODALLA Sylvain committed May 29, 2018 241   POGODALLA Sylvain committed Oct 03, 2018 242 243 244 ## Keywords The keywords are "signature, "lexicon, "nl_lexicon", "end", "type", "prefix", "infix", "binder", "lambda", and "Lambda".  245   POGODALLA Sylvain committed Oct 03, 2018 246  The reserved symbols are '=', '<<', ';', ':', ',', '('), ')', '.', '->', '=>', and ':='.  247   POGODALLA Sylvain committed Oct 03, 2018 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").`