BindingOpt.curry 19.6 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1 2
-------------------------------------------------------------------------
--- Implementation of a transformation to replace Boolean equalities
3
--- by equational constraints (which binds variables).
Michael Hanus 's avatar
Michael Hanus committed
4 5
---
--- @author Michael Hanus
6
--- @version August 2018
Michael Hanus 's avatar
Michael Hanus committed
7 8
-------------------------------------------------------------------------

9
module BindingOpt (main, transformFlatProg) where
10

11
import Language.Curry.Distribution ( installDir, curryCompiler )
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
12 13 14 15 16 17 18 19 20
import System.Directory    ( renameFile )
import System.FilePath     ( (</>), (<.>), normalise, pathSeparator
                           , takeExtension, dropExtension )
import System.Environment  ( getArgs )
import System.Process      ( system, exitWith )
import System.CPUTime      ( getCPUTime )
import Data.List
import Data.Maybe          ( fromJust )
import Control.Monad       ( when, unless )
21 22 23
import FlatCurry.Types hiding  (Cons)
import FlatCurry.Files
import FlatCurry.Goodies
Michael Hanus 's avatar
Michael Hanus committed
24

25 26 27 28
import Analysis.Types
import Analysis.ProgInfo
import Analysis.RequiredValues
import CASS.Server       ( analyzeGeneric, analyzePublic, analyzeInterface )
Michael Hanus 's avatar
Michael Hanus committed
29
import System.CurryPath  ( currySubdir, addCurrySubdir, splitModuleFileName )
Michael Hanus 's avatar
Michael Hanus committed
30
import Text.CSV
31 32


33 34 35 36 37 38
type Options = (Int, Bool, Bool) -- (verbosity, use analysis?, auto-load?)

defaultOptions :: Options
defaultOptions = (1, True, False)

systemBanner :: String
Michael Hanus 's avatar
Michael Hanus committed
39
systemBanner =
40
  let bannerText = "Curry Binding Optimizer (version of 15/08/2018)"
Michael Hanus 's avatar
Michael Hanus committed
41 42 43
      bannerLine = take (length bannerText) (repeat '=')
   in bannerLine ++ "\n" ++ bannerText ++ "\n" ++ bannerLine

44 45
usageComment :: String
usageComment = unlines
46
  [ "Usage: curry-transbooleq [option] ... [module or FlatCurry file] ..."
47 48 49 50 51 52
  , "       -v<n>  : set verbosity level (n=0|1|2|3)"
  , "       -f     : fast transformation without analysis"
  , "                (uses only information about the standard prelude)"
  , "       -l     : load optimized module into Curry system"
  , "       -h, -? : show this help text"
  ]
Michael Hanus 's avatar
Michael Hanus committed
53 54

-- main function to call the optimizer:
55 56
main :: IO ()
main = getArgs >>= checkArgs defaultOptions
Michael Hanus 's avatar
Michael Hanus committed
57

58
mainCallError :: [String] -> IO ()
Michael Hanus 's avatar
Michael Hanus committed
59
mainCallError args = do
60
  putStrLn $ systemBanner
61
    ++ "\nIllegal arguments: " ++ unwords args
62
    ++ "\n" ++ usageComment
Michael Hanus 's avatar
Michael Hanus committed
63 64
  exitWith 1

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
checkArgs :: Options -> [String] -> IO ()
checkArgs opts@(verbosity, withana, load) args = case args of
  []                   -> mainCallError []
  -- verbosity option
  ('-':'v':d:[]):margs -> let v = ord d - ord '0'
                          in if v >= 0 && v <= 4
                              then checkArgs (v, withana, load) margs
                              else mainCallError args
  -- fast option
  "-f":margs           -> checkArgs (verbosity, False, load) margs
  -- auto-loading
  "-l":margs           -> checkArgs (verbosity, withana, True) margs
  "-h":_               -> putStr (systemBanner++'\n':usageComment)
  "-?":_               -> putStr (systemBanner++'\n':usageComment)
  mods                 -> do
                          printVerbose verbosity 1 systemBanner
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
81
                          mapM_ (transformBoolEq opts) mods
