|
|
PARSERS
CASL syntax is parsable using standard technology. Different parsers
have been developed, concurrently with the concrete syntax, which was
inconvenient for the parser developers but had the advantage to help
detecting ambiguities and inconsistencies in the syntax.
-
An LL(2)
parser generated by the C++ version of PCCTS.
It produces a tree in CSF format (Aterm like).
Mixfix parsing and annotations are not supported.
- An SDF
parser based on SDF and GLR parsing, generated from an SDF definition
of CASL.
It produces the abstract syntax tree in ATerm
format CasFix.
Mixfix parsing is not supported. The parsing of mixfix terms will be
based on Bjarke Wedemeijer's Master
Thesis .
- A Java
program built with JDK 1.1.x, Pizza and JavaCC. (Pizza comes with
the distribution of the parser)
The parser internally generates an abstract syntax
tree. This abstract syntax tree can be pretty printed using the Visitor
pattern. Two pretty printer are provided. One that generates ATerms
as output and one that generates concrete syntax.
- The HOL-CASL
parser based on the generic parser of Isabelle.
It supports parsing of full CASL, including
libraries, static analysis of basic specifications, mixfix parsing of
basic specifications The output is a sequence of A-Terms (one for each
LIB-ITEM), and a global environment (containing, for the basic specifications,
the signature and the fully-qualified axioms).
|