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
183
184
185
186
187
188
189
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
|
{-# OPTIONS_FRONTEND -Wno-incomplete-patterns #-}
module Analysis.TotallyDefined
( siblingCons, showSibling
, siblingConsAndDecl, showSiblingAndDecl
, Completeness(..), showComplete, showTotally, showTotalFunc
, patCompAnalysis, totalAnalysis, totalFuncAnalysis
) where
import FlatCurry.Types
import FlatCurry.Goodies
import Data.List ( delete )
import RW.Base
import System.IO
import Analysis.ProgInfo
import Analysis.Types
import Analysis.Deterministic ( isNondetDefined )
showSibling :: AOutFormat -> [(QName,Int)] -> String
showSibling _ = show
siblingCons :: Analysis [(QName,Int)]
siblingCons = simpleConstructorAnalysis "SiblingCons" consNamesArOfType
where
consNamesArOfType cdecl (Type _ _ _ consDecls) =
map (\cd -> (consName cd, consArity cd))
(filter (\cd -> consName cd /= consName cdecl) consDecls)
consNamesArOfType _ (TypeSyn _ _ _ _) = []
consNamesArOfType _ (TypeNew _ _ _ _) = []
showSiblingAndDecl :: AOutFormat -> (TypeDecl, [(QName,Int)]) -> String
showSiblingAndDecl _ = show
siblingConsAndDecl :: Analysis (TypeDecl, [(QName,Int)])
siblingConsAndDecl =
simpleConstructorAnalysis "SiblingConsAndDecl" consNamesArOfType
where
consNamesArOfType cdecl t = (t, cs)
where cs = case t of
Type _ _ _ consDecls ->
map (\cd -> (consName cd, consArity cd))
(filter (\cd -> consName cd /= consName cdecl) consDecls)
TypeSyn _ _ _ _ -> []
TypeNew _ _ _ _ -> []
data Completeness =
Complete
| InComplete
| InCompleteOr
deriving (Eq, Show, Read)
patCompAnalysis :: Analysis Completeness
patCompAnalysis =
combinedSimpleFuncAnalysis "PatComplete" siblingCons analysePatComplete
showComplete :: AOutFormat -> Completeness -> String
showComplete AText Complete = "complete"
showComplete ANote Complete = ""
showComplete _ InComplete = "incomplete"
showComplete _ InCompleteOr = "incomplete in each disjunction"
analysePatComplete :: ProgInfo [(QName,Int)] -> FuncDecl -> Completeness
analysePatComplete consinfo fdecl = anaFun fdecl
where
anaFun (Func _ _ _ _ (Rule _ e)) = isComplete consinfo e
anaFun (Func _ _ _ _ (External _)) = Complete
isComplete :: ProgInfo [(QName,Int)] -> Expr -> Completeness
isComplete _ (Var _) = Complete
isComplete _ (Lit _) = Complete
isComplete consinfo (Comb _ f es)
| f == ("Prelude","failed") = InComplete
| f == ("Prelude","commit") && length es == 1 = isComplete consinfo (head es)
| otherwise = Complete
isComplete _ (Free _ _) = Complete
isComplete _ (Let _ _) = Complete
isComplete consinfo (Or e1 e2) =
combineOrResults (isComplete consinfo e1) (isComplete consinfo e2)
isComplete _ (Case _ _ []) = InComplete
isComplete _ (Case _ _ (Branch (LPattern _) _ : _)) = InComplete
isComplete consinfo (Case _ _ (Branch (Pattern cons _) bexp : ces)) =
combineAndResults
(checkAllCons (maybe [] (map fst) (lookupProgInfo cons consinfo)) ces)
(isComplete consinfo bexp)
where
checkAllCons [] _ = Complete
checkAllCons (_:_) [] = InComplete
checkAllCons (_:_)
(Branch (LPattern _) _ : _) = InComplete
checkAllCons (c:cs) (Branch (Pattern i _) e : ps) =
combineAndResults (checkAllCons (delete i (c:cs)) ps)
(isComplete consinfo e)
isComplete consinfo (Typed e _) = isComplete consinfo e
combineOrResults :: Completeness -> Completeness -> Completeness
combineOrResults Complete _ = Complete
combineOrResults InComplete Complete = Complete
combineOrResults InComplete InComplete = InCompleteOr
combineOrResults InComplete InCompleteOr = InCompleteOr
combineOrResults InCompleteOr Complete = Complete
combineOrResults InCompleteOr InComplete = InCompleteOr
combineOrResults InCompleteOr InCompleteOr = InCompleteOr
combineAndResults :: Completeness -> Completeness -> Completeness
combineAndResults InComplete _ = InComplete
combineAndResults Complete Complete = Complete
combineAndResults Complete InComplete = InComplete
combineAndResults Complete InCompleteOr = InCompleteOr
combineAndResults InCompleteOr Complete = InCompleteOr
combineAndResults InCompleteOr InComplete = InComplete
combineAndResults InCompleteOr InCompleteOr = InCompleteOr
totalAnalysis :: Analysis Bool
totalAnalysis =
combinedDependencyFuncAnalysis "Total" patCompAnalysis True analyseTotally
analyseTotally :: ProgInfo Completeness -> FuncDecl -> [(QName,Bool)] -> Bool
analyseTotally pcinfo fdecl calledfuncs =
(maybe False (== Complete) (lookupProgInfo (funcName fdecl) pcinfo))
&& all snd calledfuncs
showTotally :: AOutFormat -> Bool -> String
showTotally AText True = "totally defined"
showTotally ANote True = ""
showTotally _ False = "partially defined"
showTotalFunc :: AOutFormat -> Bool -> String
showTotalFunc AText True = "totally and functionally defined"
showTotalFunc ANote True = ""
showTotalFunc AText False = "partially or non-deterministically defined"
showTotalFunc ANote False = "partial/non-deterministic"
totalFuncAnalysis :: Analysis Bool
totalFuncAnalysis =
combinedDependencyFuncAnalysis "TotalFunc" totalAnalysis True analyseTotalFunc
analyseTotalFunc :: ProgInfo Bool -> FuncDecl -> [(QName,Bool)] -> Bool
analyseTotalFunc pcinfo fdecl calledfuncs =
(maybe False id (lookupProgInfo (funcName fdecl) pcinfo))
&& not (isNondetDefined fdecl)
&& all snd calledfuncs
instance ReadWrite Completeness where
readRW _ ('0' : r0) = (Complete,r0)
readRW _ ('1' : r0) = (InComplete,r0)
readRW _ ('2' : r0) = (InCompleteOr,r0)
showRW _ strs0 Complete = (strs0,showChar '0')
showRW _ strs0 InComplete = (strs0,showChar '1')
showRW _ strs0 InCompleteOr = (strs0,showChar '2')
writeRW _ h Complete strs = hPutChar h '0' >> return strs
writeRW _ h InComplete strs = hPutChar h '1' >> return strs
writeRW _ h InCompleteOr strs = hPutChar h '2' >> return strs
typeOf _ = monoRWType "Completeness"
|