← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/core/Conv.lhs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/core/Conv.lhs
1
 
\section{Conv: Checking convertibility}
2
 
 
3
 
%if False %% only to be seen by the Haskell compiler
4
 
\begin{code}
5
 
module Conv where
6
 
 
7
 
import Val
8
 
\end{code}
9
 
%endif
10
 
 
11
 
This module implements convertibility. There are functions which
12
 
checks convertibility for values, type values and vector of values.
13
 
The convertibility functions take one extra integer argument which is
14
 
used for creating
15
 
fresh generic values. This is used when we check if two functional values \texttt{f}
16
 
and \texttt{g} are convertible, we just check if \texttt{f u = g u} for a generic
17
 
value u.
18
 
 
19
 
The following functions are defined:
20
 
\begin{itemize}
21
 
\item  |eq n u v w|   checks if \texttt{v = w : u}
22
 
\item |eqs n u vs ws| checks if \texttt{vs = ws : u'}, 
23
 
       where \texttt{u'} is the argument types of \texttt{u}
24
 
\item |eqT n u v| checks if \texttt{u = v} as types.
25
 
\end{itemize}
26
 
 
27
 
We first have to define the monad for error checking:
28
 
\begin{code}
29
 
data G a = Ok a | Fail String
30
 
 
31
 
instance  Monad G  where
32
 
    (Ok x)   >>= k   =  k x
33
 
    Fail s   >>= k   =  Fail s
34
 
    return           =  Ok
35
 
    fail             =  Fail
36
 
\end{code}
37
 
The convertibility functions will use a |gensym| function to generate 
38
 
fresh generic values. The expression |gensym n s u| will generate an 
39
 
empty application from the head built up from the (unique) index |n|, 
40
 
the name |s| and the type |u|.
41
 
\begin{code}
42
 
gensym        :: Int -> Name -> Val -> G Val 
43
 
gensym n s u  = return (mvar (Gen n s u))
44
 
\end{code}
45
 
 
46
 
\subsubsection{Type convertibility}
47
 
\begin{code}
48
 
eqT :: Int -> Val -> Val -> G () 
49
 
\end{code}
50
 
To check if two types are convertible, we have the following cases:
51
 
\begin{itemize}
52
 
\item \texttt{Set} is equal to \texttt{Set}.
53
 
\begin{code}
54
 
eqT  _  Set          Set          = return ()
55
 
\end{code}
56
 
\item Two functional types are equal if their parts are equal, so to check whether 
57
 
\texttt{Fun a f = Fun a' f'} we first check if \texttt{a = a'} and then check if
58
 
\texttt{f u = f' u}, where \texttt{u} is a new generic value.
59
 
\begin{code}
60
 
eqT  n  (Fun a1 f1)  (Fun a2 f2)  = 
61
 
  do
62
 
  eqT n a1 a2 
63
 
  u <- gensym n "X" a1
64
 
  eqT (n+1) (f1 u) (f2 u)
65
 
\end{code}
66
 
\item For the remaining cases, we check if they are convertible as values in \texttt{Set}
67
 
 
68
 
\begin{code}
69
 
eqT  n  u1           u2           = eq n Set u1 u2
70
 
\end{code}
71
 
 
72
 
 
73
 
\end{itemize}
74
 
 
75
 
\subsubsection{Convertibility of values in a type}
76
 
\begin{code}
77
 
eq :: Int -> Val -> Val -> Val -> G ()
78
 
\end{code}
79
 
To check if two objects in a type are equal, we have the following cases:
80
 
\begin{itemize}
81
 
\item If the type is a functional type, then to check \texttt{u = v : Fun a f}, 
82
 
we check if \texttt{u w = v w : f w} for a generic value \texttt{w} of type \texttt{a}.
83
 
\begin{code}
84
 
eq  n       (Fun a f)  u1            u2            =
85
 
  do
86
 
  u <- gensym n "X" a
87
 
  eq (n+1) (f u) (app u1 u) (app u2 u)
88
 
\end{code}
89
 
\item Otherwise, we must check two applications. We then check that the heads are equal
90
 
and the arguments are equal.
91
 
\begin{code}
92
 
eq  n       _          (App h1 us1)  (App h2 us2)  = 
93
 
  if eqH h1 h2  then eqs n (typH h1) us1 us2 
94
 
                else fail"eq"
95
 
\end{code}
96
 
\item In all other cases, the objects are not convertible.
97
 
\begin{code}
98
 
eq  _       _          _             _             =  fail "eq"
99
 
\end{code}
100
 
\end{itemize}
101
 
 
102
 
 
103
 
\subsubsection{Convertibility of vectors}
104
 
 
105
 
\begin{code}
106
 
eqs :: Int -> Val -> [Val] -> [Val] -> G ()   
107
 
\end{code}
108
 
 
109
 
The expression |eqs n u vs ws| checks if two vectors |vs| and 
110
 
|ws| are equal and fits as arguments to the functional type |u|. We have 
111
 
the following cases:
112
 
\begin{itemize}
113
 
\item If the two vectors are empty, then we are done.
114
 
\begin{code}
115
 
eqs  n  a          []        []       = return ()
116
 
\end{code}
117
 
\item If the two vectors are nonempty, then to check if 
118
 
    \texttt{u1:us1 = u2:us2 : Fun a f} we first check if \texttt{u1 = u2 : a} and 
119
 
then check \texttt{us1 = us2 : f u1}.
120
 
\begin{code}
121
 
eqs  n  (Fun a f)  (u1:us1)  (u2:us2) =
122
 
  do
123
 
  eq n a u1 u2
124
 
  eqs n (f u1) us1 us2
125
 
\end{code}
126
 
\item In all other cases the vectors are not convertible.
127
 
 
128
 
 
129
 
\begin{code}
130
 
eqs  _  _          _         _        = fail "eqs" 
131
 
\end{code}
132
 
\end{itemize}