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
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
------------------------------------------------------------------------------
--- Determinism analysis:
--- checks whether functions are deterministic or nondeterministic, i.e.,
--- whether its evaluation on ground argument terms might cause
--- different computation paths.
---
--- @author Michael Hanus
--- @version July 2024
------------------------------------------------------------------------------

module Analysis.Deterministic
  ( overlapAnalysis, showOverlap, showDet
  , functionalAnalysis, showFunctional, isNondetDefined
  , Deterministic(..),nondetAnalysis
  , showNonDetDeps, nondetDepAnalysis, nondetDepAllAnalysis
  ) where

import Data.Char         (isDigit)
import Data.List
import FlatCurry.Types
import FlatCurry.Goodies
import RW.Base
import System.IO

import Analysis.Types

------------------------------------------------------------------------------
-- The overlapping analysis can be applied to individual functions.
-- It assigns to a FlatCurry function definition a flag which is True
-- if this function is defined with overlapping left-hand sides.

overlapAnalysis :: Analysis Bool
overlapAnalysis = simpleFuncAnalysis "Overlapping" isOverlappingFunction

isOverlappingFunction :: FuncDecl -> Bool
isOverlappingFunction (Func _ _ _ _ (Rule _ e))   = orInExpr e
isOverlappingFunction (Func f _ _ _ (External _)) = f == ("Prelude","?")

-- Check an expression for occurrences of OR:
orInExpr :: Expr -> Bool
orInExpr (Var _)       = False
orInExpr (Lit _)       = False
orInExpr (Comb _ f es) = f == (pre "?") || any orInExpr es
orInExpr (Free _ e)    = orInExpr e
orInExpr (Let bs e)    = any orInExpr (map snd bs) || orInExpr e
orInExpr (Or _ _)      = True
orInExpr (Case _ e bs) = orInExpr e || any orInBranch bs
 where orInBranch (Branch _ be) = orInExpr be
orInExpr (Typed e _) = orInExpr e

-- Show overlapping information as a string.
showOverlap :: AOutFormat -> Bool -> String
showOverlap _     True  = "overlapping"
showOverlap AText False = "non-overlapping"
showOverlap ANote False = ""

------------------------------------------------------------------------------
-- The functional analysis is a global function dependency analysis.
-- It assigns to a FlatCurry function definition a flag which is True
-- if this function is purely functional defined, i.e., its definition
-- does not depend on operation containing overlapping rules or free variables.

functionalAnalysis :: Analysis Bool
functionalAnalysis = dependencyFuncAnalysis "Functional" True isFuncDefined

-- Show functionally defined information as a string.
showFunctional :: AOutFormat -> Bool -> String
showFunctional _     True  = "functional"
showFunctional AText False = "defined with logic features"
showFunctional ANote False = ""

-- An operation is functionally defined if its definition is not
-- non-deterministic (no overlapping rules, no extra variables) and
-- it depends only on functionally defined operations.
isFuncDefined :: FuncDecl -> [(QName,Bool)] -> Bool
isFuncDefined func calledFuncs =
  not (isNondetDefined func) && all snd calledFuncs

-- Is a function f defined to be potentially non-deterministic, i.e.,
-- is the rule non-deterministic or does it contain extra variables?
isNondetDefined :: FuncDecl -> Bool
isNondetDefined (Func f _ _ _ rule) =
  f `notElem` (map pre ["failed","$!!","$##","normalForm","groundNormalForm"])
  -- these operations are internally defined in PAKCS with extra variables
  && isNondetRule rule
 where
  isNondetRule (Rule _ e) = orInExpr e || extraVarInExpr e
  isNondetRule (External _) = f==("Prelude","?")


-- check an expression for occurrences of extra variables:
extraVarInExpr :: Expr -> Bool
extraVarInExpr (Var _) = False
extraVarInExpr (Lit _) = False
extraVarInExpr (Comb _ _ es) = or (map extraVarInExpr es)
extraVarInExpr (Free vars e) = (not (null vars)) || extraVarInExpr e
extraVarInExpr (Let bs e) = any extraVarInExpr (map snd bs) || extraVarInExpr e
extraVarInExpr (Or e1 e2) = extraVarInExpr e1 || extraVarInExpr e2
extraVarInExpr (Case _  e bs) = extraVarInExpr e || any extraVarInBranch bs
                where extraVarInBranch (Branch _ be) = extraVarInExpr be
