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
------------------------------------------------------------------------------
--- Termination analysis:
--- checks whether an operation is terminating, i.e.,
--- whether all evaluations on ground argument terms are finite.
--- The method used here checks whether the arguments in all recursive
--- calls of an operation are smaller than the arguments passed to
--- the operation.
---
--- @author Michael Hanus
--- @version February 2017
------------------------------------------------------------------------------

module Analysis.Termination
  ( terminationAnalysis, showTermination
  , productivityAnalysis, showProductivity, Productivity(..)
  ) where

import Analysis.Types
import Analysis.ProgInfo
import Analysis.RootReplaced (rootCyclicAnalysis)

import Char(isDigit)
import FlatCurry.Types
import FlatCurry.Goodies
import List
import SCC(scc)
import Sort(sort)

------------------------------------------------------------------------------
-- The termination analysis is a global function dependency analysis.
-- It assigns to a FlatCurry function definition a flag which is True
-- if this operation is terminating, i.e., whether all evaluations

terminationAnalysis :: Analysis Bool
terminationAnalysis = dependencyFuncAnalysis "Terminating" False isTerminating

-- Show termination information as a string.
showTermination :: AOutFormat -> Bool -> String
showTermination AText True  = "terminating"
showTermination ANote True  = ""
showTermination AText False = "possibly non-terminating"
showTermination ANote False = "maybe not term."

-- 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.
isTerminating :: FuncDecl -> [(QName,Bool)] -> Bool
isTerminating (Func qfunc _ _ _ rule) calledFuncs = hasTermRule rule
 where
  hasTermRule (Rule args e) = hasTermExp (map (\a -> (a,[])) args) e
  -- we assume that all externally defined operations are terminating:
  hasTermRule (External _) = True

  hasTermExp _ (Var _)    = True
  hasTermExp _ (Lit _)    = True
  hasTermExp _ (Free _ _) = False -- could be improved if the domain is finite
  hasTermExp args (Let bs e) =
    -- compute strongly connected components of local let declarationss
    -- in order to check for recursive lets
    let sccs   = scc ((:[]) . fst) (allVars . snd) bs
    in if any (\scc -> any (`elem` concatMap allVars (map snd scc))
                           (map fst scc))
              sccs
         then False -- non-terminating due to recursive let
         else all (hasTermExp args) (e : map snd bs)
  hasTermExp args (Or e1 e2) =
    hasTermExp args e1 && hasTermExp args e2
  hasTermExp args (Case _ e bs) =
    hasTermExp args e &&
    all (\ (Branch pt be) -> hasTermExp (addSmallerArgs args e pt) be) bs
  hasTermExp args (Typed e _) = hasTermExp args e
  hasTermExp args (Comb ct qf es) =
    case ct of
      ConsCall       -> all (hasTermExp args) es
      ConsPartCall _ -> all (hasTermExp args) es
      _ -> (if qf == qfunc -- is this a recursive call?
              then any isSmallerArg (zip args es)
              else maybe False id (lookup qf calledFuncs)) &&
           all (hasTermExp args) es

  isSmallerArg ((_,sargs),exp) = case exp of
    Var v -> v `elem` sargs
    _     -> False

-- compute smaller args w.r.t. a given discriminating expression and
-- branch pattern
addSmallerArgs :: [(Int, [Int])] -> Expr -> Pattern -> [(Int, [Int])]
addSmallerArgs args de pat =
  case de of
    Var v -> maybe args
                   (\argpos -> let (av,vs) = args!!argpos
                               in replace (av, varsOf pat ++ vs) argpos args)
                   (findIndex (isInArg v) args)
    _     -> args -- other expression, no definite smaller expressions
 where
   varsOf (LPattern _)      = []
   varsOf (Pattern _ pargs) = pargs

   isInArg v (argv,svs) = v==argv || v `elem` svs

------------------------------------------------------------------------------
-- The productivity analysis is a global function dependency analysis
-- which depends on the termination analysis.
-- An operation is considered as being productive if it cannot
-- perform an infinite number of steps without producing
-- outermost constructors.
-- It assigns to a FlatCurry function definition an abstract value
-- indicating whether the function is looping or productive.

