README.md 4.68 KB
Newer Older
marton bognar's avatar
marton bognar committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
# AutBound: Code generator for abstract syntax trees

## Usage

The executable can be used from the command line with the following arguments:

```
autbound SOURCE_FILE OUTPUT_LANGUAGE VARIABLE_TYPE OUTPUT_NAME
```

For example, if we want to generate a Haskell module called `FCoBase` from the FCo specification, using string-based variables, we would issue the command:

```
autbound "Specifications/FCo.txt" Haskell String FCoBase
```

This will generate the file `FCoBase.hs` in the current directory.

The following options are currently available:
- `OUTPUT_LANGUAGE`: `Haskell`, `OCaml`
- `VARIABLE_TYPE`: `DeBruijn`, `String`

## Language descriptions

Language descriptions are simple text files. They consist of four different parts:

- Import declarations
- Namespace declarations
- Sort declarations
- Native code

marton bognar's avatar
marton bognar committed
32
None of these sections are mandatory, but their order is fixed.
marton bognar's avatar
marton bognar committed
33
34

For examples of language descriptions, see the `Specifications` directory.
marton bognar's avatar
marton bognar committed
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
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
106
107
108
109
110
111
112
113
114
115
116
117
118
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
155
156
157

### Import declarations

If your native code uses other modules, you can declare the import statements with the following syntax at the top of your language description:

```
import (MODULE_NAME) [ ( ENTITY [ ENTITY]* ) ]
```

Where the first parentheses contain the module name, and the optional second pair contains the specifically imported entities from the given module (separated by spaces). One line contains one module import.

Example:

```
import (Data.Map)
import (Data.List) (genericLength genericTake)
```

The Haskell implementation imports `Data.List` by default, because some of the generated functions use its functions.

### Namespace declarations

A namespace declaration consists of the namespace's name, a sort name, and optionally additional comma separated sort names (the environment of the namespace).

```
namespace NAMESPACENAME: SORTNAME[, SORTNAME]*
```

Example:
```
namespace TermVar: Term, Type
namespace TypeVar: Type
```

### Sort declarations

Sort declarations have the following structure:

- name, rewrite declaration
- context declarations
- constructor declarations
    + attribute assignments

#### Name, rewrite

```
sort SORTNAME [rewrite]
```

Declares a new sort. The optional rewrite keyword specifies whether the result of substitution functions for the given sort should be passed to an external rewrite function. The rewrite functions need to have the name `rewriteSORTNAME` and either be defined in the native code section or imported.

#### Context declarations

A sort can have multiple (or no) context attributes. These are declared after the sort name with the following syntax:

```
CTXTYPE CTXINSTANCE NAMESPACENAME
```

Where `CTXTYPE` can be `inh` for inherited and `syn` for synthesized contexts. `CTXINSTANCE` is the context instance's name, and `NAMESPACENAME` is the name of the namespace of the contained variables.

Example:
```
namespace TermVar: Term

sort Pat
    inh ictx TermVar
    syn sctx TermVar
```

#### Constructor declarations

Sorts can contain a number of constructor declarations. These follow the context declarations. A constructor declaration consists of a constructor name, parameter declarations, and context attribute assignments.

The parameter declarations can be of the following forms:
- List of a sort
- Foldable sort
- Regular sort
- Native type
- Binder parameter of a namespace

You can have zero or more parameters of each type, but the order of their declaration must correspond to the order in this list.

```
| CTORNAME [ (PARAM: [SORTNAME]) ]* [ (PARAM: FOLDNAME SORTNAME) ]* [ (PARAM: SORTNAME) ]* [ {NATIVETYPE} ]* [ [BINDPARAM: NAMESPACENAME] ]
```

The final part of the constructor declaration is the context attribute assignments. Zero or more of them can follow the parameter list in new lines.

```
    PARAM.CTXINSTANCE = PARAM.CTXINSTANCE[, PARAM]
```

Where `PARAM` can be one of the constructor parameters or `lhs` which represents the constructor's context. You can optionally also append a parameter to the assigned context instance.

Example:

```
namespace TermVar: Term

sort Term
    inh ctx TermVar
    | TmAbs (x: Term) (t: Type) [z: TermVar]
        x.ctx = lhs.ctx, z
```

### Native code

After the sort declarations you can include code written in the target language. This needs to be preceded by the `NativeCode` keyword. Everything after this keyword will be copied verbatim to the output module.

For example, if we want to generate a Haskell module, we can put the following in the language specification:

```
[import declarations...]
[namespace declarations...]
[sort declarations...]

NativeCode

rewriteCoercion :: Coercion -> Coercion
rewriteCoercion (CoTypeVar ty)    = rewriteTypeToCoercion ty
rewriteCoercion (CoArrow co1 co2) = CoArrow (rewriteCoercion co1) (rewriteCoercion co2)
```