1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
|
implementation module canon
// $Id$
import rule
import graph
import basic
import general
import StdEnv
/*
canon.lit - Area canonicalization
=================================
Description
-----------
This script defines functions for folding areas and generating canonical
forms from them for renewed symbolic reduction.
------------------------------------------------------------------------
Interface
---------
Exported identifiers:
> %export
> canonise || Transform an area into canonical form
> foldarea || Fold an area to an application of its assigned symbol
> labelarea || Use a list of symbols to label a list of areas
------------------------------------------------------------------------
Includes
--------
> %include "basic.lit" -uncurry -split
> %include "graph.lit" -extgraph
> %include "rule.lit"
------------------------------------------------------------------------
`Canonise heap' canonises an area to a standard form, so that equal
areas are detected by the `=' operator. Canonisation is done in three
steps:
(1) Splitting arguments to prevent too much sharing and allowing delta
functions to be recognised.
(2) Adding extra arguments to the full complement according to the type
rule for the top symbol.
(3) Relabeling the nodes in a standard way.
> canonise :: (*->rule **** *****) -> [***] -> rgraph * ** -> rgraph * ***
> canonise typerule heap = relabel heap.etaexpand typerule.splitrg.relabel localheap
*/
canonise :: (sym -> Int) [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1
canonise arity heap rg
= (relabel heap o etaexpand arity o splitrg o relabel localheap) rg
/*
> split :: rgraph * num -> rgraph * num
> split rgraph
> = foldsingleton single rgraph rgraph
> where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (localheap--[root]))) emptygraph)
*/
splitrg :: (Rgraph sym Int) -> Rgraph sym Int
splitrg rgraph
= foldsingleton single rgraph rgraph
where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (localheap--[root]))) emptygraph)
/*
> uncurry :: (*->rule **** *****) -> rgraph * num -> rgraph * num
> uncurry typerule rgraph
> = f (nc root)
> where f (True,(sym,args))
> = mkrgraph root (updategraph root (sym,fst (claim targs (args++localheap--nodelist graph [root]))) graph)
> where targs = lhs (typerule sym)
> f cont = rgraph
> nc = nodecontents graph
> root = rgraphroot rgraph; graph = rgraphgraph rgraph
*/
etaexpand :: (sym->Int) (Rgraph sym Int) -> Rgraph sym Int
etaexpand arity rgraph
= f (nc root)
where f (True,(sym,args))
= mkrgraph root (updategraph root (sym,take (arity sym) (args++(localheap--(varlist graph [root])))) graph)
f cont = rgraph
nc = varcontents graph
root = rgraphroot rgraph; graph = rgraphgraph rgraph
localheap :: [Int]
localheap =: [0..]
/*
------------------------------------------------------------------------
> foldarea :: (rgraph * **->*) -> rgraph * ** -> (*,[**])
> foldarea label rgraph
> = (label rgraph,foldsingleton single nosingle rgraph)
> where single root sym args = args
> nosingle = snd (varset (rgraphgraph rgraph) [rgraphroot rgraph])
*/
foldarea :: ((Rgraph sym var) -> sym) (Rgraph sym var) -> Node sym var | == var
foldarea label rgraph
= (labelrgraph,foldsingleton single nosingle rgraph)
where single root sym = id
nosingle = snd (graphvars (rgraphgraph rgraph) [rgraphroot rgraph])
labelrgraph = label rgraph
/*
------------------------------------------------------------------------
> labelarea :: [rgraph * **] -> [*] -> rgraph * ** -> *
> labelarea areas labels
> = foldmap id nolabel (maketable areas labels)
> where nolabel = error "labelarea: no label assigned to area"
> maketable :: [rgraph * **] -> [*] -> [(rgraph * **,*)]
> maketable [] = const []
> maketable (area:areas) labels
> = (area,label):maketable areas labels'
> where (label,labels') = getlabel (nc aroot) labels
> getlabel (True,(asym,aargs)) labels = (asym,labels), if ~or (map (fst.nc) aargs)
> getlabel acont (label:labels) = (label,labels)
> getlabel = error "maketable: out of labels"
> nc = varcontents agraph
> aroot = rgraphroot area; agraph = rgraphgraph area
*/
labelarea :: (sym->Bool) [Rgraph sym var] [sym] (Rgraph sym var) -> sym | == sym & == var
labelarea reusable areas labels rg
= foldmap id nolabel (maketable reusable areas labels) rg
where nolabel = abort "canon: labelarea: no label assigned to area"
maketable :: (sym->Bool) [Rgraph sym var] [sym] -> [(Rgraph sym var,sym)] | == var
maketable _ [] _ = []
maketable reusable [area:areas] labels
= [(area,label):maketable reusable areas labels`]
where (label,labels`) = getlabel (nc aroot) labels
getlabel (True,(asym,aargs)) labels
| reusable asym && not (or (map (fst o nc) aargs))
= (asym,labels)
getlabel acont [label:labels]
= (label,labels)
getlabel _ _
= abort "canon: maketable: out of labels"
nc = varcontents agraph
aroot = rgraphroot area; agraph = rgraphgraph area
/*
------------------------------------------------------------------------
> relabel :: [***] -> rgraph * ** -> rgraph * ***
> relabel heap rgraph
> = mkrgraph (move root) graph'
> where root = rgraphroot rgraph; graph = rgraphgraph rgraph
> nodes = nodelist graph [root]
> table = zip2 nodes heap
> move = foldmap id nonew table
> nonew = error "relabel: no new node assigned to node"
> graph' = foldr addnode emptygraph table
> addnode (node,node')
> = updategraph node' (sym,map move args), if def
> = id, otherwise
> where (def,(sym,args)) = nc node
> nc = nodecontents graph
*/
relabel :: [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1
relabel heap rgraph
= mkrgraph (move root) graph`
where root = rgraphroot rgraph; graph = rgraphgraph rgraph
nodes = varlist graph [root]
table = zip2 nodes heap
move = foldmap id nonew table
nonew = abort "relabel: no new node assigned to node"
graph` = foldr addnode emptygraph table
addnode (node,node`)
| def
= updategraph node` (sym,map move args)
= id
where (def,(sym,args)) = nc node
nc = varcontents graph
/*
> foldsingleton
> :: (**->*->[**]->***) ->
> *** ->
> rgraph * ** ->
> ***
> foldsingleton single nosingle rgraph
> = f (nc root)
> where f (True,(sym,args)) = single root sym args, if ~or (map (fst.nc) args)
> f cont = nosingle
> nc = nodecontents graph
> root = rgraphroot rgraph; graph = rgraphgraph rgraph
*/
foldsingleton ::
(var sym [var] -> pvar)
pvar
(Rgraph sym var)
-> pvar
| == var
foldsingleton single nosingle rgraph
= case nc root
of (True,(sym,args))
| not (or (map (fst o nc) args))
-> single root sym args
_
-> nosingle
where nc = varcontents graph
root = rgraphroot rgraph; graph = rgraphgraph rgraph
|
