Commit 157a03d0 authored by Michael Hanus 's avatar Michael Hanus
Browse files

binding optimizer updated

parent b4de6edf
......@@ -2,9 +2,16 @@ cdbi: Type-safe database programming
====================================
This package contains libraries to support type-safe database programming.
[This paper](http://www.informatik.uni-kiel.de/~mh/papers/JFLP04_dyn.html)
[This paper](http://dx.doi.org/10.4204/EPTCS.234.8)
contains a description of the basic ideas behind these libraries.
Since the current implementation is based on the
[SQLite](https://www.sqlite.org/) database system,
it must be installed together with the command line interface `sqlite3`.
This can be done in a Ubuntu distribution by
sudo apt-get install sqlite3
Usually, it is not necessary to use these libraries directly.
Instead, one can use the Curry preprocessor to formulate
type-safe SQL queries which are translated into calls to these libraries.
......
......@@ -13,12 +13,13 @@ Consider the following definition of the operation \code{last}
to extract the last element in list:
%
\begin{curry}
last xs | xs == _++[x]
last :: Data a => [a] -> a
last xs | xs === _ ++ [x]
= x
where x free
\end{curry}
%
In order to evaluate the condition \ccode{xs == \us{}++[x]},
In order to evaluate the condition \ccode{xs === \us{}++[x]},
the Boolean equality is evaluated to \code{True} or \code{False}
by instantiating the free variables \code{\us} and \code{x}.
However, since we know that a condition must be evaluated to
......@@ -26,6 +27,7 @@ However, since we know that a condition must be evaluated to
we can use the constrained equality to obtain a more efficient program:
%
\begin{curry}
last :: Data a => [a] -> a
last xs | xs =:= _++[x]
= x
where x free
......@@ -33,17 +35,20 @@ last xs | xs =:= _++[x]
%
Since the selection of the appropriate equality operator
is not obvious and might be tedious, \CYS encourages
programmers to use only the Boolean equality operator \ccode{==}
programmers to use only the Boolean equality operator \ccode{===}
in programs.
The constraint equality operator \ccode{=:=} can be considered
as an optimization of \ccode{==} if it is ensured that only
as an optimization of \ccode{===} if it is ensured that only
positive results are required, e.g., in conditions of program rules.
To support this programming style, \CYS has a built-in optimization phase
on FlatCurry files. For this purpose, the optimizer analyzes
the FlatCurry programs for occurrences of \ccode{==}
the FlatCurry programs for occurrences of \ccode{===}
and replaces them by \ccode{=:=} whenever the result \code{False}
is not required.
is not required.\footnote{The current optimizer
also replaces occurrences of \texttt{(==)} although this
transformation is valid only if the corresponding \texttt{Eq} instances
define equality rather than equivalence.}
The usage of the optimizer can be influenced by setting
the property flag \code{bindingoptimization} in the
configuration file \code{\curryrc}.
......
......@@ -38,7 +38,7 @@ genExpWithVar' n = if n==0 then Add (Var X1) (Num O)
-- return some variable occurring in an expression:
varInExp :: Exp -> VarName
varInExp exp | replace x y (Var v) == exp
varInExp exp | replace x y (Var v) === exp
= v
where x, y, v free
......@@ -53,7 +53,7 @@ test_varInExp = varInExp (genExpWithVar' 100) -=- X1
----------------------------------------------------------------
simplify :: Exp -> Exp
simplify exp | replace c p (evalTo x) == exp
simplify exp | replace c p (evalTo x) === exp
= replace c p x
where c, p, x free
......
......@@ -30,11 +30,11 @@ sem (Alt a b) = sem a ? sem b
sem (Conc a b) = sem a ++ sem b
sem (Star a) = [] ? sem (Conc a (Star a))
grep :: (Data a, Eq a) => RE a -> [a] -> Bool
grep r s | _ ++ sem r ++ _ == s = True
grep :: Data a => RE a -> [a] -> Bool
grep r s | _ ++ sem r ++ _ === s = True
bigABABC :: Int -> [Chr]
bigABABC n = take n (concatMap (\i->A : take i (repeat B)) [1..]) ++ [A,B,C]
bigABABC n = take n (concatMap (\i -> A : take i (repeat B)) [1..]) ++ [A,B,C]
main :: Bool
main = grep abstarc (bigABABC 50)
......
......@@ -18,7 +18,7 @@ add O p = p
add (S p) q = S (add p q)
half :: Peano -> Peano
half y | add x x == y
half y | add x x === y
= x
where x free
......
......@@ -2,8 +2,8 @@
import Test.Prop
last :: (Data a, Eq a) => [a] -> a
last xs | _ ++ [x] == xs = x where x free
last :: Data a => [a] -> a
last xs | _ ++ [x] === xs = x where x free
main :: Int
main = last [1,2,3]
......
......@@ -2,8 +2,8 @@
import Test.Prop
f :: (Data a, Eq a) => [a] -> [a] -> a
f xs ys | xs == _ ++ [x] && ys == _ ++ [x] ++ _ = x where x free
f :: Data a => [a] -> [a] -> a
f xs ys | xs === _ ++ [x] && ys === _ ++ [x] ++ _ = x where x free
main :: Int
main = f [1,2] [2,1]
......
......@@ -31,15 +31,20 @@ import CASS.Server ( analyzeGeneric, analyzePublic, analyzeInterface )
import System.CurryPath ( currySubdir, addCurrySubdir, splitModuleFileName )
import Text.CSV
type Options = (Int, Bool, Bool) -- (verbosity, use analysis?, auto-load?)
------------------------------------------------------------------------------
-- The options for the transformation.
data Options = Options { verbosity :: Int -- verbosity
, withAnalysis :: Bool -- use analysis?
, eqvTrans :: Bool -- transform also (==)?
, loadProg :: Bool -- load transformed program?
}
defaultOptions :: Options
defaultOptions = (1, True, False)
defaultOptions = Options 1 True True False
systemBanner :: String
systemBanner =
let bannerText = "Curry Binding Optimizer (version of 06/01/2021)"
let bannerText = "Curry Binding Optimizer (version of 07/01/2021)"
bannerLine = take (length bannerText) (repeat '=')
in bannerLine ++ "\n" ++ bannerText ++ "\n" ++ bannerLine
......@@ -49,10 +54,13 @@ usageComment = unlines
, " -v<n> : set verbosity level (n=0|1|2|3)"
, " -f : fast transformation without analysis"
, " (uses only information about the standard prelude)"
, " -s : transform only (===) but not (==)"
, " -l : load optimized module into Curry system"
, " -h, -? : show this help text"
]
------------------------------------------------------------------------------
-- main function to call the optimizer:
main :: IO ()
main = getArgs >>= checkArgs defaultOptions
......@@ -65,20 +73,18 @@ mainCallError args = do
exitWith 1
checkArgs :: Options -> [String] -> IO ()
checkArgs opts@(verbosity, withana, load) args = case args of
checkArgs opts 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
in if v >= 0 && v < 4
then checkArgs opts { verbosity = v } margs
else mainCallError args
"-f" : margs -> checkArgs opts { withAnalysis = False } margs
"-s" : margs -> checkArgs opts { eqvTrans = False } margs
"-l" : margs -> checkArgs opts { loadProg = True } margs
"-h" : _ -> putStr (systemBanner++'\n':usageComment)
"-?" : _ -> putStr (systemBanner++'\n':usageComment)
mods -> do printVerbose opts 1 systemBanner
mapM_ (transformBoolEq opts) mods
-- Verbosity level:
......@@ -86,12 +92,11 @@ checkArgs opts@(verbosity, withana, load) args = case args of
-- 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 =
unless (null message || verbosity < printlevel) $ putStrLn message
printVerbose :: Options -> Int -> String -> IO ()
printVerbose opts printlevel message =
unless (null message || verbosity opts < printlevel) $ putStrLn message
transformBoolEq :: Options -> String -> IO ()
transformBoolEq opts name = do
......@@ -113,49 +118,53 @@ modNameOfFcyName name =
dir </> intercalate "." (split (==pathSeparator) wosubdir)
transformAndStoreFlatProg :: Options -> String -> String -> Prog -> IO ()
transformAndStoreFlatProg opts@(verb, _, load) modname fcyfile prog = do
printVerbose verb 1 $ "Reading and analyzing module '" ++ modname ++ "'..."
transformAndStoreFlatProg opts modname fcyfile prog = do
printVerbose opts 1 $ "Reading and analyzing module '" ++ modname ++ "'..."
starttime <- getCPUTime
(newprog, transformed) <- transformFlatProg opts modname prog
let optfcyfile = fcyfile ++ "_OPT"
when transformed $ writeFCY optfcyfile newprog
stoptime <- getCPUTime
printVerbose verb 2 $ "Transformation time for " ++ modname ++ ": " ++
printVerbose opts 2 $ "Transformation time for " ++ modname ++ ": " ++
show (stoptime-starttime) ++ " msecs"
when transformed $ do
printVerbose verb 2 $ "Transformed program stored in " ++ optfcyfile
printVerbose opts 2 $ "Transformed program stored in " ++ optfcyfile
renameFile optfcyfile fcyfile
printVerbose verb 2 $ " ...and moved to " ++ fcyfile
when load $ system (curryComp ++ " :l " ++ modname) >> return ()
printVerbose opts 2 $ " ...and moved to " ++ fcyfile
when (loadProg opts) $ do
system $ curryComp ++ " -Dbindingoptimization=no :l " ++ modname
return ()
where curryComp = installDir </> "bin" </> curryCompiler
-- Perform the binding optimization on a FlatCurry program.
-- Return the new FlatCurry program and a flag indicating whether
-- something has been changed.
transformFlatProg :: Options -> String -> Prog -> IO (Prog, Bool)
transformFlatProg (verb, withanalysis, _) modname
transformFlatProg opts modname
(Prog mname imports tdecls fdecls opdecls)= do
lookupreqinfo <-
if withanalysis
if withAnalysis opts
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)
printVerbose opts 2 $
"\nResult of \"RequiredValue\" analysis:\n" ++
showInfos (showAFType AText)
(if verbosity opts == 3 then reqinfo else mreqinfo)
return (flip lookupProgInfo reqinfo)
else return (flip lookup preludeBoolReqValues)
let (stats,newfdecls) = unzip (map (transformFuncDecl lookupreqinfo) fdecls)
let (stats,newfdecls) = unzip (map (transformFuncDecl opts lookupreqinfo)
fdecls)
numtranseqs = totalTransEqs stats
numtranseqv = totalTransEqv stats
numbeqs = totalBEqs stats
csvfname = mname ++ "_BOPTSTATS.csv"
printVerbose verb 2 $ statSummary stats
printVerbose verb 1 $
printVerbose opts 2 $ statSummary stats
printVerbose opts 1 $
"Total number of transformed (dis)equalities: " ++
show numtranseqs ++ " (===) and " ++
show numtranseqv ++ " (==)" ++
show numtranseqs ++ " (===) " ++
(if eqvTrans opts then " and " ++ show numtranseqv ++ " (==)" else "") ++
" (out of " ++ show numbeqs ++ ")"
unless (verb<2) $ do
unless (verbosity opts < 2) $ do
writeCSVFile csvfname (stats2csv stats)
putStrLn ("Detailed statistics written to '" ++ csvfname ++"'")
return ( Prog mname imports tdecls newfdecls opdecls
......@@ -177,17 +186,17 @@ showInfos showi =
-- Transform a function declaration.
-- Some statistical information and the new function declaration are returned.
transformFuncDecl :: (QName -> Maybe AFType) -> FuncDecl
transformFuncDecl :: Options -> (QName -> Maybe AFType) -> FuncDecl
-> (TransStat, FuncDecl)
transformFuncDecl lookupreqinfo fdecl@(Func qf@(_,fn) ar vis texp rule) =
if containsBeqRule rule
transformFuncDecl opts lookupreqinfo fdecl@(Func qf@(_,fn) ar vis texp rule) =
if containsBeqRule opts rule
then
let (tst,trule) = transformRule lookupreqinfo (initTState qf) rule
let (tst,trule) = transformRule opts lookupreqinfo (initTState qf) rule
in ( TransStat fn beqs (numTransEqs tst) (numTransEqv tst)
, Func qf ar vis texp trule )
else (TransStat fn 0 0 0, fdecl)
where
beqs = numberBeqRule rule
beqs = numberBeqRule opts rule
-------------------------------------------------------------------------
-- State threaded through the program transformer:
......@@ -221,9 +230,10 @@ incNumEqv tst = tst { numTransEqv = numTransEqv tst + 1 }
---
--- (not (Prelude.constrEq e1 e2))
transformRule :: (QName -> Maybe AFType) -> TState -> Rule -> (TState,Rule)
transformRule _ tst (External s) = (tst, External s)
transformRule lookupreqinfo tstr (Rule args rhs) =
transformRule :: Options -> (QName -> Maybe AFType) -> TState -> Rule
-> (TState,Rule)
transformRule _ _ tst (External s) = (tst, External s)
transformRule opts lookupreqinfo tstr (Rule args rhs) =
let (te,tste) = transformExp tstr rhs Any
in (tste, Rule args te)
where
......@@ -232,17 +242,17 @@ transformRule lookupreqinfo tstr (Rule args rhs) =
transformExp tst (Lit v) _ = (Lit v, tst)
transformExp tst0 exp@(Comb ct qf es) reqval
| reqval == aTrue && isBoolEqualCall True exp
= case checkBoolEqualCall True (Comb ct qf tes) of
| reqval == aTrue && isBoolEqualCall opts True exp
= case checkBoolEqualCall opts True (Comb ct qf tes) of
Just (eqs,targs) -> ( Comb FuncCall (pre "constrEq") targs
, (if eqs then incNumEqs else incNumEqv) tst1 )
Nothing -> error "transfromExp"
| reqval == aFalse && isBoolEqualCall False exp
= case checkBoolEqualCall False (Comb ct qf tes) of
Nothing -> error "Internal error: Nothing in transfromExp"
| reqval == aFalse && isBoolEqualCall opts False exp
= case checkBoolEqualCall opts False (Comb ct qf tes) of
Just (eqs,targs) -> ( Comb FuncCall (pre "not")
[Comb FuncCall (pre "constrEq") targs]
, (if eqs then incNumEqs else incNumEqv) tst1 )
Nothing -> error "transfromExp"
Nothing -> error "Internal error: Nothing in transfromExp"
| qf == pre "$" && length es == 2 &&
(isFuncPartCall (head es) || isConsPartCall (head es))
= transformExp tst0 (reduceDollar es) reqval
......@@ -302,8 +312,8 @@ transformRule lookupreqinfo tstr (Rule args rhs) =
-- (where dict is a dictionary parameter)
-- * a default instance (dis)equality call:
-- apply (apply ("_impl#==#Prelude.Eq#..." []) e1) e2
checkBoolEqualCall :: Bool -> Expr -> Maybe (Bool, [Expr])
checkBoolEqualCall eq exp = case exp of
checkBoolEqualCall :: Options -> Bool -> Expr -> Maybe (Bool, [Expr])
checkBoolEqualCall opts eq exp = case exp of
Comb FuncCall qf es ->
if isEqNameOrInst qf && length es > 1
then Just (isEqsNameOrInst qf,
......@@ -330,6 +340,7 @@ checkBoolEqualCall eq exp = case exp of
else qf == pre "/=="
isEqvNameOrInst qf@(_,f) =
eqvTrans opts && -- should we also transform (==)?
if eq then qf == pre "==" || "_impl#==#Prelude.Eq#" `isPrefixOf` f
else qf == pre "/=" || "_impl#/=#Prelude.Eq#" `isPrefixOf` f
......@@ -337,8 +348,8 @@ checkBoolEqualCall eq exp = case exp of
-- Is this a call to a Boolean equality?
-- If the first argument is `True`, it must be an equality call,
-- otherwise an disequality call.
isBoolEqualCall :: Bool -> Expr -> Bool
isBoolEqualCall eq exp = isJust (checkBoolEqualCall eq exp)
isBoolEqualCall :: Options -> Bool -> Expr -> Bool
isBoolEqualCall opts eq exp = isJust (checkBoolEqualCall opts eq exp)
-------------------------------------------------------------------------
......@@ -392,16 +403,16 @@ argumentTypesFor (Just (AFType rtypes)) reqval =
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
-- Does `Prelude.===` or `Prelude.==` occur in a rule?
containsBeqRule :: Options -> Rule -> Bool
containsBeqRule _ (External _) = False
containsBeqRule opts (Rule _ rhs) = containsBeqExp rhs
where
-- containsBeq an expression w.r.t. a required value
containsBeqExp (Var _) = False
containsBeqExp (Lit _) = False
containsBeqExp exp@(Comb _ _ es) =
isBoolEqualCall True exp || isBoolEqualCall False exp ||
isBoolEqualCall opts True exp || isBoolEqualCall opts False exp ||
any containsBeqExp es
containsBeqExp (Free _ e ) = containsBeqExp e
containsBeqExp (Or e1 e2 ) = containsBeqExp e1 || containsBeqExp e2
......@@ -412,18 +423,18 @@ containsBeqRule (Rule _ rhs) = containsBeqExp rhs
containsBeqBranch (Branch _ be) = containsBeqExp be
-- Number of occurrences of Prelude.== or Prelude./= occurring in a rule:
numberBeqRule :: Rule -> Int
numberBeqRule (External _) = 0
numberBeqRule (Rule _ rhs) = numberBeqExp rhs
-- Number of occurrences of `Prelude.===` or `Prelude./==` occurring in a rule:
numberBeqRule :: Options -> Rule -> Int
numberBeqRule _ (External _) = 0
numberBeqRule opts (Rule _ rhs) = numberBeqExp rhs
where
-- numberBeq an expression w.r.t. a required value
numberBeqExp (Var _) = 0
numberBeqExp (Lit _) = 0
numberBeqExp exp@(Comb _ _ es) =
case checkBoolEqualCall True exp of
case checkBoolEqualCall opts True exp of
Just (_,targs) -> 1 + sum (map numberBeqExp targs)
Nothing -> case checkBoolEqualCall False exp of
Nothing -> case checkBoolEqualCall opts False exp of
Just (_,fargs) -> 1 + sum (map numberBeqExp fargs)
Nothing -> sum (map numberBeqExp es)
numberBeqExp (Free _ e) = numberBeqExp e
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment