blob: c2b6ce6b31445aa6b4f5e1c99077bf2273a91cbd (
plain) (
blame)
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
|
definition module strat
// $Id$
from spine import Answer
from history import History
from rule import Rule
from graph import Graph,Node
from StdOverloaded import ==
from StdClass import Eq
from cleanversion import String
from history import HistoryAssociation,HistoryPattern,Link // for History
from spine import Spine // for Answer
from spine import Subspine // for Spine
from rule import Rgraph // for History
from basic import Optional // for Spine
:: Strategy sym var pvar result
:== (Substrategy sym var pvar result)
(Graph sym var)
((Subspine sym var pvar) -> result)
result
(Node sym var)
-> result
:: Substrategy sym var pvar result
:== ((Spine sym var pvar) -> result)
result
var
-> result
:: Law sym var pvar result
:== (Substrategy sym var pvar result)
(Graph sym var)
((Subspine sym var pvar) -> result)
result
[var]
result
-> result
// Apply a strategy recursively to a graph
// by deriving the substrategy from it and feeding it back to it
// Think Y operator
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
| Eq sym
& Eq var
& Eq pvar
/* ------------------------------------------------------------------------
STRATEGY TRANSFORMERS
The funcions below tranform (simpler) strategies into more complicated ones
------------------------------------------------------------------------ */
// A strategy transformer that checks for partial applications
checkarity
:: !(sym -> Int) // Arity of function symbol
(Strategy sym var pvar .result) // Default strategy
(Substrategy sym var pvar .result) // Substrategy
(Graph sym var) // Subject graph
((Subspine sym var pvar) -> .result) // Spine continuation
.result // RNF continuation
!.(Node sym var) // Subject node
-> .result
// A strategy transformer that checks for constructor applications
checkconstr
:: (sym->String)
(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
// A strategy transformer that checks for primitive symbol applications
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
// A strategy transformer that checks (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
// A strategy transformere that checks a list of rewrite rules
// This is the real thing that characterises the functional strategy
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
// A strategy transformer that checks a function application
// for strict arguments
checkstricts
:: !(sym -> [.Bool]) // Strict arguments of function
(Strategy sym var pvar .result) // Default strategy
(Substrategy sym var pvar .result) // Substrategy
(Graph sym var) // Subject graph
((Subspine sym var pvar) -> .result) // Spine continuation
.result // RNF continuation
!.(Node sym var) // Subject node
-> .result
/* ------------------------------------------------------------------------
USEFUL AIDS FOR DEFINING STRATEGY TRANSFORMERS
The functions below are useful for inspecting a graph
such as done by a strategy transformer.
------------------------------------------------------------------------ */
// Force evaluation of stricts arguments of a node in the graph
forcenodes
:: (Substrategy sym var pvar .result)
((Subspine sym var pvar) -> .result)
.result
!.[var]
-> .result
// Try to apply a transformation rule (that doesn't need evaluated arguments)
rulelaw
:: (Rule sym pvar)
-> Law sym var pvar result
| == sym
& == var
& == pvar
// Try to apply a law
trylaw
:: (Graph sym var)
(.(Subspine sym var pvar) -> result)
.[var]
(Rule sym pvar)
result
-> result
| == sym
& == var
& == pvar
// Try a list of rewrite rules
// Requires argument evaluation for closed patterns
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
|
