@@ -9,7 +9,7 @@ A list of related publications is available at the [ACG web page](http://calligr
## 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.
`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.
Run
```bash
...
...
@@ -187,6 +187,7 @@ end
* `SYM t` if `SYM` is a prefix symbol (highest priority)
* `BINDER x y z.t` if `BINDER` is a binder
### Lexicons
There are two ways to define a lexicon:
...
...
@@ -213,3 +214,13 @@ There are two ways to define a lexicon:
lexicon my_new_lex = lex_2 << lex_1
```
## 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").
## In state 122, spurious reduction of production sig_entry -> term_declaration
##
A type expression is expected after ":".
A type expression is expected after ':'.
term_alone: IDENT SEMICOLON
##
...
...
@@ -160,7 +160,7 @@ sig_entry_eoi: BINDER TYPE
## BINDER
##
An identidier (the name of the binder) is expected after the keyword "binder".
An identidier (the name of the binder) is expected after the keyword 'binder'.
sig_entry_eoi: IDENT COLON IDENT TYPE
##
...
...
@@ -180,7 +180,7 @@ sig_entry_eoi: IDENT COLON IDENT TYPE
## In state 122, spurious reduction of production sig_entry -> term_declaration
##
After a term declaration of the form "<term>: <type>", a semicolon ";" is expected.
After a term declaration of the form "<term>: <type>", a semicolon ';' is expected.
sig_entry_eoi: IDENT COLON SYMBOL
##
...
...
@@ -215,7 +215,7 @@ sig_entry_eoi: IDENT COMMA TYPE
## IDENT COMMA
##
After a term or type declaration of the form "<ident1>, <ident2>", a type declaration of the form ": type;" (where type is a keyword) or a typing judgment of the form ": <type>;" is expected.
After a term or type declaration of the form "<ident1>, <ident2>", a type declaration of the form ": type;" (with the keyword 'type') or a typing judgment of the form ": <type>;" is expected.
sig_entry_eoi: IDENT EQUAL IDENT ARROW IDENT COLON SYMBOL
## In state 7, spurious reduction of production atomic_type_or_term -> IDENT
##
A typing judgement in the form of ": <type>;" or a type definition with a colon and the "type" keyword in the form of ": type;" is expectedin a term or a type definition.
A typing judgement in the form of ": <type>;" or a type definition with a colon ':' and the 'type' keyword in the form of ": type;" is expected in a term or a type definition.
sig_entry_eoi: IDENT EQUAL SYMBOL SYMBOL COLON TYPE
##
...
...
@@ -325,7 +325,7 @@ sig_entry_eoi: IDENT EQUAL TYPE
## IDENT EQUAL
##
A definition in the form of "<term> : <type>;" or a type definition of the form "<type> : type;" is expected after a term or a type defintion, resp.
A definition in the form of "<term> : <type>;" or a type definition of the form "<type> : type;" (with the keyword 'type') is expected after a term or a type defintion, resp.
sig_entry_eoi: IDENT TYPE
##
...
...
@@ -341,7 +341,7 @@ sig_entry_eoi: IDENT TYPE
## IDENT
##
A comma "," or a colon ":" are expected in a type or term declaration. An equality symbol "=" is expected in a type or term definition.
A comma ',' or a colon ':' are expected in a type or term declaration. An equality symbol '=' is expected in a type or term definition.
sig_entry_eoi: INFIX SYMBOL COLON TYPE
##
...
...
@@ -380,7 +380,7 @@ sig_entry_eoi: PREFIX SYMBOL EQUAL IDENT COLON TYPE
## PREFIX SYMBOL EQUAL term COLON
##
A type is expected after the colon ":".
A type is expected after the colon ':'.
sig_entry_eoi: INFIX SYMBOL EQUAL IDENT SEMICOLON
##
...
...
@@ -436,7 +436,7 @@ sig_entry_eoi: PREFIX SYMBOL EQUAL TYPE
## PREFIX SYMBOL EQUAL
##
A typing judgment in the form "term : <type>;" is expected.
A typing judgment in the form "<term> : <type>;" is expected.
sig_entry_eoi: INFIX SYMBOL TYPE
##
...
...
@@ -494,7 +494,7 @@ sig_entry_eoi: TYPE
##
##
An identifier or a keyword ("infix", "prefix, or "binder") is expected.
An identifier or a keyword ('infix', 'prefix', or 'binder') is expected.