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

------------------------------------------------------------------------------
--- Indeterminism analysis:
--- check whether functions are indeterministic, i.e., contain an
--- indirect/implicit call to a committed choice.
---
--- @author Michael Hanus
--- @version November 2020
------------------------------------------------------------------------------

module CurryBrowseAnalysis.Indeterminism
  ( analyseIndeterminism, choiceInExpr )
 where

import Data.List

import FlatCurry.Types

import CurryBrowseAnalysis.Dependency

------------------------------------------------------------------------------
-- The indeterminism analysis must be applied to complete programs,
-- i.e., modules together with all their imported modules.
-- It assigns to a FlatCurry program the list of all qualified function names
-- together with a flag which is True if this function might be defined
-- in a indeterministic manner (i.e., contains an indirect/implicit call
-- to a committed choice).

analyseIndeterminism :: [FuncDecl] -> [(QName,Bool)]
analyseIndeterminism = analyseWithDependencies isIndeterministic or

--- is a function directly (i.e., by its rhs) indeterministic?
isIndeterministic :: FuncDecl -> Bool
isIndeterministic (Func _ _ _ _ rule) = isIndetRule rule

isIndetRule :: Rule -> Bool
isIndetRule (Rule _ e) = choiceInExpr e
isIndetRule (External _) = False

-- check an expression for occurrences of committed choice or send:
choiceInExpr :: Expr -> Bool
choiceInExpr (Var _) = False
choiceInExpr (Lit _) = False
choiceInExpr (Comb _ f es) = f==("Prelude","commit") ||
                             f==("Ports","send") || f==("Ports","doSend") ||
                             foldr (||) False (map choiceInExpr es)
choiceInExpr (Free _ e) = choiceInExpr e
choiceInExpr (Let bs e) = any choiceInExpr (map snd bs) || choiceInExpr e
choiceInExpr (Or e1 e2) = choiceInExpr e1 || choiceInExpr e2
choiceInExpr (Case _  e bs) = choiceInExpr e || any choiceInBranch bs
                where choiceInBranch (Branch _ be) = choiceInExpr be
choiceInExpr (Typed e _) = choiceInExpr e

-- end of AnaIndeterminism