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
|
implementation module extract
// $Id$
/*
extract.lit - Folding of subject graphs
=======================================
Description
-----------
This module defines functions that can fold subject graphs, as they are
usually found at the tips of the trace of a symbolic reduction process.
Three versions are provided; `actualfold' for folding initiated by
autorecursion, `splitrule' for folding initiated by introduced recursion
and `finishfold' for folding initiated without recursion.
------------------------------------------------------------
Interface
---------
Exported identifiers:
> %export
> actualfold || Fold subject graph according to autorecursion
> splitrule || Fold subject graph according to introduced recursion
> finishfold || Finish folding by introducing areas
------------------------------------------------------------
Includes
--------
> %include "dnc.lit"
> %include "../src/basic.lit"
> %include "../src/pfun.lit"
> %include "../src/graph.lit"
> %include "../src/rule.lit"
------------------------------------------------------------
Implementation
--------------
`Actualfold foldarea foldcont hist rule' is the result of
folding occurrences of areas in `hist' to `foldcont', and introducing new
areas for parts that aren't folded.
`Self' determines whether an instance of a history graph is the history
graph itself. We don't want to fold back something we unfolded earlier!
> actualfold ::
> [**] ->
> [**] ->
> (rgraph * **->(*,[**])) ->
> (***->**->bool) ->
> (*,[***]) ->
> [(***,graph * ***)] ->
> rule * ** ->
> optional (rule * **,[rgraph * **])
> actualfold deltanodes rnfnodes foldarea self foldcont hist rule
> = Absent, if list3=[]
> = Present (mkrule rargs rroot rgraph'',areas'), otherwise
> where rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule
> list2 = map (pairwith (findoccs hist rule)) (nodelist rgraph [rroot]--nodelist rgraph rargs)
> || list2: list combining every node with list of every instantiable history graph
> list3 = [(rnode,hgraph,mapping)|(rnode,(((hroot,hgraph),mapping):rest))<-list2]
> || list3: list combining every instantiable node with first instantiable history graph
> rgraph'
> = foldr foldrec rgraph list3
> where foldrec (rnode,hgraph,mapping) = updategraph rnode (mapsnd (map (lookup mapping)) foldcont)
> (rgraph'',areas') = finishfold foldarea fixednodes singlenodes rroot rgraph'
> fixednodes = intersect (mkset (argnodes++foldednodes++rnfnodes)) (nodelist rgraph' [rroot])
> singlenodes = intersect deltanodes (nodelist rgraph' [rroot])
> argnodes = nodelist rgraph' rargs
> foldednodes = map fst3 list3
> findoccs
> :: [(***,graph * ***)] ->
> rule * ** ->
> ** ->
> [((***,graph * ***),[(***,**)])]
> findoccs hist rule rnode
> = [ ((hroot,hgraph),mapping)
> | ((hroot,hgraph),(seen,mapping,[]))<-list1 || Find instantiable history rgraphs...
> ; unshared rnode (hroot,hgraph) mapping || ...which don't have shared contents...
>|| ; ~self hroot rnode || ...and aren't the history graph itself
> ]
> where rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule
> list1
> = [((hroot,hgraph),inst (hroot,hgraph))|(hroot,hgraph)<-hist]
> where inst (hroot,hgraph)
> = instantiate (hgraph,rgraph) (hroot,rnode) ([],[],[])
> || list1: all instantiation attempts at rnode with the history rgraphs
> unshared rnode (hroot,hgraph) mapping
> = disjoint inner outer
> where inner = map (lookup mapping) (fst (nodeset hgraph [hroot]))
> outer = nodelist (prunegraph rnode rgraph) (rroot:rargs)--[rnode]
------------------------------------------------------------------------
Splitting a rule into areas to fold to a certain area
> splitrule
> :: (rgraph * **->(*,[**])) ->
> [**] ->
> [**] ->
> rule * ** ->
> rgraph * ** ->
> (rule * **,[rgraph * **])
> splitrule fold rnfnodes deltanodes rule area
> = (mkrule rargs rroot rgraph'',area':areas)
> where
> rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule
> aroot = rgraphroot area; agraph = rgraphgraph area
> (rgraph'',areas) = finishfold fold fixednodes deltanodes rroot rgraph'
> fixednodes = intersect (mkset (aroot:nodelist rgraph' rargs++rnfnodes)) (nodelist rgraph' [rroot])
> rgraph' = updategraph aroot (fold area') rgraph
> area' = mkrgraph aroot agraph'
> agraph' = foldr addnode emptygraph ins
> ins = nodelist agraph [aroot]--outs
> outs = nodelist (prunegraph aroot rgraph) (rroot:rargs++snd (nodeset agraph [aroot]))--[aroot]
> addnode node = updategraph node (snd (dnc (const "in splitrule") rgraph node))
------------------------------------------------------------
`Finishfold foldarea fixednodes root graph' finishes folding of a graph
by introducing areas for parts of the graph that are not fixed in some
way (e.g. when part of the pattern of the rule, already folded, or
bearing a delta function symbol).
> finishfold
> :: (rgraph * **->(*,[**])) ->
> [**] ->
> [**] ->
> ** ->
> graph * ** ->
> (graph * **,[rgraph * **])
> finishfold foldarea fixednodes singlenodes root graph
> = (graph',areas)
> where graph' = foldr foldarea' graph areas
> foldarea' area = updategraph (rgraphroot area) (foldarea area)
> areas = depthfirst generate process arearoots
> process aroot
> = mkrgraph aroot (foldr addnode emptygraph ins)
> where outs_and_aroot = nodelist (prunegraph aroot graph) arearoots++fixednodes
> ins = aroot:nodelist graph [aroot]--outs_and_aroot
> generate area
> = snd (nodeset agraph [aroot])--fixednodes
> where aroot = rgraphroot area; agraph = rgraphgraph area
> arearoots = mkset (root:singlenodes++singfixargs)--fixednodes
> singfixargs = concat (map arguments (singlenodes++fixednodes))
> arguments node
> = args, if def
> = [], otherwise
> where (def,(sym,args)) = dnc (const "in finishfold/1") graph node
> addnode node
> = updategraph node cnt, if def
> = id, otherwise
> where (def,cnt) = dnc (const "in finishfold/2") graph node
*/
|
