CASL.hs revision c6e131b1b79ccea24ebb92653a6d773b3c28194e
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettThe "CASL" folder contains the CASL (see
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly<http://www.cofi.info/CASL.html>) instance of "Logic.Logic". All the
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata for this instance is assembled in "CASL.Logic_CASL".
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachNote that the data structures are equipped with /holes/,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettrepresented by type variables, that can be instantiated later on.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachThis is needed by CASL extensions, which typically extend
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachabstract syntax, signatures and signature morphisms.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachFor CASL, these holes are just filled with the unit tpye ().
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettHowever, many pieces of code can be written for any type f
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstead of (), and thus be suitable also for CASL extensions.
78718c37b1a50086a27e0f031db4cf82bea934aeChristian MaederIt may be necessary to constrain these type variables in your
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachcode, e.g. for pretty printing prefix your types with 'Pretty f =>'.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach/Abstract Syntax/
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachThe abstract syntax of CASL basic specifications is provided in
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder"CASL.AS_Basic_CASL" as a Haskell algebraic datatype. It largely
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettfollows the CASL reference manual (see
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder<http://www.cofi.info/CASLDocuments.html>). Note that the abstract
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettsyntax of structured specifications is provided elsewhere: in the
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachfolder /Syntax/ (see "Syntax.ADoc").
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachThe CASL parser, written with <http://www.cs.uu.nl/people/daan/parsec.html>,
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachis contained in
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder"CASL.Parse_AS_Basic". Several modules provide parsers for individual
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillynon-terminals of the CASL grammar: "CASL.OpItem", "CASL.SortItem",
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach"CASL.Formula", "CASL.Quantification". The mixfix parser (which is
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maedercalled only during static analysis) is provided by
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett"CASL.MixfixParser". "CASL.LiteralFuns" deals with literals (for
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettnumbers, strings etc.). "CASL.SymbolParser" provides parsing of symbol
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettmaps (occurring in fitting maps or views). Finally,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly"CASL.RunMixfixParser" and "CASL.capa" provide command-line interfaces
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettto the parser.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Pretty printing (based on "Common.Lib.Pretty")
842ae753ab848a8508c4832ab64296b929167a97Christian Maederof CASL basic specifications is provided in
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder"CASL.Print_AS_Basic". Auxilary modules are "CASL.ShowMixfix" (for
842ae753ab848a8508c4832ab64296b929167a97Christian Maederprinting mixfix formulas and terms) and "CASL.Simplify" and
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder"CASL.SimplifySen" (for removing redundant type information).
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly"CASL.LaTeX_AS_Basic" and "CASL.LaTeX_CASL" provide LaTeX output.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettThe data structures for CASL signatures are contained in "CASL.Sign",
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederthose for signature morphisms in "CASL.Morphism". CASL sentences are
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyrepresented as abstract syntax trees of type
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly'CASL.AS_Basic_CASL.FORMULA'. In order to understand these data
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederstructures, you also should have a look at some of the "Common"
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maedermodules, providing data structures for identifiers ("Common.Id"), sets
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder("Common.Lib.Set"), maps ("Common.Lib.Map") and relations
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "CASL.MapSentence" implements translation of CASL sentences
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyalong signature morphisms.
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly/Static Analysis/
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyThe main module for static analysis of CASL basic specifications is
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder"CASL.StaticAna". The outcome basically is a signature and a set of
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maedersentences. "CASL.Overload", "CASL.Inject" and "CASL.Project" deal
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederwith subsorting.
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder"CASL.SymbolMapAnalysis" implements analysis of symbol maps,
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederyielding signature morphisms.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett"CASL.Amalgamability" implements amalgamability checks needed for
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblettarchitectural specifications.
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett"CASL.RunStaticAna" is a standalone command line interface for the
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblettstatic analysis.
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett/Consistency checking/
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett"CASL.CCC.OnePoint" checks for the existence of a one-point model.
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett"CASL.CCC.FreeTypes" checks whether a specification consists
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettof free datatypes and recursively defined, terminating functions.
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett"CASL.CCC.SignFuns" provides commonly needed analysis functions
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyfor signatures and morphisms.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly/Miscellaneous/
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett"CASL.Sublogic" provides data structures and analysis functions
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettfor the CASL sublogics.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett"CASL.Taxonomy" displays the subsorting graph of a CASL signature.
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett "CASL.Utils" contains utilities.
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett"CASL.Test" seems to be obsolete.
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maedermodule CASL where