content: module Test.Kore.Attribute.Pattern.FreeVariables (
      test_Synthetic,
      test_instance_Synthetic_TermLike,
      test_concat,
  ) where
  
  import Kore.Attribute.Pattern.FreeVariables (
      FreeVariables,
   )
  import Kore.Attribute.Pattern.FreeVariables qualified as FreeVariables
  import Kore.Attribute.Synthetic
  import Kore.Internal.TermLike (
      Symbol,
      TermLikeF (..),
   )
  import Kore.Syntax hiding (
      PatternF (..),
   )
  import Prelude.Kore
  import Test.Kore.Rewrite.MockSymbols qualified as Mock
  import Test.Tasty
  import Test.Tasty.HUnit
  
  test_Synthetic :: [TestTree]
  test_Synthetic =
      [ BinaryAnd sort x y `gives` xy $ "And"
      , BinaryAnd sort x x `gives` xx $ "And counts"
      , Application sigma [x, y] `gives` xy $ "ApplySymbol"
      , Bottom sort `gives` mempty $ "Bottom"
      , Ceil sort sort x `gives` x $ "Ceil"
      , DomainValue sort x `gives` x $ "DomainValue"
      , Equals sort sort x y `gives` xy $ "Equals"
      , Floor sort sort x `gives` x $ "Floor"
      , Iff sort x y `gives` xy $ "Iff"
      , Implies sort x y `gives` xy $ "Implies"
      , In sort sort x y `gives` xy $ "In"
      , Next sort x `gives` x $ "Next"
      , Not sort x `gives` x $ "Not"
      , BinaryOr sort x y `gives` xy $ "Or"
      , Rewrites sort x y `gives` xy $ "Rewrites"
      , Top sort `gives` mempty $ "Top"
      , -- Binders and variables are the only interesting cases:
        Exists sort Mock.x xy `gives` y $ "Exists - Bound"
      , Exists sort Mock.x y `gives` y $ "Exists - Free"
      , Forall sort Mock.x xy `gives` y $ "Forall - Bound"
      , Forall sort Mock.x y `gives` y $ "Forall - Free"
      , Mu Mock.setX sxy `gives` sy $ "Mu - Bound"
      , Mu Mock.setX sy `gives` sy $ "Mu - Free"
      , Nu Mock.setX sxy `gives` sy $ "Nu - Bound"
      , Nu Mock.setX sy `gives` sy $ "Nu - Free"
      ]
  
  test_instance_Synthetic_TermLike :: [TestTree]
  test_instance_Synthetic_TermLike =
      [ AndF (BinaryAnd sort x y) `gives'` xy $ "AndF"
      , AndF (BinaryAnd sort x x) `gives'` xx $ "AndF counts"
      , ApplySymbolF (Application sigma [x, y]) `gives'` xy $ "ApplySymbolF"
      , BottomF (Bottom sort) `gives'` mempty $ "BottomF"
      , CeilF (Ceil sort sort x) `gives'` x $ "CeilF"
      , DomainValueF (DomainValue sort x) `gives'` x $ "DomainValueF"
      , EqualsF (Equals sort sort x y) `gives'` xy $ "EqualsF"
      , FloorF (Floor sort sort x) `gives'` x $ "FloorF"
      , IffF (Iff sort x y) `gives'` xy $ "IffF"
      , ImpliesF (Implies sort x y) `gives'` xy $ "ImpliesF"
      , InF (In sort sort x y) `gives'` xy $ "InF"
      , NextF (Next sort x) `gives'` x $ "NextF"
      , NotF (Not sort x) `gives'` x $ "NotF"
      , OrF (BinaryOr sort x y) `gives'` xy $ "OrF"
      , RewritesF (Rewrites sort x y) `gives'` xy $ "RewritesF"
      , TopF (Top sort) `gives'` mempty $ "TopF"
      , -- Binders and variables are the only interesting cases:
        ExistsF (Exists sort Mock.x xy) `gives'` y $ "ExistsF - Bound"
      , ExistsF (Exists sort Mock.x y) `gives'` y $ "ExistsF - Free"
      , ForallF (Forall sort Mock.x xy) `gives'` y $ "ForallF - Bound"
      , ForallF (Forall sort Mock.x y) `gives'` y $ "ForallF - Free"
      , (VariableF . Const) (inject Mock.x) `gives'` x $ "Elem VariableF"
      , MuF (Mu Mock.setX sxy) `gives'` sy $ "MuF - Bound"
      , MuF (Mu Mock.setX sy) `gives'` sy $ "MuF - Free"
      , NuF (Nu Mock.setX sxy) `gives'` sy $ "NuF - Bound"
      , NuF (Nu Mock.setX sy) `gives'` sy $ "NuF - Free"
      , (VariableF . Const) (inject Mock.setX) `gives'` sx $ "Set VariableF"
      ]
    where
      gives' = gives @(TermLikeF VariableName)
  
  sort :: Sort
  sort = Mock.testSort
  
  sigma :: Symbol
  sigma = Mock.sigmaSymbol
  
  x, y, xx, xy, sx, sy, sxy :: FreeVariables VariableName
  x = FreeVariables.freeVariable (inject Mock.x)
  y = FreeVariables.freeVariable (inject Mock.y)
  xx = x <> x
  xy = x <> y
  sx = FreeVariables.freeVariable (inject Mock.setX)
  sy = FreeVariables.freeVariable (inject Mock.setY)
  sxy = sx <> sy
  
  test_concat :: [TestTree]
  test_concat =
      [ testCase "x not equal xx" $ do
          assertBool "" (x /= xx)
      ]
  
  gives ::
      (Synthetic (FreeVariables VariableName) base, HasCallStack) =>
      base (FreeVariables VariableName) ->
      FreeVariables VariableName ->
      String ->
      TestTree
  gives original expected name =
      testCase name $ do
          let actual = synthetic original
          assertEqual "" expected actual
  