7.2 Type-Checking

The AS type-checker has been written in Typol. It produces as result, apart error messages and warnings, two values that are attached as annotations at the root of the type-checked specification. The first one, called as_env, contains the complete environment produced by the type-checker and is used as input by the code generators. The second, called includes, contains the list of all declarations, included those that are imported in case of the current specification is an extension of a previous one. These two annotations will be saved in a file to allow separate compilation when the current specification must be extended.

The environment contains three distinct parts. All of them contain binary trees. The first one is used for formalisms, the second for phyla, the third for operators. This binary trees are part of a generic package designed for handling environment, with implementations as lists, sorted lists, binary trees and colored binary trees. In the present case, the binary trees implementation gives the best time performances (the overhead used by the colored binary trees kills the advantage of these balanced trees even for large specifications as the C abstract syntax specification).

The environment contains some paths to allow the generation of complete error messages with hyper-text links. These paths are erased in the saved version of the environment as there are of no use in the code generation process.

Two fix points are calculated. The first one checks that the specification is effective (i.e. for each phylum it is possible to construct a ground term), the second calculates the sets of operators that belong to each phylum, taking type inclusion into account. Most of the time taken by the type-checker is spent when returning (i.e. constructing the effective resulting value) from this last procedure.

The following example will be used in the two next sections to illustrate code generation.

abstract syntax of L is
   
id : string -> Phy;
f : Phy -> Phy;
   
end L;