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

-----------------------------------------------------------------------------
-- Pattern completeness 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
--
-- Johannes Koj, October 2000
-- Michael Hanus, March 2021
-----------------------------------------------------------------------------

module CurryBrowseAnalysis.PatternComplete
  ( CompletenessType(..), analyseCompleteness, analyseTotallyDefined )
 where

import FlatCurry.Types
import CurryBrowseAnalysis.Dependency(analyseWithDependencies)

------------------------------------------------------------------------------
-- The completeness analysis must be applied to complete programs,
-- i.e., modules together with all their imported modules (although
-- functions are locally checked, the definition of all data types
-- used in the patterns are needed).
-- It assigns to a FlatCurry program the list of all qualified function names
-- together with a flag indicating whether this function is completely
-- defined on its input types (i.e., reducible for all ground data terms).

-- The possible outcomes of the completeness analysis:
data CompletenessType =
     Complete       -- completely defined
   | InComplete     -- incompletely defined
   | InCompleteOr   -- incompletely defined in each branch of an "Or"

analyseTotallyDefined :: [TypeDecl] -> [FuncDecl] -> [(QName,CompletenessType)]
analyseTotallyDefined types = analyseWithDependencies (analyseCompleteness types) cAnd
 where cAnd = foldr combineAndResults Complete

analyseCompleteness :: [TypeDecl] -> FuncDecl -> CompletenessType
analyseCompleteness types fdecl = anaFun fdecl
 where
  anaFun (Func _ _ _ _ (Rule _ e)) = isComplete types e
  anaFun (Func _ _ _ _ (External _)) = Complete

isComplete :: [TypeDecl] -> Expr -> CompletenessType
isComplete _ (Var _)      = Complete
isComplete _ (Lit _)      = Complete
isComplete types (Comb _ f es) =
  if f==("Prelude","commit") && length es == 1
  then isComplete types (head es)
  else Complete
isComplete _ (Free _ _) = Complete
isComplete _ (Let _ _) = Complete
isComplete types (Or e1 e2) =
   combineOrResults (isComplete types e1) (isComplete types e2)
-- if there is no branch, it is incomplete:
isComplete _ (Case _ _ []) = InComplete
-- for literal branches we usually assume that not all alternatives are provided:
isComplete _ (Case _ _ (Branch (LPattern _)   _ : _)) = InComplete
isComplete types (Case _ _ (Branch (Pattern cons pvs) bexp : ces)) =
  checkAllCons (getConstructors cons types)
               (Branch (Pattern cons pvs) bexp : ces)
 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 (removeConstructor i (c:cs)) ps)
                       (isComplete types e)
isComplete types (Typed e _) = isComplete types e

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


-- get the list of all constructors of the same datatype for a given constructor:
getConstructors :: QName -> [TypeDecl] -> [ConsDecl]
getConstructors _ [] = error "Internal compiler error: case datatype not found!"
getConstructors cons (TypeSyn _ _ _ _  : types) = getConstructors cons types
getConstructors cons (TypeNew _ _ _ (NewCons nc v te) : types)  =
 if cons == nc then [Cons nc 1 v [te]]
               else getConstructors cons types
getConstructors cons (Type _ _ _ cdecls : types) =
 if hasCons cdecls then cdecls
                   else getConstructors cons types
 where
   hasCons [] = False
   hasCons (Cons cs _ _ _ : cstrs) = cons==cs || hasCons cstrs

-- remove a constructor from a list of constructors
removeConstructor :: QName -> [ConsDecl] -> [ConsDecl]
removeConstructor c1 [] = error ("Constructor "++show c1++" not found!!")
removeConstructor c1 ((Cons c2 a vis ts):cs)
        | c1==c2    = cs
        | otherwise = (Cons c2 a vis ts):(removeConstructor c1 cs)