Commit b2c7443b authored by marton bognar's avatar marton bognar
Browse files

Extend the readme

parent 2cd1e262
......@@ -29,6 +29,129 @@ Language descriptions are simple text files. They consist of four different part
- Sort declarations
- Native code
None of these sections are mandatory.
None of these sections are mandatory, but their order is fixed.
For examples of language descriptions, see the `Specifications` directory.
### 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.
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 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:
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.
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.
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.
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.
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...]
rewriteCoercion :: Coercion -> Coercion
rewriteCoercion (CoTypeVar ty) = rewriteTypeToCoercion ty
rewriteCoercion (CoArrow co1 co2) = CoArrow (rewriteCoercion co1) (rewriteCoercion co2)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment