README.md 6.66 KB
Newer Older
marton bognar's avatar
marton bognar committed
1
2
# AutBound: Code generator for abstract syntax trees

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
32
33
34
35
36
37
38
## Generated data structures and functions

### Data types

- For each declared sort in the specification, the corresponding data type will
  be created with the required parameters as constructor parameters. If a given
  constructor contains a binding parameter, and the generated code uses string
  variable representations, the binder will become the first constructor
  parameter in the generated type.
- A data type for the variables will also be created (`HNat` for the De Bruijn,
  `Variable` for the string representation) which has different constructors for
  each namespace declaration.

### Functions

- Mapping functions: mapping functions are created for each sort that has access
  to variables either by having a variable constructor, or a context instance of
  a sort that has access to variables (recursive case). Mapping functions take
  the following parameters: functions for each context instance sort with
  signature `[Variable] -> SORT -> SORT`, which get called if a variable of that
  sort is encountered, a variable list `c`, and the constructor of the given
  sort. An example signature for a `Term` sort with a variable constructor might
  be: `termmap :: ([Variable] -> Term -> Term) -> [Variable] -> Term -> Term`.
  The variable lists in both the map call and the parameter functions contain
  the active binders for the current context.
- Free variable functions: free variable functions are also created for sorts
  with variable access. These functions have the signature
  `[Variable] -> SORT -> [Variable]`. The functions takes the list of bound
  parameters and the term as parameters, and returns the list of free variables
  in the term.
- Substitution functions: substitution functions for sorts with variable access
  are generated for each context instance in the sort. They have the signature
  `sortCtxSortSubstitute :: Variable -> CTXSORT -> SORT -> SORT` where the free
  occurrences of the variable are replaced with the expression of type `CTXSORT`
  in the term of type `SORT`.

marton bognar's avatar
marton bognar committed
39
40
41
42
43
44
45
46
## Usage

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

```
autbound SOURCE_FILE OUTPUT_LANGUAGE VARIABLE_TYPE OUTPUT_NAME
```

47
48
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:
marton bognar's avatar
marton bognar committed
49
50
51
52
53
54
55
56
57
58
59
60
61

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

62
63
Language descriptions are simple text files. They consist of four different
parts:
marton bognar's avatar
marton bognar committed
64
65
66
67
68
69

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

marton bognar's avatar
marton bognar committed
70
None of these sections are mandatory, but their order is fixed.
marton bognar's avatar
marton bognar committed
71
72

For examples of language descriptions, see the `Specifications` directory.
marton bognar's avatar
marton bognar committed
73
74
75

### Import declarations

76
77
If your native code uses other modules, you can declare the import statements
with the following syntax at the top of your language description:
marton bognar's avatar
marton bognar committed
78
79
80
81
82

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

83
84
85
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.
marton bognar's avatar
marton bognar committed
86
87
88
89
90
91
92
93

Example:

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

94
95
The Haskell implementation imports `Data.List` by default, because some of the
generated functions use its functions.
marton bognar's avatar
marton bognar committed
96
97
98

### Namespace declarations

99
100
101
A namespace declaration consists of the namespace's name, a sort name, and
optionally additional comma separated sort names (the environment of the
namespace).
marton bognar's avatar
marton bognar committed
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

```
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]
```

128
129
130
131
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.
marton bognar's avatar
marton bognar committed
132
133
134

#### Context declarations

135
136
A sort can have multiple (or no) context attributes. These are declared after
the sort name with the following syntax:
marton bognar's avatar
marton bognar committed
137
138
139
140
141

```
CTXTYPE CTXINSTANCE NAMESPACENAME
```

142
143
144
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.
marton bognar's avatar
marton bognar committed
145
146
147
148
149
150
151
152
153
154
155
156

Example:
```
namespace TermVar: Term

sort Pat
    inh ictx TermVar
    syn sctx TermVar
```

#### Constructor declarations

157
158
159
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.
marton bognar's avatar
marton bognar committed
160
161
162
163
164
165
166
167

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

168
169
You can have zero or more parameters of each type, but the order of their
declaration must correspond to the order in this list.
marton bognar's avatar
marton bognar committed
170
171
172
173
174

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

175
176
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.
marton bognar's avatar
marton bognar committed
177
178
179
180
181

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

182
183
184
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.
marton bognar's avatar
marton bognar committed
185
186
187
188
189
190
191
192
193
194
195
196
197
198

Example:

```
namespace TermVar: Term

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

### Native code

199
200
201
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.
marton bognar's avatar
marton bognar committed
202

203
204
For example, if we want to generate a Haskell module, we can put the following
in the language specification:
marton bognar's avatar
marton bognar committed
205
206
207
208
209
210
211
212
213
214
215
216

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

NativeCode

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