1.1. Modules

DynSem specifications can be split over multiple files. Every file constituted a module. Every module begins with a module declaration and optionally provides subsections:

module trans/semantics/mymodule

IMPORTS*

SIGNATURE*

RULES*

The name of the module must consist of the path to its file relative to the root of the project, followed by the file name without the .ds extension. The example above declares the module mymodule in the file mymodule.ds which is located at trans/semantics/ relative to the project root.

1.1.1. Importing modules

Modules can import other modules using one or more imports sections. The module below imports modules A, B and C, and shows that multiple modules can be imported at once and that an imports section can appear anywhere in the module:

module trans/semantics/mymodule

imports
  trans/semantics/A
  trans/semantics/B

rules
  ...

imports
  trans/semantics/C

The semantics of imports are those of the C include directive, i.e. imports are includes and they are transitive. All signatures and rules defined in (transitively) imported modules are visibile for the importing module. Cyclic imports are automatically resolved.

1.1.2. Signatures

A module may have any number of signature sections. Signatures are used to declare sorts, constructors, components and arrows. See Term signatures for defining sorts and constructors, and Signatures of arrows, components and meta-functions for defining components, arrows and other operations.

1.1.3. Rules

Multiple rules sections are permitted in a DynSem module. Each rule section declares arbitrarily many reduction rules. See Reduction rules about defining reduction rules and the constructs supported.