Michael Hanus 's avatar
Michael Hanus committed
82 83 84 85 86 87 88 89 90 91 92

-- Verbosity level:
-- 0 : show nothing
-- 1 : show summary of optimizations performed
-- 2 : show analysis infos and details of optimizations including timings
-- 3 : show analysis infos also of imported modules
-- 4 : show intermediate data (not yet used)

-- Output a string w.r.t. verbosity level
printVerbose :: Int -> Int -> String -> IO ()
printVerbose verbosity printlevel message =
93
  unless (null message || verbosity < printlevel) $ putStrLn message
Michael Hanus 's avatar
Michael Hanus committed
94

95 96
transformBoolEq :: Options -> String -> IO ()
transformBoolEq opts@(verb, _, _) name = do
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
97
  let isfcyname = takeExtension name == ".fcy"
98
      modname   = if isfcyname
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
99
                  then modNameOfFcyName (normalise (dropExtension name))
100
                  else name
101
  printVerbose verb 1 $ "Reading and analyzing module '" ++ modname ++ "'..."
Michael Hanus 's avatar
Michael Hanus committed
102
  flatprog <- if isfcyname then readFlatCurryFile name
103 104 105 106
                           else readFlatCurry     modname
  transformAndStoreFlatProg opts modname flatprog

-- Drop a suffix from a list if present or leave the list as is otherwise.
Michael Hanus 's avatar
Michael Hanus committed
107
dropSuffix :: Eq a => [a] -> [a] -> [a]
108 109
dropSuffix sfx s | sfx `isSuffixOf` s = take (length s - length sfx) s
                 | otherwise          = s
Michael Hanus 's avatar
Michael Hanus committed
110

111 112 113
-- Extracts the module name from a given FlatCurry file name:
modNameOfFcyName :: String -> String
modNameOfFcyName name =
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
114
  let wosuffix = normalise (dropExtension name)
115 116 117
      [dir,wosubdir] = splitOn (currySubdir ++ [pathSeparator]) wosuffix
   in -- construct hierarchical module name:
      dir </> intercalate "." (split (==pathSeparator) wosubdir)
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
118

119 120
transformAndStoreFlatProg :: Options -> String -> Prog -> IO ()
transformAndStoreFlatProg opts@(verb, _, load) modname prog = do
121
  let (dir, name) = splitModuleFileName (progName prog) modname
122
      oldprogfile = normalise $ addCurrySubdir dir </>  name         <.> "fcy"
123
      newprogfile = normalise $ addCurrySubdir dir </>  name ++ "_O" <.> "fcy"
Michael Hanus 's avatar
Michael Hanus committed
124
  starttime <- getCPUTime
125
  (newprog, transformed) <- transformFlatProg opts modname prog
Michael Hanus 's avatar
Michael Hanus committed
126 127 128 129 130
  when transformed $ writeFCY newprogfile newprog
  stoptime <- getCPUTime
  printVerbose verb 2 $ "Transformation time for " ++ modname ++ ": " ++
                        show (stoptime-starttime) ++ " msecs"
  when transformed $ do
131 132 133
    printVerbose verb 2 $ "Transformed program stored in " ++ newprogfile
    renameFile newprogfile oldprogfile
    printVerbose verb 2 $ " ...and moved to " ++ oldprogfile
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
134
  when load $ system (curryComp ++ " :l " ++ modname) >> return ()
135
 where curryComp = installDir </> "bin" </> curryCompiler
Michael Hanus 's avatar
Michael Hanus committed
136 137 138 139

