The CoFI-Tools Group Home Page
   
  CoFI Tools
   
Aims and scope
Members
CASL Tool Set
Related tools
  Rewrite engines
  Provers
Papers
How to join
E-mail

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).


Back to CoFI-TOOLS Home Page