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

--- ----------------------------------------------------------------------------
--- This module provides transforms FlatCurry programs for concolic evaluation:
---   - For every case expression a fresh identifier is introduced for the
---     scrutinized expression. For instance the expression
---
---     case e of p1 -> e1; ... ; pn -> en
---
---     is transformed to
---
---     let cid = e in case cid of p1 -> e1; ... ; pn -> en
---
---     where cid is a fresh identifier
---
---   - Furthermore, cases with boolean expressions as arguments are normalized
---     in the following form:
---
---     case c1 && c2 of                            case c1 of
---       True  -> e1         is transformed to       True  -> case c2 of
---       False -> e2                                            True  -> e1
---                                                              False -> e2
---                                                   False -> e2
---
---     Disjunctions are transformed in a similar way.
---
--- @author  Jan Tikovsky
--- @version August 2017
--- ----------------------------------------------------------------------------
module IdentifyCases where

import FCYFunctorInstances
import FlatCurry.Annotated.Types
-- import FlatCurry.Annotated.Goodies (annExpr, combArgs, updCombs)

import FlatCurryGoodies (IDAnn, extendAnn)
import Utils ((<$>), (<*>))

--- Identify Cases Monad
data ICM a = IC { runICM :: VarIndex -> (a, VarIndex) }

instance Monad ICM where
  return x = IC $ \s -> (x, s)

  f >>= g = IC $ \s -> let (x, s') = runICM f s in (runICM (g x)) s'

get :: ICM VarIndex
get = IC $ \s -> (s, s)

put :: VarIndex -> ICM ()
put s = IC $ \_ -> ((), s)

--- Generate a fresh identifier
freshID :: ICM VarIndex
freshID = do
  v <- get
  put (v - 1)
  return v

--- Annotate case expressions with fresh identifiers and mark literals
idCases :: [AFuncDecl a] -> ([AFuncDecl (IDAnn a)], VarIndex)
idCases fs
  = runICM (mapM (idFunc . fmap extendAnn) fs) (-1)

idFunc :: AFuncDecl (IDAnn a) -> ICM (AFuncDecl (IDAnn a))
idFunc (AFunc qn a vis ty r) = AFunc qn a vis ty <$> idRule r

idRule :: ARule (IDAnn a) -> ICM (ARule (IDAnn a))
idRule (ARule  ann vs e) = ARule ann vs <$> idExpr e
idRule e@(AExternal _ _) = return e

idExpr :: AExpr (IDAnn a) -> ICM (AExpr (IDAnn a))
idExpr v@(AVar                 _ _) = return v
idExpr (ALit       (ann, mid, _) l) = return $ ALit (ann, mid, True) l
idExpr (AComb         ann ct qn es) = AComb ann ct qn <$> mapM idExpr es
idExpr (ALet              ann bs e) = ALet ann <$> mapM idBinding bs <*> idExpr e
  where idBinding (v, ve) = idExpr ve >>= \ve' -> return (v, ve')
idExpr (AFree             ann vs e) = AFree ann vs <$> idExpr e
idExpr (AOr              ann e1 e2) = AOr ann <$> idExpr e1 <*> idExpr e2
idExpr (ACase (ann, _, lf) ct e bs) = do
  v   <- freshID
  e'  <- idExpr e
  bs' <- mapM idBranch bs
  return $ ACase (ann, Just v, lf) ct e' bs'
 where idBranch (ABranch p be) = ABranch p <$> idExpr be
idExpr (ATyped            ann e ty) = flip (ATyped ann) ty <$> idExpr e

