2 Parser

Two different kinds of parsers have been proposed:

• Context-free parsing (for instance based on Lex and Yacc) produces from a text in plain format, an Abstract Syntax Tree on which semantic analysis is applied. This solution inherits both the simplicity and the usual restrictions of context-free parsing.
• Parsing is decomposed into two phases: context-free parsing produces a Pseudo-Abstract Syntax Tree where terms are terminals, then context sensitive parsing produces an Abstract Syntax Tree where syntactical well-formedness has been checked.

A first experiment has been made by encoding CASL basic specifications with subsorts in Isabelle. After context-free parsing, it is checked that there is just one correct sorting of the atomic formula up to a certain equivalence. For that an overload resolution algorithm is applied to get a fully qualified Abstract Syntax Tree.

A second possibility is to use ASF+SDF to produce a CASL parser.

A third solution is to desin a context-sensitive parser based on the experiment of CIGALE.