{-# LANGUAGE OverloadedStrings #-}

module Jikka.Core.Language.AssertedHintSpec (spec) where

import Data.Maybe
import Jikka.Common.Alpha
import Jikka.Common.Error
import qualified Jikka.Core.Convert.ArithmeticExpr as ArithmeticExpr
import qualified Jikka.Core.Convert.EqualitySolving as EqualitySolving
import qualified Jikka.Core.Convert.TypeInfer as TypeInfer
import Jikka.Core.Language.ArithmeticExpr
import Jikka.Core.Language.AssertedHint
import Jikka.Core.Language.Expr
import Jikka.Core.Language.RewriteRules
import Jikka.Core.Parse (parseExpr)
import Test.Hspec

parseExpr' :: [(VarName, Type)] -> String -> Expr
parseExpr' env e = fromSuccess . flip evalAlphaT 100 $ do
  e <- parseExpr e
  e <- TypeInfer.runExpr env e
  e <- fromMaybe e <$> applyRewriteRule EqualitySolving.rule (makeRewriteEnvironmentFromTypeEnv env) e
  ArithmeticExpr.runExpr env e

spec :: Spec
spec = do
  describe "parseHints" $ do
    it "works on n == 3" $ do
      let e = parseExpr' [("n", IntTy)] "n == 3"
      let expected =
            [ ("n", EqualHint (integerArithmeticExpr 3))
            ]
      parseHints e `shouldBe` expected
    it "works on length xs == 3" $ do
      let e = parseExpr' [("xs", ListTy IntTy)] "len xs == 3"
      let expected =
            [ ("xs", LengthHint IntTy (EqualHint (integerArithmeticExpr 3)))
            ]
      parseHints e `shouldBe` expected
    it "works on length xs >= 3" $ do
      let e = parseExpr' [("xs", ListTy IntTy)] "len xs >= 3"
      let expected =
            [ ("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 3)) Nothing))
            ]
      parseHints e `shouldBe` expected
    it "works on xs /= nil" $ do
      let e = parseExpr' [("xs", ListTy IntTy)] "xs /= nil"
      let expected =
            [ ("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 1)) Nothing))
            ]
      parseHints e `shouldBe` expected
    it "works on length 0 <= xs - 3" $ do
      let e = parseExpr' [("xs", ListTy IntTy)] "0 <= len xs - 3"
      let expected =
            [ ("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 3)) Nothing))
            ]
      parseHints e `shouldBe` expected

  describe "lowerBoundWithHints" $ do
    it "works on length n == 3" $ do
      let hints = [("n", EqualHint (integerArithmeticExpr 3))]
      let e = Var "n"
      let expected = Just 3
      lowerBoundWithHints hints e `shouldBe` expected

  describe "upperBoundWithHints" $ do
    it "works on length n == 3" $ do
      let hints = [("n", EqualHint (integerArithmeticExpr 3))]
      let e = Var "n"
      let expected = Just 4
      upperBoundWithHints hints e `shouldBe` expected

  describe "nullWithHints" $ do
    it "works on length xs >= 3" $ do
      let hints = [("xs", LengthHint IntTy (BoundHint (Just (integerArithmeticExpr 3)) Nothing))]
      let e = Var "xs"
      let expected = Just False
      nullWithHints hints e `shouldBe` expected
    it "works on length xs == 0" $ do
      let hints = [("xs", LengthHint IntTy (EqualHint (integerArithmeticExpr 0)))]
      let e = Var "xs"
      let expected = Just True
      nullWithHints hints e `shouldBe` expected
    it "works on length xs == 1" $ do
      let hints = [("xs", LengthHint IntTy (EqualHint (integerArithmeticExpr 1)))]
      let e = Var "xs"
      let expected = Just False
      nullWithHints hints e `shouldBe` expected
    it "works on length xs < 3" $ do
      let hints = [("xs", LengthHint IntTy (BoundHint Nothing (Just (integerArithmeticExpr 3))))]
      let e = Var "xs"
      let expected = Nothing
      nullWithHints hints e `shouldBe` expected