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
------------------------------------------------------------------------------
--- Nondeterminism analysis:
--- checks whether operations encapsulate or produce non-deterministic values
---
--- @author Michael Hanus
--- @version July 2024
------------------------------------------------------------------------------

module Analysis.NondetOps ( nondetOperations, showNondet, Nondet(..) )
 where

import Data.List         ( partition )

import FlatCurry.Types
import FlatCurry.Goodies ( allVars )
import RW.Base
import System.IO
import System.IO.Unsafe  ( trace )

import Analysis.Types

------------------------------------------------------------------------------
--- Data type to represent the (non-)determinism status of expressions and
--- functions.
data Nondet = Det | Nondet | FunD Nondet Nondet
 deriving (Eq, Read, Show)

-- Show determinism information as a string.
showNondet :: AOutFormat -> Nondet -> String
showNondet _ nd = showND True nd
 where
  showND _   Det          = "D"
  showND _   Nondet       = "ND"
  showND top (FunD d1 d2) = bracket top
                              (showND False d1 ++ " -> " ++ showND top d2)

  bracket top s = if top then s else "(" ++ s ++ ")"

-- Is the type purely deterministic?
-- A function is deterministic if its result is always deterministic.
isDetType :: Nondet -> Bool
isDetType Det          = True
isDetType Nondet       = False
isDetType (FunD _ nd2) = isDetType nd2

-- Least upper bound of non-determinism types.
lub :: Nondet -> Nondet -> Nondet
lub nd1 nd2 = case (nd1, nd2) of
  (Det             , Det             ) -> Det
  (Det             , Nondet          ) -> Nondet
  (Det             , FunD d1 d2      ) -> FunD d1 d2
  (Nondet          , _               ) -> Nondet
  (FunD _ _        , Det             ) -> if isDetType nd1 then nd1 else Nondet
  (FunD _ _        , Nondet          ) -> Nondet
  (FunD Det df1    , FunD Det df2    ) -> FunD Det    (lub df1 df2)
  (FunD Nondet df1 , FunD Nondet df2 ) -> FunD Nondet (lub df1 df2)
  (FunD Nondet df1 , FunD Det    df2 ) -> FunD Det    (lub df1 df2)
  (FunD Det df1    , FunD Nondet df2 ) -> FunD Det    (lub df1 df2)
  _ -> trace ("Warning: lub of '" ++ show nd1 ++ "' and '" ++
              show nd2 ++ "' not covered!") Nondet

--- Non-determinism type analysis.
nondetOperations :: Analysis Nondet
nondetOperations = dependencyFuncAnalysis "NonDetOps" Det ndFunc

ndFunc :: FuncDecl -> [(QName,Nondet)] -> Nondet
ndFunc (Func (m,f) ar _ _ (External _)) _ =
 maybe (genDetFun ar) -- external operations are deterministic
       id
       (lookup (m,f) stdNondetTypes)
ndFunc (Func (m,f) _ _ _ (Rule args rhs)) calledFuncs =
 maybe (ndFuncRule calledFuncs (m,f) args rhs)
       id
       (lookup (m,f) stdNondetTypes)

-- Non-determinism types for some standard operations.
stdNondetTypes :: [(QName,Nondet)]
stdNondetTypes =
  map (\ (f,nd) -> ((prelude,f), nd))
      [ ("apply"  , FunD (FunD Det Det) (FunD Det Det) )
      , ("?"      , FunD Det (FunD Det Nondet) )
      , ("unknown", FunD (FunD Det Det) Nondet )
      ] ++
  map (\ (f,nd) -> (("Control.AllValues",f), nd)) allValOps ++
  map (\ (f,nd) -> (("Control.Findall"  ,f), nd)) allValOps
 where
  allValOps =
    [ ("allSolutions", FunD Det (FunD Nondet Det))
    , ("allValues"   , FunD Nondet Det)
    , ("oneSolution" , FunD Det (FunD Nondet Det))
    , ("oneValue"    , FunD Nondet Det)
    , ("someSolution", FunD Det (FunD Nondet Det))
    , ("someValue"   , FunD Nondet Det)
    , ("isFail"      , FunD Nondet Det)
    , ("rewriteAll"  , FunD Nondet Det)
    , ("rewriteSome" , FunD Nondet Det)
    ]