-- Perform the binding optimization on a FlatCurry program.
-- Return the new FlatCurry program and a flag indicating whether
-- something has been changed.
140 141
transformFlatProg :: Options -> String -> Prog -> IO (Prog, Bool)
transformFlatProg (verb, withanalysis, _) modname
Michael Hanus 's avatar
Michael Hanus committed
142 143 144 145 146 147 148 149 150 151
                  (Prog mname imports tdecls fdecls opdecls)= do
  lookupreqinfo <-
    if withanalysis
    then do (mreqinfo,reqinfo) <- loadAnalysisWithImports reqValueAnalysis
                                                          modname imports
            printVerbose verb 2 $ "\nResult of \"RequiredValue\" analysis:\n"++
                                  showInfos (showAFType AText)
                                     (if verb==3 then reqinfo else mreqinfo)
            return (flip lookupProgInfo reqinfo)
    else return (flip lookup preludeBoolReqValues)
152 153 154 155 156 157 158 159 160 161 162
  let (stats,newfdecls) = unzip (map (transformFuncDecl lookupreqinfo) fdecls)
      numtrans = totalTrans stats
      numbeqs  = totalBEqs  stats
      csvfname = mname ++ "_BOPTSTATS.csv"
  printVerbose verb 2 $ statSummary stats
  printVerbose verb 1 $
     "Total number of transformed (dis)equalities: " ++ show numtrans ++
     " (out of " ++ show numbeqs ++ ")"
  unless (verb<2) $ do
    writeCSVFile csvfname (stats2csv stats)
    putStrLn ("Detailed statistics written to '" ++ csvfname ++"'")
163
  return (Prog mname imports tdecls newfdecls opdecls, numtrans > 0)
Michael Hanus 's avatar
Michael Hanus committed
164

165
loadAnalysisWithImports :: (Read a, Show a) => Analysis a -> String -> [String]
Michael Hanus 's avatar
Michael Hanus committed
166 167 168
                        -> IO (ProgInfo a,ProgInfo a)
loadAnalysisWithImports analysis modname imports = do
  maininfo <- analyzeGeneric analysis modname >>= return . either id error
Kai-Oliver Prott's avatar
Kai-Oliver Prott committed
169
  impinfos <- mapM (\m -> analyzePublic analysis m >>=
Michael Hanus 's avatar
Michael Hanus committed
170 171 172 173 174 175 176 177 178 179
                                                     return . either id error)
                    imports
  return $ (maininfo, foldr1 combineProgInfo (maininfo:impinfos))

showInfos :: (a -> String) -> ProgInfo a -> String
showInfos showi =
  unlines . map (\ (qn,i) -> snd qn ++ ": " ++ showi i)
          . (\p -> fst p ++ snd p) . progInfo2Lists

-- Transform a function declaration.
180 181 182 183
-- Some statistical information and the new function declaration are returned.
transformFuncDecl :: (QName -> Maybe AFType) -> FuncDecl
                  -> (TransStat,FuncDecl)
transformFuncDecl lookupreqinfo fdecl@(Func qf@(_,fn) ar vis texp rule) =
Michael Hanus 's avatar
Michael Hanus committed
184 185 186 187
  if containsBeqRule rule
  then
    let (tst,trule) = transformRule lookupreqinfo (initTState qf) rule
        on = occNumber tst
188 189 190 191
     in (TransStat fn beqs on, Func qf ar vis texp trule)
  else (TransStat fn 0 0, fdecl)
 where
  beqs = numberBeqRule rule
Michael Hanus 's avatar
Michael Hanus committed
192 193

-------------------------------------------------------------------------
194
-- State threaded through the program transformer:
Michael Hanus 's avatar
Michael Hanus committed
195
-- * name of current function
196
-- * number of occurrences of (==) that are replaced by 'constrEq'
Michael Hanus 's avatar
Michael Hanus committed
197 198
data TState = TState QName Int

199
initTState :: QName -> TState
Michael Hanus 's avatar
Michael Hanus committed
200 201
initTState qf = TState qf 0

202
occNumber :: TState -> Int
Michael Hanus 's avatar
Michael Hanus committed
203 204
occNumber (TState _ on) = on

205
incOccNumber :: TState -> TState
Michael Hanus 's avatar
Michael Hanus committed
206 207 208 209 210 211 212
incOccNumber (TState qf on) = TState qf (on+1)

