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
|
implementation module complete
// $Id$
import graph
import basic
import StdEnv
/*
To check completeness of patterns, we need to know whether, given a list
of (constructor) symbols, this list completely covers a type.
complete :: [sym] -> Bool
It is assumed that a type can never be empty, so an empty list of
constructors can never cover a type. Otherwise, separate type
information would be needed to determine the completeness of an empty
list of constructors.
The algorithm uses /multipatterns/, which are lists of simple patterns. A
multipattern is used to match at multiple node-ids in a graph in parallel.
This is necessary in the case of matching of product types.
*/
:: Pattern sym var
:== (Graph sym var,[var])
/*
Coveredby checks whether a multipattern is covered by a list of
multipatterns. There are five cases to consider.
First, if the multipattern is not the empty list, then to cover it
some multipattern must exist, so if the list of multipatterns is
empty, then the multipattern is not covered.
Second, if the multipattern is the empty list, it is trivially
covered by any list of multipatterns, including the empty.
Third, if the first pattern of the multipattern is closed, we select
only the multipatterns that it can match, then continue with the
arguments, and then the rest of the multipattern.
Fourth, if the first pattern of the multipattern is open, and all
its type constructors are present in the first patterns of the
multipatterns in the list of multipatterns, then the first pattern
of the multipattern is split according to all constructors, and all
possibilities must be covered.
Fifth, if not all constructors are present, then the multipatterns
of which the first pattern is open must cover the multipattern. So
those are selected and we continue with the tails of the
multipatterns in this list.
To understand the order of the first two cases, check how a single open
integer pattern is covered by a list of integer patterns either
containing or not containing an open pattern.
*/
coveredby
:: ([sym]->Bool)
(Graph sym var)
![Pattern sym pvar]
[var]
-> Bool
| == sym
& == var
& == pvar
coveredby complete subject [] svars = False
coveredby complete subject pvarss [] = True
coveredby complete subject pvarss [svar:svars]
| sdef
= coveredby complete subject tmpvalue (sargs++svars)
| complete (map fst3 closeds)
= and (map covered closeds)
= coveredby complete subject opens svars
where (opens,closeds) = psplit pvarss
covered (sym,repvar`,pvarss`) = coveredby complete subject pvarss` (repvar (repvar` dummyvar) svar++svars)
(sdef,(ssym,sargs)) = varcontents subject svar
tmpvalue = (fst (foldr (spl (repvar sargs) ssym) ([],[]) pvarss))
dummyvar = abort "complete: error: accessing dummy variable"
repvar pvars svar = map (const svar) pvars
/*
Split splits a list of multipatterns into parts; on one hand, those of
which the first pattern is open, and on the other hand, for every
constructor, the list of applicable multipatterns, in which case the
multipatterns with an open pattern are expanded and added as well.
*/
psplit
:: [Pattern sym var]
-> ( [Pattern sym var]
, [ ( sym
, var->[var]
, [Pattern sym var]
)
]
)
| == sym
& == var
psplit [] = ([],[])
psplit [(subject,[svar:svars]):svarss]
| not sdef
= ([(subject,svars):opens`],map add closeds`)
= (opens,[(ssym,repvar,[(subject,sargs++svars):ins]):closeds])
where (opens`,closeds`) = psplit svarss
add (sym,repvar,svarss`) = (sym,repvar,[(subject,repvar svar++svars):svarss`])
(opens,closeds) = psplit outs
(ins,outs) = foldr (spl repvar ssym) ([],[]) svarss
repvar svar = map (const svar) sargs
(sdef,(ssym,sargs)) = varcontents subject svar
/*
Spl, given a symbol, derives two lists of multipatterns from one. The
first are the multipatterns of which the first pattern can match the
symbol, i.e. open ones and closed ones with the correct symbol. The
second are the multipatterns that can match other symbols, i.e. also
open ones, and closed ones with the wrong symbol.
*/
spl
:: (var -> [var])
sym
(Pattern sym var)
([Pattern sym var],[Pattern sym var])
-> ([Pattern sym var],[Pattern sym var])
| == sym
& == var
spl repvar sym (subject,[svar:svars]) (ins,outs)
| not sdef
= ([(subject,repvar svar++svars):ins],[(subject,[svar:svars]):outs])
| ssym==sym
= ([(subject,sargs++svars):ins],outs)
= (ins,[(subject,[svar:svars]):outs])
where (sdef,(ssym,sargs)) = varcontents subject svar
|
