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

-----------------------------------------------------------------------------
--- Pattern completeness and totally definedness analysis for Curry programs
---
--- This analysis checks for each function in a Curry program  whether
--- this function is completely defined, i.e., reducible on all ground
--- constructor terms
---
--- @author Johannes Koj, Michael Hanus
--- @version June 2022
-----------------------------------------------------------------------------

module Analysis.TotallyDefined
  ( siblingCons, showSibling
  , siblingConsAndDecl, showSiblingAndDecl
  , Completeness(..), showComplete, showTotally, showTotalFunc
  , patCompAnalysis, totalAnalysis, totalFuncAnalysis
  ) where

import Analysis.ProgInfo
import Analysis.Types
import Analysis.Deterministic ( isNondetDefined )
import FlatCurry.Types
import FlatCurry.Goodies
import Data.List              ( delete )

-----------------------------------------------------------------------
--- An analysis to compute the sibling constructors (belonging to the
--- same data type) for a data constructor.

--- Shows the result of the sibling constructors analysis, i.e.,
--- shows a list of constructor names together with their arities.
showSibling :: AOutFormat -> [(QName,Int)] -> String
showSibling _ = show

siblingCons :: Analysis [(QName,Int)]
siblingCons = simpleConstructorAnalysis "SiblingCons" consNamesArOfType
 where
  -- get all constructor names and arities of a datatype declaration
  consNamesArOfType cdecl (Type _ _ _ consDecls) =
    map (\cd -> (consName cd, consArity cd))
        (filter (\cd -> consName cd /= consName cdecl) consDecls)
  consNamesArOfType _ (TypeSyn _ _ _ _) = []
  consNamesArOfType _ (TypeNew _ _ _ _) = []

-----------------------------------------------------------------------
--- An analysis to compute the sibling constructors (belonging to the
--- same data type) and type declaration for a data constructor.

--- Shows the result of the sibling constructors analysis, i.e.,
--- shows a tuple of a type declaration and a list of constructor
--- names together with their arities.
showSiblingAndDecl :: AOutFormat -> (TypeDecl, [(QName,Int)]) -> String
showSiblingAndDecl _ = show

siblingConsAndDecl :: Analysis (TypeDecl, [(QName,Int)])
siblingConsAndDecl =
  simpleConstructorAnalysis "SiblingConsAndDecl" consNamesArOfType
 where
  -- get all constructor names and arities of a datatype declaration
  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 _ _ _ _ -> []

------------------------------------------------------------------------------
-- The completeness analysis assigns to an operation a flag indicating
-- whether this operation is completely defined on its input types,
-- i.e., reducible for all ground data terms.

-- The possible outcomes of the completeness analysis:
data Completeness =
     Complete       -- completely defined
   | InComplete     -- incompletely defined
   | InCompleteOr   -- incompletely defined in each branch of an "Or"
 deriving (Eq, Show, Read)

--- Pattern completeness analysis
patCompAnalysis :: Analysis Completeness
patCompAnalysis =
  combinedSimpleFuncAnalysis "PatComplete" siblingCons analysePatComplete

-- Shows the result of the completeness analysis.
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) =
  if f==("Prelude","commit") && length es == 1
  then isComplete consinfo (head es)
  else Complete
isComplete _ (Free _ _) = Complete
isComplete _ (Let _ _) = Complete
isComplete consinfo (Or e1 e2) =
   combineOrResults (isComplete consinfo e1) (isComplete consinfo e2)
-- if there is no branch, it is incomplete:
isComplete _ (Case _ _ []) = InComplete
-- for literal branches we assume that not all alternatives are provided:
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
   -- check for occurrences of all constructors in each case branch:
   checkAllCons []    _  = Complete
   checkAllCons (_:_) [] = InComplete
   checkAllCons (_:_)
                (Branch (LPattern _)   _ : _) = InComplete -- should not occur
   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

-- Combines the completeness results in different Or branches.
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

-- Combines the completeness results in different case branches.
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

------------------------------------------------------------------------------
--- An operation is totally defined if it is pattern complete and depends
--- only on totally defined functions.
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

-- Shows the result of the totally-defined analysis.
showTotally :: AOutFormat -> Bool -> String
showTotally AText True  = "totally defined"
showTotally ANote True  = ""
showTotally _     False = "partially defined"

------------------------------------------------------------------------------
-- The completeness analysis assigns to an operation a flag indicating
-- whether this operation is completely defined on its input types,
-- i.e., reducible for all ground data terms.

-- Shows the result of the totally-defined function analysis.
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"

--- An operation is totally and functionally defined if it is totally defined
--- and functionally defined (see `Analysis.Deterministic`).
--- Thus, it is defined without any pattern failures in the sense
--- of purely functional programming.
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

------------------------------------------------------------------------------