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
|
canon.lit - Area canonicalization
=================================
Description
-----------
This script defines functions for folding areas and generating canonical
forms from them for renewed symbolic reduction.
------------------------------------------------------------------------
Interface
---------
Exported identifiers:
> %export
> canonise || Transform an area into canonical form
> foldarea || Fold an area to an application of its assigned symbol
> labelarea || Use a list of symbols to label a list of areas
------------------------------------------------------------------------
Includes
--------
> %include "basic.lit" -uncurry -split
> %include "graph.lit" -extgraph
> %include "rule.lit"
------------------------------------------------------------------------
`Canonise heap' canonises an area to a standard form, so that equal
areas are detected by the `=' operator. Canonisation is done in three
steps:
(1) Splitting arguments to prevent too much sharing and allowing delta
functions to be recognised.
(2) Adding extra arguments to the full complement according to the type
rule for the top symbol.
(3) Relabeling the nodes in a standard way.
> canonise :: (*->rule **** *****) -> [***] -> rgraph * ** -> rgraph * ***
> canonise typerule heap = relabel heap.uncurry typerule.split.relabel localheap
> split :: rgraph * num -> rgraph * num
> split rgraph
> = foldsingleton single rgraph rgraph
> where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (localheap--[root]))) emptygraph)
> uncurry :: (*->rule **** *****) -> rgraph * num -> rgraph * num
> uncurry typerule rgraph
> = f (nc root)
> where f (True,(sym,args))
> = mkrgraph root (updategraph root (sym,fst (claim targs (args++localheap--nodelist graph [root]))) graph)
> where targs = lhs (typerule sym)
> f cont = rgraph
> nc = nodecontents graph
> root = rgraphroot rgraph; graph = rgraphgraph rgraph
> localheap = [0..]
------------------------------------------------------------------------
> foldarea :: (rgraph * **->*) -> rgraph * ** -> (*,[**])
> foldarea label rgraph
> = (label rgraph,foldsingleton single nosingle rgraph)
> where single root sym args = args
> nosingle = snd (nodeset (rgraphgraph rgraph) [rgraphroot rgraph])
------------------------------------------------------------------------
> labelarea :: [rgraph * **] -> [*] -> rgraph * ** -> *
> labelarea areas labels
> = foldmap id nolabel (maketable areas labels)
> where nolabel = error "labelarea: no label assigned to area"
> maketable :: [rgraph * **] -> [*] -> [(rgraph * **,*)]
> maketable [] = const []
> maketable (area:areas) labels
> = (area,label):maketable areas labels'
> where (label,labels') = getlabel (nc aroot) labels
> getlabel (True,(asym,aargs)) labels = (asym,labels), if ~or (map (fst.nc) aargs)
> getlabel acont (label:labels) = (label,labels)
> getlabel = error "maketable: out of labels"
> nc = nodecontents agraph
> aroot = rgraphroot area; agraph = rgraphgraph area
------------------------------------------------------------------------
> relabel :: [***] -> rgraph * ** -> rgraph * ***
> relabel heap rgraph
> = mkrgraph (move root) graph'
> where root = rgraphroot rgraph; graph = rgraphgraph rgraph
> nodes = nodelist graph [root]
> table = zip2 nodes heap
> move = foldmap id nonew table
> nonew = error "relabel: no new node assigned to node"
> graph' = foldr addnode emptygraph table
> addnode (node,node')
> = updategraph node' (sym,map move args), if def
> = id, otherwise
> where (def,(sym,args)) = nc node
> nc = nodecontents graph
> foldsingleton
> :: (**->*->[**]->***) ->
> *** ->
> rgraph * ** ->
> ***
> foldsingleton single nosingle rgraph
> = f (nc root)
> where f (True,(sym,args)) = single root sym args, if ~or (map (fst.nc) args)
> f cont = nosingle
> nc = nodecontents graph
> root = rgraphroot rgraph; graph = rgraphgraph rgraph
|
