Commit 8f284291 authored by Sven Keidel's avatar Sven Keidel

fix fixpoint spec

parent 213fe823
Pipeline #26914 passed with stages
in 44 minutes
......@@ -80,8 +80,8 @@ withBounds2 f (Interval i1 i2) (Interval j1 j2) =
instance (Ord n, Bounded n) => UpperBounded (Interval n) where
top = Interval minBound maxBound
widening :: Ord n => Interval n -> Widening (Interval (InfiniteNumber n))
widening (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
bounded :: Ord n => Interval n -> Widening (Interval (InfiniteNumber n))
bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
(if j1 P./= i1 || j2 P./= i2 then Unstable else Stable,
Interval (if | lower P.< Number lowerBound -> NegInfinity
| Number upperBound P.< lower -> Number upperBound
......@@ -93,6 +93,11 @@ widening (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
lower = min i1 j1
upper = max i2 j2
widening :: Ord n => Widening (Interval (InfiniteNumber n))
widening (Interval i1 i2) (Interval j1 j2) =
(if j1 P./= i1 || j2 P./= i2 then Unstable else Stable,
Interval (if i1 P./= j1 then NegInfinity else i1) (if i2 P./= j2 then Infinity else i2))
metric :: Metric m n -> Metric (Interval m) (Product n n)
metric m (Interval i1 i2) (Interval j1 j2) = Product (m i1 j1) (m i2 j2)
{-# INLINE metric #-}
......@@ -123,7 +123,7 @@ evalInterval env0 e = snd $
Fix.filter apply Fix.iterateInner
widenVal :: Widening Val
widenVal = widening (I.widening ?bound)
widenVal = widening (I.bounded ?bound)
evalInterval' :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval' env expr = snd $ evalInterval env expr
......
......@@ -119,7 +119,7 @@ run k env ss = fmap (fmap (fmap fst)) <$> snd $
. Fix.iterateInner
widenEnvStore = M.widening widenVal W.** SM.widening W.finite
widenVal = widening (I.widening ?bound)
widenVal = widening (I.bounded ?bound)
widenExc (Exception m1) (Exception m2) = Exception <$> M.widening widenVal m1 m2
widenResult = T.widening $ E.widening W.finite (Exc.widening widenExc (M.widening widenVal W.** W.finite))
thrd (_,_,z) = z
......
......@@ -107,7 +107,7 @@ run k lstmts =
statementLabel st = case st of (s:_) -> Just (label s); [] -> Nothing
widenEnvStore = SM.widening W.finite W.** M.widening (widenVal W.** W.finite)
widenVal = widening (I.widening ?bound)
widenVal = widening (I.bounded ?bound)
widenExc (Exception m1) (Exception m2) = Exception <$> M.widening widenVal m1 m2
widenResult = T.widening $ E.widening W.finite (Exc.widening widenExc (M.widening (widenVal W.** W.finite) W.** W.finite))
......
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