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
|
implementation module spine
// $Id$
import rule
import pfun
import basic
import StdEnv
/*
spine.lit - The extended functional strategy
============================================
Description
-----------
This script implements the strategy answer, and a function to compute it
for a given graph in a rewrite system.
The strategy answer is a spine -- in principle a colon of partial
matches from patterns of rewrite rules to the graph, with at the bottom
the insteresting part: a redex, an open node or something else. See the
definition of subspine for that.
The strategy function attempts to find a redex to reduce the graph to
normal form instead of root normal form. This is done by applying a
root normal form strategy recursively in preorder over the graph (of
course ignoring cycles). The node at which the root normal form
strategy was applied is returned in the strategy answer, so laziness can
be preserved.
------------------------------------------------------------
Interface
---------
Exported identifiers:
> %export
> answer || Strategy answer type
> foldspine || Higher order general spine folding
> ifopen || Check for answer indicating Open
> printanswer || Make a human-readable representation of an answer
> printspine || Make a human-readable representation of a spine
> showanswer || Make a representation of an answer
> showspine || Make a representation of a spine
> showsubspine || Make a representation of a subspine
> spine || Colon of partial matches
> spinenodes || Determine nodes in a spine
> spinetip || Determine bottom of spine
> subspine || Bottom of spine
> history || Symbolic reduction history type
> printhistory || Make a human-readable representation of a history
> showhistory || Make a representation of a history
Required types:
subspine - rule@rule.lit,rgraph@rule.lit,pfun@pfun.lit
------------------------------------------------------------
Includes
--------
> %include "basic.lit" || optional
> %include "pfun.lit" || pfun
> %include "graph.lit" || graph
> %include "rule.lit" || rgraph rule
------------------------------------------------------------
Implementation
--------------
Answer describes the answer of a strategy. Absence of a spine implies
that the node was in root normal form.
> answer * ** *** == optional (spine * ** ***)
> showanswer showa showb showc = showoptional (showspine showa showb showc)
> printanswer printa printb printc = foldoptional ["Rnf"] (printspine printa printb printc)
*/
:: Answer sym var pvar
:== Optional (Spine sym var pvar)
/*
Spine describes the spine returned by a strategy. It contains the node
at which the strategy was applied, and the result for that node.
> spine * ** *** == (**,subspine * ** ***)
> showspine showa showb showc = showpair showb (showsubspine showa showb showc)
> printspine printa printb printc
> = foldspine pair cycle delta force missingcase open partial unsafe redex strict
> where pair node (line,lines) = (printb node++" => "++line):lines
> cycle = ("Cycle",[])
> delta = ("Delta",[])
> force lines = ("Force",lines)
> missingcase = ("MissingCase",[])
> open rgraph = ("Open "++printrgraph printa printc rgraph,[])
> partial rule matching lines = ("Partial <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,lines)
> unsafe rgraph = ("Unsafe "++printrgraph printa printb rgraph,[])
> redex rule matching = ("Redex <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,[])
> strict = ("Strict",[])
*/
:: Spine sym var pvar
:== (var,Subspine sym var pvar)
/*
Subspine describes what was the result of the strategy applied to a node
in a graph.
> subspine * ** ***
> ::= Cycle | || The spine contains a cycle
> Delta | || An imported (delta) rule was found
> Force (spine * ** ***) | || Global strictness annotation forced evaluation of a subgraph
> MissingCase | || All alternatives failed for a function symbol
> Open (rgraph * ***) | || Need root normal form of open node for matching
> Partial (rule * ***) (pfun *** **) (spine * ** ***) | || A rule was strictly partially matched
> Unsafe (rgraph * **) | || Terminated due to immininent recursion
> Redex (rule * ***) (pfun *** **) | || Total match
> Strict || Need root normal form due to strictness
> showsubspine showa showb showc
> = sh
> where sh Cycle = "Cycle"
> sh Delta = "Delta"
> sh (Force spine) = "(Force "++showspine showa showb showc spine++")"
> sh MissingCase = "MissingCase"
> sh (Open rgraph) = "(Open "++showrgraph showa showc rgraph++")"
> sh (Partial rule matching spine) = "(Partial "++showrule showa showc rule++' ':showpfun showc showb matching++' ':showspine showa showb showc spine++")"
> sh (Unsafe rgraph) = "(Unsafe "++showrgraph showa showb rgraph++")"
> sh (Redex rule matching) = "(Redex "++showrule showa showc rule++' ':showpfun showc showb matching++")"
> sh Strict = "Strict"
printsubspine printa printb printc
= pr
where pr Cycle = "Cycle"
pr Delta = "Delta"
pr (Force spine) = "(Force "++printspine printa printb printc spine++")"
pr MissingCase = "MissingCase"
pr (Open rgraph) = "(Open "++printrgraph printa printc rgraph++")"
pr (Partial rule matching spine) = "(Partial "++printrule printa printc rule++' ':printpfun printc printb matching++' ':printspine printa printb printc spine++")"
pr (Unsafe rgraph) = "(Unsafe "++printrgraph printa printb rgraph++")"
pr (Redex rule matching) = "(Redex "++printrule printa printc rule++' ':printpfun printc printb matching++")"
pr Strict = "Strict"
*/
:: Subspine sym var pvar
= Cycle // The spine contains a cycle
| Delta // An imported (delta) rule was found
| Force (Spine sym var pvar) // Global strictness annotation forced evaluation of a subgraph
| MissingCase // All alternatives failed for a function symbol
| Open (Rgraph sym pvar) // Need root normal form of open node for matching
| Partial (Rule sym pvar) (Pfun pvar var) (Spine sym var pvar) // A rule was strictly partially matched
| Unsafe (Rgraph sym var) // Terminated due to immininent recursion
| Redex (Rule sym pvar) (Pfun pvar var) // Total match
| Strict // Need root normal form due to strictness
/*
> foldspine
> :: (**->****->*****) ->
> **** ->
> **** ->
> (*****->****) ->
> **** ->
> (rgraph * ***->****) ->
> (rule * ***->pfun *** **->*****->****) ->
> (rgraph * **->****) ->
> (rule * ***->pfun *** **->****) ->
> **** ->
> spine * ** *** ->
> *****
> foldspine pair cycle delta force missingcase open partial unsafe redex strict
> = fold
> where fold (node,subspine) = pair node (foldsub subspine)
> foldsub Cycle = cycle
> foldsub Delta = delta
> foldsub (Force spine) = force (fold spine)
> foldsub MissingCase = missingcase
> foldsub (Open rgraph) = open rgraph
> foldsub (Partial rule matching spine) = partial rule matching (fold spine)
> foldsub (Unsafe rgraph) = unsafe rgraph
> foldsub (Redex rule matching) = redex rule matching
> foldsub Strict = strict
*/
foldspine
:: !(var .subresult -> .result)
.subresult
.subresult
(.result -> .subresult)
.subresult
((Rgraph sym pvar) -> .subresult)
((Rule sym pvar) (Pfun pvar var) .result -> .subresult)
((Rgraph sym var) -> .subresult)
((Rule sym pvar) (Pfun pvar var) -> .subresult)
.subresult
.(Spine sym var pvar)
-> .result
foldspine pair cycle delta force missingcase open partial unsafe redex strict spine
= fold spine
where fold spine
= pair node (foldsub subspine)
where (node,subspine) = spine
foldsub Cycle = cycle
foldsub Delta = delta
foldsub (Force spine) = force (fold spine)
foldsub MissingCase = missingcase
foldsub (Open rgraph) = open rgraph
foldsub (Partial rule matching spine) = partial rule matching (fold spine)
foldsub (Unsafe rgraph) = unsafe rgraph
foldsub (Redex rule matching) = redex rule matching
foldsub Strict = strict
spinetip :: !(Spine sym var pvar) -> Spine sym var pvar
spinetip (_,Force spine) = spinetip spine
spinetip (_,Partial _ _ spine) = spinetip spine
spinetip spine = spine
spinenodes :: .(Spine sym var pvar) -> [var]
spinenodes spine
= foldspine cons [] [] id [] (const []) partial (const []) redex [] spine
where partial _ _ = id
redex _ _ = []
ifopen :: result result !.(Answer sym var pvar) -> result
ifopen open other spine
= foldoptional other (checkopen o spinetip) spine
where checkopen (onode,Open pattern) = open
checkopen tip = other
|