-------------------------------------------------------------------------
--- Transform a FlatCurry program rule w.r.t. information about required
--- values. If there is an occurrence of (e1==e2) where the value `True`
--- is required, then this occurrence is replaced by
---
213
---     (constrEq e1 e2)
Michael Hanus 's avatar
Michael Hanus committed
214 215 216
---
--- Similarly, (e1/=e2) with required value `False` is replaced by
---
217
---     (not (constrEq e1 e2))
Michael Hanus 's avatar
Michael Hanus committed
218 219 220 221 222 223 224 225 226 227

transformRule :: (QName -> Maybe AFType) -> TState -> Rule -> (TState,Rule)
transformRule _ tst (External s) = (tst, External s)
transformRule lookupreqinfo tstr (Rule args rhs) =
  let (te,tste) = transformExp tstr rhs Any
   in (tste, Rule args te)
 where
  -- transform an expression w.r.t. a required value
  transformExp tst (Var i) _ = (Var i, tst)
  transformExp tst (Lit v) _ = (Lit v, tst)
228
  transformExp tst0 exp@(Comb ct qf es) reqval
Michael Hanus 's avatar
Michael Hanus committed
229
    | reqval == aTrue && isBoolEqualCall "==" exp
230
    = (Comb FuncCall (pre "constrEq") (argsOfBoolEqualCall "==" (Comb ct qf tes))
231
      , incOccNumber tst1)
Michael Hanus 's avatar
Michael Hanus committed
232
    | reqval == aFalse && isBoolEqualCall "/=" exp
233
    = (Comb FuncCall (pre "not")
234
         [Comb FuncCall (pre "constrEq") (argsOfBoolEqualCall "/=" (Comb ct qf tes))]
235
      , incOccNumber tst1)
236 237 238 239 240 241 242
    | qf == pre "$" && length es == 2 &&
      (isFuncPartCall (head es) || isConsPartCall (head es))
    = transformExp tst0 (reduceDollar es) reqval
    | otherwise
    = (Comb ct qf tes, tst1)
   where reqargtypes = argumentTypesFor (lookupreqinfo qf) reqval
         (tes,tst1)  = transformExps tst0 (zip es reqargtypes)
Michael Hanus 's avatar
Michael Hanus committed
243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
  transformExp tst0 (Free vars e) reqval =
    let (te,tst1) = transformExp tst0 e reqval
     in (Free vars te, tst1)
  transformExp tst0 (Or e1 e2) reqval =
    let (te1,tst1) = transformExp tst0 e1 reqval
        (te2,tst2) = transformExp tst1 e2 reqval
     in (Or te1 te2, tst2)
  transformExp tst0 (Typed e t) reqval =
    let (te,tst1) = transformExp tst0 e reqval
     in (Typed te t, tst1)
  transformExp tst0 (Case ct e bs) reqval =
    let (te ,tst1) = transformExp tst0 e (caseArgType bs)
        (tbs,tst2) = transformBranches tst1 bs reqval
     in (Case ct te tbs, tst2)
  transformExp tst0 (Let bs e) reqval =
    let (tbes,tst1) = transformExps tst0 (zip (map snd bs) (repeat Any))
        (te,tst2) = transformExp tst1 e reqval
     in (Let (zip (map fst bs) tbes) te, tst2)

  transformExps tst [] = ([],tst)
  transformExps tst ((exp,rv):exps) =
    let (te, tste ) = transformExp tst exp rv
        (tes,tstes) = transformExps tste exps
     in (te:tes, tstes)

  transformBranches tst [] _ = ([],tst)
  transformBranches tst (br:brs) reqval =
    let (tbr,tst1) = transformBranch tst br reqval
        (tbrs,tst2) = transformBranches tst1 brs reqval
     in (tbr:tbrs, tst2)

  transformBranch tst (Branch pat be) reqval =
    let (tbe,tstb) = transformExp tst be reqval
     in (Branch pat tbe, tstb)