-- Generate a deterministic operation type of a given arity.
genDetFun :: Int -> Nondet
genDetFun n = if n==0 then Det else FunD Det (genDetFun (n-1))

-- Generate a non-deterministic operation type of a given arity.
genNondetFun :: Int -> Nondet
genNondetFun n = if n==0 then Nondet else FunD Det (genNondetFun (n-1))

-- Generate a `Nondet` type from an argument environment and a result type.
genArgEnvFun :: [(Int,Nondet)] -> Nondet -> Nondet
genArgEnvFun []               ndr = ndr
genArgEnvFun ((_,nda):argenv) ndr = FunD nda (genArgEnvFun argenv ndr)

-- Analyze an operation defined by a rule.
ndFuncRule :: [(QName,Nondet)] -> QName -> [Int] -> Expr -> Nondet
ndFuncRule calledFuncs qf args rhs = tryNondetArg [] args
 where
  tryNondetArg argsenv []     = genArgEnvFun argsenv (ndExp argsenv rhs)
  tryNondetArg argsenv (i:is) =
    -- Try whether argument i as ND yields D.
    -- If yes, set it to ND, otherwise to D.
    let ndres = ndExp (argsenv ++ [(i,Nondet)] ++ map (\j -> (j,Det)) is) rhs
        argnd = if ndres == Det then Nondet else Det
    in tryNondetArg (argsenv ++ [(i,argnd)]) is

  applyToAbsValue g absfun =
    maybe (error $ "Abstract value of " ++ show g ++ " not found!")
          absfun
          (lookup g calledFuncs)

  ndExp env (Var i)        = maybe (trace (show (snd qf) ++ ": variable " ++
                                           show i ++ " undefined!") Nondet)
                                   id
                                   (lookup i env)
  ndExp _   (Lit _)        = Det
  ndExp env (Comb ct g es) = case ct of
    FuncCall       -> ndFuncCall g 0 ndargs
    FuncPartCall m -> ndFuncCall g m ndargs
    ConsPartCall m -> if all isDetType ndargs then genDetFun m
                                              else genNondetFun m
    ConsCall       -> if all isDetType ndargs then Det else Nondet
   where ndargs = map (ndExp env) es
  ndExp env (Free vs e)    = ndExp (map (\i -> (i,Nondet)) vs ++ env) e
  ndExp env (Let bs e)     = ndLet env bs e
  ndExp _   (Or _ _)       = Nondet
  ndExp env (Case _  e bs)
    | ndExp env e == Nondet = Nondet
    | otherwise             = foldr lub Det (map ndBranch bs)
   where
    ndBranch (Branch (Pattern _ vs) be) = ndExp (map (\i -> (i,Det)) vs ++ env)
                                                be
    ndBranch (Branch (LPattern _)   be) = ndExp env be
  ndExp env (Typed e _)    = ndExp env e

  ndFuncCall g m ndargs
    | g == (prelude, "apply")
    = case ndargs of
        [FunD Nondet Det, _] -> Det -- specific case not covered by std ND type
        _                    -> applyToAbsValue g (matchArgs qf g m ndargs)
    | isSetCombinator g
    = ndSetFunc m ndargs
    | otherwise
    = applyToAbsValue g (matchArgs qf g m ndargs)

  ndSetFunc _ [] = error $ "Illegal use of set function in '" ++ snd qf ++ "'!"
  ndSetFunc m (ndfunc:ndargs) =
    matchArgs qf ("??","??") m ndargs (setResultD ndfunc)

  -- Analyse let expressions. For recursive bindings, analyse all these
  -- bindings where `Det` is assumed as the initial value for the variables.
  -- If some analysis returns `Nondet`, change the assumption to `Nondet`.
  ndLet env []          e = ndExp env e
  ndLet env ((i,be):bs) e =
    if all (`notElem` (i : map fst bs)) (allVars be)
      then -- no recursive binding:
           ndLet ((i, ndExp env be) : env) bs e
      else -- recursive binding: find binding group and try `Det` or `Nondet`:
           ndLetGroup env [] [(i,be)] bs e

  ndLetGroup env recbs []           allbs e =
    -- Analyze the first recursive binding group and proceed with
    -- an appropriately extended environment:
    let vardetenv    = map (\ (i,_) -> (i,Det)  ) recbs ++ env
        varnondetenv = map (\ (i,_) -> (i,Nondet)) recbs ++ env
        nds = map (ndExp vardetenv) (map snd recbs)
    in if all (== Det) nds
         then ndLet vardetenv    allbs e
         else ndLet varnondetenv allbs e
  ndLetGroup env grpbs ((i,be):rbs) allbs e =
    let (recbs, otherbs) = selectBindings (allVars be) allbs
    in ndLetGroup env (grpbs ++ [(i,be)]) (rbs ++ recbs) otherbs e

  -- Select in a list of bindings all recursive bindings of the given variables
  -- and return them together with the remaining ones:
  selectBindings []     bs = ([], bs)
  selectBindings (v:vs) bs =
    let (vbs,obs) = partition ((==v) . fst) bs
        (rbs,nbs) = selectBindings vs obs
    in  (vbs ++ rbs, nbs)


