
\begin{DoxyItemize}
\item infos = Information about the typechecker plugin is in keys below
\item infos/author = Armin Wurzinger \href{mailto:e1528532@libelektra.org}{\tt e1528532@libelektra.\+org}
\item infos/licence = B\+SD
\item infos/needs =
\item infos/needs = regexdispatcher
\item infos/provides = typechecker
\item infos/recommends =
\item infos/placements = postgetstorage presetstorage
\item infos/status = maintained global experimental
\item infos/metadata =
\item infos/description = a plugin that type checks configuration specifications
\end{DoxyItemize}

A plugin that type checks specifications before setting keys and after getting keys from a mounted specification.

The type checker uses regular expressions as the foundation. It assigns a regex to each key describing its possible contents, thus defining a key\textquotesingle{}s type. Links between keys will fail the type check if the regexes describing the linked keys are not compatible with each other, i.\+e. the regex of the linked key is equal or a subset of the regex of the linking key. This concept is not only useful for defining links. It can be used to restrict the input types of transformations for instance as well.

\subsection*{Usage}

There are basically two ways to use type checker plugin. First we describe how the plugin is used in general for users. Afterwards we describe how the type checker plugin can be extended with the semantics of additional configuration specification keywords. This is interesting for plugin developers who want to make use of the type system for their work as well.

\subsubsection*{General Usage}

In order to use the type checker, mount a configuration specification along with this plugin. There are already a lot of commonly used keywords supported out of the box specified in the file \href{/home/jenkins/workspace/libelektra_master-Q2SIBK3KE2NBEMJ4WVGJXAXCSCB77DUBUULVLZDKHQEV3WNDXBMA/src/plugins/typechecker/typechecker/prelude.ini}{\tt prelude.\+ini}. Usually one wants to mount that file as well beforehand for the standard configuration.

{\ttfamily kdb mount prelude.\+ini spec/$<$path$>$/spec/elektra ini} {\ttfamily kdb mount $<$specification$>$ spec/$<$path$>$ $<$storage plugin to read the specification$>$ typechecker}

Retrieving any key from the specification using {\ttfamily kdb get $<$path$>$} will cause the type checking to happen. The type checker will issue a warning if it detects any problems with it. In case a key covered by a configuration specification is accessed programmatically, the type checking will also happen if the type checker is mounted.

When altering a mounted specification using {\ttfamily kdb set $<$path$>$} or {\ttfamily kdb setmeta $<$path$>$ $<$value$>$}, the type checker will issue an error if the newly added key or metakey will lead to an inconsistent configuration specification according to the type system specification.

It is often necessary to set multiple specification keywords at once in order to transform a valid configuration specification to another valid one. Therefore some kind of transaction is required so the type checking only happens when the whole changes have been made. The easiest way to do this is to use the command {\ttfamily kdb shell}. An example of its usage is shown below. In case you prefer a graphical tool to edit configuration specifications you can use the qt-\/gui for Elektra.

Please keep in mind that its better to unmount in the reverse way, so first unmount your specification and then prelude.

\subsubsection*{Usage for custom configuration specification keywords}

In case a new plugin has been written which can be described using regular expressions, a plugin developer may want to teach the type system about this plugin. In order to do that, each configuration specification may contain a section describing the effects of keywords. There are three metakeys that are interpreted by the typechecker, {\ttfamily elektra/spec/order}, {\ttfamily elektra/spec/type} and {\ttfamily elektra/spec/impl}. These metakeys get explained and introduced along the following examples. Let\textquotesingle{}s take the example of the fallback keyword, that would be formalized in the ini format as follows\+:


