grisette-0.5.0.0: test/Grisette/SymPrim/Prim/TabularFunTests.hs

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Grisette.SymPrim.Prim.TabularFunTests (tabularFunTests) where

import Grisette
  ( type (=->) (TabularFun),
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalApplyTerm (pevalApplyTerm),
    SupportedPrim (pevalITETerm),
    Term,
    applyTerm,
    conTerm,
    pevalEqTerm,
    ssymTerm,
  )
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@=?))

tabularFunTests :: Test
tabularFunTests =
  testGroup
    "TabularFun"
    [ testGroup
        "Apply"
        [ testCase "On concrete" $ do
            let f :: Integer =-> Integer =
                  TabularFun [(1, 2), (3, 4)] 5
            pevalApplyTerm (conTerm f) (conTerm 0) @=? conTerm 5
            pevalApplyTerm (conTerm f) (conTerm 1) @=? conTerm 2
            pevalApplyTerm (conTerm f) (conTerm 2) @=? conTerm 5
            pevalApplyTerm (conTerm f) (conTerm 3) @=? conTerm 4
            pevalApplyTerm (conTerm f) (conTerm 4) @=? conTerm 5,
          testCase "On concrete function" $ do
            let f :: Integer =-> Integer =
                  TabularFun [(1, 2), (3, 4)] 5
            pevalApplyTerm (conTerm f) (ssymTerm "b")
              @=? pevalITETerm
                (pevalEqTerm (conTerm 1 :: Term Integer) (ssymTerm "b"))
                (conTerm 2)
                ( pevalITETerm
                    (pevalEqTerm (conTerm 3 :: Term Integer) (ssymTerm "b"))
                    (conTerm 4)
                    (conTerm 5)
                ),
          testCase "On symbolic" $ do
            pevalApplyTerm (ssymTerm "f" :: Term (Integer =-> Integer)) (ssymTerm "a")
              @=? applyTerm
                (ssymTerm "f" :: Term (Integer =-> Integer))
                (ssymTerm "a" :: Term Integer)
        ]
    ]