extraVarInExpr (Typed e _) = extraVarInExpr e

------------------------------------------------------------------------------
-- The determinism analysis is a global function dependency analysis.
-- It assigns to a function a flag which indicates whether is function
-- might be non-deterministic, i.e., might reduce in different ways
-- for given ground arguments.
-- If the non-determinism is encapsulated (set functions, getAllValues),
-- it is classified as deterministic.

--- Data type to represent determinism information.
data Deterministic = NDet | Det
  deriving (Eq, Ord, Show, Read)

-- Show determinism information as a string.
showDet :: AOutFormat -> Deterministic -> String
showDet _     NDet = "non-deterministic"
showDet AText Det  = "deterministic"
showDet ANote Det  = ""

nondetAnalysis :: Analysis Deterministic
nondetAnalysis = dependencyFuncAnalysis "Deterministic" Det nondetFunc

-- An operation is non-deterministic if its definition is potentially
-- non-deterministic or it calls a non-deterministic operation
-- where the non-deterministic call is not encapsulated.
nondetFunc :: FuncDecl -> [(QName,Deterministic)] -> Deterministic
nondetFunc func@(Func _ _ _ _ rule) calledFuncs =
  if isNondetDefined func || callsNDOpInRule rule
   then NDet
   else Det
 where
  callsNDOpInRule (Rule _ e) = callsNDOp e
  callsNDOpInRule (External _) = False

  callsNDOp (Var _)    = False
  callsNDOp (Lit _)    = False
  callsNDOp (Free _ e) = callsNDOp e
  callsNDOp (Let bs e) = any callsNDOp (map snd bs) || callsNDOp e
  callsNDOp (Or _ _)   = True
  callsNDOp (Case _ e bs) =
    callsNDOp e || any (\ (Branch _ be) -> callsNDOp be) bs
  callsNDOp (Typed e _) = callsNDOp e
  callsNDOp (Comb _ qf@(mn,fn) es)
    | mn == "SetFunctions" && take 3 fn == "set" && all isDigit (drop 3 fn)
    = -- non-determinism of function (first argument) is encapsulated so that
      -- its called ND functions are not relevant:
      if null es then False -- this case should not occur
                 else any callsNDOp (tail es)
    | isStrongEncapsOp qf
    = -- non-determinism of argument is encapsulated so that
      -- its called ND functions are not relevant:
      False
    | otherwise
    = maybe False (==NDet) (lookup qf calledFuncs) || any callsNDOp es

-- Does the operation ensures the strong encapsulation of its argument?
isStrongEncapsOp :: QName -> Bool
isStrongEncapsOp (mn,_) =
  mn `elem` ["Control.AllSolutions", "Control.AllValues"]

------------------------------------------------------------------------------
--- Data type to represent information about non-deterministic dependencies.
--- Basically, it is the set (represented as a sorted list) of
--- all function names that are defined by overlapping rules or rules
--- containing free variables which might be called.
--- In addition, the second component is (possibly) the list of
--- functions from which this non-deterministic function is called.
--- The length of this list is limited by 'maxDepsLength' in the
--- `NonDetAllDeps` analysis or to 1 (i.e., only the direct caller is
--- stored) in the `NonDetDeps` analysis.
type NonDetDeps = [(QName,[QName])]

--- The maximal length of a call chain associated with a non-deterministic
--- operation dependency. We limit the length in order to avoid large
--- analysis times for the `NonDetAllDeps` analysis.
maxDepsLength :: Int
maxDepsLength = 10

