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
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
------------------------------------------------------------------------
--- Groundness/non-determinism effect analysis based on
--- [Brassel/Hanus'05](http://www.informatik.uni-kiel.de/~mh/papers/ICLP05.html).
---
--- @author Michael Hanus
--- @version July 2024
------------------------------------------------------------------------

module Analysis.Groundness
  ( Ground(..), showGround, groundAnalysis
  , NDEffect(..), showNDEffect, ndEffectAnalysis
  ) where

import FlatCurry.Types
import Data.List
import RW.Base
import System.IO

import Analysis.Types
import Analysis.ProgInfo

------------------------------------------------------------------------
-- Analyze the groundness of functions.
------------------------------------------------------------------------

--- Type to represent groundness information.
--- Definitely ground (G), maybe non-ground (A), or maybe non-ground
--- if i-th argument is non-ground (P [...,i,...]).
data Ground = G | A | P [Int]
 deriving (Show, Read, Eq)

-- Show groundness information as a string.
showGround :: AOutFormat -> Ground -> String
showGround ANote G      = "G"
showGround AText G      = "always ground result"
showGround ANote A      = "A"
showGround AText A      = "possibly non-ground result"
showGround ANote (P ps) = show ps
showGround AText (P ps) =
  "ground if argument" ++
  (if length ps == 1 then ' ' : show (head ps) ++ " is ground"
                     else "s " ++ show ps ++ " are ground")

-- Lowest upper bound on groundness information.
lubG :: Ground -> Ground -> Ground
lubG G      y      = y
lubG A      _      = A
lubG (P ps) G      = P ps
lubG (P _ ) A      = A
lubG (P ps) (P qs) = P (mergeInts ps qs)

------------------------------------------------------------------------
-- Analyze the groundness information of functions.

groundAnalysis :: Analysis Ground
groundAnalysis = dependencyFuncAnalysis "Groundness" G groundFunc

groundFunc :: FuncDecl -> [(QName,Ground)] -> Ground
groundFunc (Func (m,f) _ _ _ rule) calledFuncs
 | m==prelude && f `elem` preludeGroundFuncs = G
 | m==prelude = maybe anaresult id (lookup f preludeFuncs)
 | otherwise  = anaresult
 where
  anaresult = groundFuncRule calledFuncs rule

  preludeFuncs = [("cond",P [2]),("seq",P [2]),("ensureNotFree",P [1])]

  preludeGroundFuncs =
    ["+","-","*","div","mod","divMod","quot","rem","quotRem","negateFloat",
     "==","=:=","=:<=","compare","<",">","<=",">=","failed","error"]


groundFuncRule :: [(QName,Ground)] -> Rule -> Ground
groundFuncRule _ (External _) = A -- nothing known about other externals
groundFuncRule calledFuncs (Rule args rhs) =
  absEvalExpr (zip args (map (\i->P [i]) [1..])) rhs
 where
  -- abstract evaluation of an expression w.r.t. groundness environment
  absEvalExpr env (Var i)  = maybe A -- occurs in case of recursive lets
                                   id  (lookup i env)
  absEvalExpr _   (Lit _)  = G
  absEvalExpr env (Comb ct g es) =
    if ct == FuncCall
    then maybe (error $ "Abstract value of " ++ show g ++ " not found!")
               (\gd -> let curargs = zip [1..] (map (absEvalExpr env) es)
                        in groundApply gd curargs)
               (lookup g calledFuncs)
    else foldr lubG G (map (absEvalExpr env) es)
  absEvalExpr env (Free vs e) = absEvalExpr (zip vs (repeat A) ++ env) e
  absEvalExpr env (Let bs e)  = absEvalExpr (absEvalBindings env bs) e
  absEvalExpr env (Or e1 e2)  = lubG (absEvalExpr env e1) (absEvalExpr env e2)
  absEvalExpr env (Typed e _) = absEvalExpr env e
  absEvalExpr env (Case _  e bs) = foldr lubG G (map absEvalBranch bs)
   where
    gcase = absEvalExpr env e

    absEvalBranch (Branch (LPattern _) be) = absEvalExpr env be
    absEvalBranch (Branch (Pattern _ pargs) be) =
      absEvalExpr (map (\pi -> (pi,gcase)) pargs ++ env) be

  -- could be improved for recursive lets with local fixpoint computation
  absEvalBindings env [] = env
  absEvalBindings env ((i,exp):bs) =
    absEvalBindings ((i, absEvalExpr env exp) : env) bs

-- compute groundness information for an application
groundApply :: Ground -> [(Int,Ground)] -> Ground
groundApply G _ = G
groundApply A _ = A
groundApply (P ps) gargs =
  foldr lubG G (map (\p -> maybe A id (lookup p gargs)) ps)


-----------------------------------------------------------------------
-- Non-determinism effect analysis
-----------------------------------------------------------------------

--- Type to represent non-determinism effects.
--- A non-determinism effect can be due to an Or (first argument),
--- due to a narrowing step (second argument), or if i-th argument
--- is non-ground (if i is a member of the third argument).
data NDEffect = NDEffect Bool Bool [Int]
  deriving (Eq, Ord, Show, Read)

noEffect :: NDEffect
noEffect = NDEffect False False []

orEffect :: NDEffect
orEffect = NDEffect True False []

narrEffect :: NDEffect
narrEffect = NDEffect False True []

narrIfEffect :: [Int] -> NDEffect
narrIfEffect = NDEffect False False

-- Show non-determinitic effect information as a string.
showNDEffect :: AOutFormat -> NDEffect -> String
showNDEffect ANote (NDEffect ornd narr ifs) = intercalate " " $
  (if ornd then ["choice"] else []) ++
  (if narr then ["narr"]   else []) ++
  (if not (null ifs) then ["narrIf"++show ifs] else [])
showNDEffect AText (NDEffect ornd narr ifs) = intercalate " / " $
  (if ornd then ["choice"] else []) ++
  (if narr then ["possibly non-deterministic narrowing steps"] else []) ++
  (if not (null ifs)
   then ["non-deterministic narrowing if argument" ++
         (if length ifs == 1 then ' ' : show (head ifs) ++ " is non-ground"
                            else "s " ++ show ifs ++ " are non-ground")]
   else [])

-- Lowest upper bound on non-determinism effects.
lubE :: NDEffect -> NDEffect -> NDEffect
lubE (NDEffect ornd1 narr1 ifs1) (NDEffect ornd2 narr2 ifs2) =
  NDEffect (ornd1 || ornd2) narr (if narr then [] else mergeInts ifs1 ifs2)
 where
   narr = narr1 || narr2

-- Lowest upper bound on groundness/non-determinism effects.
lubGE :: (Ground,NDEffect) -> (Ground,NDEffect) -> (Ground,NDEffect)
lubGE (g1,ne1) (g2,ne2) = (lubG g1 g2, lubE ne1 ne2)

------------------------------------------------------------------------
-- Analyze the non-determinism effect of functions.

ndEffectAnalysis :: Analysis NDEffect
ndEffectAnalysis =
  combinedDependencyFuncAnalysis "NDEffect" groundAnalysis noEffect ndEffectFunc

ndEffectFunc :: ProgInfo Ground -> FuncDecl -> [(QName,NDEffect)] -> NDEffect
ndEffectFunc groundinfo (Func (m,f) _ _ _ rule) calledFuncs
 | m==prelude = maybe anaresult id (lookup f preludeFuncs)
 | otherwise  = anaresult
 where
  anaresult = ndEffectFuncRule groundinfo calledFuncs rule

  preludeFuncs = [("?",orEffect)]


ndEffectFuncRule :: ProgInfo Ground -> [(QName,NDEffect)] -> Rule -> NDEffect
ndEffectFuncRule _ _ (External _) = noEffect -- externals are deterministic
ndEffectFuncRule groundinfo calledFuncs (Rule args rhs) =
  snd (absEvalExpr (zip args (map (\i->(P [i],noEffect)) [1..])) rhs)
 where
  -- abstract evaluation of an expression w.r.t. NDEffect environment
  absEvalExpr env (Var i)  = maybe (A,noEffect) id (lookup i env)
  absEvalExpr _   (Lit _)  = (G,noEffect)
  absEvalExpr env (Comb ct g es) =
    if ct == FuncCall
    then maybe (error $ "Abstract value of " ++ show g ++ " not found!")
               (\gnd -> let curargs = zip [1..] (map (absEvalExpr env) es) in
                   maybe (error $ "Ground value of " ++ show g ++ " not found!")
                         (\ggd -> ndEffectApply (ggd,gnd) curargs)
                         (lookupProgInfo g groundinfo))
               (lookup g calledFuncs)
    else foldr lubGE (G,noEffect) (map (absEvalExpr env) es)
  absEvalExpr env (Free vs e) =
    absEvalExpr (zip vs (repeat (A,noEffect)) ++ env) e
  absEvalExpr env (Let bs e)  = absEvalExpr (absEvalBindings env bs) e
  absEvalExpr env (Or e1 e2)  =
    let (g1,nd1) = absEvalExpr env e1
        (g2,nd2) = absEvalExpr env e2
     in (lubG g1 g2, lubE orEffect (lubE nd1 nd2))
  absEvalExpr env (Typed e _) = absEvalExpr env e
  absEvalExpr env (Case ctype e bs) =
    if ctype==Rigid {- not really for KiCS2 -} || gcase==G || length bs == 1
    then (gbrs, lubE ndbrs ndcase)
    else (gbrs, lubE (ground2nondet gcase) (lubE ndbrs ndcase))
   where
    (gcase,ndcase) = absEvalExpr env e

    (gbrs,ndbrs) = foldr lubGE (G,noEffect) (map absEvalBranch bs)

    ground2nondet G      = noEffect
    ground2nondet A      = narrEffect
    ground2nondet (P ps) = narrIfEffect ps

    absEvalBranch (Branch (LPattern _) be) = absEvalExpr env be
    absEvalBranch (Branch (Pattern _ pargs) be) =
      absEvalExpr (map (\pi -> (pi,(gcase,noEffect))) pargs ++ env) be

  -- could be improved for recursive lets with local fixpoint computation
  absEvalBindings env [] = env
  absEvalBindings env ((i,exp):bs) =
    absEvalBindings ((i, absEvalExpr env exp) : env) bs

-- compute ground/nondet effect information for an application
ndEffectApply :: (Ground,NDEffect) -> [(Int,(Ground,NDEffect))]
              -> (Ground,NDEffect)
ndEffectApply (fgd,fnd) argsgnd =
  let (argsgd,argsnd) = unzip (map (\ (i,(gd,nd)) -> ((i,gd),nd)) argsgnd)
   in (groundApply fgd argsgd,
       foldr lubE (ndEffectReplace argsgd fnd) argsnd)

-- replace (narrIf i) by i-th ground value
ndEffectReplace :: [(Int,Ground)] -> NDEffect -> NDEffect
ndEffectReplace argsgd (NDEffect ornd narrnd ifs) = replaceProjs [] ifs
 where
  -- replace i by i-th ground value
  replaceProjs ps [] = NDEffect ornd narrnd ps
  replaceProjs ps (i:is) =
    maybe (error $ "Ground value of argument " ++ show i ++ " not found!")
          (\g -> case g of G     -> replaceProjs ps is
                           A     -> NDEffect ornd True []
                           P ips -> replaceProjs (mergeInts ips ps) is)
          (lookup i argsgd)

-----------------------------------------------------------------------
-- merge ascending lists of integers and remove duplicates
mergeInts :: [Int] -> [Int] -> [Int]
mergeInts []     ys = ys
mergeInts (x:xs) [] = x:xs
mergeInts (x:xs) (y:ys) | x==y = x : mergeInts xs ys
                        | x<y  = x : mergeInts xs (y:ys)
                        | x>y  = y : mergeInts (x:xs) ys

prelude :: String
prelude = "Prelude"

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

instance ReadWrite Ground where
  readRW strs ('0' : r0) = (G,r0)
  readRW strs ('1' : r0) = (A,r0)
  readRW strs ('2' : r0) = (P a',r1)
    where
      (a',r1) = readRW strs r0

  showRW params strs0 G = (strs0,showChar '0')
  showRW params strs0 A = (strs0,showChar '1')
  showRW params strs0 (P a') = (strs1,showChar '2' . show1)
    where
      (strs1,show1) = showRW params strs0 a'

  writeRW params h G strs = hPutChar h '0' >> return strs
  writeRW params h A strs = hPutChar h '1' >> return strs
  writeRW params h (P a') strs = hPutChar h '2' >> writeRW params h a' strs

  typeOf _ = monoRWType "Ground"

instance ReadWrite NDEffect where
  readRW strs r0 = (NDEffect a' b' c',r3)
    where
      (a',r1) = readRW strs r0
      (b',r2) = readRW strs r1
      (c',r3) = readRW strs r2

  showRW params strs0 (NDEffect a' b' c') = (strs3,show1 . (show2 . show3))
    where
      (strs1,show1) = showRW params strs0 a'
      (strs2,show2) = showRW params strs1 b'
      (strs3,show3) = showRW params strs2 c'

  writeRW params h (NDEffect a' b' c') strs =
    (writeRW params h a' strs >>= writeRW params h b') >>= writeRW params h c'

  typeOf _ = monoRWType "NDEffect"

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