extract.icl 7.44 KB
Newer Older
1
2
3
4
implementation module extract

// $Id$

5
6
7
8
9
10
11
import rule
import dnc
import graph
import basic
from general import Yes,No
import StdEnv

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
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!
62
*/
63

64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
actualfold ::
    [var]
    [var]
    ((Rgraph sym var)->Node sym var)
    (pvar->var->bool)
    (sym,[pvar])
    [(pvar,Graph sym pvar)]
    (Rule sym var)
 -> Optional (Rule sym var,[Rgraph sym var])
 |  == var
 &  == pvar

actualfold deltanodes rnfnodes foldarea self foldcont hist rule
| isEmpty list3
  = No
= Yes (mkrule rargs rroot rgraph``,areas`)
  where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule

        list2 = map (pairwith (findoccs hist rule)) (removeMembers (varlist rgraph [rroot]) (varlist rgraph rargs))
        // list2: list combining every node with list of every instantiable history graph

85
        list3 = [(rnode,mapping) \\ (rnode,[mapping:_])<-list2]
86
87
88
89
        // list3: list combining every instantiable node with first instantiable history graph

        rgraph`
        = foldr foldrec rgraph list3
90
          where foldrec (rnode,mapping) = updategraph rnode (mapsnd (map (lookup mapping)) foldcont)
91
92
93
94
95

        (rgraph``,areas`) = finishfold foldarea fixednodes singlenodes rroot rgraph`
        fixednodes = intersect (removeDup (argnodes++foldednodes++rnfnodes)) (varlist rgraph` [rroot])
        singlenodes = intersect deltanodes (varlist rgraph` [rroot])
        argnodes = varlist rgraph` rargs
96
        foldednodes = map fst list3
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
>   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]
122
123
124
125
126
127
*/

findoccs ::
    [(pvar,Graph sym pvar)]
    (Rule sym var)
    var
128
 -> [[(pvar,var)]]
129
130
131
132
 |  == var
 &  == pvar

findoccs hist rule rnode
133
= [  mapping
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
  \\ ((hroot,hgraph),(seen,mapping,[]))<-list1 // Find instantiable history rgraphs...
  |  unshared rnode (hroot,hgraph) mapping     // ...which don't have shared contents
  ]
  where rargs = arguments rule; rroot = ruleroot 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 (graphvars hgraph [hroot]))
                outer = removeMembers (varlist (prunegraph rnode rgraph) [rroot:rargs]) [rnode]

instantiate = undef
150

151
/*
152
153
154
155
------------------------------------------------------------------------


Splitting a rule into areas to fold to a certain area
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
splitrule ::
    ((Rgraph sym var)->Node sym var)
    [var]
    [var]
    (Rule sym var)
    (Rgraph sym var)
 -> (Rule sym var,[Rgraph sym var])
 |  == var

splitrule fold rnfnodes deltanodes rule area
= (mkrule rargs rroot rgraph``,[area`:areas])
  where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule
        aroot = rgraphroot area; agraph = rgraphgraph area

        (rgraph``,areas) = finishfold fold fixednodes deltanodes rroot rgraph`
        fixednodes = intersect (removeDup [aroot:varlist rgraph` rargs++rnfnodes]) (varlist rgraph` [rroot])
        rgraph` = updategraph aroot (fold area`) rgraph
        area` = mkrgraph aroot agraph`
        agraph` = foldr addnode emptygraph ins
        ins = removeMembers (varlist agraph [aroot]) outs
        outs = removeMembers (varlist (prunegraph aroot rgraph) [rroot:rargs++snd (graphvars agraph [aroot])]) [aroot]

        addnode node = updategraph node (snd (dnc (const "in splitrule") rgraph node))
181

182
/*
183
184
185
186
187
188
189
------------------------------------------------------------


`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).
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

finishfold ::
    ((Rgraph sym var)->Node sym var)
    [var]
    [var]
    var
    (Graph sym var)
 -> (Graph sym var,[Rgraph sym var])
 |  == var

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 = varlist (prunegraph aroot graph) arearoots++fixednodes
                ins = [aroot:removeMembers (varlist graph [aroot]) outs_and_aroot]
        generate area
        = removeMembers (snd (graphvars agraph [aroot])) fixednodes
          where aroot = rgraphroot area; agraph = rgraphgraph area
        arearoots = removeMembers (removeDup [root:singlenodes++singfixargs]) fixednodes
        singfixargs = flatten (map arguments (singlenodes++fixednodes))

        arguments node
        = if def args []
          where (def,(_,args)) = dnc (const "in finishfold/1") graph node

        addnode node
        = if def (updategraph node cnt) id
          where (def,cnt) = dnc (const "in finishfold/2") graph node