Go backward to 1 Introduction
Go up to Top
Go forward to 3 Comments and special purpose annotations

2 Annotations to be handled uniformly

There are annotations that should be handled uniformly by all CASL parsers because the information is needed for further parsing stages, e.g. mixfix parsing.

[1.] Parsing annotations [CoF98, Sec. C.5.2.3] are needed for the mixfix parsing stage.

I assume that these annotations include the annotations prec, left assoc, right assoc, and brackets proposed in [RM99].

There are annotations that should be handled uniformly by all parsers which support them. These include:

[2.] Label annotations [CoF98, Sec. C.5.2.1]
[3.] Display annotations [CoF98, Sec. C.5.2.2]
[4.] Semantic annotations [CoF98, Sec. C.5.2.4], [RM99] proposes cons and def

These annotations may or may not be exploited by the particular CASL tool using the AST. E.g. a pretty printer will exploit display annotations, a static type checker depends on none of these annotations, and a theorem prover might not use label or display annotations, but exploits semantic annotations.¹

Since the annotations mentioned in this section do not have a uniform syntax, each CASL lexer/parser has to understand them explicitly in order to determine the end of an annotation. This holds true even if the parser chooses to ignore the annotation. This implies that CASL lexers/parsers have to be changed when a new such standard annotation is added to CASL.

For a parser created by flex/bison to be able to handle such annotations it is necessary in particular to extend the grammar describing the concrete syntax of CASL such that the annotations occur in the grammar in the places in which the annotation is allowed in the CASL text.

As an example consider the definition of SPEC in [CoF98, p. C.5], the fifth alternative of which reads

SPEC            ::= ... | SPEC then SPEC then...then SPEC | ...

Writing this out in a left-recursive manner using an auxiliary non-terminal THEN-SPEC and providing rules for the optional semantic annotations THEN-ANNOTATION the part of the grammar could look similar to the following.²

SPEC            ::= ... | THEN-SPEC | ...
THEN-SPEC       ::= SPEC then THEN-ANNOTATION/ SPEC
                  | THEN-SPEC then THEN-ANNOTATION/ SPEC
THEN-ANNOTATION ::= "%cons" | "%def"

Because all CASL parsers have to be changed whenever such annotations are added to CASL or their syntax is changed, annotations defined and used by one specific tool should not fall under this category. This note proposes to handle these special purpose annotations similarly to the way comments are handled (cf. the following section).

CoFI Note: T-7 -- Version: 1 -- 28 April 1999.
Comments to schairer@dfki.de