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
|
------------------------------------------------------------------------------
--- Indeterminism analysis:
--- check whether functions are indeterministic, i.e., might deliver
--- different results for different runs of a program.
--- This could be the case if there are explicit or implicit calls
--- to `SetFunctions.select` or to a committed choice.
---
--- @author Michael Hanus
--- @version April 2013
------------------------------------------------------------------------------
module Indeterministic(indetAnalysis,showIndet) where
import Analysis
import FlatCurry.Types
------------------------------------------------------------------------------
--- The indeterminism analysis is a global function dependency analysis.
--- It assigns to a function a flag which is True if this function
--- might be indeterministic (i.e., calls directly or indirectly
--- a select or committed choice operation).
indetAnalysis :: Analysis Bool
indetAnalysis = dependencyFuncAnalysis "Indeterministic" False indetFunc
--- An operation is indeterministic if it calls a select or committed choice
--- or depends on some indeterministic operation.
indetFunc :: FuncDecl -> [(QName,Bool)] -> Bool
indetFunc func calledFuncs =
hasIndetRules func || any snd calledFuncs
-- Show right-linearity information as a string.
showIndet :: AOutFormat -> Bool -> String
showIndet AText True = "impure (indeterministic) operation"
showIndet ANote True = "indeterministic"
showIndet AText False = "referentially transparent operation"
showIndet ANote False = ""
------------------------------------------------------------------------------
-- The right-linearity analysis can also be applied to individual functions.
-- It returns True for a function if it is defined by right-linear rules.
hasIndetRules :: FuncDecl -> Bool
hasIndetRules (Func _ _ _ _ (Rule _ e)) = choiceInExpr e
hasIndetRules (Func _ _ _ _ (External _)) = False
-- check an expression for occurrences of select, committed choice, or send:
choiceInExpr :: Expr -> Bool
choiceInExpr (Var _) = False
choiceInExpr (Lit _) = False
choiceInExpr (Comb _ f es) = f `elem` indetFuns || any 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
indetFuns :: [QName]
indetFuns = [("Prelude","commit"),
("Ports","send"),("Ports","doSend"),
("SetFunctions","select")]
-- end of Indeterministic
|
