%> do tex %F -l -l -d"-t a4"
%> do tex %F -l -b -l -l -d"-t a4"

\def\TOPO{{\sc topo }}
\def\LOTOS{{\sc lotos }}
\def\ILDI{{\sc ildi }}
\def\LDM{$\Lambda\delta$-machine }

\documentstyle[]{article}

\textwidth=16cm
\oddsidemargin=1cm
\evensidemargin=1cm
\textheight=22cm
\topmargin=0cm
\parindent=0mm
\parskip=4mm
\unitlength=1mm

\input{psfig.tex}


\title{\ILDI: interpreter of LOTOS ADTs}

\author{Tom\'{a} Robles Valladares              \\[1ex]
        Dpt. Ingenier\'{\i}a Telem\'atica       \\
        E.T.S.I. de Telecomunicaci\'on          \\
        Univ. Polit\'ecnica de Madrid           \\
        E-28040 Madrid, SPAIN                   \\
                                                \\
        {\tt <lotos@dit.upm.es>}
        }

\date{December 17, 1992}

\begin{document}
\bibliographystyle{abbrv}
\maketitle

\begin{abstract}
\ILDI is an interactive interpreter of LOTOS ADTs.
It allows the testing and debugging of LOTOS ADTs.
\ILDI uses \LDM format as input.
This format is fully compatible with those used 
by the idle (compiler of ADTs used by \TOPO).

The interface is provided through an interactive command menu,
and may also be used in bath mode.
\end{abstract}

\section{Introduction}
The \LOTOS compiler \TOPO incorporates a Compiler of ADTs.
This compiler generated a {\em C} or {\em Ada} code
that is compiled with others pieces of code
and provides the implementation of the LOTOS Specification.

The testing and debugging of LOTOS ADTs requires a compilation process.
In this environment \ILDI objectives are:

\begin{itemize}
\itemsep=-\parsep
\item
   To provide a useful tool  for debugging and testing LOTOS ADTs.
\item
   Easiness of use, both in interactive or in bath mode.
\item
   To avoid the compilation phase.
\item
   Full compatibility  with \TOPO compiler.
\end{itemize}

As in the \TOPO compiler \LOTOS equations are interpreted as rewriting
rules,
and equality is based on comparing the canonical forms.

\section{\ILDI structure}
In order to complete the previous objectives,
\ILDI has the next characteristics:

\subsection{Input: spec.ldi}
The LOTOS specification has to be processed using:
lfe (syntactic checker), lsa (semantics checker),
and idle (intermediate code generator).
It is the same file used as input for the LOTOS compiler.

The input format is described in \cite{robles:ldmt}.


\subsection{Architecture}

    \begin{figure}
    \centerline{\psfig{figure=struct.id}}
    \caption{General Diagram}
    \end{figure}

The internal architecture of \ILDI is divided into two main parts:

\begin{description}
\item[Library interface:]
   The core of ildi is formed by 4 files 
   that offer a library of functions to perform: 
   equality resolution and rewriting of expressions.
   Those files are:

   \begin{description}
   \item[ldi.h and ildi.c:]
      They generate the structures used in the interpretation of
      expressions.
      These structures are built when reading the file spec.ldi.
      Ildi files are generated for each specification
      using DTOK and ALGA modules.

      The structures generated are:

      \begin{itemize}
      \item
	 Sort declaration list.
      \item
	 Operation declaration list.
      \item
	 Equations for rewriting.
      \end{itemize}

   \item[kaos.h and kaos.c:]
      They implement the operational part of the interpreter.
      They provide functions that implement the rewriting
      and equality resolution.
      It also offers a function for drawing expressions.

      They are general for whatever specification,
      and it is not necessary to generate them each time.

   \end{description}

\item[Command interpreter:]
   The interface of the ildi is offered by a command interpreter.
   It works like a shell that reads commands
   and makes the corresponding calls to functions of kaos or ildi.
\end{description}

\newpage

\section{Manual}

{\bf NAME}

  ildi: interactive interpreter of LOTOS ADTs.

{\bf SYNOPSIS}

  ildi.

{\bf DESCRIPTION}

  ``ildi'' is a tool for testing and debugging LOTOS ADTs.
  It allows the rewriting of expressions and the checking of equality,
  inside the environment of a LOTOS Specification.

  ``ildi'' ildi reads an specification previously processed with TOPO.
  To get the appropriate file, it performs the next call:


\begin{verbatim}
     topo spec -ildi
\end{verbatim}


{\bf COMMANDS}

``ildi'' offers a menu with the next commands:

\begin{itemize}

\item[-] \verb+load <spec>+\\

    It loads in the environment of work the specification of file
    $<$spec$>$.ldi.
    Each time this command is executed,
    every previous information is lost.


\item[-] \verb+rewrite <expression> [<sort>]+\\

    It performs the rewriting of \verb+<expression>+ 
    applying the rewriting rules of the specification currently
    loaded.
    If some error happens, it will be reported on the screen.
    
    The notation is prefix,
    and the arguments must be enclosed with brackets.
    Infix notation is ignored.
    The field $<sort>$  is optional and must be used only when
    there exist two operations with the same arguments,
    but different result.
    If it is used,
    the interpreter will resolve the overloading.


\item[-] \verb+check <exp1> = <exp2> [<sort>]+\\

    It checks if the result of rewriting the two expressions 
    is the same.
    The format of the expressions as the one described 
    for {\em rewrite} command.
    Also the field $<sort>$ is optional,
    and used for overloading resolution.


