| CoFI Tools | |
|
Aims and scope |
|
|
Members |
|
CASL Tool Set |
|
Related tools |
| Rewrite engines | |
| Provers | |
|
|
Papers |
|
|
How to join |
 |
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).
