\section{Conv: Checking convertibility}

%if False %% only to be seen by the Haskell compiler
\begin{code}
module Conv where

import Val
\end{code}
%endif

This module implements convertibility. There are functions which
checks convertibility for values, type values and vector of values.
The convertibility functions take one extra integer argument which is
used for creating
fresh generic values. This is used when we check if two functional values \texttt{f}
and \texttt{g} are convertible, we just check if \texttt{f u = g u} for a generic
value u.

The following functions are defined:
\begin{itemize}
\item  |eq n u v w|   checks if \texttt{v = w : u}
\item |eqs n u vs ws| checks if \texttt{vs = ws : u'}, 
       where \texttt{u'} is the argument types of \texttt{u}
\item |eqT n u v| checks if \texttt{u = v} as types.
\end{itemize}

We first have to define the monad for error checking:
\begin{code}
data G a = Ok a | Fail String

instance  Monad G  where
    (Ok x)   >>= k   =  k x
    Fail s   >>= k   =  Fail s
    return           =  Ok
    fail             =  Fail
\end{code}
The convertibility functions will use a |gensym| function to generate 
fresh generic values. The expression |gensym n s u| will generate an 
empty application from the head built up from the (unique) index |n|, 
the name |s| and the type |u|.
\begin{code}
gensym        :: Int -> Name -> Val -> G Val 
gensym n s u  = return (mvar (Gen n s u))
\end{code}

\subsubsection{Type convertibility}
\begin{code}
eqT :: Int -> Val -> Val -> G () 
\end{code}
To check if two types are convertible, we have the following cases:
\begin{itemize}
\item \texttt{Set} is equal to \texttt{Set}.
\begin{code}
eqT  _  Set          Set          = return ()
\end{code}
\item Two functional types are equal if their parts are equal, so to check whether 
\texttt{Fun a f = Fun a' f'} we first check if \texttt{a = a'} and then check if
\texttt{f u = f' u}, where \texttt{u} is a new generic value.
\begin{code}
eqT  n  (Fun a1 f1)  (Fun a2 f2)  = 
  do
  eqT n a1 a2 
  u <- gensym n "X" a1
  eqT (n+1) (f1 u) (f2 u)
\end{code}
\item For the remaining cases, we check if they are convertible as values in \texttt{Set}

\begin{code}
eqT  n  u1           u2           = eq n Set u1 u2
\end{code}


\end{itemize}

\subsubsection{Convertibility of values in a type}
\begin{code}
eq :: Int -> Val -> Val -> Val -> G ()
\end{code}
To check if two objects in a type are equal, we have the following cases:
\begin{itemize}
\item If the type is a functional type, then to check \texttt{u = v : Fun a f}, 
we check if \texttt{u w = v w : f w} for a generic value \texttt{w} of type \texttt{a}.
\begin{code}
eq  n       (Fun a f)  u1            u2            =
  do
  u <- gensym n "X" a
  eq (n+1) (f u) (app u1 u) (app u2 u)
\end{code}
\item Otherwise, we must check two applications. We then check that the heads are equal
and the arguments are equal.
\begin{code}
eq  n       _          (App h1 us1)  (App h2 us2)  = 
  if eqH h1 h2  then eqs n (typH h1) us1 us2 
                else fail"eq"
\end{code}
\item In all other cases, the objects are not convertible.
\begin{code}
eq  _       _          _             _             =  fail "eq"
\end{code}
\end{itemize}


\subsubsection{Convertibility of vectors}

\begin{code}
eqs :: Int -> Val -> [Val] -> [Val] -> G ()   
\end{code}

The expression |eqs n u vs ws| checks if two vectors |vs| and 
|ws| are equal and fits as arguments to the functional type |u|. We have 
the following cases:
\begin{itemize}
\item If the two vectors are empty, then we are done.
\begin{code}
eqs  n  a          []        []       = return ()
\end{code}
\item If the two vectors are nonempty, then to check if 
    \texttt{u1:us1 = u2:us2 : Fun a f} we first check if \texttt{u1 = u2 : a} and 
then check \texttt{us1 = us2 : f u1}.
\begin{code}
eqs  n  (Fun a f)  (u1:us1)  (u2:us2) =
  do
  eq n a u1 u2
  eqs n (f u1) us1 us2
\end{code}
\item In all other cases the vectors are not convertible.


\begin{code}
eqs  _  _          _         _        = fail "eqs" 
\end{code}
\end{itemize}