Commit ef4c3b94 authored by Sven Keidel's avatar Sven Keidel

PCF: add factorial test

parent 88370e6b
Pipeline #31415 passed with stages
in 40 minutes and 35 seconds
......@@ -85,7 +85,7 @@ withBounds2 f (Interval i1 i2) (Interval j1 j2) =
instance (Ord n, Bounded n) => UpperBounded (Interval n) where
top = Interval minBound maxBound
bounded :: Ord n => Interval n -> Widening (Interval (InfiniteNumber n))
bounded :: Ord n => Interval (InfiniteNumber n) -> Widening (Interval (InfiniteNumber n))
bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
( if (i1,i2) P.== (r1,r2) || (j1,j2) P.== (r1,r2) then Stable else Unstable
, Interval r1 r2
......@@ -94,11 +94,11 @@ bounded (Interval lowerBound upperBound) (Interval i1 i2) (Interval j1 j2) =
lower = min i1 j1
upper = max i2 j2
r1 = if | lower P.< Number lowerBound -> NegInfinity
| Number upperBound P.< lower -> Number upperBound
r1 = if | lower P.< lowerBound -> NegInfinity
| upperBound P.< lower -> upperBound
| otherwise -> lower
r2 = if | Number upperBound P.< upper -> Infinity
| upper P.< Number lowerBound -> Number lowerBound
r2 = if | upperBound P.< upper -> Infinity
| upper P.< lowerBound -> lowerBound
| otherwise -> upper
widening :: Ord n => Widening (Interval (InfiniteNumber n))
......
......@@ -53,6 +53,10 @@ instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c) => IsVal V
NumVal n -> returnA -< NumVal (n - 1)
_ -> fail -< "Expected a number as argument for 'pred'"
mult = proc x -> case x of
(NumVal n, NumVal m) -> returnA -< NumVal (n * m)
_ -> fail -< "Expected two numbers as argument for 'mult'"
zero = arr $ const (NumVal 0)
if_ f g = proc (v1, (x, y)) -> case v1 of
......
......@@ -40,6 +40,10 @@ eval = fix $ \ev -> proc e0 -> case e0 of
Pred e _ -> do
v <- ev -< e
pred -< v
Mult e1 e2 _ -> do
v1 <- ev -< e1
v2 <- ev -< e2
mult -< (v1,v2)
IfZero e1 e2 e3 _ -> do
v1 <- ev -< e1
if_ ev ev -< (v1, (e2, e3))
......@@ -70,4 +74,6 @@ class IsVal v c | c -> v where
-- | creates the numeric value zero.
zero :: c () v
mult :: c (v,v) v
if_ :: Join z c => c x z -> c y z -> c (v, (x, y)) z
......@@ -93,7 +93,7 @@ type Out = (Store, Terminating (Error (Pow String) Val))
-- | Run the abstract interpreter for an interval analysis. The arguments are the
-- maximum interval bound, the depth @k@ of the longest call string,
-- an environment, and the input of the computation.
evalInterval :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> (Store, Terminating (Error (Pow String) Val))
evalInterval :: (?sensitivity :: Int, ?bound :: IV) => [(Text,Val)] -> State Label Expr -> (Store, Terminating (Error (Pow String) Val))
evalInterval env0 e = snd $
run (extend' (Generic.eval ::
Fix'
......@@ -128,7 +128,7 @@ evalInterval env0 e = snd $
widenVal :: Widening Val
widenVal = widening (I.bounded ?bound)
evalInterval' :: (?sensitivity :: Int, ?bound :: Interval Int) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval' :: (?sensitivity :: Int, ?bound :: IV) => [(Text,Val)] -> State Label Expr -> Terminating (Error (Pow String) Val)
evalInterval' env expr = snd $ evalInterval env expr
{-# INLINE evalInterval' #-}
......@@ -143,6 +143,10 @@ instance (IsString e, ArrowChoice c, ArrowFail e c) => IsVal Val (ValueT Val c)
NumVal n -> returnA -< NumVal $ n - 1
_ -> fail -< "Expected a number as argument for 'pred'"
mult = proc x -> case x of
(NumVal n, NumVal m) -> returnA -< NumVal $ n * m
_ -> fail -< "Expected two numbers as argument for 'mult'"
zero = proc _ -> returnA -< NumVal 0
if_ f g = proc v -> case v of
......
......@@ -25,6 +25,7 @@ data Expr
| Lam [Text] Expr Label
| App Expr [Expr] Label
| Zero Label
| Mult Expr Expr Label
| Succ Expr Label
| Pred Expr Label
| IfZero Expr Expr Expr Label
......@@ -52,6 +53,9 @@ succ e = Succ <$> e <*> fresh
pred :: State Label Expr -> State Label Expr
pred e = Pred <$> e <*> fresh
mult :: State Label Expr -> State Label Expr -> State Label Expr
mult e1 e2 = Mult <$> e1 <*> e2 <*> fresh
ifZero :: State Label Expr -> State Label Expr -> State Label Expr -> State Label Expr
ifZero e1 e2 e3 = IfZero <$> e1 <*> e2 <*> e3 <*> fresh
......@@ -78,6 +82,10 @@ instance Show Expr where
$ showsPrec (app_prec + 1) e1
. showString " "
. showsPrec (app_prec + 1) e2
Mult e1 e2 _ -> showParen (d > mult_prec)
$ showsPrec (mult_prec + 1) e1
. showString " * "
. showsPrec (mult_prec + 1) e2
Lam x e2 _ -> showParen (d > lam_prec)
$ showString "λ"
. showString (unwords (map unpack x))
......@@ -86,6 +94,7 @@ instance Show Expr where
where
app_prec = 10
lam_prec = 9
mult_prec = 8
instance HasLabel Expr where
label e = case e of
......@@ -95,6 +104,7 @@ instance HasLabel Expr where
Zero l -> l
Succ _ l -> l
Pred _ l -> l
Mult _ _ l -> l
IfZero _ _ _ l -> l
Let _ _ l -> l
Apply _ l -> l
......@@ -123,6 +133,7 @@ freeVars e0 = execState (go e0) M.empty
Zero _ -> return H.empty
Succ e1 _ -> go e1
Pred e1 _ -> go e1
Mult e1 e2 _ -> H.union <$> go e1 <*> go e2
IfZero e1 e2 e3 _ -> do
m1 <- go e1
m2 <- go e2
......
......@@ -9,6 +9,7 @@ import Data.Abstract.DiscretePowerset(Pow)
import Data.Abstract.Error hiding (toEither)
import qualified Data.Abstract.Interval as I
import Data.Abstract.Terminating hiding (toEither)
import Data.Abstract.InfiniteNumbers(InfiniteNumber(..))
import Test.Hspec
import SharedSpecs
......@@ -53,6 +54,13 @@ spec = do
-- `x` and therefore introduces some imprecision.
`shouldBe` Terminating (Success (num 2 7))
context "the factorial function" $
it "should only return positive numbers" $
let ?bound = I.Interval 0 Infinity
?sensitivity = 1
in evalInterval' [("x", num 0 Infinity)] (let_ [("fact", lam ["n"] (ifZero "n" (succ zero) (mult (app "fact" [pred "n"]) "n")))] (app "fact" ["x"])) `shouldBe`
Terminating (Success (num NegInfinity Infinity))
it "context sensitivity" $
let diamond = let_ [("second",second),("id",id)] (app "second" [app "id" [one],app "id" [two]]) in
let ?bound = I.Interval 0 5 in do
......
......@@ -96,7 +96,7 @@ newtype Exception = Exception (Map Text Val) deriving (PreOrd,Complete,Show,Eq)
-- 'Generic.run' with the components for fixpoint computation
-- ('FixT'), termination ('TerminatingT'), failure ('ErrorT'), store
-- ('StoreT'), environments ('EnvT'), and values ('IntervalT').
run :: (?bound :: Interval Int) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run :: (?bound :: IV) => Int -> [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run k env ss = fmap (fmap (fmap fst)) <$> snd $
Trans.run
(Generic.run ::
......
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