content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE OverloadedStrings #-}
  module IntervalAnalysisSpec where
  
  import           Prelude hiding (succ,pred,id)
  
  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
  
  import           IntervalAnalysis
  
  import           Syntax
  
  import           GHC.Exts(toList)
  
  main :: IO ()
  main = hspec spec
  
  spec :: Spec
  spec = do
    let ?bound = I.Interval (-100) 100
        ?sensitivity = 3
    sharedSpec (toEither . evalInterval' []) (NumVal . fromIntegral)
  
    describe "behavior specific to interval analysis" $ do
      it "should execute both branches on IfZero on interval containing zero" $
        let ?bound = I.Interval (-100) 100
            ?sensitivity = 1
        in evalInterval' [("x", num (-5) 5)]
            (ifZero "x" (succ zero) (pred zero))
            `shouldBe` Terminating (Success (num (-1) 1))
  
      it "should compute 0 + -1 + 1 = 0" $
        let ?bound = I.Interval (-100) 100
            ?sensitivity = 1
        in evalInterval' [] (succ (pred zero)) `shouldBe`
             Terminating (Success (num 0 0))
  
      it "should analyse addition correctly" $
        let ?bound = I.Interval 0 10
            ?sensitivity = 2
        in do
          evalInterval' [] (let_ [("add",add)] (app "add" [zero,two])) `shouldBe` Terminating (Success (num 2 2))
          evalInterval' [] (let_ [("add",add)] (app "add" [one,two])) `shouldBe` Terminating (Success (num 3 3))
          evalInterval' [("x", num 0 1)] (let_ [("add",add)] (app "add" ["x",two]))
            -- Most precise would be [2,3], however, the analysis does not refine
            -- `x` and therefore introduces some imprecision.
            `shouldBe` Terminating (Success (num 2 5))
  
      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
        let ?sensitivity = 0 in evalInterval' [] diamond `shouldBe` Terminating (Success (num 1 2))
        let ?sensitivity = 1 in evalInterval' [] diamond `shouldBe` Terminating (Success (num 2 2))
  
      it "should terminate for the non-terminating program" $
        let ?bound = I.Interval 0 5
            ?sensitivity = 2
        in evalInterval' [] (let_ [("id", lam ["x"] "x"),
                                  ("fix",lam ["x"] (app "fix" ["x"]))]
                           (app "fix" ["id"]))
             `shouldBe` NonTerminating
  
    where
      id = lam ["x"] "x"
      second = lam ["_","y"] "y"
      add = lam ["x","y"] $ ifZero "x" "y" (succ (app "add" [pred "x","y"]))
  
      one = succ zero
      two = succ one
  
      num i j = NumVal $ I.Interval i j
  
      toEither :: Terminating (Error (Pow String) a) -> Either String a
      toEither (Terminating (Fail e)) = Left (unwords (toList e))
      toEither (Terminating (Success x)) = Right x
      toEither NonTerminating = Left "NonTerminating"
  