e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\documentclass{article}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\title{Creating ATermConvertible-Instances with \emph{genRules} and \emph{DrIFT}}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\author{Felix Reckers}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\begin{document}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersThe tool \emph{genRules} provides the ability to create automatically rules, which can
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersbe proceeded by \emph{DrIFT}. The directory \emph{ATC} includes the files with ATermConvertible
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersinstances, which are necessary to read datatypes from and to write them to files in the
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersShared-ATerm-format.\\
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersTo create a new ATermConvertible instance for the datatypes in one file or more, you can invoke
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\emph{genRules} in the directory \emph{utils}. It will generate a file with the specified
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersrules for \emph{DrIFT}. Then you can invoke \emph{DrIFT} on that file to create the instances.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\emph{genRules} will generate a file with a \verb|.der.hs|-suffix, it will contain all necessary
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersimports and the \emph{DrIFT}-rules for each datatype. If the input is one file, the name of the
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersoutput file will be the same as the input plus the special suffix. If there is more than one
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersinput file, the output file will have the name of the first of them. Every specific logic
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersinstance is saved in the directory which represents that logic: CASL, HasCASL, Haskell and CspCASL.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersThese files begin with an
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\emph{ATC\_} followed by the logic name. All the other ATC-files are saved in the directory \emph{ATC}.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\section*{Invoking \emph{genRules}}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersThe following options are available:
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\begin{description}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\item[-r:] This option must be declared, it specifies the rule for generation.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersIn this case it must be \emph{ShATermConvertible}.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\item[-o:] Specifies the output directory, commonly the output directory is \emph{ATC}.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersIf the output directory is the same as the directory from the used file(s) it is supposed
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersthat the instance is a specific logic instance.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\item[-x:] Excludes the specified datatype(s). That means, that there will no rules be
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers generated for that datatype(s).
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\item[-h:] Specifies a header file.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\end{description}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\section*{Header files}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersHeader files must have the suffix \verb|.header.hs| and the name of the file they
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersare created for. They must be in the \emph{ATC}-directory.\\
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersA header file will be parsed and every instance in that file will be omited
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersat the rule-generation. You can also include rules for omitting any datatype(s)
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersfrom the parsed file. The syntax for omitting a datatype is:
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\begin{verbatim}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers{-| Exclude: Datatype |-}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\end{verbatim}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckerswhere "Datatype" is the name of the datatype, which should be omited. In a header file can be
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckershaskell-comments, they will not be considered. \\
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersEvery logic specific ATC-instance, although it was generated from more than one file, has only one
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersheader file, which has the logic name (i.e., CASL.header.hs).\\
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersHeader files are necessary, because \emph{DrIFT} can't generate all instances automatically.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\section*{Automatic file-generation with \emph{make}}
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersTo generate a file automatically before compiling \emph{hets}, you must include the file name
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersin the variable \emph{genrule\_files} in the Makefile. All files in that variable will be seperated
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersinto files which are from a specific logic directory (CASL, HasCASL, CspCASL, Haskell) and those which
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersare not. The files from every logic will be packed in the specific logic ATC-file (look above).
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersSo every instance of a file which is not in a logic directory, will be put in the ATC-directory.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersThis prospective filenames must be also added to the variable \emph{gendrifted\_files}. For example,
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersfor the file name \emph{Commom/Named.hs} in the variable \emph{genrule\_files}, there must also be
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersthe file name \emph{ATC/Named.hs} in the variable \emph{gendrifted\_files}.\\
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix ReckersIt must be noted, that the order in the variable \emph{gendrifted\_files} is significant. So if
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckersan instance file A imports an other instance file B, B must stand before A in the variable.
e82e433fe62fc83daaad3d96aaa01ee111e49d39Felix Reckers\end{document}