\begin{DoxyCode}
#@META elektra/spec/order = 10
#@META elektra/spec/impl = fallback a b = link a b
[fallback/#]
\end{DoxyCode}


In the implementation {\ttfamily elektra/spec/impl} we are limited to the two functions {\ttfamily link} and {\ttfamily intersect} forming the basic building blocks for describing more complex keywords. They respective type signatures are {\ttfamily Regex\+Contains b a =$>$ Key b \+:\+: . -\/$>$ Key a -\/$>$ Key a} for {\ttfamily link} and {\ttfamily Intersectable (Regex\+Intersection a b) =$>$ Key a -\/$>$ Regex b -\/$>$ Key (Regex\+Intersection a b)} for {\ttfamily intersect}. A type signature, inspired by Haskell\textquotesingle{}s type signatures, typically has two parts. The first part describes its constraints followed by {\ttfamily =$>$}. Then its parameter\textquotesingle{}s types follow separated by a {\ttfamily -\/$>$}, where the last parameter type is the result type. A constraint can bei either a containment constraint or an intersection constraint, written {\ttfamily Regex\+Contains} or {\ttfamily Intersectable} followed by two type variables. Type variables may as well be a string constant describing a regex as we will see in the next example. In our case {\ttfamily Regex\+Contains b a} means that the regex stored in the type variable a is either equal to or a subset of the regex stored in the type variable b. The type variables arise from the type parameters. A type parameter may either refer to a {\ttfamily Key} or to a {\ttfamily Regex}. A {\ttfamily Key} may either refer to the path of another key which is given relatively to the current key after the {\ttfamily \+:\+:} symbol, or to the annotated key itself, in which case no extra annotation is necessary. A {\ttfamily Regex} refers directly to a regex which can then be used as a type variable. Last, we see the type {\ttfamily Regex\+Intersection} that represents the result of the intersection of two regexes. The {\ttfamily Intersectable} constraints checks whether such an intersection is possible. This is used to prevent two incompatible checks from being applied to a single key. For instance, consider a check for letters and another check for numbers, there would be nothing that could be stored in such a key. The metakey {\ttfamily elektra/spec/order} is used to specify the order in which checks or links are applied. This is interesting because links should happen when all the checks on a single key have already been applied so all the limitations of a key are already in effect.

Summing up the above example can be read as "If the regex of the key b, which path is obtained by taking the value of the current key, relatively referred to via {\ttfamily .} is equal to or a subset of the regex describing the current key, this link is allowed. In that case the type of the current key will not be changed and remain to be the regex stored in the type variable a.

Let us look at another example which makes use of {\ttfamily intersect}. Suppose you want to make a specification keyword that checks whether the key\textquotesingle{}s content lies with the boundaries of a 16 bit unsigned short value, corresponding to the range 0-\/65535, or rewritten as a regex, {\ttfamily (\mbox{[}0-\/9\mbox{]}$\vert$\mbox{[}1-\/8\mbox{]}\mbox{[}0-\/9\mbox{]}$\vert$9\mbox{[}0-\/9\mbox{]}$\vert$\mbox{[}1-\/8\mbox{]}\mbox{[}0-\/9\mbox{]}\{2\}$\vert$9\mbox{[}0-\/8\mbox{]}\mbox{[}0-\/9\mbox{]}$\vert$99\mbox{[}0-\/9\mbox{]}$\vert$\mbox{[}1-\/8\mbox{]}\mbox{[}0-\/9\mbox{]}\{3\}$\vert$9\mbox{[}0-\/8\mbox{]}\mbox{[}0-\/9\mbox{]}\{2\}$\vert$99\mbox{[}0-\/8\mbox{]}\mbox{[}0-\/9\mbox{]}$\vert$999\mbox{[}0-\/9\mbox{]}$\vert$\mbox{[}1-\/5\mbox{]}\mbox{[}0-\/9\mbox{]}\{4\}$\vert$6\mbox{[}0-\/4\mbox{]}\mbox{[}0-\/9\mbox{]}\{3\}$\vert$65\mbox{[}0-\/4\mbox{]}\mbox{[}0-\/9\mbox{]}\{2\}$\vert$655\mbox{[}0-\/2\mbox{]}\mbox{[}0-\/9\mbox{]}$\vert$6553\mbox{[}0-\/5\mbox{]})}


\begin{DoxyCode}
#@META elektra/spec/impl = checkunsignedshort a = intersect a (Key :: Regex
       "([0-9]|[1-8][0-9]|9[0-9]|[1-8][
      0-9]\{2\}|9[0-8][0-9]|99[0-9]|[1-8][0-9]\{3\}|9[0-8][0-9]\{2\}|99[0-8][0-9]|999[0-9]|[1-5][0-9]\{4\}|6[0-4][0-9]\{3\}|65[0-4][0-9]\{2\}|655[0-2][0-9]|6553[0-5])")
[check/unsignedshort]
\end{DoxyCode}


This function means "If the regex represented by the type variable a, which in that case refers to the current key\textquotesingle{}s regex, can be intersected with the regex depicting the range, the check passes successfully and the resulting type is the intersection between the two regexes." This approach is typically used with checker plugins which further restrict what kind of contents a key may contain, and each intersection limits the type more and more. The constraints prevents that two incompatible checks can be used for a single key.

It is also possible to explicitly state the type signature for a metakey in case its effect cannot be specified and inferred using {\ttfamily link} or {\ttfamily intersect}. In that case we can use {\ttfamily undefined} as the result of the function. For instance the following example defines a transformation that can be used on keys representing letters, and outputs a number\+:


\begin{DoxyCode}
#@META elektra/spec/order = 0
#@META elektra/spec/type = RegexContains a "[a-zA-Z]*" => Key a -> Key "[1-9][0-9]*|0"
#@META elektra/spec/impl = transformcountletters a = undefined
[transform/countLetters]
\end{DoxyCode}


\subsection*{Examples}

