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

------------------------------------------------------------------------------
-- Nondeterminism analysis:
-- check whether functions are set-valued/nondeterministic, i.e., might
-- have several results even for ground argument terms.
--
-- Michael Hanus, March 2012
------------------------------------------------------------------------------

module Nondeterminism(analyseNondeterminism,analyseSetValued) where

import FlatCurry.Types
import Overlapping(orInExpr)
import Dependency(analyseWithDependencies)

------------------------------------------------------------------------------
-- The non-determinism analysis is a global analysis that must be applied to
-- the complete list of defined functions.
-- It assigns to a list of functions the list of all function names
-- together with a flag which is True if this function might be non-deterministic,
-- might have two different evaluations for given ground arguments.

analyseNondeterminism :: [FuncDecl] -> [(QName,Bool)]
analyseNondeterminism = analyseWithDependencies isNondeterministicDefined or

-- Is a function nondeterministically defined, i.e., does the rule contain or's?
isNondeterministicDefined :: FuncDecl -> Bool
isNondeterministicDefined (Func _ _ _ _ rule) = isNondeterministicRule rule

isNondeterministicRule (Rule _ e) = orInExpr e
isNondeterministicRule (External _) = False


------------------------------------------------------------------------------
-- The set-valued analysis is a global analysis that must be applied to
-- the complete list of defined functions.
-- It assigns to a list of functions the list of all function names
-- together with a flag which is True if this function might be set-valued,
-- might reduce to different values for given ground arguments.

analyseSetValued :: [FuncDecl] -> [(QName,Bool)]
analyseSetValued = analyseWithDependencies isSetValuedDefined or

-- Is a function f defined to be potentially set-valued, i.e., is the rule
-- nondeterministic or does it contain extra variables?
isSetValuedDefined :: FuncDecl -> Bool
isSetValuedDefined (Func f _ _ _ rule) =
  f `notElem` [pre "failed",pre "$!!",pre "$##"] && isSetValuedRule rule

isSetValuedRule (Rule _ e) = orInExpr e || extraVarInExpr e
isSetValuedRule (External _) = False


-- check an expression for occurrences of extra variables:
extraVarInExpr :: Expr -> Bool
extraVarInExpr (Var _) = False
extraVarInExpr (Lit _) = False
extraVarInExpr (Comb _ _ es) = or (map extraVarInExpr es)
extraVarInExpr (Free vars e) = (not (null vars)) || extraVarInExpr e
extraVarInExpr (Let bs e) = any extraVarInExpr (map snd bs) || extraVarInExpr e
extraVarInExpr (Or e1 e2) = extraVarInExpr e1 || extraVarInExpr e2
extraVarInExpr (Case _  e bs) = extraVarInExpr e || any extraVarInBranch bs
                where extraVarInBranch (Branch _ be) = extraVarInExpr be


pre n = ("Prelude",n)