\item[-] \verb+setdeb [yes] [no]+\\

    It changes the trade mode of the interpreter.
    With the trace mode {\bf on},
    the rewrite rules applied ,
    when rewritten an expression,
    are reported on the screen.
    If trace mode is {\bf off} it works silently.
    
    {\bf OPTIONS}

    \begin{itemize}
      \item 
	 yes: it puts trace mode on.

      \item 
	 no: it puts trace mode off.

      \item 
	 no options: it shows the current mode.
    \end{itemize}


\item[-] \verb+display [sorts] [operations]+\\

    It shows on the screen the list of sorts and/or 
    operations of the current specification.

    {\bf OPTIONS}

    \begin{itemize}
      \item
	 sorts: it shows the list of sorts.

      \item
	 operations: it shows the list of operations

      \item
	 no options: it shows both sorts and operations.
    \end{itemize}


\item[-] \verb+help+\\
    It shows on the screen the available commands with
    their correct syntax.

\item[-] \verb+quit+\\
    It leaves the interpreter.

\end{itemize}

{\bf FILES}

  $<$spec$>$.lot  LOTOS specification.

  $<$spec$>$.ldi Specification in the input format of the interpreter.

{\bf MESSAGES}

  The errors detected in the loaded specification,
  and in the rewriting phase generate the suitable
  report on the screen.

  It is not possible to use specifications with:
  the same name, the same arguments and the same result.
  Any other overloading is permitted,
  and the interpreter will solve it.

  When parsing an user expression,
  any operation without arguments that does not match with a
  LOTOS constant will be interpreted as a new constant.
  Then it is important to take care of misspelling LOTOS
  constants when writing expressions.

\newpage
\section{Example}
In this section we are going to see an example of the application of
the interpreter.
We are going to use a LOTOS specification with
the natural number modulus four:

\begin{verbatim}
TYPE Nat14 IS
  SORTS
    boolean, Nat14
  OPNS
    true, false: -> boolean
    n1, n2, n3, n4: -> Nat14
    succ, pred: Nat14 -> Nat14
    _ plus _: Nat14, Nat14 -> Nat14
    _ eq _: Nat14, Nat14 -> boolean
  EQNS
    OFSORT Nat14
    FORALL m, n: Nat14
      n2 = succ (n1) ;
      n3 = succ (succ (n1)) ;
      n4 = succ (n3) ;
      pred (m) = succ (succ (succ (m))) ;
      m plus succ (n) = succ (m plus n) ;
      m plus n1 = succ (m) ;
      succ (succ (succ (succ (n1)))) = n1 ;
      succ (succ (succ (succ (succ (m))))) = succ (m) ;

    OFSORT boolean
    FORALL x, y: Nat14
      x eq x = true ;
      x eq succ (x) = false ;
      x eq succ (succ (x)) = false ;
      x eq succ (succ (succ (x))) = false ;
      x eq succ (succ (succ (succ (x)))) = true ;
      n1 eq succ (succ (succ (succ (y)))) = n1 eq y ;
      succ (x) eq y = x eq succ (succ (succ (y))) ;
  ENDTYPE
\end{verbatim}

ILDI is started from \verb/topo/:

\begin{verbatim}
...> topo nat14 -ildi
Interactive Lotos Data Interpreter ...
lfe  nat14.lot > ./tmp_topo575
mv ./tmp_topo575 nat14.lfe
lsa -f -C  < nat14.lfe > ./tmp_topo575
mv ./tmp_topo575 nat14.lsf
idle -s -r  -tnat14.at < nat14.lsf > ./tmp_topo575
mv ./tmp_topo575 nat14.ldi
ildi nat14

Lotos Data Command Interpreter. 
Introduce command:
ildi> 
\end{verbatim}

Now the specification is ready to be processed.
When we are working with several specifications
or we do not know well the specification,
it is interesting to examine the sorts and operations of the
specification:

\begin{verbatim}
ildi> display sort

SORTS: 
* boolean
* Nat14

ildi> display opn      

OPERATIONS: 
* true      -> boolean
* false      -> boolean
* n1      -> Nat14
* n2      -> Nat14
* n3      -> Nat14
* n4      -> Nat14
* succ     Nat14 -> Nat14
* pred     Nat14 -> Nat14
* plus     Nat14 , Nat14 -> Nat14
* eq     Nat14 , Nat14 -> boolean
\end{verbatim}

Next we show some examples of rewriting and equality checking.

\begin{verbatim}
ildi> rewrite plus(succ(n1),pred(n4))
------->>>>>>     n1

ildi> check n1 = pred(plus(n1,n3))
[ n1 = pred(plus(n1,n3)) ] => FAILS 

ildi> check n1 = plus(succ(n1),pred(n4))
[ n1 = plus(succ(n1),pred(n4)) ] => OK 
\end{verbatim}

To know what equations are applied to rewrite an expression,
we have to use the {\em setdeb} command.
Let's see an example of trace activation,
and the messages produced when a rewriting is performed:

\begin{verbatim}
ildi> setdeb yes
Operation OK. 

ildi> rewrite plus(succ(n1),pred(n4))
  pred(m) = succ(succ(succ(m))) ;
  succ(succ(succ(succ(n1)))) = n1 ;
  m plus succ(n) = succ(m plus n) ;
  m plus succ(n) = succ(m plus n) ;
  m plus n1 = succ(m) ;
  succ(succ(succ(succ(n1)))) = n1 ;
------->>>>>>     n1
\end{verbatim}

\bibliography{ALL}
\end{document}

% Local Variables:
% mode: indented-text
% comment-column: 0
% comment-start: "% "
% comment-end: ""
% comment-start-skip: "% *"
