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
|
implementation module rewr
import rule
import graph
import pfun
import basic
import StdEnv
/*
Rewriting of graphs
Exported identifiers:
\begin{description}
\item[\tt unfold] Apply a rewrite rule to a graph
\item[\tt xunfold] As {\tt unfold}, but also provides full matching
from the applied rule to the (resulting) subject
graph
\item[\tt fold] Apply a rewrite rule in reverse to a graph
\item[\tt instantiate] Instantiate a graph with a pattern
\end{description}
Temporarily hidden:
\begin{description}
\item[\tt build] Build a copy of a graph
\end{description}
Temporarily not exported:
\begin{description}
\item[\tt getmap] Determine mapping from one graph to another
\item[\tt existmap] Determine if a mapping from one graph to another exists
\end{description}
> %export foldfn getmapping instantiate xunfold
unfold
:: pfun *** ** -> || Mapping as result from match of lhs
rule * *** -> || Rule to unfold
([**],graph * **,**) -> || Heap,graph,node
([**],graph * **,**) || New heap,graph,node
> xunfold
> :: ** -> || Root of the redex to unfold
> rule * *** -> || Rule to unfold by
> ( [**], || Unused heap
> **, || Root of subject
> graph * **, || Subject graph
> pfun *** ** || Matching of pattern from rule to subject
> ) ->
> ( [**], || Remaining heap
> **, || Possibly redirected root of subject
> graph * **, || Extended subject graph
> pfun *** ** || Extended matching from rule to subject
> )
fold
:: pfun *** ** -> || Mapping as result from match of rhs
rule * *** -> || Rule to fold
([**],graph * **,**) -> || Heap,graph,node
([**],graph * **,**) || New heap,graph,node
> build
> :: graph * *** -> *** -> || Graph,root to be copied
> ([**],[**],graph * **,pfun *** **) -> || Heap,init nodes,init graph,init mapping
> ([**],[**],graph * **,pfun *** **) || New heap,new nodes,new graph,new mapping
> getmap :: graph * *** -> *** -> graph * ** -> ** -> pfun *** **
> existmap :: graph * *** -> *** -> graph * ** -> ** -> bool
Implementation
> %include "basic.lit"
> %include "pfun.lit"
> %include "graph.lit" -instantiate
> %include "rule.lit"
*/
xunfold
:: var
(Rule sym pvar)
!( [var]
, var
, Graph sym var
, Pfun pvar var
)
-> ( [var]
, var
, Graph sym var
, Pfun pvar var
) | == var & == pvar
xunfold redexroot rule (heap,root,subject,matching)
= (heap`,redirection root,redirectgraph redirection subject`,matching`)
where (heap`,[rhs`:_],subject`,matching`)
= build (rulegraph rule) (ruleroot rule) (heap,[],subject,matching)
redirection = adjust redexroot rhs` id
instantiate
:: .(Graph sym pvar) // Pattern to instantiate with
pvar // Root of the pattern
var // Open node to instantiate
(.[var],.Graph sym var) // Heap,graph
-> .([var],Graph sym var) // New heap,graph
| == var
& == pvar
instantiate pattern proot node (heap,graph)
| not closed
= (heap,graph)
= (heap``,graph``)
where (heap``,params``,graph``,_)
= foldr (build pattern) (heap,[],graph`,extend proot node emptypfun) params
(closed,(f,params)) = varcontents pattern proot
graph` = updategraph node (f,params``) graph
build
:: (Graph sym pvar)
pvar
( [var]
, [var]
, Graph sym var
, !Pfun pvar var
)
-> ( [var]
, [var]
, Graph sym var
, Pfun pvar var
) | == var & == pvar
build pattern node (heap,nodes,graph,mapping)
| seen
= (heap,[seenas:nodes],graph,mapping)
| not closed
= (heap`,[node`:nodes],graph,mapping`)
= (heap``,[node`:nodes],graph``,mapping``)
where (seen,seenas) = apply mapping node
[node`:heap`] = heap
mapping` = extend node node` mapping
(closed,(f,params)) = varcontents pattern node
(heap``,params``,graph``,mapping``)
= foldr (build pattern) (heap`,[],graph`,mapping`) params
graph` = updategraph node` (f,params``) graph
/*
Mapping
> getmap pattern patnode graph node
> = getmapping nomatch pattern graph (patnode,node) id emptypfun
> where nomatch = error "getmap: pattern and graph do not match"
> existmap pattern patnode graph node
> = getmapping False pattern graph (patnode,node) (const True) emptypfun
*/
getmapping
:: tsym
(Graph sym pvar)
(Graph sym var)
!(pvar,var)
((Pfun pvar var) -> tsym)
!(Pfun pvar var)
-> tsym
| == sym
& == var
& == pvar
getmapping failure patgraph graph (patnode,node) success mapping
| seen
= if (seenas==node) (success mapping) failure
| not patdef
= success mapping`
| not (def && patfunc==func && eqlen patargs args)
= failure
= foldr (getmapping failure patgraph graph) success (zip2 patargs args) mapping`
where (seen,seenas) = apply mapping patnode
(patdef,(patfunc,patargs)) = varcontents patgraph patnode
(def,(func,args)) = varcontents graph node
mapping` = extend patnode node mapping
/*
The foldfn operation folds an area of a graph back to a function call.
The following two conditions must be satisfied in order not to need a
heap of fresh nodes:
1: At least one node is freed by the fold operation to hold the root of
the redex. This is the root of the reduct; since it must be freed,
the rule that is folded by must not be a projection function;
2: No other new nodes are necessary. Therefore, all nodes of the
pattern of the rule that is folded by except the root must also
occur in the replacement.
Furthermore, the pattern of the rule is only given by its root symbol
and its arguments; the arguments are open nodes.
*/
foldfn
:: (Pfun pvar var) // Matching of replacement
sym // Symbol at root of pattern
[pvar] // Arguments of pattern
pvar // Root of replacement
(Graph sym var) // Subject graph
-> Graph sym var // Folded subject
| == pvar
foldfn matching symbol arguments replacementroot sgraph
= updategraph (domatching replacementroot) (symbol,map domatching arguments) sgraph
where domatching = total nomatching matching
nomatching = abort "foldfn: no matching of argument of pattern"
|
