The CASL folder contains the CASL (see http://www.cofi.info/CASL.html) instance of Logic.Logic. All the data for this instance is assembled in CASL.Logic_CASL.

Note that the data structures are equipped with holes, represented by type variables, that can be instantiated later on. This is needed by CASL extensions, which typically extend abstract syntax, signatures and signature morphisms. For CASL, these holes are just filled with the unit tpye (). However, many pieces of code can be written for any type f instead of (), and thus be suitable also for CASL extensions. It may be necessary to constrain these type variables in your code, e.g. for pretty printing prefix your types with 'Pretty f =>'.

Abstract Syntax

The abstract syntax of CASL basic specifications is provided in CASL.AS_Basic_CASL as a Haskell algebraic datatype. It largely follows the CASL reference manual (see http://www.cofi.info/CASLDocuments.html). Note that the abstract syntax of structured specifications is provided elsewhere: in the folder Syntax (see Syntax.ADoc).

Parser

The CASL parser, written with http://www.cs.uu.nl/people/daan/parsec.html, is contained in CASL.Parse_AS_Basic. Several modules provide parsers for individual non-terminals of the CASL grammar: CASL.OpItem, CASL.SortItem, CASL.Formula, CASL.Quantification. The mixfix parser (which is called only during static analysis) is provided by CASL.MixfixParser. CASL.LiteralFuns deals with literals (for numbers, strings etc.). CASL.SymbolParser provides parsing of symbol maps (occurring in fitting maps or views). Finally, CASL.RunMixfixParser and "CASL.capa" provide command-line interfaces to the parser.

Printing

Pretty printing (based on Common.Lib.Pretty) of CASL basic specifications is provided in CASL.Print_AS_Basic. Auxilary modules are CASL.ShowMixfix (for printing mixfix formulas and terms) and CASL.Simplify and CASL.SimplifySen (for removing redundant type information).

CASL.LaTeX_AS_Basic and CASL.LaTeX_CASL provide LaTeX output.

Signatures

The data structures for CASL signatures are contained in CASL.Sign, those for signature morphisms in CASL.Morphism. CASL sentences are represented as abstract syntax trees of type FORMULA. In order to understand these data structures, you also should have a look at some of the Common modules, providing data structures for identifiers (Common.Id), sets (Common.Lib.Set), maps (Common.Lib.Map) and relations (Common.Lib.Rel).

CASL.MapSentence implements translation of CASL sentences along signature morphisms.

Static Analysis

The main module for static analysis of CASL basic specifications is CASL.StaticAna. The outcome basically is a signature and a set of sentences. CASL.Overload, CASL.Inject and CASL.Project deal with subsorting.

CASL.SymbolMapAnalysis implements analysis of symbol maps, yielding signature morphisms.

CASL.Amalgamability implements amalgamability checks needed for architectural specifications.

CASL.RunStaticAna is a standalone command line interface for the static analysis.

Consistency checking

CASL.CCC.OnePoint checks for the existence of a one-point model. CASL.CCC.FreeTypes checks whether a specification consists of free datatypes and recursively defined, terminating functions. CASL.CCC.SignFuns provides commonly needed analysis functions for signatures and morphisms.

Miscellaneous

CASL.Sublogic provides data structures and analysis functions for the CASL sublogics.

CASL.Taxonomy displays the subsorting graph of a CASL signature.

CASL.Utils contains utilities.

CASL.Test seems to be obsolete.