CASLParserOverview.tex revision ffd0977cdd45c37bcfaa32b3535ef97909cfad63
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder\documentclass{article}
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder\parindent 0pt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski\begin{document}
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\title{CASL basic items}
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder\author{C. Maeder}
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder\section{Preliminaries}
d48085f765fca838c1d972d2123601997174583dChristian Maedersee the documentation for HetCATS
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder\section{Compiling the CASL parser}
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder\texttt{cd HetCATS/CASL} and call \texttt{./ghc-call} (a script that contains
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederall necessary ghc options and parameters). An alternative is to call
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{gmake capa} in the top directory.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederThis creates a binary called \texttt{capa} that can parse (and pretty
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederprint) ``Basic Specification with Subsorts'' of the CASL Summary
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederversion 1.0.1 \\ (www.brics.dk/Projects/CoFI/Documents/CASL/Summary/).
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian MaederStructured specifications (see \texttt{Static/hetpa.hs}) must be parsed by the heterogenous parser
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederNote: if module \texttt{AS\_Basic\_CASL} can not be found, then
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{AS\_Basic\_CASL.hs} was not ``drifted'' (i.e., derived from
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{AS\_Basic\_CASL.der.hs}).
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederAlso \texttt{Common/AS\_Annotation.hs} must have been drifted.
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder\section{Testing}
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederA test call might be:
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederThe binary \texttt{capa} is also used to test various parsers. Test cases are
eab576044505ba1fbc64610323053490fbd9e82cChristian Maedergiven as \texttt{*.casl} files.
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederCalling \texttt{./runcheck.sh ./capa} performs many tests and compares the
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederresults with corresponding \texttt{*.output} files.
eab576044505ba1fbc64610323053490fbd9e82cChristian MaederAlternatively a test can be run using \texttt{runhugs}. For this the
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederfile \texttt{capa.lhs} is executable and the test can be run
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{Wrong*.casl} files contain wrong CASL code and should produce
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maedererror messages. Apart from extra tests, correct (\texttt{Bla.casl})
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederand wrong files (\texttt{WrongBla.casl}) are tested. If a \texttt{diff}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederwith the expected output fails, then also the number of
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder``\texttt{error}'' occurrences (in the produced output) is counted. For a
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedersuccessful comparison a ``\texttt{passed}'' is emitted.
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederCalling ``\texttt{./runcheck.sh ./capa set}'' will update the
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder\texttt{*.output} files (and a subsequent \texttt{./runcheck.sh ./capa} should
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederAlternatively, all checks can be preformed by \texttt{make check}. Output
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederfiles will be overwritten by \texttt{make output}. With \texttt{cvs up} or
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{cvs diff} changes can be compared to checked-in versions of the output
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\section{Source files in \texttt{HetCATS/CASL}}
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder\begin{description}
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder\item[AS\_Basic\_CASL.der.hs] defines the abstract syntax tree for CASL
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\item[Formula.hs] parser \texttt{term} and \texttt{formula}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\item[ItemList.hs] parses items (separated by semicolons) generically
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (\texttt{itemList}) and annotations between or following these
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\item[LiteralFuns.hs] used by \texttt{Print\_AS\_Basic.hs}
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder\item[Logic\_CASL.hs] contains the instance for the class \texttt{Logic.Logic}
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder\item[MixfixParser.hs] uses precedence and associativity to resolve
d48085f765fca838c1d972d2123601997174583dChristian Maeder mixfix terms (and formulae). Also \%list, \%string, \%number and
d48085f765fca838c1d972d2123601997174583dChristian Maeder \%floating annotations are resolved
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\item[OpItem.hs] parsers \texttt{opItem(s)} and \texttt{predItem(s)}
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\item[Parse\_AS\_Basic.hs] supplies the top-level parsers \texttt{basicSpec,
d48085f765fca838c1d972d2123601997174583dChristian Maeder basicItems, dotFormulae} and \texttt{sigItems}
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\item[Print\_AS\_Basic.hs] pretty prints data types of
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder \texttt{AS\_Basic\_CASL.hs}
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\item[RunMixfixParser.hs] is an additional driver to test the mixfix
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\item[RunParsers.hs] contains the driver called in Main for test parsers and
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder is reused in \texttt{HetCATS/HasCASL}. (It declares an existential type.)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\item[RunStaticAna.hs] is an additional driver to test the static
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder analysis (call \texttt{capa analysis <file>})
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\item[Sign.hs] is the analysed abstract syntax and the signature for an
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder instance of the class \texttt{Logic}.
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\item[SortItem.hs] parser \texttt{sortItem(s)} (requires \texttt{Formula.hs}
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder for subsort definitions)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\item[Static.hs] implements the static analysis
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\item[Sublogics.hs] used by \texttt{Logic\_CASL.hs}
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\item[SymbolParser.hs] parses symbols and symbol maps that are not needed for
d48085f765fca838c1d972d2123601997174583dChristian Maeder basic specs but for heterogeneous structured specifications
2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder (\texttt{Logic\_CASL.hs}). These parsers do not deal with annotations,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\item[TypeItem.hs] parsers \texttt{datatype} and \texttt{typeItems}
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder\item[capa.lhs] is the main module that simply lists the test parsers
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder and is executable for hugs
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\end{description}
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\section{Remarks}
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederThe following files have been moved to the \texttt{Common} directory.
d48085f765fca838c1d972d2123601997174583dChristian Maeder\begin{description}
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\item[Token.hs] generic parser for mixfix ids and some keyword parsers
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (reused in \texttt{HetCATS/HasCASL}). The haskell data types
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder \texttt{Token} and \texttt{Id} are defined in \texttt{Common/Id.hs}!
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\item[Lexer.hs] various scanners and extensions of the Parsec library
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\item[Keywords.hs] CASL keywords as named identifiers (to be used
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder for parsing and printing and thus ensuring consistent spellings)
d48085f765fca838c1d972d2123601997174583dChristian Maeder\end{description}
d48085f765fca838c1d972d2123601997174583dChristian MaederThe above files rely on the data types in \texttt{Id.hs} and
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\texttt{AS\_Annotation.der.hs} in the \texttt{Common} directory. For pretty
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederprinting the class in \texttt{PrettyPrint.hs} is required.
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\texttt{PrettyPrint.hs} in turn relies on
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\texttt{GlobalAnnotations.hs} and \texttt{LaTeX\_funs.hs} and
d48085f765fca838c1d972d2123601997174583dChristian Maeder\texttt{LaTeX\_maps.hs} (to consider \%display annotations).
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\texttt{Common/Lib/Pretty.lhs} is an adapted copy of\\
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder\texttt{//research.microsoft.com/\~{}simonpj/downloads/pretty-printer/pretty.html}
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederthat is also included as Haskell (\texttt{text}) library.
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\texttt{PrettyPrint.hs} supplies an instance for \texttt{Id}. The
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederinstance for annotations is given in \texttt{Print\_AS\_Annotation.hs}.
d48085f765fca838c1d972d2123601997174583dChristian Maeder\texttt{CASL/Print\_AS\_Basic} further imports
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\texttt{Common.PPUtils}. (Pretty printing requires ``glasgow extensions''.)
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\texttt{GlobalAnnotations.hs} contains the \texttt{PrecedenceGraph} and
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederimports \texttt{Map} and \texttt{Graph}. \texttt{Graph} has its own
d48085f765fca838c1d972d2123601997174583dChristian Maederimplementation of maps, namely \texttt{SimpleMap.hs}.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{Graph} came
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederfrom \texttt{www.cs.orst.edu/\~{}erwig/fgl/}.
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder\texttt{Map} and \texttt{Set}
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maedercome from \texttt{www.cs.uu.nl/\~{}daan/ddata.html}.
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederWith \texttt{GlobalAnnotations.hs} also
ae8052003e1ec7247597f034069db0939a7387e1Christian Maeder\texttt{GlobalAnnotationsFunctions.hs} is sometimes needed. The later
eab576044505ba1fbc64610323053490fbd9e82cChristian Maederdepends on \texttt{GraphUtils.hs}.
d48085f765fca838c1d972d2123601997174583dChristian Maeder\texttt{CASL/MixfixParser.hs} uses \texttt{Result.hs} to combine
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdiagnostic messages (and \texttt{Set} to combine states).
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederThe actually parser combinators come from
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder\texttt{www.cs.uu.nl/\~{}daan/parsec.html} that are part of the
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederHaskell library but also have been slightly extended (by
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{consumeNothing}) and included in the \texttt{Common/Lib}
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maedersubdirectory. \texttt{Parsec.hs} simply re-exports parts from
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder\texttt{Parsec.Pos} is reused in \texttt{Id.hs}.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder\texttt{Anno\_Parser.hs} uses the mixfix ids from \texttt{Token.hs}.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder(\texttt{CaslLanguage.hs} that is based on \texttt{Parsec.Token} and
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{Parsec.Language} supplies an alternative parser for ids.)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{Anno\_Parser.hs} further uses \texttt{Parsec.Perm} (that relies on
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederglasgow extensions).
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederThe \texttt{MixfixParser} only operates on \texttt{FORMULA} and
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{TERM} from \texttt{AS\_Basic\_CASL} and not on
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertypes in \texttt{Sign.hs}.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederType checking (considering subtypes and overloading) of terms and
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederformulae (plus their conversions to the types in \texttt{Sign.hs}) is
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederstill missing.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\section{Scripts}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{runcheck.sh} includes \texttt{checkFunctions.sh}.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\texttt{iterate.sh} checks differences between the working copy and
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederthe most recent cvs version.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\end{document}