278 279 280 281 282 283
-------------------------------------------------------------------------
-- Check whether the expression argument is a call to a Boolean (dis)equality
-- and return the arguments of the call.
-- The first argument is "==" (for checking equalities) or "/="
-- (for checking disequalities).
-- If type classes are present, a Boolean (dis)equality call can be
284 285
-- * an instance (dis)equality call: "_impl#==#Prelude.Eq#..." ... e1 e2
--   (where there can be additional arguments for other Eq dicts)
286 287 288 289
-- * a class (dis)equality call: apply (apply ("==" [dict]) e1) e2
--   (where dict is a dictionary parameter)
-- * a default instance (dis)equality call:
--   apply (apply ("_impl#==#Prelude.Eq#..." []) e1) e2
Michael Hanus 's avatar
Michael Hanus committed
290 291
checkBoolEqualCall :: String -> Expr -> Maybe [Expr]
checkBoolEqualCall deq exp = case exp of
292 293
  Comb FuncCall qf es ->
    if isNotEqualInstanceFunc qf && length es > 1
294 295
      then Just (drop (length es - 2) es)
                -- drop possible Eq dictionary arguments
296 297 298 299
      else if qf == pre "apply"
             then case es of
                    [Comb FuncCall qfa [Comb FuncCall qfe [_],e1],e2] ->
                      if qfa == pre "apply" &&
Michael Hanus 's avatar
Michael Hanus committed
300
                         (qfe == pre deq || isNotEqualInstanceFunc qfe)
301 302 303 304
                        then Just [e1,e2]
                        else Nothing
                    [Comb FuncCall qfa [Comb FuncCall qfe [],e1],e2] ->
                      if qfa == pre "apply" &&
Michael Hanus 's avatar
Michael Hanus committed
305
                         (qfe == pre deq || isNotEqualInstanceFunc qfe)
306 307 308 309 310 311 312 313 314 315
                        then Just [e1,e2]
                        else Nothing
                    _ -> Nothing
             else Nothing
  _ -> Nothing
 where
  isNotEqualInstanceFunc (_,f) =
    ("_impl#"++deq++"#Prelude.Eq#") `isPrefixOf` f

-- Is this a call to a Boolean equality?
Michael Hanus 's avatar
Michael Hanus committed
316 317
isBoolEqualCall :: String -> Expr -> Bool
isBoolEqualCall deq exp = checkBoolEqualCall deq exp /= Nothing
318 319

-- Returns the arguments of a call to a Boolean equality.
Michael Hanus 's avatar
Michael Hanus committed
320 321
argsOfBoolEqualCall :: String -> Expr -> [Expr]
argsOfBoolEqualCall deq exp = fromJust (checkBoolEqualCall deq exp)
322 323

-------------------------------------------------------------------------
324

Michael Hanus 's avatar
Michael Hanus committed
325
--- Reduce an application of Prelude.$ to a combination:
326 327 328 329 330 331 332
reduceDollar :: [Expr] -> Expr
reduceDollar args = case args of
  [Comb (FuncPartCall n) qf es, arg2]
    -> Comb (if n==1 then FuncCall else (FuncPartCall (n-1))) qf (es++[arg2])
  [Comb (ConsPartCall n) qf es, arg2]
    -> Comb (if n==1 then ConsCall else (ConsPartCall (n-1))) qf (es++[arg2])
  _ -> error "reduceDollar"
Michael Hanus 's avatar
Michael Hanus committed
333 334

--- Try to compute the required value of a case argument expression.
335 336 337 338 339
--- If one branch of the case expression is "False -> failed",
--- then the required value is `True` (this is due to the specific
--- translation of Boolean conditional rules of the front end).
--- If the case expression has one non-failing branch, the constructor
--- of this branch is chosen, otherwise it is `Any`.
340
caseArgType :: [BranchExpr] -> AType
341 342 343 344 345 346 347
caseArgType branches
  | not (null (tail branches)) &&
    branches!!1 == Branch (Pattern (pre "False") []) failedFC
  = aCons (pre "True")
  | length nfbranches /= 1
  = Any
  | otherwise = getPatCons (head nfbranches)
