blob: 341b55081fdb36c807c6358cee8e4fd85dada63a (
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
|
definition module strat
// $Id$
from history import History
from spine import Answer
from rule import Rule
from graph import Graph,Node
from StdOverloaded import ==
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
| == sym
& == var
& == pvar
/* ------------------------------------------------------------------------
STRATEGY TRANSFORMERS
The funcions below tranform (simpler) strategies into more complicated ones
------------------------------------------------------------------------ */
// A strategy transformer that checks for constructor applications
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
// 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 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
/* ------------------------------------------------------------------------
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
|