--- Data type to represent productivity status of an operation.
data Productivity =
    NoInfo
  | Terminating    -- definitely terminating operation
  | DCalls [QName] -- possible direct (top-level) calls to operations that may
                   -- not terminate, which corresponds to being productive
  | Looping        -- possibly looping

productivityAnalysis :: Analysis Productivity
productivityAnalysis =
  combinedDependencyFuncAnalysis "Productive"
                                 terminationAnalysis
                                 NoInfo
                                 isProductive

-- Show productivity information as a string.
showProductivity :: AOutFormat -> Productivity -> String
showProductivity _ NoInfo      = "no info"
showProductivity _ Terminating = "terminating"
showProductivity _ (DCalls qfs) =
  "productive / calls: " ++ "[" ++ intercalate ", " (map snd qfs) ++ "]"
showProductivity _ Looping     = "possibly looping"

lubProd :: Productivity -> Productivity -> Productivity
lubProd Looping      _            = Looping
lubProd (DCalls _ )  Looping      = Looping
lubProd (DCalls xs)  (DCalls ys)  = DCalls (sort (union xs ys))
lubProd (DCalls xs)  Terminating  = DCalls xs
lubProd (DCalls xs)  NoInfo       = DCalls xs
lubProd Terminating  p            = if p==NoInfo then Terminating else p
lubProd NoInfo       p            = p

-- An operation is productive if its recursive calls are below
-- a constructor (except for calls to terminating operations so that
-- this property is also checked).
isProductive :: ProgInfo Bool -> FuncDecl -> [(QName,Productivity)]
             -> Productivity
isProductive terminfo (Func qf _ _ _ rule) calledFuncs = hasProdRule rule
 where
  -- we assume that all externally defined operations are terminating:
  hasProdRule (External _) = Terminating
  hasProdRule (Rule _ e) =
    case hasProdExp False e of
      DCalls fs -> if qf `elem` fs then Looping else DCalls fs
      prodinfo  -> prodinfo

  -- first argument: True if we are below a constructor
  hasProdExp _  (Var _)    = Terminating
  hasProdExp _  (Lit _)    = Terminating
  hasProdExp bc (Free _ e) = -- could be improved for finite domains:
    lubProd (DCalls []) (hasProdExp bc e)
  hasProdExp bc (Let bs e) =
    -- compute strongly connected components of local let declarationss
    -- in order to check for recursive lets
    let sccs   = scc ((:[]) . fst) (allVars . snd) bs
    in if any (\scc -> any (`elem` concatMap allVars (map snd scc))
                           (map fst scc))
              sccs
         then Looping -- improve: check for variable occs under constructors
         else foldr lubProd (hasProdExp bc e)
                    (map (\ (_,be) -> hasProdExp bc be) bs)
  hasProdExp bc (Or e1 e2) = lubProd (hasProdExp bc e1) (hasProdExp bc e2)
  hasProdExp bc (Case _ e bs) =
    foldr lubProd (hasProdExp bc e)
          (map (\ (Branch _ be) -> hasProdExp bc be) bs)
  hasProdExp bc (Typed e _) = hasProdExp bc e
  hasProdExp bc (Comb ct qg es) = case ct of
    ConsCall       -> cprodargs
    ConsPartCall _ -> cprodargs
    FuncCall       -> if qg == ("Prelude","?")
                        then fprodargs -- equivalent to Or
                        else funCallInfo
    FuncPartCall _ -> funCallInfo
   where
    cprodargs = foldr lubProd NoInfo (map (hasProdExp True) es)
    fprodargs = foldr lubProd NoInfo (map (hasProdExp bc  ) es)

    funCallInfo =
      let prodinfo = if fprodargs <= Terminating
                     then if maybe False id (lookupProgInfo qg terminfo)
                            then Terminating
                            else lubProd (DCalls [qg])
                                   (maybe Looping id (lookup qg calledFuncs))
                     else Looping -- worst case assumption, could be improved...
      in if not bc then prodinfo
                   else case prodinfo of
                          DCalls _ -> DCalls []
                          _        -> prodinfo

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