-- --- Add a unique identifier to all expressions which are scrutinized in cases
-- idCases :: [AFuncDecl TypeExpr] -> ([AFuncDecl TypeExpr], VarIndex)
-- idCases fs = (runICM (mapM icFunc fs)) (-1)
--
-- icFunc :: AFuncDecl TypeExpr -> ICM (AFuncDecl TypeExpr)
-- icFunc (AFunc qn a vis ty r) = AFunc qn a vis ty <$> icRule r
--
-- icRule :: ARule TypeExpr -> ICM (ARule TypeExpr)
-- icRule (ARule  ann vs e) = ARule ann vs <$> splitCases e -- icExpr e
-- icRule e@(AExternal _ _) = return e
--
-- icExpr :: AExpr TypeExpr -> ICM (AExpr TypeExpr)
-- icExpr v@(AVar         _ _) = return v
-- icExpr l@(ALit         _ _) = return l
-- icExpr (AComb ann ct qn es) = AComb ann ct qn <$> mapM icExpr es
-- icExpr (ALet      ann bs e) = ALet ann <$> mapM icBinding bs <*> icExpr e
--   where icBinding (v, ve) = icExpr ve >>= \ve' -> return (v, ve')
-- icExpr (AFree     ann vs e) = AFree ann vs <$> icExpr e
-- icExpr (AOr      ann e1 e2) = AOr ann <$> icExpr e1 <*> icExpr e2
-- icExpr (ACase  ann ct e bs) = do
--   v <- freshID
--   bs' <- mapM icBranch bs
--   return $ ALet ann [((v, annE), e)] (ACase ann ct (AVar annE v) bs')
--  where annE                    = annExpr e
--        icBranch (ABranch p be) = ABranch p <$> icExpr be
-- icExpr (ATyped   ann e ty) = flip (ATyped ann) ty <$> icExpr e
--
-- splitCases :: AExpr TypeExpr -> ICM (AExpr TypeExpr)
-- splitCases v@(AVar        _ _) = return v
-- splitCases l@(ALit        _ _) = return l
-- splitCases (AComb ty ct qn es) = AComb ty ct qn <$> mapM splitCases es
-- splitCases (ALet      ty bs e) = ALet ty <$> mapM splitBinding bs
--                                          <*> splitCases e
--   where splitBinding (v, ve) = splitCases ve >>= \ve' -> return (v, ve')
-- splitCases (AFree     ty vs e) = AFree ty vs <$> splitCases e
-- splitCases (AOr      ty e1 e2) = AOr ty <$> splitCases e1 <*> splitCases e2
-- splitCases c@(ACase  ty ct e bs)
-- --  | isBoolType (annExpr e)     = idCase (splitCase ty ct e bs)
--   | otherwise                  = idCase c
-- splitCases (ATyped   ty e ty') = flip (ATyped ty) ty' <$> splitCases e
--
-- --- Split up case expressions over conditionals (i.e. sequences of simple
-- --- boolean expressions connected with `&&` or `||`)
-- splitCase :: TypeExpr -> CaseType -> AExpr TypeExpr -> [ABranchExpr TypeExpr]
--           -> AExpr TypeExpr
-- splitCase ty ct e bs
--   | isConj e  = splitCase ty ct c1 (branch truePat  : selBranch falsePat bs)
--   | isDisj e  = splitCase ty ct c1 (branch falsePat : selBranch truePat  bs)
--   | otherwise = ACase ty ct (rnmCmpOps e) bs
--   where [c1,c2]   = combArgs e
--         innerCase = splitCase ty ct c2 bs
--         branch p  = ABranch p innerCase
--
-- --- Add a unique identifier to a case expression
-- idCase :: AExpr TypeExpr -> ICM (AExpr TypeExpr)
-- idCase exp = case exp of
--   ACase ty ct e bs -> do
--     v   <- freshID
--     bs' <- mapM splitBranch bs
--     return $ ALet ty [((v, tyE), e)] (ACase ty ct (AVar tyE v) bs')
--    where tyE                        = annExpr e
--          splitBranch (ABranch p be) = ABranch p <$> splitCases be
--   _                -> splitCases exp
--
-- --- Rename all operators for comparisons on literals
-- rnmCmpOps :: AExpr a -> AExpr a
-- rnmCmpOps = updCombs rplCmp
--   where rplCmp ann ct f@(qn, qna) args = case lookup qn builtinCmpOps of
--           Nothing  -> AComb ann ct f args
--           Just qn' -> let n   = 2 - length args
--                           ct' = if n == 0 then FuncCall else FuncPartCall n
--                       in AComb ann ct' (qn', qna) args
--
-- -- helper
--
-- -- select the branch expression matching the given pattern
-- selBranch :: APattern a -> [ABranchExpr a] -> [ABranchExpr a]
-- selBranch _ []                     = []
-- selBranch p (b@(ABranch q _) : bs)
--   | eqPattern p q                  = [b]
--   | otherwise                      = selBranch p bs
--
-- --- Logical operations on integers and floats which are builtin
-- builtinCmpOps :: [(QName, QName)]
-- builtinCmpOps = map (\(a, b) -> (prel a, prel b))
--   -- integers
--   [ ("_impl#==#Prelude.Eq#Prelude.Int" , "_==")
--   , ("_impl#/=#Prelude.Eq#Prelude.Int" , "_/=")
--   , ("_impl#<#Prelude.Ord#Prelude.Int" , "_<")
--   , ("_impl#<=#Prelude.Ord#Prelude.Int", "_<=")
--   , ("_impl#>#Prelude.Ord#Prelude.Int" , "_>")
--   , ("_impl#>=#Prelude.Ord#Prelude.Int", "_>=")
--   -- floats
--   , ("_impl#==#Prelude.Eq#Prelude.Float" , "_==")
--   , ("_impl#/=#Prelude.Eq#Prelude.Float" , "_/=")
--   , ("_impl#<#Prelude.Ord#Prelude.Float" , "_<")
--   , ("_impl#<=#Prelude.Ord#Prelude.Float", "_<=")
--   , ("_impl#>#Prelude.Ord#Prelude.Float" , "_>")
--   , ("_impl#>=#Prelude.Ord#Prelude.Float", "_>=")
--   ]