Commit f98b45a3 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

structor of CExp changed

parent def9c133
......@@ -14,18 +14,19 @@ main = do
as <- getArgs
let ?to = 5
case as of
(fp:i:_) -> run1 fp (read i)
[fp] -> run1 fp Nothing
(fp:i:_) -> run1 fp (Just (read i))
_ -> print usage
where
usage = "<file>"
ec :: Program -> Int -> IO (Maybe (Result (CExp Rational)))
ec p i = listToMaybe <$> run (Pick i) (ect (fst (gen p)) zero)
ec :: Program -> Maybe Int -> IO (Maybe (Result (CExp Rational)))
ec p i = listToMaybe <$> run (sel i) (ect (fst (gen p)) zero) where
sel = maybe Any Pick
run1 :: (?to :: Int) => FilePath -> Int -> IO ()
run1 :: (?to :: Int) => FilePath -> Maybe Int -> IO ()
run1 fp i = do
programM <- fromFile fp
case programM of
......
......@@ -7,8 +7,7 @@ def trader():
price = price + 1
else:
price = price - 1
nShares = unif(0,10)
nShares = unif(0,20)
while nShares > 0:
nShares = nShares - 1
tick price
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DeriveTraversable, PatternSynonyms, StandaloneDeriving #-}
module Data.PWhile.BoolExpression
(
Conj (..)
......@@ -11,6 +10,7 @@ module Data.PWhile.BoolExpression
, disj, conj
, literals
, mapLiterals
, traverseLiterals
, top, bot
, le, leq, ge, geq
, lit
......@@ -32,14 +32,14 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.PWhile.Expression hiding (variables)
import qualified Data.PWhile.Expression as E
data Literal p q = p :>=: q
deriving (Eq, Ord, Read, Show, Data)
data Literal p = p :>=: p
deriving (Eq, Ord, Read, Show, Data, Functor, Foldable, Traversable)
type BLit = Literal Exp Exp
type BLit = Literal Exp
newtype Conj a = Conj { litsSet :: S.Set a } deriving (Eq, Ord, Read, Show, Data)
newtype Conj a = Conj { litsSet :: S.Set a } deriving (Eq, Ord, Read, Show, Data, Foldable)
newtype DNF a = Disj { conjSet :: S.Set (Conj a) } deriving (Eq, Ord, Read, Show, Data)
newtype DNF a = Disj { conjSet :: S.Set (Conj a) } deriving (Eq, Ord, Read, Show, Data, Foldable)
type BExp = DNF BLit
......@@ -65,13 +65,19 @@ conjs = S.toList . conjSet
lits :: Conj a -> [a]
lits = S.toList . litsSet
literals :: Ord l => DNF l -> S.Set l
literals = S.unions . S.map litsSet . conjSet
mapLiterals :: (Ord b) => (a -> b) -> DNF a -> DNF b
mapLiterals :: Ord b => (a -> b) -> DNF a -> DNF b
mapLiterals f (Disj cs) = bigOr [ disj [Conj (f `S.map` litsSet c)] | c <- S.toList cs]
traverseLiterals :: (Applicative f, Ord b) => (a -> f b) -> DNF a -> f (DNF b)
traverseLiterals f (Disj cs) =
bigOr <$> sequenceA [ disj <$> (: []) <$> traverseConj c | c <- S.toList cs]
where
traverseConj c = Conj <$> S.fromList <$> traverse f (S.toList (litsSet c))
top, bot :: DNF a
top = Top
bot = Bot
......@@ -139,7 +145,7 @@ variables g = S.unions [ E.variables a `S.union` E.variables b | (a :>=: b) <-
-- pretty
----------------------------------------------------------------------
instance (PP.Pretty p, PP.Pretty q) => PP.Pretty (Literal p q) where
instance PP.Pretty p => PP.Pretty (Literal p) where
pretty (e1 :>=: e2) =
PP.nest 2 (PP.group (PP.pretty e1 PP.<$> PP.nest 2 (PP.group (PP.text "≥" PP.<$> PP.pretty e2))))
......
{-# LANGUAGE DeriveTraversable, StandaloneDeriving #-}
module Data.PWhile.CostExpression where
import Data.Functor.Identity (runIdentity)
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import qualified Data.Set as S
......@@ -8,29 +8,45 @@ import Data.PWhile.BoolExpression hiding (variables)
import qualified Data.PWhile.BoolExpression as B
import qualified Data.PWhile.Expression as E
data GExp c = GExp BExp (E.Expression c)
data GExp c = GExp BExp c E.Exp
deriving Show
norm :: (Eq c, Num c) => BExp -> E.Exp -> GExp c
norm g e = GExp g e' where
e' = fmap fromIntegral e
-- plusG :: (Eq c, Ord c, Num c) => GExp c -> GExp c -> GExp c
-- plusG (GExp g1 e1) (GExp g2 e2) = GExp (g1 .&& g2) (e1 + e2)
mulG :: (Eq c, Ord c, Num c) => GExp c -> GExp c -> GExp c
mulG (GExp g1 k1 e1) (GExp g2 k2 e2) = GExp (g1 .&& g2) (k1 * k2) (e1 * e2)
-- norm :: (Eq c, Num c) => BExp c -> E.Expression c -> GExp c
-- norm g e = GExp g e' where
-- e' = fmap fromIntegral e
fromExp :: (Eq c, Num c) => E.Exp -> CExp c
fromExp = E . fmap fromIntegral
plusG :: (Eq c, Num c) => GExp c -> GExp c -> GExp c
plusG (GExp g1 e1) (GExp g2 e2) = GExp (g1 .&& g2) (e1 + e2)
mulG :: (Eq c, Num c) => GExp c -> GExp c -> GExp c
mulG (GExp g1 e1) (GExp g2 e2) = GExp (g1 .&& g2) (e1 * e2)
data CExp c =
E (E.Expression c)
| Div (CExp c) (E.Expression c)
E E.Exp
| Coeff c (CExp c)
| Div (CExp c) E.Exp
| Plus (CExp c) (CExp c)
| Sup (CExp c) (CExp c)
| Cond BExp (CExp c) (CExp c)
deriving (Eq, Ord, Read, Show, Foldable, Functor, Traversable)
deriving (Eq, Ord, Read, Show)
traverseCoeff :: (Num c', Ord c', Applicative f) => (c -> f c') -> CExp c -> f (CExp c')
traverseCoeff f = walk where
walk (E e) = pure (E e)
walk (Coeff k c) = coeff <$> f k <*> walk c
walk (Div c e) = divBy <$> walk c <*> pure e
walk (Plus c d) = plus <$> walk c <*> walk d
walk (Sup c d) = sup <$> walk c <*> walk d
walk (Cond b c d) = cond <$> pure b <*> walk c <*> walk d
mapCoeff :: (Num c', Ord c') => (c -> c') -> CExp c -> CExp c'
mapCoeff f = runIdentity . traverseCoeff (pure . f)
zero :: (Eq c, Num c) => CExp c
zero = E 0
......@@ -38,13 +54,22 @@ zero = E 0
one :: (Eq c, Num c) => CExp c
one = E 1
plus :: (Eq c, Num c) => CExp c -> CExp c -> CExp c
coeff :: (Eq c, Num c) => c -> CExp c -> CExp c
coeff 0 _ = zero
coeff 1 c = c
coeff k c = Coeff k c
plus :: (Eq c, Num c, Ord c) => CExp c -> CExp c -> CExp c
plus (Coeff k1 c1) (Coeff k2 c2)
| k1 == k2 = Coeff k1 (c1 `plus` c2)
plus (Div c1 e1) (Div c2 e2)
| e1 == e2 = (c1 `plus` c2) `divBy` e1
plus (E 0) c2 = c2
plus c1 (E 0) = c1
plus (E e1) (E e2) = E (e1 + e2)
plus c1 c2 = Plus c1 c2
sum :: (Eq c, Num c) => [CExp c] -> CExp c
sum :: (Eq c, Num c, Ord c) => [CExp c] -> CExp c
sum = foldl plus zero
sup :: (Eq c, Num c) => CExp c -> CExp c -> CExp c
......@@ -57,7 +82,7 @@ cond :: Eq c => BExp -> CExp c -> CExp c -> CExp c
cond Top c _ = c
cond Bot _ d = d
cond _ c d
| c == d = c
| c == d && c /= oneV = c
cond g (Cond g' c1 c2) d
| c2 == d = cond (g .&& g') c1 d
cond g c d = Cond g c d
......@@ -65,198 +90,78 @@ cond g c d = Cond g c d
guarded :: (Eq c, Num c) => BExp -> CExp c -> CExp c
guarded g c = cond g c zero
oneV :: CExp c
oneV = E "@@ONE@@"
pred :: (Eq c, Num c) => BExp -> CExp c
pred g = cond g one zero
pred g = cond g oneV zero
divBy :: (Eq c, Num c) => CExp c -> E.Expression c -> CExp c
divBy :: (Eq c, Ord c, Num c) => CExp c -> E.Exp -> CExp c
divBy c 1 = c
divBy (E e) f = case snd (E.factor e f) of { (e',1) -> E e'; (e',f') -> Div (E e') f' }
divBy (Div c e) f = Div c (e * f)
divBy c f = Div c f
simplify :: (Eq c, Num c) => CExp c -> CExp c
simplify (E e) = E (E.norm e)
simplify (Div c e) = simplify c `divBy` E.norm e
simplify (Plus c d) = simplify c `plus` simplify d
simplify (Sup c d) = simplify c `sup` simplify d
simplify (Cond g c d) = cond g (simplify c) (simplify d)
scale :: (Eq c, Num c) => E.Expression c -> CExp c -> CExp c
-- simplify :: (Eq c, Ord c, Num c) => CExp c -> CExp c
-- simplify (E e) = E (E.norm e)
-- simplify (Coeff k c)
-- | k == 0 = zero
-- | otherwise = Coeff k (simplify c)
-- simplify (Div c e) = simplify c `divBy` E.norm e
-- simplify (Plus c d) = simplify c `plus` simplify d
-- simplify (Sup c d) = simplify c `sup` simplify d
-- simplify (Cond g c d) = cond g (simplify c) (simplify d)
scale :: (Eq c, Ord c, Num c) => E.Exp -> CExp c -> CExp c
scale 0 _ = zero
scale 1 c = c
scale e (Coeff k c) = Coeff k (scale e c)
scale e (E f) = E (e * f)
scale e (Div d f) = scale e' d `divBy` f' where
(_,(e',f')) = E.factor e f
scale e (Div d f) = scale e' d `divBy` f' where (_,(e',f')) = E.factor e f
scale e (Plus d1 d2) = scale e d1 `plus` scale e d2
scale e (Sup d1 d2) = scale e d1 `sup` scale e d2
scale e (Cond g d1 d2) = cond g (scale e d1) (scale e d2)
toExp :: (Eq c, Num c) => CExp c -> Maybe (E.Expression c)
toExp (E f) = Just f
toExp (Plus d1 d2) = (+) <$> toExp d1 <*> toExp d2
toExp _ = Nothing
gExps :: CExp c -> [GExp c]
gExps = walk B.Top where
walk b (E e) = [GExp b e]
walk b (Div c _) = walk b c
walk b (Plus c d) = walk b c ++ walk b d
walk b (Sup c d) = walk b c ++ walk b d
walk b (Cond g c d) = walk (b .&& g) c ++ walk (b .&& neg g) d
fromGExp :: (Eq c, Num c) => GExp c -> CExp c
fromGExp (GExp g e) = guarded g (E e)
-- toExp :: (Eq c, Num c) => CExp c -> Maybe (E.Expression c)
-- toExp (E f) = Just f
-- toExp (Plus d1 d2) = (+) <$> toExp d1 <*> toExp d2
-- toExp _ = Nothing
gExps :: (Eq c, Num c) => CExp c -> [GExp c]
gExps = walk B.Top 1 where
walk B.Bot _ _ = []
walk b k (E e) = [GExp b k e]
walk b k (Coeff l c) = walk b (k * l) c
walk b k (Div c _) = walk b k c
walk b k (Plus c d) = walk b k c ++ walk b k d
walk b k (Sup c d) = walk b k c ++ walk b k d
walk b k (Cond g c d) = walk (b .&& g) k c ++ walk (b .&& neg g) k d
fromGExp :: (Eq c, Ord c, Num c) => GExp c -> CExp c
fromGExp (GExp g k e)
| k == 0 || e == 0 = zero
| otherwise = guarded g (coeff k (E e))
variables :: CExp c -> S.Set E.Var
variables (E e) = E.variables e
variables (Div c f) = variables c `S.union` E.variables f
variables (Plus c d) = variables c `S.union` variables d
variables (Sup c d) = variables c `S.union` variables d
variables (E e) = E.variables e
variables (Coeff _ c) = variables c
variables (Div c f) = variables c `S.union` E.variables f
variables (Plus c d) = variables c `S.union` variables d
variables (Sup c d) = variables c `S.union` variables d
variables (Cond g c d) = B.variables g `S.union` variables c `S.union` variables d
instance (Eq c, Num c) => E.Substitutable (CExp c) where
instance (Eq c, Ord c, Num c) => E.Substitutable (CExp c) where
substitute s e (E f) = E (E.substitute s e f)
substitute s e (Coeff k c) = Coeff k (E.substitute s e c)
substitute s e (Div c f) = E.substitute s e c `divBy` E.substitute s e f
substitute s e (Plus c d) = E.substitute s e c `plus` E.substitute s e d
substitute s e (Sup c d) = E.substitute s e c `sup` E.substitute s e d
substitute s e (Cond b c d) = cond (E.substitute s e b) (E.substitute s e c) (E.substitute s e d)
-- type CExp c = [CExp' c]
-- zero :: CExp c
-- zero = []
-- factorise :: Exp c -> Exp c -> (Exp c, (Exp c, Exp c))
-- factorise = undefined
-- scale :: CExp c -> Exp c -> CExp c
-- scale cs e = sum [ scale' c' | c' <- cs ] where
-- scale' (E f) = f * e
-- -- TODO factorise
-- scale' (c :/ f) = scale c e :/ f
-- scale' (Ite g c1 c2) = Ite g (scale c1 e) (scale c2 e)
-- scale' (Maximum cs) = supremum [ scale c' e | c' <- cs]
-- plus' :: CExp' c -> CExp c -> CExp c
-- plus' c' [] = [c']
-- plus' (E e) (E f : ds) = E (e + f) : ds
-- -- todo factorise
-- plus' (c :/ e) ((d :/ f) : ds) = ((scale c f `plus` scale d e) :/ (e * f)) : ds
-- plus' (Ite g c1 c2) (Ite h d1 d2 : ds)
-- | g == h = Ite g (c1 `plus` d1) (c2 `plus` d2) : ds
-- | g == neg h = Ite g (c1 `plus` d2) (c2 `plus` d1) : ds
-- plus' (Maximum cs) ds = Maximum cs : ds
-- plus' c' (d' : ds) = d' : plus c' ds
-- plus :: CExp c -> CExp c -> CExp c
-- plus = foldl plus'
-- sum :: [CExp c] -> CExp c
-- sum = foldl plus zero
-- supremum :: [CExp c] -> CExp c
-- supremum = Maximum
-- constant :: c -> CExp c
-- constant c = E (E.constant c)
-- instance (Eq c, Num c) => E.Substitutable (CExp' c) where
-- substitute s (E e) = E (substitute s e)
-- substitute s (c' :/ d) = E.substitute s c' :/ E.substitue s d
-- substitute s (Ite b c d) = Ite (E.substitute s b) (E.substitute s c) (E.substitute s d)
-- substitute s (Maximum cs) = supremum [ c' | c' <- substitute s `map` cs, c' \= zero]
-- instance (Eq c, Num c) => E.Substitutable (CExp c) where
-- substitute s = map (substitute s)
-- pretty
-- #ifndef DEBUG
-- instance {-# OVERLAPPING #-} PP.Pretty Rational where
-- pretty r
-- | d == 1 = PP.pretty n
-- | d == 0 = PP.pretty d
-- | otherwise = PP.pretty n <> PP.text "/" <> PP.pretty d
-- where (n,d) = (numerator r, denominator r)
-- #else
-- instance {-# OVERLAPPING #-} PP.Pretty Rational where
-- pretty r = PP.pretty n <> PP.text "/" <> PP.pretty d
-- where (n,d) = (numerator r, denominator r)
-- #endif
-- #ifndef DEBUG
-- instance (Eq a, Num a, PP.Pretty a) => PP.Pretty (Ratio a) where
-- pretty r
-- | d == 1 = PP.pretty n
-- | d == 0 = PP.pretty d
-- | otherwise = PP.parens (PP.pretty n) <> PP.text "/" <> PP.parens (PP.pretty d)
-- where (n,d) = (numerator r, denominator r)
-- #else
-- instance (Eq a, Num a, PP.Pretty a) => PP.Pretty (Ratio a) where
-- pretty r = PP.parens (PP.pretty n) <> PP.text "/" <> PP.parens (PP.pretty d)
-- where (n,d) = (numerator r, denominator r)
-- #endif
-- #ifndef DEBUG
-- instance PP.Pretty Norm where
-- pretty (Norm (E.Constant k)) = PP.pretty k
-- pretty (Norm n) = ppBars (PP.pretty (- (P.fromMonos as))
-- PP.<> PP.text ","
-- PP.<> PP.pretty (P.fromMonos bs))
-- where
-- (as,bs) = partition (\ (c,_) -> c < 0) (P.toMonos n)
-- ppBars d = PP.char '|' <> d <> PP.char '|'
-- #else
-- instance PP.Pretty Norm where
-- pretty (Norm e) = ppBars (PP.pretty e)
-- where
-- ppBars d = PP.char '|' <> d <> PP.char '|'
-- #endif
-- instance {-# OVERLAPPING #-} (PP.Pretty c, Num c, Eq c) => PP.Pretty (NormPoly c) where
-- pretty = P.ppPoly PP.pretty (PP.underline . PP.pretty)
-- #ifndef DEBUG
-- instance (PP.Pretty a, Num a, Eq a) => PP.Pretty (NormPolyFrac a) where
-- pretty (n :% d)
-- | d == 1 = PP.pretty n
-- | otherwise = PP.parens (PP.pretty n) PP.<> PP.text "/" PP.<> PP.parens (PP.pretty d)
-- #else
-- instance (PP.Pretty a, Num a, Eq a) => PP.Pretty (NormPolyFrac a) where
-- pretty (n :% d) = PP.parens (PP.pretty n) PP.<> PP.text "/" PP.<> PP.parens (PP.pretty d)
-- #endif
-- #ifndef DEBUG
-- instance PP.Pretty a => PP.Pretty (MaxExp a) where
-- pretty (Max []) = PP.text "0"
-- pretty (Max [a]) = PP.pretty a
-- pretty (Max as) = PP.text "max" PP.<> PP.tupled [ PP.pretty a | a <- as]
-- #else
-- instance PP.Pretty a => PP.Pretty (MaxExp a) where
-- pretty (Max as) = PP.text "max" PP.<> PP.tupled [ PP.pretty a | a <- as]
-- #endif
-- #ifndef DEBUG
-- instance PP.Pretty a => PP.Pretty (GuardedSum a) where
-- pretty (GS s) = PP.encloseSep PP.empty PP.empty add (pp `map` M.toList s)
-- where
-- add = ppSpace PP.<> ppAdd PP.<> ppSpace
-- pp (Top,e) = PP.pretty e
-- pp (b,e) = PP.brackets (PP.pretty b) PP.<> ppCdot PP.<> PP.parens (PP.pretty e)
-- #else
-- instance PP.Pretty a => PP.Pretty (GuardedSum a) where
-- pretty (GS s) = PP.encloseSep PP.empty PP.empty add (pp `map` M.toList s)
-- where
-- add = ppSpace PP.<> ppAdd PP.<> ppSpace
-- pp (b,e) = PP.brackets (PP.pretty b) PP.<> ppCdot PP.<> PP.parens (PP.pretty e)
-- #endif
instance (PP.Pretty c, Eq c, Num c) => PP.Pretty (CExp c) where
pretty = pp id where
pp _ (E e) = ppFun "E" [PP.pretty e]
pp _ (Coeff k c) = ppFun "mul" [PP.pretty k, PP.pretty c]
pp _ (Div c e) = ppFun "div" [ PP.pretty c, PP.pretty e ]
pp _ (Plus c d) = ppFun "plus" [ PP.pretty c, PP.pretty d ]
-- pp par (Div c e) = PP.parens (infx (pp id c) "/" (PP.pretty e))
......@@ -268,5 +173,5 @@ instance (PP.Pretty c, Eq c, Num c) => PP.Pretty (CExp c) where
-- infx d1 s d2 = d1 PP.</> PP.text s PP.<+> d2
ppFun f ls = PP.text f PP.<> PP.tupled ls
instance (PP.Pretty c, Eq c, Num c) => PP.Pretty (GExp c) where
instance (PP.Pretty c, Eq c, Ord c, Num c) => PP.Pretty (GExp c) where
pretty = PP.pretty . fromGExp
......@@ -46,12 +46,19 @@ variable = P.variable
variables :: Expression c -> S.Set Var
variables = S.fromList . P.variables
factor :: (Eq c, Num c) => Expression c -> Expression c -> (Expression c, (Expression c, Expression c))
-- factor :: (Eq c, Num c) => Expression c -> Expression c -> (Expression c, (Expression c, Expression c))
-- factor e1 e2 =
-- case P.factoriseMono [e1,e2] of
-- Just (m,[e1',e2']) -> (P.fromMono m, (e1',e2'))
-- _ -> (1,(e1,e2))
factor :: Exp -> Exp -> (Exp, (Exp, Exp))
factor e1 e2 =
case P.factoriseMono [e1,e2] of
Just (m,[e1',e2']) -> (P.fromMono m, (e1',e2'))
case P.factorise [P.norm e1,P.norm e2] of
Just ((c,m),[e1',e2']) -> (P.coefficient c * P.fromMono m, (e1',e2'))
_ -> (1,(e1,e2))
-- patterns
const_ :: (Ord v, Eq c, Num c) => P.Polynomial v c -> Maybe c
const_ (P.norm -> e)
......
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-unused-local-binds -Wno-orphans -Wno-unused-top-binds -Wno-type-defaults #-}
{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternSynonyms, ViewPatterns
, NoOverloadedStrings #-}
......@@ -23,8 +22,6 @@ import Data.Tree (Forest)
import qualified Data.Set as S
import qualified GUBS.Polynomial as P
import Data.Ratio
import ListT (ListT)
import qualified ListT as L
import qualified Text.PrettyPrint.ANSI.Leijen as PP
......@@ -34,6 +31,7 @@ import Control.Monad.Trace
import PWhile.InvariantSolver
import PWhile.InvariantSolver.Naive
import Data.PWhile.BoolExpression
import qualified Data.PWhile.BoolExpression as B
import qualified Data.PWhile.Expression as E
import qualified Data.PWhile.CostExpression as C
import Data.PWhile.Program
......@@ -59,11 +57,11 @@ memoized f k c e = do
return v
Just v -> return v
newtype SolveM a = SolveM { runSolveM_ :: ExceptT String (TraceT String (ListT (MemoT IO))) a }
newtype SolveM a = SolveM { runSolveM_ :: ExceptT String (TraceT String (L.ListT (MemoT IO))) a }
deriving (Applicative, Functor, Monad, MonadError String, MonadTrace String, MonadIO)
-- prvoides a 'Stream' of possible failing computations with logging
runSolveM' :: SolveM a -> ListT (MemoT IO) (Either String a, Forest String)
runSolveM' :: SolveM a -> L.ListT (MemoT IO) (Either String a, Forest String)
runSolveM' = runTraceT . runExceptT . runSolveM_
runSolveM :: SolveM a -> IO [(Either String a, Forest String)]
......@@ -84,13 +82,13 @@ instance Alternative SolveM where
liftMemoT :: MemoT IO a -> SolveM a
liftMemoT = SolveM . lift . lift . lift
liftListT :: ListT (MemoT IO) a -> SolveM a
liftListT :: L.ListT (MemoT IO) a -> SolveM a
liftListT = SolveM . lift . lift
alternative :: Foldable f => f a -> SolveM a
alternative = liftListT . L.fromFoldable
first :: Monad m => (a -> Bool) -> ListT m a -> m [a]
first :: Monad m => (a -> Bool) -> L.ListT m a -> m [a]
first p = go where
go m = do
aM <- L.uncons m
......@@ -153,23 +151,25 @@ run t = fmap (map toResult) . runMemoT . select t . runSolveM' where
runAny :: SolveM a -> IO (Maybe (Result a))
runAny m = listToMaybe <$> run Any m
-- estimating expectations
-- cost functions
----------------------------------------------------------------------
ramp :: (Eq c, Num c) => E.Exp -> C.CExp c
ramp e = C.guarded (e .>= 0) (C.fromExp e)
isConstGExp (C.GExp g _ e) = null (E.variables e) && S.null (B.variables g)
rankFromCExp :: C.CExp c -> [C.GExp c]
rankFromCExp = filter (not . isConst) . C.gExps
where isConst (C.GExp _ e) = null (E.variables e)
varGExps :: (Eq c, Num c) => C.CExp c -> [C.GExp c]
varGExps = filter (not . isConstGExp) . C.gExps
divBy :: CExp -> E.Expression Rational -> CExp
divBy c (E.Constant r) = C.scale (E.constant (denominator r % numerator r)) c
divBy c e = C.divBy c e
-- estimating expectations
----------------------------------------------------------------------
discreteExpectation :: [(E.Exp, e)] -> (e -> SolveM CExp) -> SolveM CExp
discreteExpectation [(_,e)] f = f e
discreteExpectation ls f =
divBy <$> (C.sum <$> sequence [C.scale w <$> f e | (w,e) <- ls'])
<*> pure (sum [e | (e,_) <- ls'])
C.divBy <$> (C.sum <$> sequence [C.scale w <$> f e | (w,e) <- ls'])
<*> pure (sum [e | (e,_) <- ls'])
where ls' = [ (fmap fromIntegral w, e) | (w,e) <- ls ]
boundedSum :: (E.Exp -> CExp) -> (E.Exp, E.Exp) -> SolveM CExp
......@@ -203,7 +203,7 @@ boundedSum f (l,o) = logBlkIdM msg $ bs fi where
, step = (E.substitute i (vi + 1) . C.fromGExp) `map` ns
, cont = C.zero
, limt = ns }
ns = rankFromCExp g
ns = varGExps g
expectation :: E.Dist E.Exp -> (E.Exp -> CExp) -> SolveM CExp
......@@ -221,7 +221,7 @@ expectation (E.Rand n) f =
-- TODO!
-- | Just g <- linFn fi vi (C.scale (1 / 2) (C.E n)) -> return g
E.Constant n' -> discreteExpectation [(1,E.constant i) | i <- [0..n'-1]] (return . f)
_ | otherwise -> divBy <$> boundedSum f (0,n-1) <*> pure (fmap fromIntegral n)
_ | otherwise -> C.divBy <$> boundedSum f (0,n-1) <*> pure (fmap fromIntegral n)
where
noccur v e = v `notElem` E.variables e
......@@ -267,65 +267,47 @@ extractRanking body i c g f = do
<|> (logMsg "multiplicative" >> pure multiplicative)
rankFromBExp <-
(logMsg "optimistic" >> pure (ranksFromBExpWith optimistic))
-- MS: not a solution, but shift is not working as intended
-- before we could compare norms; now we have reduced expression
-- <|> (logMsg "optimistic2" >> pure (ranksFromBExpWith (optimistic' 2)))
-- <|> (logMsg "optimistic4" >> pure (ranksFromBExpWith (optimistic' 4)))
-- <|> (logMsg "optimistic8" >> pure (ranksFromBExpWith (optimistic' 8)))
<|> (logMsg "shift" >> pure (ranksFromBExpWith shift))
<|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
gRanks <- combine <$> rankFromBExp (i .&& c) <*> pure (rankFromCExp g)
fRanks <- pure (rankFromCExp f)