← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/core/Val.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/Val.lhs
1
 
\section{Val: Values}
2
 
%if False %% only to be seen by the Haskell compiler
3
 
\begin{code}
4
 
module Val where
5
 
\end{code}
6
 
\%endif
7
 
 
8
 
We are using the functions in Haskell to represent the functional
9
 
values in the core language.
10
 
 
11
 
Constants (i.e. either explicitly defined (abbreviations), implicitly
12
 
defined (recursively defined or data types) are represented together
13
 
with their concrete name (a string) and their type (which is a
14
 
value). A generic value is represented in the same way, except that it
15
 
also have an integer which is used to distinguish it from other
16
 
generic values.
17
 
 
18
 
The set of values is defined by the following domain equation:
19
 
\begin{displaymath}
20
 
  \Val = \lambda\ ( \Val\  \to\  \Val)
21
 
 ||\  \App\  \Hh\  \Val ^*\ ||\  \Set\ 
22
 
 ||\  \Fun\  \Val\  (\Val\  \to \Val)
23
 
\end{displaymath}
24
 
This can be expressed in Haskell by the following data type:
25
 
\begin{code}
26
 
data Val =
27
 
     Lam (Val -> Val)
28
 
  |  App Head [Val]
29
 
  |  Set
30
 
  |  Fun Val (Val -> Val)
31
 
\end{code}
32
 
The head of a function application is either a constant or a generic
33
 
     variable. In both cases it is represented as a name together with
34
 
     its type. A generic variable comes together with an integer to distinguish it
35
 
     from other generic variables. We use the function |typH| to
36
 
     compute the type of a head. 
37
 
\begin{code}
38
 
data Head =
39
 
     Gen Int Name Val           -- generic variables
40
 
  |  Const Name Val             -- constants
41
 
eqH                              :: Head -> Head -> Bool
42
 
eqH  (Gen n1 _ _)  (Gen n2 _ _)  = n1 == n2
43
 
eqH  (Const s1 _)  (Const s2 _)  = s1 == s2
44
 
eqH  _             _             = False
45
 
 
46
 
type Name = String
47
 
 
48
 
typH               :: Head -> Val
49
 
typH  (Gen _ _ v)  = v
50
 
typH  (Const _ v)  = v
51
 
\end{code}
52
 
We need functions to convert a constant and a type to a head applied
53
 
   to no arguments:
54
 
\begin{code}
55
 
mvar    :: Head -> Val
56
 
mvar h  = App h []
57
 
 
58
 
mconst      :: Name -> Val -> Val
59
 
mconst s v  = mvar (Const s v) 
60
 
\end{code}
61
 
The expression |apps v [v1; ...; vn]| computes the application
62
 
 |v v1 ... vn|
63
 
\begin{code}
64
 
apps                       :: Val -> [Val] -> Val
65
 
apps  v            []      = v
66
 
apps  (Lam f)      (u:us)  = apps (f u) us
67
 
apps  (App h us)   vs      = App h (us ++ vs)
68
 
 
69
 
app        :: Val -> Val -> Val
70
 
app u1 u2  = apps u1 [u2]
71
 
\end{code}
72
 
The expression |itCurry|
73
 
 
74
 
 to be completed
75
 
 
76
 
\begin{code}
77
 
 
78
 
itCurry                  :: Val -> Val -> (Val -> Val) -> Val
79
 
itCurry u  (Fun v g)  f  = Fun v (\ w -> itCurry (app u w) (g w) f)
80
 
itCurry u  _          f  = f u
81
 
 
82
 
inst :: Val -> [Val] -> Val
83
 
inst  w          []     = w
84
 
inst  (Fun _ f)  (u:us) = inst (f u) us
85
 
  
86
 
\end{code}
87