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
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
|
implementation module strat
// $Id$
import history
import spine
import dnc
import rule
import graph
import pfun
import basic
import StdEnv
/*
strat.lit - Extended functional strategy
========================================
Description
-----------
Describe in a few paragraphs what this module defines.
------------------------------------------------------------
Interface
---------
Exported identifiers:
> %export
> law
> strategy
> substrategy
> makernfstrategy
> checkconstr
> checkimport
> checklaws
> checkrules
> checktype
> forcenodes
> rulelaw
> trylaw
> tryrules
Required types:
identifier - type@source.lit type@source.lit
...
------------------------------------------------------------
Includes
--------
> %include "dnc.lit"
> %include "../src/basic.lit"
> %include "../src/pfun.lit"
> %include "../src/graph.lit" -instantiate
> %include "../src/rule.lit"
> %include "../src/spine.lit"
------------------------------------------------------------
Types
-----
*/
:: Substrategy sym var pvar result
:== ((Spine sym var pvar) -> result)
result
var
-> result
:: Strategy sym var pvar result
:== (Substrategy sym var pvar result)
(Graph sym var)
((Subspine sym var pvar) -> result)
result
(Node sym var)
-> result
:: Law sym var pvar result
:== (Substrategy sym var pvar result)
(Graph sym var)
((Subspine sym var pvar) -> result)
result
[var]
result
-> result
//------------------------------------------------------------------------
makernfstrategy
:: .(History sym var) // History of previous rooted graphs attached to nodes
(Strategy sym var pvar (Answer sym var pvar)) // Strategy for a defined node
.[var] // List of nodes known in RNF (closed pattern nodes of subject rule+strict args)
var // Root of replacement
.(Graph sym var) // Subject graph
-> Answer sym var pvar
| == sym
& == var
& == pvar
makernfstrategy hist strat rnfnodes node graph
= substrat [] spinecont rnfanswer node
where spinecont spine = Present spine
rnfanswer = Absent
substrat spinenodes spinecont rnfanswer node
| isMember node spinenodes
= subspinecont Cycle
| isMember node rnfnodes
= rnfanswer
| not def
= subspinecont Strict
= strat` (substrat spinenodes`) graph subspinecont rnfanswer cnt
where (def,cnt) = dnc (const "in makernfstrategy") graph node
spinenodes` = [node:spinenodes]
subspinecont subspine = spinecont (node,subspine)
strat` = checkinstance (graph,node) histpatts strat
histpatts = foldr (foldmap (++) id hist) [] spinenodes`
/*
------------------------------------------------------------------------
NORMAL REWRITE RULE STRATEGY
*/
tryrules
:: ((Graph sym pvar) pvar var -> .Bool)
(Substrategy sym var pvar result)
.(Graph sym var)
((Subspine sym var pvar) -> result)
.[var]
-> result
[.Rule sym pvar]
-> result
| == sym
& == var
& == pvar
tryrules matchable substrat subject found sargs
= foldr (matchrule matchable substrat subject found sargs)
matchrule
:: ((Graph sym pvar) pvar var -> .Bool)
(Substrategy sym var pvar result)
.(Graph sym var)
((Subspine sym var pvar) -> result)
.[var]
.(Rule sym pvar)
result
-> result
| == sym
& == var
& == pvar
matchrule matchable substrat subject found sargs rule fail
| eqlen pargs sargs
= matchnodes matchable` subject substrat foundsub fail pattern foundmatch pairs emptypfun
= fail
where pargs = arguments rule
pattern = rulegraph rule
pairs = zip2 pargs sargs
matchable` = matchable pattern
foundsub matching spine = found (Partial rule matching spine)
foundmatch matching = found (Redex rule matching)
matchnodes
:: (pvar var -> .Bool)
.(Graph sym var)
(Substrategy sym var pvar result)
((Pfun pvar var) (Spine sym var pvar) -> result)
result
.(Graph sym pvar)
-> ((Pfun pvar var) -> result)
[.(pvar,var)]
(Pfun pvar var)
-> result
| == sym
& == var
& == pvar
matchnodes matchable subject substrat found fail pattern
= foldr matchpair
where matchpair (pnode,snode) match matching
| not (matchable pnode snode)
= fail
| not pdef
= match (extend pnode snode matching)
| not sdef
= found matching openspine
= substrat (found matching) rnfanswer snode
where openspine = (snode,Open (mkrgraph pnode pattern))
rnfanswer
| psym==ssym && eqlen pargs sargs
= foldr matchpair match` psargs matching
= fail
match` matching = match (extend pnode snode matching)
psargs = zip2 pargs sargs
(pdef,(psym,pargs)) = (dnc (const "in matchnodes (pattern)")) pattern pnode
(sdef,(ssym,sargs)) = (dnc (const "in matchnodes (subject)")) subject snode
/*
------------------------------------------------------------------------
SPECIAL LAW STRATEGY
Does not try to reduce arguments before matching.
> rulelaw
> :: rule * *** ->
> law * ** *** ****
> rulelaw rule substrat subject found rnf snids fail
> = trylaw subject found snids rule fail
> trylaw
> :: graph * ** ->
> (subspine * ** ***->****) ->
> [**] ->
> rule * *** ->
> **** ->
> ****
> trylaw graph found sargs rule fail
> = lawmatch pattern graph fail found' pairs emptypfun, if eqlen pargs sargs
> = fail, otherwise
> where pargs = lhs rule; pattern = rulegraph rule
> found' matching = found (Redex rule matching)
> pairs = zip2 pargs sargs
> lawmatch
> :: graph * *** ->
> graph * ** ->
> **** ->
> (pfun *** **->****) ->
> [(***,**)] ->
> pfun *** ** -> ****
> lawmatch pattern subject fail
> = foldr lawmatch'
> where lawmatch' (pnode,snode) success matching
> = success matching', if ~pdef
> = fail, if ~sdef \/ ssym~=psym \/ ~eqlen pargs sargs
> = foldr lawmatch' success (zip2 pargs sargs) matching', otherwise
> where matching' = extend pnode snode matching
> (pdef,(psym,pargs)) = (dnc (const "in lawmatch/1")) pattern pnode
> (sdef,(ssym,sargs)) = (dnc (const "in lawmatch/2")) subject snode
*/
rulelaw
:: .(Rule sym pvar)
-> Law sym var pvar result
| == sym
& == var
& == pvar
rulelaw rule
= law
where law substrat subject found rnf snids fail
= trylaw subject found snids rule fail
trylaw
:: .(Graph sym var)
(.(Subspine sym var pvar) -> result)
.[var]
.(Rule sym pvar)
result
-> result
| == sym
& == var
& == pvar
trylaw graph found sargs rule fail
| eqlen pargs sargs
= lawmatch pattern graph fail found` pairs emptypfun
= fail
where pargs = arguments rule; pattern = rulegraph rule
found` matching = found (Redex rule matching)
pairs = zip2 pargs sargs
lawmatch
:: .(Graph sym pvar)
.(Graph sym var)
result
-> ((Pfun pvar var) -> result)
[.(pvar,var)]
(Pfun pvar var)
-> result
| == sym
& == var
& == pvar
lawmatch pattern subject fail
= foldr lawmatch`
where lawmatch` (pnode,snode) success matching
| not pdef
= success matching`
| not sdef || ssym <> psym || not (eqlen pargs sargs)
= fail
= foldr lawmatch` success (zip2 pargs sargs) matching`
where matching` = extend pnode snode matching
(pdef,(psym,pargs)) = (dnc (const "in lawmatch (pattern)")) pattern pnode
(sdef,(ssym,sargs)) = (dnc (const "in lawmatch (subject)")) subject snode
/*
------------------------------------------------------------------------
FORCING EVALUATION OF (STRICT) ARGUMENTS
*/
forcenodes
:: (Substrategy .sym .var .pvar .result)
((Subspine .sym .var .pvar) -> .result)
.result
![.var]
-> .result
forcenodes substrat found rnf nodes
= foldr forcenode rnf nodes
where forcenode nid rnfrest = substrat foundforce rnfrest nid
foundforce spine = found (Force spine)
/*
------------------------------------------------------------------------
STRATEGY COMPOSITION
Check for an instance in the termination history.
*/
checkinstance
:: (.Graph sym var,var)
[.Rgraph sym var]
(Strategy sym var .pvar result)
-> Strategy sym var .pvar result
| == sym
& == var
& == pvar
checkinstance (graph,node) history defaultstrategy
= foldr check defaultstrategy history
where check hrgraph defaultstrategy substrat subject found rnf (ssym,sargs)
| isinstance (hgraph,hroot) (graph,node)
= found (Unsafe hrgraph)
= defaultstrategy substrat subject found rnf (ssym,sargs)
where hgraph = rgraphgraph hrgraph; hroot = rgraphroot hrgraph
// Check a type rule for curried applications and strict arguments
checktype
:: !(sym -> (Rule .tsym tvar,[.Bool]))
(Strategy sym var .pvar .result)
(Substrategy sym var .pvar .result)
.(Graph sym var)
((Subspine sym var .pvar) -> .result)
.result
!.(Node sym var)
-> .result
checktype typeinfo defaultstrategy substrat subject found rnf (ssym,sargs)
| shorter targs sargs
= rnf
| eqlen targs sargs
= forcenodes substrat found rnf` strictnodes
= abort "checktype: symbol occurrence with arity greater than its type"
where rnf` = defaultstrategy substrat subject found rnf (ssym,sargs)
(trule,tstricts) = typeinfo ssym
targs = arguments trule
strictnodes = [sarg\\(True,sarg)<-zip2 tstricts sargs]
// Check (hard coded) laws
checklaws
:: [(sym,Law sym var pvar result)]
(Strategy sym var pvar result)
(Substrategy sym var pvar result)
(Graph sym var)
((Subspine sym var pvar) -> result)
result
(Node sym var)
-> result
| == sym
checklaws laws defaultstrategy substrat subject found rnf (ssym,sargs)
= foldr checklaw (defaultstrategy substrat subject found rnf (ssym,sargs)) laws
where checklaw (lsym,law) fail
| lsym==ssym
= law substrat subject found rnf sargs fail
= fail
// Check a list of rewrite rules (this is the real thing)
checkrules
:: ((Graph sym pvar) pvar var -> .Bool)
(sym -> [.Rule sym pvar])
(Strategy sym var pvar result)
(Substrategy sym var pvar result)
(Graph sym var)
((Subspine sym var pvar) -> result)
result
(Node sym var)
-> result
| == sym
& == var
& == pvar
checkrules matchable ruledefs defstrat substrat subject found rnf (ssym,sargs)
= tryrules matchable substrat subject found sargs fail (ruledefs ssym)
where fail = defstrat substrat subject found rnf (ssym,sargs)
// Check for delta/imported/abstract/black-box (whatever) symbols
checkimport
:: !(sym->.Bool)
(Strategy sym .var .pvar .result)
(Substrategy sym .var .pvar .result)
(Graph sym .var)
((Subspine sym .var .pvar) -> .result)
.result
(Node sym .var)
-> .result
checkimport local defstrat substrat subject found rnf (ssym,sargs)
| not (local ssym)
= found Delta
= defstrat substrat subject found rnf (ssym,sargs)
// Check for constructors
checkconstr
:: (sym->.Bool)
(Strategy sym .var .pvar .result)
(Substrategy sym .var .pvar .result)
(Graph sym .var)
((Subspine sym .var .pvar) -> .result)
.result
(Node sym .var)
-> .result
checkconstr isconstr defstrat substrat subject found rnf (ssym,sargs)
| isconstr ssym
= rnf
= defstrat substrat subject found rnf (ssym,sargs)
|
