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
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
|
implementation module loop
import trace
import strat
import history
import spine
import rewr
import rule
import graph
import pfun
import basic
import StdEnv
/*
loop.lit - Looping to produce a trace
=====================================
Description
-----------
This module describes the transformation of a tree of spines into a
trace. This is where the actual transformations on graphs are applied
like instantiation, reduction or strict annotation.
------------------------------------------------------------
Types
-----
*/
/* The action itself takes various arguments, and returns a transformation
*/
:: Action sym var pvar
:== (Actcont sym var pvar) // Continuation to do subsequent symbolic reduction
(History sym var) // Termination patterns
(Failinfo sym var pvar) // Failed matches
Bool // Instantiation attempted
[Bool] // Strict arguments of function to generate
var // Root of subject graph
(Graph sym var) // Subject graph
[var] // Heap of unused nodes
-> Transformation sym var pvar
/* Action continuation
An action continuation takes the result of a single partial evaluation action,
and ultimately collects all suchs actions into a trace.
*/
:: Actcont sym var pvar
:== (History sym var) // Termination patterns
(Failinfo sym var pvar) // Failed matches
Bool // Instantiation attempted
[Bool] // Strict arguments of function to generate
var // Root of subject graph
(Graph sym var) // Subject graph
[var] // Heap of unused nodes
-> Trace sym var pvar
/* Failinfo is a function type
A function of this type assigns a list of rooted graphs to a varable.
This list of rooted graphs are precisely those patterns that symfailedsym to
match at the given variable in the subject graph.
*/
:: Failinfo sym var pvar
:== var
-> [Rgraph sym pvar]
/*
------------------------------------------------------------
Implementation
--------------
*/
loop
:: (((Graph sym pvar) pvar var -> ub:Bool) -> Strategy sym var pvar (Answer sym var pvar))
([Rgraph sym pvar] (Rgraph sym pvar) -> ub:Bool)
!(.[var],.Rule sym var)
-> Trace sym var pvar
| == sym
& == var
& == pvar
loop strategy matchable (initheap,rule)
= maketrace inithistory initfailinfo initinstdone initstricts initsroot initsubject initheap
where maketrace history failinfo instdone stricts sroot subject heap
= Trace stricts (mkrule sargs sroot subject) answer history transf
where answer = makernfstrategy history (strategy matchable`) rnfnodes sroot subject
transf = transform sroot sargs answer maketrace history failinfo instdone stricts sroot subject heap
rnfnodes = removeDup (listselect stricts sargs++fst (graphvars subject sargs))
matchable` pgraph pnode snode
= matchable (failinfo snode) (mkrgraph pnode pgraph)
inithistory = []
initfailinfo = const []
initinstdone = False
initstricts = map (const False) sargs
sargs = arguments rule; initsroot = ruleroot rule; initsubject = rulegraph rule
listselect :: [.Bool] [.elem] -> [.elem]
listselect _ _ = undef
initrule
:: ![var]
(sym->[pvar])
sym
-> ([var],Rule sym var)
initrule [root:heap] template sym
= (heap`,mkrule args root (updategraph root (sym,args) emptygraph))
where (args,heap`) = claim (template sym) heap
initrule _ _ _
= abort "initrule: out of heap space"
/* ------------------------------------------------------------------------ */
transform
:: var // Top of spine (starting point for strategy)
[var] // Arguments of function to generate
!(Answer sym var pvar) // Result of strategy
-> Action sym var pvar
| == var
& == pvar
transform anode sargs (Present spine)
= selectfromtip (spinetip spine)
where selectfromtip (nid,Open rgraph) = tryinstantiate nid rgraph anode sargs
selectfromtip (nid,Redex rule matching) = tryunfold nid rule matching spine
selectfromtip (nid,Strict) = tryannotate nid sargs
selectfromtip spine = dostop
transform anode sargs Absent
= dostop
// ==== ATTEMPT TO INSTANTIATE A FREE VARIABLE WITH A PATTERN ====
tryinstantiate
:: var // The open node
(Rgraph sym pvar) // The pattern to instantiate with
var // The root of the spine
[var] // Arguments of the function to generate
-> Action sym var pvar
| == var
& == pvar
tryinstantiate onode rpattern anode sargs
= act
where act continue history failinfo instdone stricts sroot subject heap
| anode==sroot // Check if strategy applied at root
&& goodorder strictargs sargs subject subject` // Check if order of arguments of rule ok
= Instantiate success fail
= Stop
where success = continue history failinfo True stricts` sroot subject` heap`
fail = continue history failinfo` True stricts` sroot subject heap
failinfo` = adjust onode [rpattern:failinfo onode] failinfo
(heap`,subject`) = instantiate pgraph proot onode (heap,subject)
proot = rgraphroot rpattern; pgraph = rgraphgraph rpattern
stricts` = if instdone stricts (map2 ((||) o (==) onode) sargs stricts)
// Quickly annotate the open node as strict if this is the first instantiation
strictargs = [sarg\\(True,sarg)<-zip2 stricts` sargs]
goodorder
:: [var]
[var]
(Graph sym var)
(Graph sym var)
-> Bool
| == var
goodorder stricts sargs subject subject`
= startswith match match`
where match = removeMembers (fst (graphvars subject sargs)) stricts
match` = removeMembers (fst (graphvars subject` sargs)) stricts
// See if second argument list has the first one as its initial part
startswith
:: .[elem] // list S
.[elem] // list L
-> .Bool // whether L starts with S
| == elem
startswith [] _ = True
startswith [x:xs] [y:ys]
| x==y
= startswith xs ys
startswith _ _ = False
// ==== ATTEMPT TO UNFOLD A REWRITE RULE ====
tryunfold
:: var // The root of the redex
(Rule sym pvar) // The rule to unfold
(Pfun pvar var) // The matching from rule's pattern to subject
(Spine sym var pvar) // The spine returned by the strategy
-> Action sym var pvar
| == var
& == pvar
tryunfold redexroot rule matching spine
= act
where act continue history failinfo instdone stricts sroot subject heap
= Reduce reductroot trace
where (heap`,sroot`,subject`,matching`)
= xunfold redexroot rule (heap,sroot,subject,matching)
noredir = abort "transtree: no mapping foor root of replacement"
reductroot = total noredir matching` (ruleroot rule)
redirect = adjust redexroot reductroot id
history` = extendhistory subject redirect spine history
trace = continue history` failinfo instdone stricts sroot` subject` heap`
tryannotate
:: var // The node to be made strict
[var] // Arguments of the function to generate
-> Action sym var pvar
| == var
tryannotate strictnode sargs
= act
where act continue history failinfo instdone stricts sroot subject heap
| not instdone && isMember strictnode sargs
= Annotate trace
= Stop
where stricts` = map2 ((||) o (==) strictnode) sargs stricts
trace = continue history failinfo instdone stricts` sroot subject heap
// ==== STOP PARTIAL EVALUATION ====
dostop
:: Action sym var pvar
dostop
= ds
where ds continue history failinfo instdone stricts sroot subject heap = Stop
|
