InferEt.hs 14.1 KB
Newer Older
mschaper's avatar
mschaper committed
1
{-# OPTIONS_GHC -Wno-unused-local-binds -Wno-orphans -Wno-unused-top-binds -Wno-type-defaults #-}
AVANZINI Martin's avatar
AVANZINI Martin committed
2
3
{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternSynonyms, ViewPatterns
           , NoOverloadedStrings #-}
mschaper's avatar
mschaper committed
4
5
module PWhile.InferEt
  (
AVANZINI Martin's avatar
AVANZINI Martin committed
6
    Result (..)
mschaper's avatar
mschaper committed
7
  , FilterResult (..)
8
  , Log
AVANZINI Martin's avatar
AVANZINI Martin committed
9
  , SolveM
mschaper's avatar
mschaper committed
10
  , run, runAny
AVANZINI Martin's avatar
AVANZINI Martin committed
11
  , ect, evt
AVANZINI Martin's avatar
AVANZINI Martin committed
12
  , showResult
mschaper's avatar
mschaper committed
13
  ) where
AVANZINI Martin's avatar
AVANZINI Martin committed
14

mschaper's avatar
mschaper committed
15

mschaper's avatar
mschaper committed
16
import           Control.Applicative
mschaper's avatar
mschaper committed
17
import           Control.Monad.Except
mschaper's avatar
mschaper committed
18
import qualified Control.Monad.State          as St
AVANZINI Martin's avatar
AVANZINI Martin committed
19
import           Data.Maybe                   (listToMaybe)
mschaper's avatar
mschaper committed
20
import qualified Data.Map.Strict              as M
mschaper's avatar
mschaper committed
21
import           Data.Tree                    (Forest)
AVANZINI Martin's avatar
AVANZINI Martin committed
22
import qualified Data.Set                     as S
23
import qualified GUBS.Polynomial as P
mschaper's avatar
mschaper committed
24

mschaper's avatar
mschaper committed
25
import qualified ListT                        as L
mschaper's avatar
mschaper committed
26
import qualified Text.PrettyPrint.ANSI.Leijen as PP
AVANZINI Martin's avatar
AVANZINI Martin committed
27

mschaper's avatar
mschaper committed
28
import           Control.Monad.Trace
AVANZINI Martin's avatar
AVANZINI Martin committed
29
-- import           Debug.Trace                  as D
AVANZINI Martin's avatar
AVANZINI Martin committed
30

AVANZINI Martin's avatar
AVANZINI Martin committed
31
32
33
import           PWhile.InvariantSolver
import           PWhile.InvariantSolver.Naive
import           Data.PWhile.BoolExpression
AVANZINI Martin's avatar
AVANZINI Martin committed
34
import qualified Data.PWhile.BoolExpression   as B
AVANZINI Martin's avatar
AVANZINI Martin committed
35
36
import qualified Data.PWhile.Expression       as E
import qualified Data.PWhile.CostExpression   as C
mschaper's avatar
mschaper committed
37
38
import           Data.PWhile.Program
import           PWhile.Util
mschaper's avatar
mschaper committed
39

mschaper's avatar
mschaper committed
40

mschaper's avatar
mschaper committed
41
--- * Solver Monad ---------------------------------------------------------------------------------------------------
mschaper's avatar
mschaper committed
42

43
type CExp = C.CExp Rational
AVANZINI Martin's avatar
AVANZINI Martin committed
44

45
type MemoT = St.StateT (M.Map (Knd,C,CExp) CExp)
mschaper's avatar
mschaper committed
46
47
48
49

runMemoT :: Monad m => MemoT m v -> m v
runMemoT = flip St.evalStateT M.empty

50
memoized :: (Knd -> C -> CExp -> SolveM CExp) -> Knd -> C -> CExp -> SolveM CExp
mschaper's avatar
mschaper committed
51
52
53
54
55
56
57
memoized f k c e = do
  memo <- liftMemoT St.get
  case M.lookup (k,c,e) memo of
    Nothing -> do
      v <- f k c e
      liftMemoT $ St.modify (M.insert (k,c,e) v)
      return v
AVANZINI Martin's avatar
AVANZINI Martin committed
58
    Just v  -> return v
mschaper's avatar
mschaper committed
59

AVANZINI Martin's avatar
AVANZINI Martin committed
60
newtype SolveM a = SolveM { runSolveM_ :: ExceptT String (TraceT String (L.ListT (MemoT IO))) a }
mschaper's avatar
mschaper committed
61
  deriving (Applicative, Functor, Monad, MonadError String, MonadTrace String, MonadIO)
mschaper's avatar
mschaper committed
62

mschaper's avatar
mschaper committed
63
-- prvoides a 'Stream' of possible failing computations with logging
AVANZINI Martin's avatar
AVANZINI Martin committed
64
runSolveM' :: SolveM a -> L.ListT (MemoT IO) (Either String a, Forest String)
mschaper's avatar
mschaper committed
65
66
67
runSolveM' = runTraceT . runExceptT . runSolveM_

runSolveM :: SolveM a -> IO [(Either String a, Forest String)]
mschaper's avatar
mschaper committed
68
69
runSolveM = runMemoT . L.toList . runTraceT . runExceptT . runSolveM_

mschaper's avatar
mschaper committed
70

mschaper's avatar
mschaper committed
71
72
73

-- * Alternative

mschaper's avatar
mschaper committed
74
75
76
77
78
79
80
instance Alternative SolveM where
  empty     = SolveM $ ExceptT $ TraceT empty
  ma <|> mb = do
    let
      a = runExceptT (runSolveM_ ma)
      b = runExceptT (runSolveM_ mb)
    SolveM $ ExceptT $ a <|> b
mschaper's avatar
mschaper committed
81

mschaper's avatar
mschaper committed
82
83
84
liftMemoT :: MemoT IO a -> SolveM a
liftMemoT = SolveM . lift . lift . lift

AVANZINI Martin's avatar
AVANZINI Martin committed
85
liftListT :: L.ListT (MemoT IO) a -> SolveM a
mschaper's avatar
mschaper committed
86
liftListT = SolveM . lift . lift
mschaper's avatar
mschaper committed
87

88
89
alternative :: Foldable f => f a -> SolveM a
alternative = liftListT . L.fromFoldable
mschaper's avatar
mschaper committed
90

AVANZINI Martin's avatar
AVANZINI Martin committed
91
first :: Monad m => (a -> Bool) -> L.ListT m a -> m [a]
mschaper's avatar
mschaper committed
92
first p = go where
mschaper's avatar
mschaper committed
93
  go m = do
mschaper's avatar
mschaper committed
94
    aM <- L.uncons m
mschaper's avatar
mschaper committed
95
    case aM of
mschaper's avatar
mschaper committed
96
97
      Nothing    -> return []
      Just (a,l) -> if p a then return [a] else go l
mschaper's avatar
mschaper committed
98

mschaper's avatar
mschaper committed
99
100

-- ** Logging
mschaper's avatar
mschaper committed
101

AVANZINI Martin's avatar
AVANZINI Martin committed
102
103
logMsgIdM :: PP.Pretty a => SolveM a -> SolveM a
logMsgIdM ma =  ma >>= \a -> logMsg (renderPretty $ PP.pretty a) >> return a
mschaper's avatar
mschaper committed
104

AVANZINI Martin's avatar
AVANZINI Martin committed
105
logBlkIdM :: PP.Pretty a => String -> SolveM a -> SolveM a
mschaper's avatar
mschaper committed
106
107
logBlkIdM s = logBlk s . logMsgIdM

AVANZINI Martin's avatar
AVANZINI Martin committed
108
109
110
debugM :: (Applicative f, PP.Pretty e) => String -> e -> f e
debugM = debugMsgA "InferEt"

111
112
113
debug :: (PP.Pretty e) => String -> e -> e
debug = debugMsg "InferEt"

mschaper's avatar
mschaper committed
114

mschaper's avatar
mschaper committed
115
-- ** Result
AVANZINI Martin's avatar
AVANZINI Martin committed
116
type Log = Forest String
mschaper's avatar
mschaper committed
117

AVANZINI Martin's avatar
AVANZINI Martin committed
118
119
data Result a = Failure String Log
              | Success a Log
mschaper's avatar
mschaper committed
120

AVANZINI Martin's avatar
AVANZINI Martin committed
121
122
123
instance PP.Pretty a => PP.Pretty (Result a) where
  pretty (Failure m l) = renderLog l PP.<$$> PP.red (PP.text "[Failure]" PP.<+> PP.text m)
  pretty (Success f l) = renderLog l PP.<$$> PP.green (PP.text "[Success]" PP.<+> PP.pretty f)
mschaper's avatar
mschaper committed
124

AVANZINI Martin's avatar
AVANZINI Martin committed
125
126
127
128

showResult :: PP.Pretty a => Result a -> String
showResult = show . PP.pretty

AVANZINI Martin's avatar
AVANZINI Martin committed
129
130
131
-- instance PP.Pretty [Result] where
--   pretty rs = PP.vcat
--     [ PP.pretty "***" PP.<//> PP.pretty r PP.<//> PP.pretty "<<<" PP.<//> PP.text "" | r <- rs]
mschaper's avatar
mschaper committed
132

mschaper's avatar
mschaper committed
133
134
135
136
137
data FilterResult
  = Any       -- return first successful result
  | Take Int  -- take first n results
  | Pick Int  -- pick ith result
  | All       -- take all results
mschaper's avatar
mschaper committed
138
139
  deriving (Show, Eq)

AVANZINI Martin's avatar
AVANZINI Martin committed
140
141
142
143
144
145
146
147
148
149
run :: FilterResult -> SolveM a -> IO [Result a]
run t = fmap (map toResult) . runMemoT . select t . runSolveM' where
  select Any = first success where
    success (fst -> Right{}) = True
    success _                = False
  select (Take i) = L.toList . L.take i
  select (Pick i) = L.toList . L.drop (pred i) . L.take i
  select All      = L.toList
  toResult (Left err, l) = Failure err l
  toResult (Right a, l) = Success a l
150

AVANZINI Martin's avatar
AVANZINI Martin committed
151
152
runAny :: SolveM a -> IO (Maybe (Result a))
runAny m = listToMaybe <$> run Any m
153

AVANZINI Martin's avatar
AVANZINI Martin committed
154
-- cost functions
155
156
----------------------------------------------------------------------

AVANZINI Martin's avatar
AVANZINI Martin committed
157
158
varGNorms :: (Eq c, Num c) => C.CExp c -> [C.GNorm c]
varGNorms = filter (not . C.isConstGN) . C.gNorms
159

AVANZINI Martin's avatar
AVANZINI Martin committed
160
161
-- estimating expectations
----------------------------------------------------------------------
162
163

discreteExpectation :: [(E.Exp, e)] -> (e -> SolveM CExp) -> SolveM CExp
AVANZINI Martin's avatar
AVANZINI Martin committed
164
discreteExpectation [(_,e)] f = f e
165
discreteExpectation ls f =
AVANZINI Martin's avatar
AVANZINI Martin committed
166
167
  C.divBy <$> (C.sum <$> sequence [C.scale w <$> f e | (w,e) <- ls'])
          <*> pure (sum [e | (e,_) <- ls'])
168
169
170
171
172
  where ls' = [ (fmap fromIntegral w, e) | (w,e) <- ls ]

boundedSum :: (E.Exp -> CExp) -> (E.Exp, E.Exp) -> SolveM CExp
boundedSum f (l,o) = logBlkIdM msg $ bs fi where
    i = E.Var "@i"
173
    vi = E.variable i
174
175
176
    fi = f vi
    msg = "[sum] " ++ renderPretty (PP.text "sum" PP.<> PP.tupled [ PP.pretty l, PP.pretty o, PP.pretty fi])

AVANZINI Martin's avatar
AVANZINI Martin committed
177
178
179
180
181
182
    bs g
      | g == C.zero     = return C.zero
    bs (C.Plus g1 g2)   = C.plus <$> bs g1 <*> bs g2
    bs (C.Cond g g1 g2)
      | g2 /= C.zero    = C.plus <$> bs (C.guarded g g1) <*> bs (C.guarded (neg g) g2)
    bs g                = do
183
      logMsg2 "norms" ns
184
185
      (ui,s,dir) <- alternative [(uiDown, o, "Down"), (uiUp, l, "Up")]
      logMsg2 ("SumFn["++dir++"]") ui
186
187
188
189
      f' <- debugM "result" =<< solveInvariant ui
      logMsg2 "Solution" f'
      return (E.substitute i s f')
        where
190
191
192
193
          uiDown = UpperInvariant {
            inv  = o .>= vi
            , cnd = vi .>= l
            , cost = g
AVANZINI Martin's avatar
AVANZINI Martin committed
194
            , step = (E.substitute i (vi - 1) . C.fromNorm)  `map` ns
195
196
197
198
199
200
            , cont = C.zero
            , limt = ns }
          uiUp = UpperInvariant {
            inv  = vi .>= l
            , cnd = o .>= vi
            , cost = g
AVANZINI Martin's avatar
AVANZINI Martin committed
201
            , step = (E.substitute i (vi + 1) . C.fromNorm)  `map` ns
202
203
            , cont = C.zero
            , limt = ns }
AVANZINI Martin's avatar
AVANZINI Martin committed
204
205
206
207
          ns = [ C.norm (e .>= 0) e  `C.mulN` n
               | C.GNorm b _ n <- varGNorms g
               , e1 :>=: e2 <- S.toList (literals b)
               , let e = e1 - e2 + 1]
208
209
210


expectation :: E.Dist E.Exp -> (E.Exp -> CExp) -> SolveM CExp
211
expectation (E.Discrete ls) f = discreteExpectation ls (return . f)
212
213
-- expectation (E.Rand (E.Constant n)) f =
--   discreteExpectation [(1,E.constant i) | i <- [0..n-1]] (return . f)
214
215
expectation (E.Rand n) f =
  logBlkIdM ("[expectation] " ++ "rand(" ++ show (PP.pretty n) ++ ")") $ do
216
  let (vi,vj) = (E.Var "@i", E.Var "@j")
217
      (fi,fj) = (f (E.variable vi), f (E.variable vj))
218
  logMsg2 "f" fi
219
  C.guarded (n .> 0) <$>
220
    case n of
221
      _ | fi == fj  -> return fi
222
223
      -- TODO!
        -- | Just g <- linFn fi vi (C.scale (1 / 2) (C.E n)) -> return g
224
      E.Constant n' -> discreteExpectation [(1,E.constant i) | i <- [0..n'-1]] (return . f)
AVANZINI Martin's avatar
AVANZINI Martin committed
225
      _  -> C.divBy <$> boundedSum f (0,n-1) <*> pure (fmap fromIntegral n)
226
  where
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
    noccur v e = v `notElem` E.variables e

  -- TODO: add linFn
    -- linFn :: CExp -> E.Var -> CExp -> Maybe (CExp)
    -- linFn (C.guardedExpressions -> [(Top,p C.:% q)]) v avg
    --   | not (v `S.member` C.variables (C.toCost q)) =
    --       (*) <$> (sum <$> sequence [linMono m v avg | m <- P.toMonos p ])
    --           <*> pure (C.toCost (1 C.:% q))
    -- linFn _ _ _ = Nothing

    -- linMono (coeff,P.toPowers -> powers) v avg = C.scale coeff <$> lin powers where
    --   lin [] = return 1
    --   lin (p:ps)
    --     | v `noccur` fst p = (*) (C.fromPowers [p]) <$> lin ps
    --   lin ((C.Norm e,1):ps) = (*) <$> linExp e v avg <*> con ps
    --   lin _ = Nothing

    --   con [] = return 1
    --   con (p:ps)
    --     | v `noccur` fst p = (*) (C.fromPowers [p]) <$> con ps
    --   con _ = Nothing

    -- linExp :: E.Exp -> E.Var -> CExp -> Maybe (CExp)
    -- linExp e v avg
    --   | c >= 0 && d >= 0
    --     && E.constant c * E.variable v + E.constant d == e =
    --       Just (C.scale (toRational c) avg + C.constant (toRational d))
    --   | otherwise = Nothing
    --   where
    --     c = P.coefficientOf (P.fromPowers [(v,1)]) e
    --     d = P.coefficientOf (P.fromPowers []) e
258
259
260



261
262
263
-- Expectation Transformer
----------------------------------------------------------------------

AVANZINI Martin's avatar
AVANZINI Martin committed
264
265
266
267
268
269
270
type NormTemplate = P.Polynomial C.Norm Int

normTemplateEq :: NormTemplate -> NormTemplate -> Bool
p1 `normTemplateEq` p2 = and $ P.coefficients $
  P.zipCoefficientsWith (const False) (const False) (\ _ _ -> True) p1 p2

norm :: C.Norm -> NormTemplate
271
272
norm (C.Norm _ (E.Constant _)) = P.coefficient 1
norm n                         = P.variable n
AVANZINI Martin's avatar
AVANZINI Martin committed
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291

normFromExp :: E.Exp -> NormTemplate
normFromExp e = norm (C.Norm (e .>= 0) e)

normFromBExp :: BExp -> NormTemplate
normFromBExp b = sum [ normFromExp (e1 - e2 + 1)
                     | e1 :>=: e2 <- S.toList (literals b) ]

normFromCExp :: C.CExp Rational -> NormTemplate
normFromCExp d = sum [ normFromBExp b + norm n
                     | C.GNorm b k n <- varGNorms d
                     , k > 0, not (C.isZeroN n) ]

substituteM :: (C.Norm -> SolveM NormTemplate) -> NormTemplate -> SolveM NormTemplate
substituteM s = P.fromPolynomialM s (pure . P.coefficient)


template :: String -> SolveM NormTemplate -> SolveM NormTemplate
template name = logBlkIdM (name++"-template")
AVANZINI Martin's avatar
AVANZINI Martin committed
292

AVANZINI Martin's avatar
AVANZINI Martin committed
293

AVANZINI Martin's avatar
AVANZINI Martin committed
294
extractRanking :: C -> BExp -> BExp -> CExp -> CExp -> SolveM [C.Norm]
AVANZINI Martin's avatar
AVANZINI Martin committed
295
296
297
298
299
300
301
302
303
304
305
extractRanking body i c g f = fmap toNormList $ do
  lin <- linearTemplate
  template "linear" (pure lin)
    <|> template "shift-avg" (refine shiftAvg lin)
    <|> template "shift-avg" (refine shiftAvg lin)
    <|> template "conditions" (refine conds lin)
    <|> template "shift-max" (refine shiftMax lin)
    <|> do
            let sq = lin * lin
            template "square" (pure sq)
   where
AVANZINI Martin's avatar
AVANZINI Martin committed
306
307
    toNormList p = filter (not . zeroN) [ C.prodN [ C.expN n k | (n,k) <- P.toPowers m ]
                                        | (_,m) <- P.toMonos p]
AVANZINI Martin's avatar
AVANZINI Martin committed
308
        where zeroN (C.Norm _ e) = e == 0
AVANZINI Martin's avatar
AVANZINI Martin committed
309

AVANZINI Martin's avatar
AVANZINI Martin committed
310
311
312
    refine m r = do
      r' <- m r
      if r' `normTemplateEq` r then empty else pure r'
AVANZINI Martin's avatar
AVANZINI Martin committed
313

AVANZINI Martin's avatar
AVANZINI Martin committed
314
    linearTemplate = do
AVANZINI Martin's avatar
AVANZINI Martin committed
315
316
317
318
319
320
321
322
      let gNorm = normFromCExp (C.guarded c g)
          fNorm = normFromCExp (C.guarded (neg c) f)
      df <- substituteM delta fNorm
      pure (normFromExp 1 + normFromBExp i + normFromBExp c
             + fNorm + gNorm + sum [ normFromBExp c * df ])

    shiftAvg = substituteM s where
      s n@(C.Norm _ e) = do
AVANZINI Martin's avatar
AVANZINI Martin committed
323
        evn <- etM Evt body (C.nm 1 n)
AVANZINI Martin's avatar
AVANZINI Martin committed
324
        pure $ normFromExp $ E.maxE $ e : [2 * e - fmap floor e' | e' <- lfs evn ]
AVANZINI Martin's avatar
AVANZINI Martin committed
325
326
327

    shiftMax = substituteM s where
      s n@(C.Norm _ e) = do
AVANZINI Martin's avatar
AVANZINI Martin committed
328
        evn <- etM Evt body (C.nm 1 n)
AVANZINI Martin's avatar
AVANZINI Martin committed
329
        pure $ normFromExp $ E.maxE $ e : [2 * e - e' | C.GNorm _ _ (C.Norm _ e') <- varGNorms evn ]
AVANZINI Martin's avatar
AVANZINI Martin committed
330
331
332
333
334
335
336
337

    conds = substituteM s where
      s n = do
        evn <- etM Evt body (C.nm 1 n)
        pure $ norm n + sum [ normFromBExp b | C.GNorm b _ _ <-  varGNorms evn ]

    delta n@(C.Norm _ e) = do
      ns <- S.toList . C.norms <$> etM Evt body (C.nm 1 n)
AVANZINI Martin's avatar
AVANZINI Martin committed
338
      let d = E.maxE [ ne | C.Norm _ ne <- ns ] - e
AVANZINI Martin's avatar
AVANZINI Martin committed
339
340
341
342
343
344
345
346
      return (normFromExp d)

    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]

347
348
349
isConstantWrt :: CExp -> C -> Bool
f `isConstantWrt` c = C.variables f `S.disjoint` vs where
  vs = S.fromList [ v | Ass v _ <- subPrograms c]
mschaper's avatar
mschaper committed
350
351


352
isTickFree :: C -> Bool
AVANZINI Martin's avatar
AVANZINI Martin committed
353
isTickFree = not . any isTick . subPrograms where
354
355
  isTick Tic{} = True
  isTick _     = False
AVANZINI Martin's avatar
AVANZINI Martin committed
356
357

isSimple :: C -> Bool
AVANZINI Martin's avatar
AVANZINI Martin committed
358
isSimple = not . any isWhile . subPrograms where
AVANZINI Martin's avatar
AVANZINI Martin committed
359
360
361
  isWhile While{} = True
  isWhile _       = False

mschaper's avatar
mschaper committed
362

363
solveInvariant :: UpperInvariant -> SolveM CExp
AVANZINI Martin's avatar
AVANZINI Martin committed
364
365
366
solveInvariant ui =
    maybe (throwError "no solution") return $
    solve (NaiveSolver 1 2) =<< debugM "invariant" ui
mschaper's avatar
mschaper committed
367

mschaper's avatar
mschaper committed
368

369

AVANZINI Martin's avatar
AVANZINI Martin committed
370
data Knd = Evt | Ect deriving (Eq, Ord, Show)
AVANZINI Martin's avatar
AVANZINI Martin committed
371

372
ect, evt :: C -> CExp -> SolveM CExp
mschaper's avatar
mschaper committed
373
ect c f =
AVANZINI Martin's avatar
AVANZINI Martin committed
374
  logBlkIdM ("[ect] " ++ show (PP.pretty f)) $
375
  logMsg2 "Problem" c *> etM Ect c f
AVANZINI Martin's avatar
AVANZINI Martin committed
376

mschaper's avatar
mschaper committed
377
evt c f =
AVANZINI Martin's avatar
AVANZINI Martin committed
378
  logBlkIdM ("[evt] " ++ show (PP.pretty f)) $
379
  logMsg2 "Problem" c *> etM Evt c f
mschaper's avatar
mschaper committed
380

381
etM :: Knd -> C -> CExp -> SolveM CExp
AVANZINI Martin's avatar
AVANZINI Martin committed
382
etM = memoized et
mschaper's avatar
mschaper committed
383

mschaper's avatar
mschaper committed
384

385
386
387
388
et :: Knd -> C -> CExp -> SolveM CExp
et Ect c f
  | f == C.zero
    && isTickFree c        = return C.zero
AVANZINI Martin's avatar
AVANZINI Martin committed
389
et Evt c f
390
391
392
393
394
395
396
  | not (isSimple c)
    && f `isConstantWrt` c = return f
et Evt c (C.Plus f1 f2)
  | not (isSimple c)       = C.plus <$> evt c f1 <*> evt c f2
et _   Abort _             = return C.zero
et _   Skip  f             = return f
et Evt (Tic _) f           = return f
AVANZINI Martin's avatar
AVANZINI Martin committed
397
et Ect (Tic e) f           = return $ C.ramp e `C.plus` f
398
399
400
401
et _   (Ass v d) f         = expectation d (\ e -> E.substitute v e f)
et t (NonDet e1 e2) f      = C.sup <$> etM t e1 f <*> etM t e2 f
et t (Choice ls) f         = discreteExpectation ls (\ c -> etM t c f)
et t (Cond _ i b c1 c2) f  =  C.guarded i <$> (C.cond b <$> etM t c1 f <*> etM t c2 f)
AVANZINI Martin's avatar
AVANZINI Martin committed
402
et Ect (Seq c1 c2) f
403
  | isSimple c1            = et Ect c1 =<< et Ect c2 f
404
  | otherwise              = C.plus <$> ect c1 C.zero <*> (evt c1 =<< ect c2 f)
405
et t (Seq c1 c2) f         = etM t c1 =<< etM t c2 f
406
et t (While _  i b c) f =
AVANZINI Martin's avatar
AVANZINI Martin committed
407
  logBlkIdM "[While.Step]" $ do
408
409
  g <- case t of {Evt -> return C.zero; Ect -> ect c C.zero}
  ns <- extractRanking c i b g f
AVANZINI Martin's avatar
AVANZINI Martin committed
410
  logMsg2 "Norms" ns
AVANZINI Martin's avatar
AVANZINI Martin committed
411
  hs <- traverse (evt c . C.fromNorm) ns
AVANZINI Martin's avatar
AVANZINI Martin committed
412
  let ui = UpperInvariant { inv  = i
413
                          , cnd = b
AVANZINI Martin's avatar
AVANZINI Martin committed
414
415
416
417
418
                          , cost = g
                          , step = hs
                          , cont = f
                          , limt = ns}
  logMsg2 "Invariant" ui
419
  h <- solveInvariant ui
420
  return (C.cond b h f)
mschaper's avatar
mschaper committed
421

mschaper's avatar
mschaper committed
422

mschaper's avatar
mschaper committed
423
-- * Pretty
mschaper's avatar
mschaper committed
424

AVANZINI Martin's avatar
AVANZINI Martin committed
425
instance PP.Pretty Knd where
mschaper's avatar
mschaper committed
426
  pretty = PP.text . show