Michael Hanus 's avatar
Michael Hanus committed
348
 where
349 350 351 352 353 354
  failedFC = Comb FuncCall (pre "failed") []

  nfbranches = filter (\ (Branch _ be) -> be /= failedFC) branches

  getPatCons (Branch (Pattern qc _) _) = aCons qc
  getPatCons (Branch (LPattern _)   _) = Any
Michael Hanus 's avatar
Michael Hanus committed
355 356 357

--- Compute the argument types for a given abstract function type
--- and required value.
358
argumentTypesFor :: Maybe AFType -> AType -> [AType]
359 360
argumentTypesFor Nothing                _      = repeat Any
argumentTypesFor (Just EmptyFunc)       _      = repeat Any
361
argumentTypesFor (Just (AFType rtypes)) reqval =
Michael Hanus 's avatar
Michael Hanus committed
362 363
  maybe (-- no exactly matching type, look for Any type:
         maybe (-- no Any type: if reqtype==Any, try lub of all other types:
364
                if (reqval==Any || reqval==AnyC) && not (null rtypes)
Michael Hanus 's avatar
Michael Hanus committed
365 366 367
                then foldr1 lubArgs (map fst rtypes)
                else repeat Any)
               fst
368
               (find ((`elem` [AnyC,Any]) . snd) rtypes))
Michael Hanus 's avatar
Michael Hanus committed
369 370 371 372 373 374 375 376 377 378 379 380
        fst
        (find ((==reqval) . snd) rtypes)
 where
  lubArgs xs ys = map (uncurry lubAType) (zip xs ys)


-- Does Prelude.== occur in a rule?
containsBeqRule :: Rule -> Bool
containsBeqRule (External _) = False
containsBeqRule (Rule _ rhs) = containsBeqExp rhs
 where
  -- containsBeq an expression w.r.t. a required value
381 382 383
  containsBeqExp (Var _) = False
  containsBeqExp (Lit _) = False
  containsBeqExp exp@(Comb _ _ es) =
Michael Hanus 's avatar
Michael Hanus committed
384
    isBoolEqualCall "==" exp || isBoolEqualCall "/=" exp ||
385 386 387 388 389 390 391
    any containsBeqExp es
  containsBeqExp (Free _ e   ) = containsBeqExp e
  containsBeqExp (Or e1 e2   ) = containsBeqExp e1 || containsBeqExp e2
  containsBeqExp (Typed e _  ) = containsBeqExp e
  containsBeqExp (Case _ e bs) = containsBeqExp e || any containsBeqBranch bs
  containsBeqExp (Let bs e   ) = containsBeqExp e ||
                                 any containsBeqExp (map snd bs)
Michael Hanus 's avatar
Michael Hanus committed
392 393 394

  containsBeqBranch (Branch _ be) = containsBeqExp be

395 396 397 398 399 400
-- Number of occurrences of Prelude.== or Prelude./= occurring in a rule:
numberBeqRule :: Rule -> Int
numberBeqRule (External _) = 0
numberBeqRule (Rule _ rhs) = numberBeqExp rhs
 where
  -- numberBeq an expression w.r.t. a required value
401 402 403
  numberBeqExp (Var _) = 0
  numberBeqExp (Lit _) = 0
  numberBeqExp exp@(Comb _ _ es) =
Michael Hanus 's avatar
Michael Hanus committed
404 405 406 407
    if isBoolEqualCall "==" exp
      then 1 + sum (map numberBeqExp (argsOfBoolEqualCall "==" exp))
      else if isBoolEqualCall "/=" exp
             then 1  + sum (map numberBeqExp (argsOfBoolEqualCall "/=" exp))
