ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\documentclass{article}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\parindent 0pt
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\begin{document}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\title{CASL basic items}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\author{C. Maeder}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\section{Preliminaries}
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maedersee the documentation for HetCATS and Common
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\section{Compiling the CASL parser}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{cd HetCATS/CASL} and call \texttt{./ghc-call} (a script that contains
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederall necessary ghc options and parameters). An alternative is to call
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{gmake capa} in the top directory.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederThis creates a binary called \texttt{capa} that can parse (and pretty
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederprint) ``Basic Specification with Subsorts'' of the CASL Summary
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederversion 1.0.1 \\ (www.brics.dk/Projects/CoFI/Documents/CASL/Summary/).
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian MaederStructured specifications (see \texttt{Static/hetpa.hs}) must be parsed by the
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maederheterogenous parser.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederNote: if module \texttt{AS\_Basic\_CASL} can not be found, then
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{AS\_Basic\_CASL.hs} was not ``drifted'' (i.e., derived from
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{AS\_Basic\_CASL.der.hs}).
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederAlso \texttt{Common/AS\_Annotation.hs} must have been drifted.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\section{Testing}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederA test call might be:
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederThe binary \texttt{capa} is also used to test various parsers. Test cases are
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maedergiven as \texttt{*.casl} files in the \texttt{test} subdirectory. Calling
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\texttt{./runcheck.sh ../capa} performs many tests and compares the results
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maederwith corresponding \texttt{*.output} files.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederAlternatively a test can be run using \texttt{runhugs}. For this the
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederfile \texttt{capa.lhs} is executable and the test can be run
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{Wrong*.casl} files contain wrong CASL code and should produce
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedererror messages. Apart from extra tests, correct (\texttt{Bla.casl})
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederand wrong files (\texttt{WrongBla.casl}) are tested. If a \texttt{diff}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederwith the expected output fails, then also the number of
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder``\texttt{error}'' occurrences (in the produced output) is counted. For a
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedersuccessful comparison a ``\texttt{passed}'' is emitted.
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian MaederCalling ``\texttt{./runcheck.sh ../capa set}'' will update the
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\texttt{*.output} files (and a subsequent \texttt{./runcheck.sh ../capa} should
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederAlternatively, all checks can be preformed by \texttt{make check}. Output
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maederfiles will be overwritten by \texttt{make output}. With \texttt{cvs up} or
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{cvs diff} changes can be compared to checked-in versions of the output
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\section{Source files in \texttt{HetCATS/CASL}}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\begin{description}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[AS\_Basic\_CASL.der.hs] defines the abstract syntax tree for CASL
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\item[Formula.hs] parsers \texttt{term} and \texttt{formula}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[LiteralFuns.hs] used by \texttt{Print\_AS\_Basic.hs}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[Logic\_CASL.hs] contains the instance for the class \texttt{Logic.Logic}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[MixfixParser.hs] uses precedence and associativity to resolve
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder mixfix terms (and formulae). Also \%list, \%string, \%number and
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder \%floating annotations are resolved
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[Morphism.hs] symbol and morphism stuff for \texttt{Logic}
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\item[OpItem.hs] parsers \texttt{opItem} and \texttt{predItem}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[Parse\_AS\_Basic.hs] supplies the top-level parsers \texttt{basicSpec,
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder basicItems, dotFormulae} and \texttt{sigItems}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[Print\_AS\_Basic.hs] pretty prints data types of
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder \texttt{AS\_Basic\_CASL.hs}
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\item[RunMixfixParser.hs] is a driver to test the mixfix
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[RunStaticAna.hs] is an additional driver to test the static
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder analysis (call \texttt{capa analysis < file})
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[Sign.hs] (unused) was the analysed abstract syntax
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\item[SortItem.hs] parsers \texttt{sortItem} and \texttt{datatype} (requires
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder \texttt{Formula.hs} for subsort definitions)
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[Static.hs] (unused) implements the static analysis
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[StaticAna.hs] implements a simple static analysis
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[Sublogic.hs] used by \texttt{Logic\_CASL.hs}
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[Sublogics.hs] older version
9a6861ccf8fce8d034ef0810a09e7abdf8d2fc94Christian Maeder\item[SymbolAnalysis] (unused)
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[SymbolParser.hs] parses symbols and symbol maps that are not needed for
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder basic specs but for heterogeneous structured specifications
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder (\texttt{Logic\_CASL.hs}). These parsers do not deal with annotations,
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\item[capa.lhs] is the main module that simply lists the test parsers
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder and is executable for hugs
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\end{description}
c38f6bd7e9fcd7bec8896d7d6e393dbf61c93013Christian Maeder\section{Remarks}
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederThe \texttt{MixfixParser} only operates on \texttt{FORMULA} and
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\texttt{TERM} from \texttt{AS\_Basic\_CASL} and not on
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maedertypes in \texttt{Sign.hs}.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian MaederType checking (considering subtypes and overloading) of terms and
7346dce678f0786a8faed1d83bdea2bd79dcc65eChristian Maederformulae is still missing. The static analysis currently collects the bare
7346dce678f0786a8faed1d83bdea2bd79dcc65eChristian Maedersignature and the subsort relation.
ffd0977cdd45c37bcfaa32b3535ef97909cfad63Christian Maeder\end{document}