Create a sample configuration specification with three keys. As it is valid, there will be no error issued. We rely on the existence of \href{/home/jenkins/workspace/libelektra_master-Q2SIBK3KE2NBEMJ4WVGJXAXCSCB77DUBUULVLZDKHQEV3WNDXBMA/src/plugins/typechecker/typechecker/prelude.ini}{\tt prelude.\+ini}, which already contains the type definitions for {\ttfamily check/range}, {\ttfamily check/long} and {\ttfamily fallback/\#} and mount it along. Please note not to mount prelude below the specification. We use kdb shell to delay the type checking until we have finished writing the whole specification.


\begin{DoxyCode}
# Backup-and-Restore:spec/tests/typechecker
sudo kdb mount simplespecification.ini spec/tests/typechecker ini regexdispatcher typechecker

echo 'kdbGet spec/tests/typechecker \(\backslash\)
keySetName spec/tests/typechecker/key1 \(\backslash\)
keySetMeta check/range 0-5000 \(\backslash\)
ksAppendKey \(\backslash\)
keyClear \(\backslash\)
keySetName spec/tests/typechecker/key2 \(\backslash\)
keySetMeta check/range 7200-10000 \(\backslash\)
ksAppendKey \(\backslash\)
keyClear \(\backslash\)
keySetName spec/tests/typechecker/key3 \(\backslash\)
keySetMeta check/long \(\backslash\)
keySetMeta fallback/#1 spec/tests/typechecker/key1 \(\backslash\)
ksAppendKey \(\backslash\)
keyClear \(\backslash\)
keySetName spec/tests/typechecker/key4 \(\backslash\)
keySetMeta check/validation a[0-9]+ \(\backslash\)
ksAppendKey \(\backslash\)
keyClear \(\backslash\)
keySetName spec/tests/typechecker/key5 \(\backslash\)
keySetMeta check/validation [a-z][0-9]+ \(\backslash\)
keySetMeta fallback/#1 spec/tests/typechecker/key4 \(\backslash\)
ksAppendKey \(\backslash\)
keyClear \(\backslash\)
kdbSet spec/tests/typechecker' | kdb shell

kdb get spec/tests/typechecker/key1
\end{DoxyCode}


Add an invalid link now and see how it refuses the specification, showing the erroneous parts instead. As the two keys represent the ranges 0-\/5000 and 7200-\/10000, they obviously cannot be linked together.


\begin{DoxyCode}
kdb setmeta spec/tests/typechecker/key2 fallback/#1 spec/tests/typechecker/key1
# RET: 5
# STDERR: .*Could not deduce:.*

sudo kdb umount spec/tests/typechecker
\end{DoxyCode}


As indicated in the limitations, error messages are currently rather raw and haskell-\/focused\+:


\begin{DoxyCode}
Type checking or compilation failed:
 /tmp/testSpecification80690-1.hs:15:8: error:
     • Could not deduce: RegexContains
                           "[0-9]|[1-9][0-9]|[1-9][0-9][0-9]|[1-4][0-9][0-9][0-9]|5000"
                           "[7-9][2-9][0-9][0-9]|10000"
         arising from a use of ‘fallback’
     • In the expression:
         fallback
           key1
           (checkvalidation
              (Key :: Regex "[7-9][2-9][0-9][0-9]|10000") (Key :: Regex ".*"))
       In an equation for ‘key2’:
           key2
             = fallback
                 key1
                 (checkvalidation
                    (Key :: Regex "[7-9][2-9][0-9][0-9]|10000") (Key :: Regex ".*"))
\end{DoxyCode}


It is still fairly easy to map the error message back to the configuration specification. The above error message shows that there was an error when type checking the specification of {\ttfamily key2} as indicated by the line \char`\"{}\+In an equation for ...\char`\"{}. The line \char`\"{}\+In the expression\+: ...\char`\"{} then shows the exact part where its happen. The incompatibility arises during checking the fallback from {\ttfamily key2} to {\ttfamily key1}. The regexes describing the contents of the two keys are not compatible with each other. The first key contains numbers between 0 and 5000, while the secondkey is restricted to numbers between 7200 and 10000.

\subsection*{Debugging}

This test specification has no errors by default and will thus report nothing, but if you alter it you can experiment with the type checker. If Elektra is compiled with the E\+N\+A\+B\+L\+E\+\_\+\+L\+O\+G\+G\+ER flag, it will log the inferred types in all cases so the type behavior can be observed when getting/setting a key in a specification.

\subsection*{Dependencies}


\begin{DoxyItemize}
\item ghc $>$= 8.\+0.\+1 and $<$= 8.\+2
\item ghc-\/pkg, usually bundled with ghc
\item cabal, the haskell build system, usually bundled with ghc
\item augeas, which provides libfa utilized by this plugin
\end{DoxyItemize}

Furthermore the following haskell dependencies need to be installed to the sandbox as explained in the bindings readme\+:


\begin{DoxyCode}
cabal install 'base >=4.9 && <4.12' 'containers >=0.5 && <0.6' \(\backslash\)
        'directory >=1.2 && <1.4' 'process >=1.4 && <1.7' 'binary >=0.8 && <0.9' \(\backslash\)
        'haskell-src-exts-any' 'pretty -any' 'hint >=0.7.0 && <0.8.0' 'temporary -any' \(\backslash\)
        'exceptions -any' 'text -any' 'simple-logger -any' 'megaparsec -any' \(\backslash\)
        'hspec -any' 'QuickCheck-any' --avoid-reinstalls
\end{DoxyCode}


\subsection*{Limitations}


\begin{DoxyItemize}
\item Type checking only happens when getting or setting a key in a mounted specification. This is also the case if cascading keys are used.
\item Errors are currently raw and haskell-\/focused. 
\end{DoxyItemize}