Commit 058665be authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

minor cleanup

parent 2b4350e2
......@@ -7,7 +7,7 @@ def trader():
price = price + 1
else:
price = price - 1
nShares = unif(0,1)
nShares = unif(3,6)
while nShares > 0:
nShares = nShares - 1
tick price
......@@ -13,6 +13,7 @@ module Data.PWhile.Expression
, variables
, factor
, cfactor
, maxE
, P.norm
, Substitutable (..)
-- distributions
......@@ -63,6 +64,9 @@ cfactor e = case monos of
monos = P.toMonos e
f = foldl1' gcd [ c | (c,_) <- monos]
maxE :: (Eq c, Ord c, Num c) => [Expression c] -> Expression c
maxE [] = 0
maxE es = P.norm (foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es)
-- patterns
const_ :: (Ord v, Eq c, Num c) => P.Polynomial v c -> Maybe c
......
......@@ -317,27 +317,15 @@ extractRanking body i c g f = fmap toNormList $ do
pure (normFromExp 1 + normFromBExp i + normFromBExp c
+ fNorm + gNorm + sum [ normFromBExp c * df ])
-- refine = template "standard" (const stdTemplate)
-- <|>> (\ l -> template "shift-avg" shiftAvg
-- <|>> template "shift-max" shiftMax
-- <|>> template "cond" conds
-- <|>> template "square" square)
-- infixr 3 <|>>
-- m1 <|>> m2 = \ r0 -> do { r1 <- m1 r0; check r0 r1 <|> m2 r1 } where
-- check r r' = if r `normPolyEq` r' then empty else pure r'
shiftAvg = substituteM s where
s n@(C.Norm _ e) = do
evn <- etM Evt body (C.nm 1 n)
pure $ normFromExp $ maxE $ e : [2 * e - fmap floor e' | e' <- lfs evn ]
pure $ normFromExp $ E.maxE $ e : [2 * e - fmap floor e' | e' <- lfs evn ]
shiftMax = substituteM s where
s n@(C.Norm _ e) = do
evn <- etM Evt body (C.nm 1 n)
pure $ normFromExp $ maxE $ e : [2 * e - e' | C.GNorm _ _ (C.Norm _ e') <- varGNorms evn ]
pure $ normFromExp $ E.maxE $ e : [2 * e - e' | C.GNorm _ _ (C.Norm _ e') <- varGNorms evn ]
conds = substituteM s where
s n = do
......@@ -346,71 +334,15 @@ extractRanking body i c g f = fmap toNormList $ do
delta n@(C.Norm _ e) = do
ns <- S.toList . C.norms <$> etM Evt body (C.nm 1 n)
let d = maxE [ ne | C.Norm _ ne <- ns ] - e
let d = E.maxE [ ne | C.Norm _ ne <- ns ] - e
return (normFromExp d)
square n = pure (n * n)
lfs (C.Sup c1 c2) = lfs c1 ++ lfs c2
lfs (C.Cond _ c1 c2) = lfs c1 ++ lfs c2
lfs (C.Div d _) = lfs d
lfs (C.Plus c1 c2) = [e1 + e2 | e1 <- lfs c1, e2 <- lfs c2]
lfs (C.N k (C.Norm _ e)) = [E.constant k * fmap fromIntegral e]
maxE [] = 0
maxE es = E.norm (foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es)
-- trivial (b, C.Norm _ e) = b == Bot || S.null (E.variables e)
-- combine <-
-- (logMsg "additive" >> pure additive)
-- <|> (logMsg "multiplicative" >> pure multiplicative)
-- rankFromBExp <-
-- (logMsg "optimistic" >> pure (ranksFromBExpWith optimistic))
-- <|> (logMsg "shift" >> pure (ranksFromBExpWith shift))
-- <|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
-- gRanks <- combine rankFromBExp (c .&& i) (varGNorms g)
-- fRanks <- pure (sum (fromGNorm `map` C.gNorms f))
-- fRanks' <- (*) <$> rankFromBExp c
-- <*> P.fromPolynomialM (fmap P.variable . delta) (pure . P.coefficient) fRanks
-- return (toNormList (norm 1 + fRanks + gRanks + fRanks')) --
-- where
-- fromGNorm (C.GNorm _ _ n) = P.variable n
-- maxE [] = 0
-- maxE es = foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es
-- additive fromBExp b gexps =
-- (+) (sum (fromGNorm `map` gexps))
-- <$> fromBExp (b .&& bigAnd [ b' | C.GNorm b' _ _ <- gexps ])
-- multiplicative fromBExp b gexps =
-- (+) <$> additive fromBExp b gexps
-- <*> (sum <$> sequence [ (*) (P.variable n) <$> fromBExp (b .&& b')
-- | C.GNorm b' _ n <- gexps])
-- squared m x = sq <$> m x where sq n = n * n
-- delta n@(C.Norm _ e) = do
-- ns <- S.toList <$> C.norms <$> evt body (C.nm 1 n)
-- let f = maxE [ ne | C.Norm _ ne <- ns ] - e
-- return (C.norm (f .>= 0) f)
-- shift l@(a :>=: b) =
-- -- TODO: this is a mess; maybe define wp for non-recursive language?
-- mkNorm <$> maxE <$> concatMap diffs <$> C.gNorms <$> evt body (C.predicate (a .>= b))
-- where
-- diffs (C.GNorm gd _ n)
-- | not (C.isZeroN n) = [ (a' - b') - (a - b) | a' :>=: b' <- S.toList (literals gd) ]
-- | otherwise = []
-- -- TODO
-- mkNorm (E.AddConst _ df) = norm (a - b + 1 + E.constant df)
isConstantWrt :: CExp -> C -> Bool
f `isConstantWrt` c = C.variables f `S.disjoint` vs where
vs = S.fromList [ v | Ass v _ <- subPrograms c]
......@@ -436,8 +368,6 @@ solveInvariant ui =
data Knd = Evt | Ect deriving (Eq, Ord, Show)
ect, evt :: C -> CExp -> SolveM CExp
ect c f =
logBlkIdM ("[ect] " ++ show (PP.pretty f)) $
......@@ -477,7 +407,6 @@ et t (While _ i b c) f =
g <- case t of {Evt -> return C.zero; Ect -> ect c C.zero}
ns <- extractRanking c i b g f
logMsg2 "Norms" ns
-- TODO: filter those ni's for which hi cannot be computed?
hs <- traverse (evt c . C.fromNorm) ns
let ui = UpperInvariant { inv = i
, cnd = b
......
Supports Markdown
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