CASL.hs

{- |
Module      :  $Id$
Description :  basics of the common algebraic specification language
Copyright   :  (c) Christian Maeder and DFKI Lab Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable (except CASL.Logic_CASL and CASL.QuickCheck)

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
'CASL.AS_Basic_CASL.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.

-}

module CASL where