408 409 410 411 412 413
             else sum (map numberBeqExp es)
  numberBeqExp (Free _ e) = numberBeqExp e
  numberBeqExp (Or e1 e2) = numberBeqExp e1 + numberBeqExp e2
  numberBeqExp (Typed e _) = numberBeqExp e
  numberBeqExp (Case _ e bs) = numberBeqExp e + sum (map numberBeqBranch bs)
  numberBeqExp (Let bs e) = numberBeqExp e + sum (map numberBeqExp (map snd bs))
414 415 416

  numberBeqBranch (Branch _ be) = numberBeqExp be

417 418
pre :: String -> QName
pre n = ("Prelude", n)
Michael Hanus 's avatar
Michael Hanus committed
419 420 421

-------------------------------------------------------------------------
-- Loading prelude analysis result:
422
loadPreludeBoolReqValues :: IO [(QName, AFType)]
Michael Hanus 's avatar
Michael Hanus committed
423 424 425 426 427
loadPreludeBoolReqValues = do
  maininfo <- analyzeInterface reqValueAnalysis "Prelude" >>=
                                                return . either id error
  return (filter (hasBoolReqValue . snd) maininfo)
 where
428
  hasBoolReqValue EmptyFunc = False
Michael Hanus 's avatar
Michael Hanus committed
429 430 431
  hasBoolReqValue (AFType rtypes) =
    maybe False (const True) (find (isBoolReqValue . snd) rtypes)

432
  isBoolReqValue rt = rt == aFalse || rt == aTrue
Michael Hanus 's avatar
Michael Hanus committed
433 434

-- Current relevant Boolean functions of the prelude:
435
preludeBoolReqValues :: [(QName, AFType)]
Michael Hanus 's avatar
Michael Hanus committed
436
preludeBoolReqValues =
437 438 439
 [(pre "&&",    AFType [([Any,Any],aFalse), ([aTrue,aTrue],aTrue)])
 ,(pre "not",   AFType [([aTrue],aFalse), ([aFalse],aTrue)])
 ,(pre "||",    AFType [([aFalse,aFalse],aFalse), ([Any,Any],aTrue)])
440
 ,(pre "&",     AFType [([aTrue,aTrue],aTrue)])
441 442
 ,(pre "solve", AFType [([aTrue],aTrue)])
 ,(pre "&&>",   AFType [([aTrue,Any],AnyC)])
Michael Hanus 's avatar
Michael Hanus committed
443
 ]
444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474

--- Map a constructor into an abstract value representing this constructor:
aCons :: QName -> AType
aCons qn = Cons [qn]

--- Abstract `False` value
aFalse :: AType
aFalse = aCons (pre "False")

--- Abstract `True` value
aTrue :: AType
aTrue  = aCons (pre "True")

-------------------------------------------------------------------------
--- Statistical information (e.g., for benchmarking the tool):
--- * function name
--- * number of Boolean (dis)equalities in the rule
--- * number of transformed (dis)equalities in the rule
data TransStat = TransStat String Int Int

--- Number of all transformations:
totalTrans :: [TransStat] -> Int
totalTrans = sum . map (\ (TransStat _ _ teqs) -> teqs)

--- Number of all Boolean (dis)equalities:
totalBEqs :: [TransStat] -> Int
totalBEqs = sum . map (\ (TransStat _ beqs _) -> beqs)

--- Show a summary of the actual transformations:
statSummary :: [TransStat] -> String
statSummary = concatMap showSum
475
 where
476 477 478 479 480
  showSum (TransStat fn _ teqs) =
    if teqs==0
      then ""
      else "Function "++fn++": "++
           (if teqs==1 then "one occurrence" else show teqs++" occurrences") ++
481
           " of (==) transformed into 'constrEq'\n"
482 483 484 485 486 487 488 489

--- Translate statistics into CSV format:
stats2csv :: [TransStat] -> [[String]]
stats2csv stats =
  ["Function","Boolean equalities", "Transformed equalities"] :
  map (\ (TransStat fn beqs teqs) -> [fn, show beqs, show teqs]) stats

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