content: {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE OverloadedLists #-}
  module IntervalAnalysisSpec where
  
  import Prelude hiding ((<),Bool(..))
  import Syntax
  import IntervalAnalysis
  
  import Data.Abstract.Interval as I
  import Data.Abstract.Terminating as Term
  import Data.Abstract.Error as Err
  import Data.Abstract.Except as Exc
  import Data.Abstract.Boolean(Bool(..))
  
  import Test.Hspec
  
  main :: IO ()
  main = hspec spec
  
  spec :: Spec
  spec = do
    it "x:=2; y:=4; x:=1; z:=0; if(y>x) {z:=y} {z:=y*y}; x:=z" $ do
      let ?bound = I.Interval (-500) 500
      run 3 [("x",0),("y",1),("z",2)] ["x" =: 2, "y" =: 4, "x" =: 1, "z" =: 0, ifExpr ("x" ~= "y") ["z" =: "y"] ["z" =: "y" * "y"], "x" =: "z"]
        `shouldBe` res [(0,num 16 16), (1,num 4 4), (2,num 16 16)]
  
    it "9 < 10 == true" $ do
      let ?bound = I.Interval (-500) 500
      run 3 [("x",0)] ["x" =: 9 < 10]
        `shouldBe` res [(0, BoolVal True)]
  
    it "10 < 10 == false" $ do
      let ?bound = I.Interval (-500) 500
      run 3 [("x",0)] ["x" =: 10 < 10]
        `shouldBe` res [(0, BoolVal False)]
  
    it "while(true) {}" $ do
      let ?bound = I.Interval (-500) 500
      run 3 [] [while true []]
        `shouldBe` NonTerminating
  
    it "x := 1; while(x < 10){x:= x + 1}" $ do
      let ?bound = I.Interval (-500) 500
      run 15 [("x",0)] ["x" =: 1, while ("x" < 10) ["x" =: "x" + 1]]
        `shouldBe` res [(0, num 10 10)]
  
    it "x := 1; while(x < 10){x:= x + 1; while(x > 0) {x := x - 1}}" $ do
      let ?bound = I.Interval (-500) 500
      run 15 [] ["x" =: 1, while ("x" < 10) ["x" =: "x" + 1, while (0 < "x") ["x" =: "x" - 1 ]]]
        `shouldBe` NonTerminating
  
    it "x := 1; y := 1; while(x < 3){x:= x + 1; i := 1, while(i < 2) {y := y + 1}}" $ do
      let ?bound = I.Interval (-500) 500
      run 10 [("x",0),("y",1)] ["x" =: 1, "y" =: 1, while ("x" < 3) ["x" =: "x" + 1, "i" =: 1, while ("i" < 2) ["i" =: "i" + 1, "y" =: "y" + 1 ]]]
        `shouldBe` res [(0, num 3 3),(1,num 3 3),(14,num 2 2)]
  
    where
      res x = Term.Terminating (Err.Success (Exc.Success x))
      num i j = NumVal (I.Interval i j)
  