From ef4c3b94cc530c9179e98578ee4e7bfdd33f1748 Mon Sep 17 00:00:00 2001 From: Sven Keidel Date: Fri, 17 Jan 2020 15:16:13 +0100 Subject: [PATCH] PCF: add factorial test --- lib/src/Data/Abstract/Interval.hs | 10 +++++----- pcf/src/ConcreteInterpreter.hs | 4 ++++ pcf/src/GenericInterpreter.hs | 6 ++++++ pcf/src/IntervalAnalysis.hs | 8 ++++++-- pcf/src/Syntax.hs | 11 +++++++++++ pcf/test/IntervalAnalysisSpec.hs | 8 ++++++++ while/src/IntervalAnalysis.hs | 2 +- 7 files changed, 41 insertions(+), 8 deletions(-) diff --git a/lib/src/Data/Abstract/Interval.hs b/lib/src/Data/Abstract/Interval.hs index 0f1b75c..296d334 100644 --- a/lib/src/Data/Abstract/Interval.hs +++ b/lib/src/Data/Abstract/Interval.hs @@ -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)) diff --git a/pcf/src/ConcreteInterpreter.hs b/pcf/src/ConcreteInterpreter.hs index 442e796..51b4d1d 100644 --- a/pcf/src/ConcreteInterpreter.hs +++ b/pcf/src/ConcreteInterpreter.hs @@ -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 diff --git a/pcf/src/GenericInterpreter.hs b/pcf/src/GenericInterpreter.hs index 7de759f..1b079fe 100644 --- a/pcf/src/GenericInterpreter.hs +++ b/pcf/src/GenericInterpreter.hs @@ -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 diff --git a/pcf/src/IntervalAnalysis.hs b/pcf/src/IntervalAnalysis.hs index e9fba7e..a4b7fc8 100644 --- a/pcf/src/IntervalAnalysis.hs +++ b/pcf/src/IntervalAnalysis.hs @@ -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 diff --git a/pcf/src/Syntax.hs b/pcf/src/Syntax.hs index 12b6262..192dfb1 100644 --- a/pcf/src/Syntax.hs +++ b/pcf/src/Syntax.hs @@ -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 diff --git a/pcf/test/IntervalAnalysisSpec.hs b/pcf/test/IntervalAnalysisSpec.hs index 9d3d73f..6ca4ad1 100644 --- a/pcf/test/IntervalAnalysisSpec.hs +++ b/pcf/test/IntervalAnalysisSpec.hs @@ -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 diff --git a/while/src/IntervalAnalysis.hs b/while/src/IntervalAnalysis.hs index 20c999d..ed09920 100644 --- a/while/src/IntervalAnalysis.hs +++ b/while/src/IntervalAnalysis.hs @@ -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 :: -- 2.26.2