-- Match the actual arguments against a non-deterministic operation type.
matchArgs :: QName -> QName -> Int -> [Nondet] -> Nondet -> Nondet
matchArgs f g misargs ndofargs ndoffunc = matchA ndofargs ndoffunc
 where
  matchA []           nd = nd
  matchA (nd1:ndargs) nd = case nd of
    Det -> -- possibly unknown ND status:
           if all isDetType (nd1:ndargs) then genDetFun misargs
                                         else genNondetFun misargs
    _   -> case nd1 of
             Det -> case nd of
               FunD _ ndfunc -> matchA ndargs ndfunc
               _             -> noMatchWarning
             Nondet -> case nd of
               FunD Nondet         ndfunc -> matchA ndargs ndfunc
               FunD Det            ndfunc -> matchA ndargs (setResultND ndfunc)
               FunD (FunD Det Det) ndfunc -> matchA ndargs (setResultND ndfunc)
               _                          -> noMatchWarning
             FunD _ _ -> case nd of
               FunD ndf1 ndfunc -> if isDetType nd1
                                     then matchA ndargs ndfunc
                                     else if ndf1 == Nondet
                                            then matchA ndargs ndfunc
                                            else matchA ndargs
                                                        (setResultND ndfunc)
               _                -> noMatchWarning

  noMatchWarning =
    trace ("Warning: matchArgs '" ++ show ndofargs ++ "' against '" ++
           show ndoffunc ++ "' not covered in application of " ++
           show g ++ " in function '" ++ snd f ++ "'!") Nondet

-- Sets the result type (of a function) to `Nondet`.
setResultND :: Nondet -> Nondet
setResultND nd = case nd of FunD _ ndr -> FunD Det (setResultND ndr)
                            _          -> Nondet


-- Sets the result type (of a function) to `Det`.
setResultD :: Nondet -> Nondet
setResultD nd = case nd of FunD _ ndr -> FunD Det (setResultD ndr)
                           _          -> Det

prelude :: String
prelude = "Prelude"

-- Name of a set function combinator?
isSetCombinator :: QName -> Bool
isSetCombinator (mn,fn) = mn == "Control.SetFunctions" && take 3 fn == "set"

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

instance ReadWrite Nondet where
  readRW strs ('0' : r0) = (Det,r0)
  readRW strs ('1' : r0) = (Nondet,r0)
  readRW strs ('2' : r0) = (FunD a' b',r2)
    where
      (a',r1) = readRW strs r0
      (b',r2) = readRW strs r1

  showRW params strs0 Det = (strs0,showChar '0')
  showRW params strs0 Nondet = (strs0,showChar '1')
  showRW params strs0 (FunD a' b') = (strs2,showChar '2' . (show1 . show2))
    where
      (strs1,show1) = showRW params strs0 a'
      (strs2,show2) = showRW params strs1 b'

  writeRW params h Det strs = hPutChar h '0' >> return strs
  writeRW params h Nondet strs = hPutChar h '1' >> return strs
  writeRW params h (FunD a' b') strs =
    hPutChar h '2' >> (writeRW params h a' strs >>= writeRW params h b')

  typeOf _ = monoRWType "Nondet"

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