-- Show determinism dependency information as a string.
showNonDetDeps :: AOutFormat -> NonDetDeps -> String
showNonDetDeps AText []     = "deterministic"
showNonDetDeps ANote []     = ""
showNonDetDeps ANote xs@(_:_) = intercalate " " (nub (map (snd . fst) xs))
showNonDetDeps AText xs@(_:_) =
  "depends on non-det. operations: " ++
  intercalate ", " (map showNDOpInfo xs)
 where
  showNDOpInfo (ndop,cfs) = showQName ndop ++
    (if null cfs
      then ""
      else " (called from " ++ intercalate " -> " (map showQName cfs) ++ ")")

  showQName (mn,fn) = mn++"."++fn

--- Non-deterministic dependency analysis.
--- The analysis computes for each operation the set of operations
--- with a non-deterministic definition which might be called by this
--- operation. Non-deterministic operations that are called by other
--- non-deterministic operations are ignored so that only the first
--- (w.r.t. the call sequence) non-deterministic operations are returned.
nondetDepAnalysis :: Analysis NonDetDeps
nondetDepAnalysis =
  dependencyFuncAnalysis "NonDetDeps" [] (nondetDeps False)

--- Non-deterministic dependency analysis.
--- The analysis computes for each operation the set of *all* operations
--- with a non-deterministic definition which might be called by this
--- operation.
nondetDepAllAnalysis :: Analysis NonDetDeps
nondetDepAllAnalysis =
  dependencyFuncAnalysis "NonDetAllDeps" [] (nondetDeps True)

-- An operation is non-deterministic if its definition is potentially
-- non-deterministic (i.e., the dependency is the operation itself)
-- or it depends on some called non-deterministic function.
nondetDeps :: Bool -> FuncDecl -> [(QName,NonDetDeps)] -> NonDetDeps
nondetDeps alldeps func@(Func f _ _ _ rule) calledFuncs =
  let calledndfuncs = sort (nub (map addCaller (calledNDFuncsInRule rule)))
      addCaller (ndf,cfs)
        | null cfs                      = (ndf,[f])
        | alldeps && f `notElem` cfs
          && length cfs < maxDepsLength = (ndf,f:cfs)
        | otherwise                     = (ndf,cfs)
   in if isNondetDefined func
       then (f,[]) : (if alldeps then calledndfuncs else [])
       else calledndfuncs
 where
  calledNDFuncsInRule (Rule _ e) = calledNDFuncs e
  calledNDFuncsInRule (External _) = []

  calledNDFuncs (Var _) = []
  calledNDFuncs (Lit _) = []
  calledNDFuncs (Free _ e) = calledNDFuncs e
  calledNDFuncs (Let bs e) =
    concatMap calledNDFuncs (map snd bs) ++ calledNDFuncs e
  calledNDFuncs (Or e1 e2) = calledNDFuncs e1 ++ calledNDFuncs e2
  calledNDFuncs (Case _ e bs) =
    calledNDFuncs e ++ concatMap (\ (Branch _ be) -> calledNDFuncs be) bs
  calledNDFuncs (Typed e _) = calledNDFuncs e
  calledNDFuncs (Comb _ qf@(mn,fn) es)
    | mn == "SetFunctions" && take 3 fn == "set" && all isDigit (drop 3 fn)
    = -- non-determinism of function (first argument) is encapsulated so that
      -- its called ND functions are not relevant:
      if null es then [] -- this case should not occur
                 else concatMap calledNDFuncs (tail es)
    | isStrongEncapsOp qf
    = -- non-determinism of argument is encapsulated so that
      -- its called ND functions are not relevant:
      []
    | otherwise
    = maybe [] id (lookup qf calledFuncs) ++ concatMap calledNDFuncs es

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

pre :: String -> QName
pre n = ("Prelude",n)

------------------------------------------------------------------------------
-- ReadWrite instances:

instance ReadWrite Deterministic where
  readRW _ ('0' : r0) = (NDet,r0)
  readRW _ ('1' : r0) = (Det,r0)

  showRW _ strs0 NDet = (strs0,showChar '0')
  showRW _ strs0 Det  = (strs0,showChar '1')

  writeRW _ h NDet strs = hPutChar h '0' >> return strs
  writeRW _ h Det strs  = hPutChar h '1' >> return strs

  typeOf _ = monoRWType "Deterministic"

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