content: module Test.Kore.Rewrite.Axiom.Matcher (
      test_matcherEqualHeads,
      test_matcherVariableFunction,
      test_matcherNonVarToPattern,
      test_matcherMergeSubresults,
      test_matching_Bool,
      test_matching_Int,
      test_matching_String,
      test_matching_List,
      test_matching_Set,
      test_matching_Map,
      test_matching_Pair,
      test_matching_Exists,
      test_matching_Forall,
      test_matching_Equals,
      test_matching_And,
      test_matcherOverloading,
      match,
      MatchResult,
      matches,
      doesn'tMatch,
  ) where
  
  import Data.Map.Strict (
      Map,
   )
  import Data.Map.Strict qualified as Map
  import Data.Text (
      Text,
   )
  import Kore.Builtin.Bool qualified as Bool
  import Kore.Builtin.String qualified as String
  import Kore.Internal.Predicate (
      Predicate,
      makeCeilPredicate,
      makeTruePredicate,
   )
  import Kore.Internal.SideCondition qualified as SideCondition
  import Kore.Internal.TermLike
  import Kore.Rewrite.Axiom.Matcher (
      patternMatch,
   )
  import Kore.Rewrite.RewritingVariable (
      RewritingVariableName,
      configElementVariableFromId,
      mkConfigVariable,
   )
  import Prelude.Kore
  import Test.Kore (
      testId,
   )
  import Test.Kore.Builtin.Definition qualified as Test
  import Test.Kore.Rewrite.MockSymbols qualified as Mock
  import Test.Kore.Simplify
  import Test.Tasty
  import Test.Tasty.HUnit.Ext
  
  test_matcherEqualHeads :: [TestTree]
  test_matcherEqualHeads =
      [ testGroup
          "Application"
          [ matches
              "same symbol"
              (Mock.plain10 (mkElemVar Mock.xConfig))
              (Mock.plain10 Mock.a)
              [(inject Mock.xConfig, Mock.a)]
          , matches
              "same symbol, set variables"
              (Mock.plain10 (mkSetVar Mock.setXConfig))
              (Mock.plain10 (mkTop Mock.testSort))
              [(inject Mock.setXConfig, mkTop Mock.testSort)]
          , doesn'tMatch
              "different constructors"
              (Mock.constr10 (mkElemVar Mock.xConfig))
              (Mock.constr11 Mock.a)
          , doesn'tMatch
              "different functions"
              (Mock.f Mock.b)
              (Mock.g Mock.a)
          , doesn'tMatch
              "different functions with variable"
              (Mock.f (mkElemVar Mock.xConfig))
              (Mock.g Mock.a)
          , doesn'tMatch
              "different symbols"
              (Mock.plain10 Mock.b)
              (Mock.plain11 Mock.a)
          , doesn'tMatch
              "different symbols with variable"
              (Mock.plain10 (mkElemVar Mock.xConfig))
              (Mock.plain11 Mock.a)
          , doesn'tMatch
              "inj{src, tgt1}(x:src) does not match inj{src, tgt2}(x:src)"
              (Mock.sortInjection10 (mkElemVar Mock.xConfig0))
              (Mock.sortInjection0ToTop (mkElemVar Mock.xConfig0))
          ]
      , testCase "Bottom" $ do
          let expect = Right (makeTruePredicate, Map.empty)
          actual <-
              matchDefinition
                  (mkBottom Mock.topSort)
                  (mkBottom Mock.topSort)
          assertEqual "" expect actual
      , testCase "Ceil" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.singleton (inject Mock.xConfig) Mock.a
                      )
          actual <-
              matchDefinition
                  (mkCeil Mock.topSort (Mock.plain10 (mkElemVar Mock.xConfig)))
                  (mkCeil Mock.topSort (Mock.plain10 Mock.a))
          assertEqual "" expect actual
      , testCase "Match multiple opaque parts" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.fromList
                          [ (inject Mock.setXConfigSetSort, mkElemVar Mock.xConfigSet)
                          , (inject Mock.setYConfigSetSort, mkElemVar Mock.yConfigSet)
                          ]
                      )
          actual <-
              matchDefinition
                  ( Mock.framedSet
                      []
                      [ mkSetVar Mock.setXConfigSetSort
                      , mkSetVar Mock.setYConfigSetSort
                      ]
                  )
                  ( Mock.framedSet
                      []
                      [mkElemVar Mock.xConfigSet, mkElemVar Mock.yConfigSet]
                  )
          assertEqual "" expect actual
      , testCase "Equals" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.singleton
                          (inject Mock.xConfig)
                          (mkElemVar Mock.yConfig)
                      )
          actual <-
              matchDefinition
                  ( mkEquals
                      Mock.topSort
                      (Mock.plain10 (mkElemVar Mock.xConfig))
                      (Mock.plain10 Mock.a)
                  )
                  ( mkEquals
                      Mock.topSort
                      (Mock.plain10 (mkElemVar Mock.yConfig))
                      (Mock.plain10 Mock.a)
                  )
          assertEqual "" expect actual
      , testCase "Builtin" $ do
          actual <-
              matchDefinition
                  ( mkDomainValue
                      DomainValue
                          { domainValueSort = Mock.testSort1
                          , domainValueChild = mkStringLiteral "10"
                          }
                  )
                  ( mkDomainValue
                      DomainValue
                          { domainValueSort = Mock.testSort1
                          , domainValueChild = mkStringLiteral "10"
                          }
                  )
          assertEqual "" topCondition actual
      , testCase "Equals and builtin" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , [
                            ( inject Mock.tConfig
                            , mkElemVar Mock.xConfig
                            )
                        ,
                            ( inject Mock.zConfig
                            , Mock.a
                            )
                        ,
                            ( inject Mock.uConfig
                            , Mock.b
                            )
                        ]
                          & Map.fromList
                      )
          actual <-
              matchDefinition
                  ( mkEquals
                      Mock.testSort
                      (Mock.functional20 (mkElemVar Mock.tConfig) (mkElemVar Mock.zConfig))
                      (Mock.functional20 (mkElemVar Mock.tConfig) (mkElemVar Mock.uConfig))
                  )
                  ( mkEquals
                      Mock.testSort
                      (Mock.functional20 (mkElemVar Mock.xConfig) Mock.a)
                      (Mock.functional20 (mkElemVar Mock.xConfig) Mock.b)
                  )
          assertEqual "" expect actual
      , testCase "DomainValue" $ do
          actual <-
              matchDefinition
                  ( mkDomainValue
                      DomainValue
                          { domainValueSort = Mock.testSort1
                          , domainValueChild = mkStringLiteral "10"
                          }
                  )
                  ( mkDomainValue
                      DomainValue
                          { domainValueSort = Mock.testSort1
                          , domainValueChild = mkStringLiteral "10"
                          }
                  )
          assertEqual "" topCondition actual
      , testCase "StringLiteral" $ do
          actual <-
              matchDefinition
                  (mkStringLiteral "10")
                  (mkStringLiteral "10")
          assertEqual "" topCondition actual
      , testCase "Top" $ do
          actual <-
              matchDefinition
                  (mkTop Mock.topSort)
                  (mkTop Mock.topSort)
          assertEqual "" topCondition actual
      , testCase "Iff vs Or" $ do
          let expect = Left "unimplemented matching case"
          actual <-
              matchDefinition
                  (mkIff (Mock.plain10 Mock.a) (mkElemVar Mock.xConfig))
                  (mkOr (Mock.plain10 Mock.a) Mock.b)
          assertEqual "" expect actual
      , testGroup
          "Simplification"
          [ testCase "same symbol" $ do
              let expect =
                      mkMatchResult
                          ( makeTruePredicate
                          , Map.singleton (inject Mock.xConfig) Mock.a
                          )
              actual <-
                  matchSimplification
                      (Mock.plain10 (mkElemVar Mock.xConfig))
                      (Mock.plain10 Mock.a)
              assertEqual "" expect actual
          ]
      , testGroup
          "Not"
          [ matches
              "not equals"
              (mkNot $ mkEquals Mock.topSort Mock.a (mkElemVar Mock.xConfig))
              (mkNot $ mkEquals Mock.topSort Mock.a Mock.b)
              [((inject Mock.xConfig), Mock.b)]
          , matches
              "not symbol"
              (mkNot $ mkElemVar Mock.xConfig)
              (mkNot Mock.a)
              [((inject Mock.xConfig), Mock.a)]
          , doesn'tMatch
              "not with different arguments"
              (mkNot $ mkElemVar Mock.xConfig)
              (mkNot $ mkEquals Mock.topSort Mock.a Mock.b)
          ]
      ]
  
  test_matcherVariableFunction :: [TestTree]
  test_matcherVariableFunction =
      [ testCase "Functional" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.singleton
                          (inject Mock.xConfig)
                          Mock.functional00
                      )
          actual <- matchDefinition (mkElemVar Mock.xConfig) Mock.functional00
          assertEqual "" expect actual
      , testCase "SetVariable vs Function" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.singleton
                          (inject Mock.setXConfig)
                          Mock.cf
                      )
          actual <- matchDefinition (mkSetVar Mock.setXConfig) Mock.cf
          assertEqual "" expect actual
      , testCase "SetVariable vs Bottom" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.singleton
                          (inject Mock.setXConfig)
                          (mkBottom Mock.testSort)
                      )
          actual <-
              matchDefinition (mkSetVar Mock.setXConfig) (mkBottom Mock.testSort)
          assertEqual "" expect actual
      , testCase "Function" $ do
          let expect =
                  mkMatchResult
                      ( makeCeilPredicate Mock.cf
                      , Map.singleton (inject Mock.xConfig) Mock.cf
                      )
          actual <- matchDefinition (mkElemVar Mock.xConfig) Mock.cf
          assertEqual "" expect actual
      , testCase "Non-functional" $ do
          let expect = Left "unimplemented matching case"
          actual <- matchDefinition (mkElemVar Mock.xConfig) (Mock.constr10 Mock.cf)
          assertEqual "" expect actual
      , testCase "Unidirectional" $ do
          let expect = Left "unimplemented matching case"
          actual <-
              matchDefinition
                  (Mock.functional10 (mkElemVar Mock.yConfig))
                  (mkElemVar Mock.xConfig)
          assertEqual "" expect actual
      , testCase "Injection" $ do
          let a = Mock.functional00SubSubSort
              x = configElementVariableFromId (testId "x") Mock.subSort
              expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.singleton
                          (inject x)
                          (Mock.sortInjectionSubSubToSub a)
                      )
          actual <-
              matchDefinition
                  (Mock.sortInjectionSubToTop (mkElemVar x))
                  (Mock.sortInjectionSubSubToTop a)
          assertEqual "" expect actual
      , testCase "Injection reverse" $ do
          let a = Mock.functional00SubSubSort
              x = configElementVariableFromId (testId "x") Mock.subSort
              expect = Left "unimplemented matching case"
          actual <-
              matchDefinition
                  (Mock.sortInjectionSubSubToTop a)
                  (Mock.sortInjectionSubToTop (mkElemVar x))
          assertEqual "" expect actual
      , testCase "Injection + substitution" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.fromList
                          [
                              ( inject xSub
                              , Mock.sortInjectionSubSubToSub aSubSub
                              )
                          ,
                              ( inject Mock.xConfig
                              , Mock.functional10 Mock.a
                              )
                          ]
                      )
          actual <-
              matchDefinition
                  ( Mock.functionalTopConstr20
                      (Mock.sortInjectionSubToTop (mkElemVar xSub))
                      (mkElemVar Mock.xConfig)
                  )
                  ( Mock.functionalTopConstr20
                      (Mock.sortInjectionSubSubToTop aSubSub)
                      (Mock.functional10 Mock.a)
                  )
          assertEqual "" expect actual
      , testCase "substitution + Injection" $ do
          let expect =
                  mkMatchResult
                      ( makeTruePredicate
                      , Map.fromList
                          [
                              ( inject xSub
                              , Mock.sortInjectionSubSubToSub aSubSub
                              )
                          ,
                              ( inject Mock.xConfig
                              , Mock.functional10 Mock.a
                              )
                          ]
                      )
          actual <-
              matchDefinition
                  ( Mock.functionalTopConstr21
                      (mkElemVar Mock.xConfig)
                      (Mock.sortInjectionSubToTop (mkElemVar xSub))
                  )
                  ( Mock.functionalTopConstr21
                      (Mock.functional10 Mock.a)
                      (Mock.sortInjectionSubSubToTop aSubSub)
                  )
          assertEqual "" expect actual
      , testGroup
          "Simplification"
          [ testCase "Function" $ do
              let expect =
                      mkMatchResult
                          ( makeCeilPredicate Mock.cf
                          , Map.singleton (inject Mock.xConfig) Mock.cf
                          )
              actual <- matchSimplification (mkElemVar Mock.xConfig) Mock.cf
              assertEqual "" expect actual
          , testCase "Non-function" $ do
              let expect = Left "unimplemented matching case"
              actual <-
                  matchSimplification
                      (mkElemVar Mock.xConfig)
                      (Mock.constr10 Mock.cf)
              assertEqual "" expect actual
          ]
      , testGroup
          "AC (Set) under function"
          [ testCase "Syntactically equivalent" $ do
              let config =
                      Mock.fSet2
                          (Mock.framedSet [mkElemVar Mock.xRuleInt] [mkElemVar Mock.xRuleSet])
                          (Mock.framedSet [mkElemVar Mock.yRuleInt] [])
                  ruleLHS =
                      Mock.fSet2
                          (Mock.framedSet [mkElemVar Mock.xEquationInt] [mkElemVar Mock.xEquationSet])
                          (Mock.framedSet [mkElemVar Mock.yEquationInt] [])
                  expected =
                      mkMatchResult
                          ( makeTruePredicate
                          , [ (inject Mock.xEquationInt, mkElemVar Mock.xRuleInt)
                            , -- I was expecting the following to be:
                              -- (inject Mock.xEquationSet, mkElemVar Mock.xRuleSet)
                              (inject Mock.xEquationSet, Mock.framedSet [] [mkElemVar Mock.xRuleSet])
                            , (inject Mock.yEquationInt, mkElemVar Mock.yRuleInt)
                            ]
                              & Map.fromList
                          )
              actual <- match ruleLHS config
              assertEqual "" expected actual
          , testCase "Second set matches variable" $ do
              let config =
                      Mock.fSet2
                          (Mock.framedSet [mkElemVar Mock.xRuleInt] [mkElemVar Mock.xRuleSet])
                          (Mock.framedSet [mkElemVar Mock.yRuleInt] [])
                  ruleLHS =
                      Mock.fSet2
                          (Mock.framedSet [mkElemVar Mock.xEquationInt] [mkElemVar Mock.xEquationSet])
                          (mkElemVar Mock.yEquationSet)
                  expected =
                      mkMatchResult
                          ( makeTruePredicate
                          , [ (inject Mock.xEquationInt, mkElemVar Mock.xRuleInt)
                            , -- I was expecting the following to be:
                              -- (inject Mock.xEquationSet, mkElemVar Mock.xRuleSet)
                              (inject Mock.xEquationSet, Mock.framedSet [] [mkElemVar Mock.xRuleSet])
                            , (inject Mock.yEquationSet, Mock.framedSet [mkElemVar Mock.yRuleInt] [])
                            ]
                              & Map.fromList
                          )
              actual <- match ruleLHS config
              assertEqual "" expected actual
          , testCase "Concrete first set" $ do
              let config =
                      Mock.fSet2
                          (Mock.framedSet [Mock.builtinInt 1] [])
                          (Mock.framedSet [mkElemVar Mock.yRuleInt] [])
                  ruleLHS =
                      Mock.fSet2
                          (Mock.framedSet [mkElemVar Mock.xEquationInt] [mkElemVar Mock.xEquationSet])
                          (Mock.framedSet [mkElemVar Mock.yEquationInt] [])
                  expected =
                      mkMatchResult
                          ( makeTruePredicate
                          , [ (inject Mock.xEquationInt, Mock.builtinInt 1)
                            , (inject Mock.xEquationSet, Mock.framedSet [] [])
                            , (inject Mock.yEquationInt, mkElemVar Mock.yRuleInt)
                            ]
                              & Map.fromList
                          )
              actual <- match ruleLHS config
              assertEqual "" expected actual
          , testCase "Concrete first set, second matches variable" $ do
              let config =
                      Mock.fSet2
                          (Mock.framedSet [Mock.builtinInt 1] [])
                          (Mock.framedSet [mkElemVar Mock.yRuleInt] [])
                  ruleLHS =
                      Mock.fSet2
                          (Mock.framedSet [mkElemVar Mock.xEquationInt] [mkElemVar Mock.xEquationSet])
                          (mkElemVar Mock.yEquationSet)
                  expected =
                      mkMatchResult
                          ( makeTruePredicate
                          , [ (inject Mock.xEquationInt, Mock.builtinInt 1)
                            , (inject Mock.xEquationSet, Mock.framedSet [] [])
                            , (inject Mock.yEquationSet, Mock.framedSet [mkElemVar Mock.yRuleInt] [])
                            ]
                              & Map.fromList
                          )
              actual <- match ruleLHS config
              assertEqual "" expected actual
          , testCase "Different sorts don't match" $ do
              let config = Mock.a
                  ruleLHS = mkElemVar Mock.xEquationInt
                  expected = Left "sorts don't match"
              actual <- match ruleLHS config
              assertEqual "" expected actual
          ]
      ]
    where
      aSubSub = Mock.functional00SubSubSort
      xSub = configElementVariableFromId (testId "xSub") Mock.subSort
  
  test_matcherNonVarToPattern :: [TestTree]
  test_matcherNonVarToPattern =
      [ failure Mock.a Mock.b "no-var - no-var"
      , failure (mkElemVar Mock.xConfig) Mock.a "var - no-var"
      , failure Mock.a (mkElemVar Mock.xConfig) "no-var - var"
      , failure (mkElemVar Mock.xConfig) (mkElemVar Mock.yConfig) "no-var - var"
      ]
    where
      failure term1 term2 name =
          doesn'tMatch name (Mock.plain10 term1) (Mock.plain11 term2)
  
  test_matcherMergeSubresults :: [TestTree]
  test_matcherMergeSubresults =
      [ testCase "Application" $ do
          let expect =
                  mkMatchResult
                      ( makeCeilPredicate Mock.cf
                      , Map.fromList
                          [ (inject Mock.xConfig, Mock.cf)
                          , (inject Mock.yConfig, Mock.b)
                          ]
                      )
          actual <-
              matchDefinition
                  ( Mock.plain20
                      (mkElemVar Mock.xConfig)
                      (Mock.constr20 Mock.cf (mkElemVar Mock.yConfig))
                  )
                  ( Mock.plain20
                      Mock.cf
                      (Mock.constr20 Mock.cf Mock.b)
                  )
          assertEqual "" expect actual
      , testCase "Merge error" $ do
          let expect = Left "unimplemented matching case"
          actual <-
              matchDefinition
                  (mkAnd (mkElemVar Mock.xConfig) (mkElemVar Mock.xConfig))
                  ( mkAnd
                      (mkElemVar Mock.yConfig)
                      (Mock.f (mkElemVar Mock.yConfig))
                  )
          assertEqual "" expect actual
      ]
  
  test_matching_Bool :: [TestTree]
  test_matching_Bool =
      [ testCase "concrete top" $ do
          let expect = top
          actual <- matchConcrete True True
          assertEqual "" expect actual
      , testCase "concrete bottom" $ do
          let expect = Left "distinct builtin booleans"
          actual <- matchConcrete True False
          assertEqual "" expect actual
      , testCase "variable vs concrete" $ do
          let expect = substitution [(inject Mock.xConfigBool, True)]
          actual <- matchVariable Mock.xConfigBool True
          assertEqual "" expect actual
      , doesn'tMatch
          "true does not match x:Bool"
          (mkBool True)
          (mkElemVar Mock.xConfigBool)
      , doesn'tMatch
          "false does not match x:Bool"
          (mkBool False)
          (mkElemVar Mock.xConfigBool)
      ]
    where
      top = topCondition
      substitution subst =
          mkMatchResult
              ( makeTruePredicate
              , Map.fromList ((fmap . fmap) mkBool subst)
              )
      mkBool = Bool.asInternal Mock.boolSort
      matchConcrete = matchDefinition `on` mkBool
      matchVariable var val =
          matchDefinition (mkElemVar var) (mkBool val)
  
  test_matching_Int :: [TestTree]
  test_matching_Int =
      [ testCase "concrete top" $ do
          let expect = top
          actual <- matchConcrete 1 1
          assertEqual "" expect actual
      , doesn'tMatch "1 does not match 2" (mkInt 1) (mkInt 2)
      , testCase "variable vs concrete" $ do
          let expect = substitution [(inject Mock.xConfigInt, 1)]
          actual <- matchVariable Mock.xConfigInt 1
          assertEqual "" expect actual
      , doesn'tMatch
          "1 does not match x:Int"
          (mkInt 1)
          (mkElemVar xInt)
      ]
    where
      top = topCondition
      substitution subst =
          mkMatchResult
              ( makeTruePredicate
              , Map.fromList ((fmap . fmap) mkInt subst)
              )
      matchConcrete = matchDefinition `on` mkInt
      matchVariable var val =
          matchDefinition (mkElemVar var) (mkInt val)
  
  test_matching_String :: [TestTree]
  test_matching_String =
      [ testCase "concrete top" $ do
          let expect = topCondition
          actual <- matchConcrete "str" "str"
          assertEqual "" expect actual
      , testCase "concrete bottom" $ do
          let expect = Left "distinct builtin strings"
          actual <- matchConcrete "s1" "s2"
          assertEqual "" expect actual
      , testCase "variable vs concrete" $ do
          let expect =
                  substitution [(inject Mock.xConfigString, "str")]
          actual <- matchVariable Mock.xConfigString "str"
          assertEqual "" expect actual
      , doesn'tMatch
          "\"str\" does not match x:String"
          (mkStr "str")
          (mkElemVar Mock.xConfigString)
      ]
    where
      substitution subst =
          mkMatchResult
              ( makeTruePredicate
              , Map.fromList ((fmap . fmap) mkStr subst)
              )
      mkStr = String.asInternal Mock.stringSort
      matchConcrete = matchDefinition `on` mkStr
      matchVariable var val =
          matchDefinition (mkElemVar var) (mkStr val)
  
  test_matching_List :: [TestTree]
  test_matching_List =
      [ matches
          "[1, 2] matches [1, 2]"
          (concreteList [1, 2])
          (concreteList [1, 2])
          []
      , doesn'tMatch
          "[1, 2] does not match [1, 3]"
          (concreteList [1, 2])
          (concreteList [1, 3])
      , doesn'tMatch
          "[1, 2] does not match [1, 2, 3]"
          (concreteList [1, 2])
          (concreteList [1, 2, 3])
      , doesn'tMatch
          "[1] does not match x:List"
          (concreteList [1])
          (mkElemVar Mock.xConfigList)
      , matches
          "[1, x:Int] matches [1, 2]"
          (mkList [mkInt 1, mkElemVar Mock.xConfigInt])
          (concreteList [1, 2])
          [(inject Mock.xConfigInt, mkInt 2)]
      , matches
          "[x:Int, y:Int] matches [1, 2]"
          (mkList [mkElemVar xInt, mkElemVar yInt])
          (mkList [mkInt 1, mkInt 2])
          [(inject xInt, mkInt 1), (inject yInt, mkInt 2)]
      , matches
          "[1, x:Int, 3, y:Int] matches [1, 2, 3, 4]"
          (mkList [mkInt 1, mkElemVar xInt, mkInt 3, mkElemVar yInt])
          (mkList [mkInt 1, mkInt 2, mkInt 3, mkInt 4])
          [(inject xInt, mkInt 2), (inject yInt, mkInt 4)]
      , doesn'tMatch
          "[1, x:Int] does not match [2, 1]"
          (mkList [mkInt 1, mkElemVar xInt])
          (concreteList [2, 1])
      , matches
          "concatList([], x:List) matches [1, 2, 3]"
          (concatList (mkList []) (mkVar xList))
          (mkList [mkInt 1, mkInt 2, mkInt 3])
          [(xList, mkList [mkInt 1, mkInt 2, mkInt 3])]
      , matches
          "concatList([1, 2, 3], x:List) matches [1, 2, 3]"
          (prefixList [mkInt 1, mkInt 2, mkInt 3] xList)
          (concreteList [1, 2, 3])
          [(xList, unitList)]
      , matches
          "concatList(x:List, []) matches [1, 2, 3]"
          (concatList (mkVar xList) unitList)
          (concreteList [1, 2, 3])
          [(xList, concreteList [1, 2, 3])]
      , matches
          "concatList(x:List, [1, 2, 3]) matches [1, 2, 3]"
          (concatList (mkVar xList) (concreteList [1, 2, 3]))
          (concreteList [1, 2, 3])
          [(xList, unitList)]
      , matches
          "[x:Int] x:List matches [1, 2, 3]"
          (concatList (mkList [mkElemVar xInt]) (mkVar xList))
          (mkList [mkInt 1, mkInt 2, mkInt 3])
          [(inject xInt, mkInt 1), (xList, mkList [mkInt 2, mkInt 3])]
      , matches
          "x:List [x:Int] matches [1, 2, 3]"
          (concatList (mkVar xList) (mkList [mkElemVar xInt]))
          (mkList [mkInt 1, mkInt 2, mkInt 3])
          [(inject xInt, mkInt 3), (xList, mkList [mkInt 1, mkInt 2])]
      , doesn'tMatch "[] does not match y:List" unitList (mkVar yList)
      , doesn'tMatch
          "[1] x:List does not match y:List"
          (prefixList [one] xList)
          (mkVar yList)
      , doesn'tMatch
          "x:List [1] does not match y:List"
          (suffixList xList [one])
          (mkVar yList)
      , matches "[] ~ []" unitList unitList []
      , doesn'tMatch "[] does not match [1]" unitList (mkList [one])
      , doesn'tMatch
          "[] does not match [1] x:List"
          unitList
          (prefixList [one] xList)
      , doesn'tMatch
          "[] does not match x:List [1]"
          unitList
          (suffixList xList [one])
      , doesn'tMatch "[1] does not match []" (mkList [one]) unitList
      , matches
          "[1] ~ [1]"
          (mkList [one])
          (mkList [one])
          []
      , matches
          "[x:Int] ~ [1]"
          (mkList [mkElemVar xInt])
          (mkList [one])
          [(inject xInt, one)]
      , doesn'tMatch
          "[1] does not match [1] x:List"
          (mkList [one])
          (prefixList [one] xList)
      , doesn'tMatch
          "[1] does not match x:List [1]"
          (mkList [one])
          (suffixList xList [one])
      , doesn'tMatch
          "[1] x:List does not match []"
          (prefixList [one] xList)
          unitList
      , matches
          "[1] x:List ~ [1]"
          (prefixList [one] xList)
          (mkList [one])
          [(xList, unitList)]
      , matches
          "[x:Int] y:List ~ [1]"
          (prefixList [mkElemVar xInt] yList)
          (mkList [one])
          [ (inject xInt, one)
          , (yList, unitList)
          ]
      , matches
          "[1] x:List ~ [1, 2]"
          (prefixList [one] xList)
          (mkList [one, two])
          [(xList, mkList [two])]
      , matches
          "[x:Int] y:List ~ [1, 2]"
          (prefixList [mkElemVar xInt] yList)
          (mkList [one, two])
          [ (inject xInt, one)
          , (yList, mkList [two])
          ]
      , doesn'tMatch
          "x:List [1] does not match []"
          (suffixList xList [one])
          unitList
      , matches
          "x:List [1] ~ [1]"
          (suffixList xList [one])
          (mkList [one])
          [(xList, unitList)]
      , matches
          "y:List [x:Int] ~ [1]"
          (suffixList yList [mkElemVar xInt])
          (mkList [one])
          [ (inject xInt, one)
          , (yList, unitList)
          ]
      , matches
          "x:List [2] ~ [1, 2]"
          (suffixList xList [two])
          (mkList [one, two])
          [(xList, mkList [one])]
      , matches
          "y:List [x:Int] ~ [1, 2]"
          (suffixList yList [mkElemVar xInt])
          (mkList [one, two])
          [ (inject xInt, two)
          , (yList, mkList [one])
          ]
      ]
    where
      xList = inject $ configElementVariableFromId (testId "xList") Mock.listSort
      yList = inject $ configElementVariableFromId (testId "yList") Mock.listSort
      one = mkInt 1
      two = mkInt 2
      concatList = Mock.concatList
      unitList = mkList []
      prefixList elems frame = concatList (mkList elems) (mkVar frame)
      suffixList frame elems = concatList (mkVar frame) (mkList elems)
      concreteList = mkList . map mkInt
      mkList = Mock.builtinList
  
  test_matching_Exists :: [TestTree]
  test_matching_Exists =
      [ matches
          "∃ x:Int. x matches ∃ y:Int. y"
          (mkExists xInt $ mkElemVar xInt)
          (mkExists yInt $ mkElemVar yInt)
          []
      , matches
          "∃ x:Int. (x, z:Int) matches ∃ y:Int. (y, 1)"
          (mkExists xInt $ mkPair (mkElemVar xInt) (mkElemVar zInt))
          (mkExists yInt $ mkPair (mkElemVar yInt) (mkInt 1))
          [(inject zInt, mkInt 1)]
      , matches
          "∃ x:Int y:Int. (x, y) matches ∃ y:Int x:Int. (y, x)"
          (mkExistsN [xInt, yInt] $ mkPair (mkElemVar xInt) (mkElemVar yInt))
          (mkExistsN [yInt, xInt] $ mkPair (mkElemVar yInt) (mkElemVar xInt))
          []
      , doesn'tMatch
          "∃ x:Int. (x, z:Int) doesn't match ∃ y:Int. (y, y)"
          (mkExists xInt $ mkPair (mkElemVar xInt) (mkElemVar zInt))
          (mkExists yInt $ mkPair (mkElemVar yInt) (mkElemVar yInt))
      , doesn'tMatch
          "∃ x:Int y:Int. (x, y) doesn't match ∃ y:Int x:Int. (x, y)"
          (mkExistsN [xInt, yInt] $ mkPair (mkElemVar xInt) (mkElemVar yInt))
          (mkExistsN [yInt, xInt] $ mkPair (mkElemVar xInt) (mkElemVar yInt))
      , doesn'tMatch
          "∃ x:Int. (x, z:Int) doesn't match ∃ m:Map. (m, 1)"
          (mkExists xInt $ mkPair (mkElemVar xInt) (mkElemVar zInt))
          (mkExists mMap $ mkPair (mkElemVar mMap) (mkInt 1))
      , -- Renaming bound variables
        doesn'tMatch
          "∃ x:Int x:Int. (x, x) doesn't match ∃ x:Int y:Int. (x, x)"
          (mkExistsN [xInt, xInt] $ mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkExistsN [xInt, yInt] $ mkPair (mkElemVar xInt) (mkElemVar xInt))
      , matches
          "∃ x:Int x:Int. (x, x) matches ∃ x:Int y:Int. (y, y)"
          (mkExistsN [xInt, xInt] $ mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkExistsN [xInt, yInt] $ mkPair (mkElemVar yInt) (mkElemVar yInt))
          []
      ]
  
  test_matching_Equals :: [TestTree]
  test_matching_Equals =
      [ matches
          "equals(x,y) matches equals(1,y)"
          (mkEquals' (mkElemVar xInt) (mkElemVar yInt))
          (mkEquals' (mkInt 1) (mkElemVar yInt))
          [(inject xInt, mkInt 1)]
      , doesn'tMatch
          "equals(x,1) doesn't match equals(y,2)"
          (mkEquals' (mkElemVar xInt) (mkInt 1))
          (mkEquals' (mkElemVar yInt) (mkInt 2))
      , doesn'tMatch
          "equals(x,x) doesn't match equals(1,2)"
          (mkEquals' (mkElemVar xInt) (mkElemVar xInt))
          (mkEquals' (mkInt 1) (mkInt 2))
      ]
    where
      mkEquals' = mkEquals Mock.intSort
  
  test_matching_Forall :: [TestTree]
  test_matching_Forall =
      [ matches
          "∀ x:Int. x matches ∀ y:Int. y"
          (mkForall xInt $ mkElemVar xInt)
          (mkForall yInt $ mkElemVar yInt)
          []
      , matches
          "∀ x:Int. (x, z:Int) matches ∀ y:Int. (y, 1)"
          (mkForall xInt $ mkPair (mkElemVar xInt) (mkElemVar zInt))
          (mkForall yInt $ mkPair (mkElemVar yInt) (mkInt 1))
          [(inject zInt, mkInt 1)]
      , matches
          "∀ x:Int y:Int. (x, y) matches ∀ y:Int x:Int. (y, x)"
          (mkForallN [xInt, yInt] $ mkPair (mkElemVar xInt) (mkElemVar yInt))
          (mkForallN [yInt, xInt] $ mkPair (mkElemVar yInt) (mkElemVar xInt))
          []
      , doesn'tMatch
          "∀ x:Int. (x, z:Int) doesn't match ∀ y:Int. (y, y)"
          (mkForall xInt $ mkPair (mkElemVar xInt) (mkElemVar zInt))
          (mkForall yInt $ mkPair (mkElemVar yInt) (mkElemVar yInt))
      , doesn'tMatch
          "∀ x:Int y:Int. (x, y) doesn't match ∀ y:Int x:Int. (x, y)"
          (mkForallN [xInt, yInt] $ mkPair (mkElemVar xInt) (mkElemVar yInt))
          (mkForallN [yInt, xInt] $ mkPair (mkElemVar xInt) (mkElemVar yInt))
      , doesn'tMatch
          "∀ x:Int. (x, z:Int) doesn't match ∀ m:Map. (m, 1)"
          (mkForall xInt $ mkPair (mkElemVar xInt) (mkElemVar zInt))
          (mkForall mMap $ mkPair (mkElemVar mMap) (mkInt 1))
      , -- Renaming bound variables
        doesn'tMatch
          "∀ x:Int x:Int. (x, x) doesn't match ∀ x:Int y:Int. (x, x)"
          (mkForallN [xInt, xInt] $ mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkForallN [xInt, yInt] $ mkPair (mkElemVar xInt) (mkElemVar xInt))
      , matches
          "∀ x:Int x:Int. (x, x) matches ∀ x:Int y:Int. (y, y)"
          (mkForallN [xInt, xInt] $ mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkForallN [xInt, yInt] $ mkPair (mkElemVar yInt) (mkElemVar yInt))
          []
      ]
  
  test_matching_Pair :: [TestTree]
  test_matching_Pair =
      [ doesn'tMatch
          "(x, x) does not match (y, z)"
          (mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkPair (mkElemVar yInt) (mkElemVar zInt))
      , matches
          "(x, y) matches (y, y)"
          (mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkPair (mkElemVar yInt) (mkElemVar yInt))
          [(inject xInt, mkElemVar yInt)]
      , doesn'tMatch
          "(x, x) does not match (1, 2)"
          (mkPair (mkElemVar xInt) (mkElemVar xInt))
          (mkPair (mkInt 1) (mkInt 2))
      , matches
          "(x, y) matches (y, z)"
          (mkPair (mkElemVar xInt) (mkElemVar yInt))
          (mkPair (mkElemVar yInt) (mkElemVar zInt))
          [(inject xInt, mkElemVar yInt), (inject yInt, mkElemVar zInt)]
      , matches
          "(y, x) matches (z, y)"
          (mkPair (mkElemVar yInt) (mkElemVar xInt))
          (mkPair (mkElemVar zInt) (mkElemVar yInt))
          [(inject xInt, mkElemVar yInt), (inject yInt, mkElemVar zInt)]
      ]
  
  test_matching_And :: [TestTree]
  test_matching_And =
      [ matches
          "and(x, x) matches x"
          (mkAnd (mkElemVar xInt) (mkElemVar xInt))
          (mkElemVar xInt)
          []
      , matches
          "and(x, y) matches y"
          (mkAnd (mkElemVar xInt) (mkElemVar yInt))
          (mkElemVar yInt)
          [(inject xInt, mkElemVar yInt)]
      , matches
          "and(y, x) matches y"
          (mkAnd (mkElemVar yInt) (mkElemVar xInt))
          (mkElemVar yInt)
          [(inject xInt, mkElemVar yInt)]
      , matches
          "and(x, y) matches z"
          (mkAnd (mkElemVar xInt) (mkElemVar yInt))
          (mkElemVar zInt)
          [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)]
      , doesn'tMatch
          "and(x, 1) does not match 2"
          (mkAnd (mkElemVar xInt) (mkInt 1))
          (mkInt 2)
      , doesn'tMatch
          "and(1, x) does not match 2"
          (mkAnd (mkInt 1) (mkElemVar xInt))
          (mkInt 2)
      ]
  
  mkPair ::
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName
  mkPair = Test.pair
  
  topCondition :: MatchResult
  topCondition = Right (makeTruePredicate, Map.empty)
  
  test_matching_Set :: [TestTree]
  test_matching_Set =
      [ matches
          "[] matches []"
          (mkSet [] [])
          (mkSet [] [])
          []
      , matches
          "[0, 1, 2] matches [0, 1, 2]"
          (mkSet [mkInt 0, mkInt 1, mkInt 2] [])
          (mkSet [mkInt 0, mkInt 1, mkInt 2] [])
          []
      , doesn'tMatch
          "[] does not match [0]"
          (mkSet [] [])
          (mkSet [mkInt 0] [])
      , doesn'tMatch
          "[0] does not match []"
          (mkSet [mkInt 0] [])
          (mkSet [] [])
      , doesn'tMatch
          "[0] does not match [1]"
          (mkSet [mkInt 0] [])
          (mkSet [mkInt 1] [])
      , matches
          "[x:Int] matches [0]"
          (mkSet [mkElemVar xInt] [])
          (mkSet [mkInt 0] [])
          [(inject xInt, mkInt 0)]
      , matches
          "[x:Int] s:Set matches [0]"
          (mkSet [mkElemVar xInt] [mkVar sSet])
          (mkSet [mkInt 0] [])
          [ (inject xInt, mkInt 0)
          , (sSet, mkSet [] [])
          ]
      , matchesMulti
          "[x:Int] s:Set matches [0, 1]"
          (mkSet [mkElemVar xInt] [mkVar sSet])
          (mkSet [mkInt 0, mkInt 1] [])
          [
              [ (inject xInt, mkInt 0)
              , (sSet, mkSet [mkInt 1] [])
              ]
          ,
              [ (inject xInt, mkInt 1)
              , (sSet, mkSet [mkInt 0] [])
              ]
          ]
      , matches
          "[y:Int] matches [x:Int]"
          (mkSet [mkElemVar yInt] [])
          (mkSet [mkElemVar xInt] [])
          [(inject yInt, mkElemVar xInt)]
      , doesn'tMatch
          "[y:Int, 1] doesn't match [x:Int]"
          (mkSet [mkElemVar yInt, mkInt 1] [])
          (mkSet [mkElemVar xInt] [])
      , doesn'tMatch
          "[0, y:Int] doesn't match [1, x:Int]"
          (mkSet [mkInt 0, mkElemVar yInt] [])
          (mkSet [mkInt 1, mkElemVar xInt] [])
      , matches
          "[y:Int, 1] matches [1, x:Int]"
          (mkSet [mkElemVar yInt, mkInt 1] [])
          (mkSet [mkInt 1, mkElemVar xInt] [])
          [(inject yInt, mkElemVar xInt)]
      , matches
          "[y:Int, 1] s:Set matches [1, x:Int] s':Set"
          (mkSet [mkElemVar yInt, mkInt 1] [mkVar sSet])
          (mkSet [mkInt 1, mkElemVar xInt] [mkVar s'Set])
          [ (inject yInt, mkElemVar xInt)
          , (sSet, mkVar s'Set)
          ]
      , -- This should work, but it doesn't with the current
        -- AC matching algorithm
        -- , matches
        --     "[y:Int, 1] s:Set matches [1, x:Int]"
        --     (mkSet [mkElemVar yInt, mkInt 1] [mkVar sSet])
        --     (mkSet [mkInt 1, mkElemVar xInt] [])
        --     [ (inject yInt, mkElemVar xInt)
        --     , (sSet, mkSet [] [])
        --     ]
        matches
          "s:Set matches [x:Int]"
          (mkVar sSet)
          (mkSet [mkElemVar xInt] [])
          [(sSet, mkSet [mkElemVar xInt] [])]
      , matches
          "[x:Int] s:Set matches [1] s':Set"
          (mkSet [mkElemVar xInt] [mkVar sSet])
          (mkSet [mkInt 1] [mkVar s'Set])
          [ (inject xInt, mkInt 1)
          , (sSet, mkSet [] [mkVar s'Set])
          ]
      ]
  
  sSet :: SomeVariable RewritingVariableName
  sSet =
      inject $
          mkElementVariable (testId "sSet") Mock.setSort
              & mapElementVariable (pure mkConfigVariable)
  
  s'Set :: SomeVariable RewritingVariableName
  s'Set =
      inject $
          mkElementVariable (testId "s'Set") Mock.setSort
              & mapElementVariable (pure mkConfigVariable)
  
  mkSet ::
      [TermLike RewritingVariableName] ->
      [TermLike RewritingVariableName] ->
      TermLike RewritingVariableName
  mkSet =
      Mock.framedSet
  
  test_matching_Map :: [TestTree]
  test_matching_Map =
      [ matches
          "0 |-> 1  1 |-> 2  matches itself"
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [])
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [])
          []
      , doesn'tMatch
          "0 |-> 1  1 |-> 2  does not match 0 |-> 1"
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [])
          (mkMap [(mkInt 0, mkInt 1)] [])
      , doesn'tMatch
          "0 |-> 1  1 |-> 2  does not match 0 |-> 1  1 |-> 3"
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [])
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 3)] [])
      , doesn'tMatch
          "0 |-> 1 does not match m:Map"
          (mkMap [(mkInt 0, mkInt 1)] [])
          (mkElemVar mMap)
      , matches
          "0 |-> x:Int matches 0 |-> 1"
          (mkMap [(mkInt 0, mkElemVar xInt)] [])
          (mkMap [(mkInt 0, mkInt 1)] [])
          [(inject xInt, mkInt 1)]
      , matches
          "0 |-> x:Int  1 |-> y:Int matches 0 |-> 1  1 |-> 2"
          (mkMap [(mkInt 0, mkElemVar xInt), (mkInt 1, mkElemVar yInt)] [])
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [])
          [(inject xInt, mkInt 1), (inject yInt, mkInt 2)]
      , matches
          "0 |-> 1  1 |-> 2  m:Map matches 0 |-> 1  1 |-> 2"
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [mkElemVar mMap])
          (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] [])
          [(inject mMap, mkMap [] [])]
      , matches
          "(x:Int, [x:Int -> y:Int] m:Map) matches (0, [0 -> 1, 1 -> 2])"
          (mkPair (mkElemVar xInt) (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap]))
          (mkPair (mkInt 0) (mkMap [(mkInt 0, mkInt 1), (mkInt 1, mkInt 2)] []))
          [ (inject xInt, mkInt 0)
          , (inject yInt, mkInt 1)
          , (inject mMap, mkMap [(mkInt 1, mkInt 2)] [])
          ]
      , matches
          "x:Int |-> y:Int matches x:Int |-> 0"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [])
          (mkMap [(mkElemVar xInt, mkInt 0)] [])
          [(inject yInt, mkInt 0)]
      , matches
          "x:Int |-> y:Int 1 -> z:Int matches x:Int |-> 0  1 -> 2"
          (mkMap [(mkElemVar xInt, mkElemVar yInt), (mkInt 1, mkElemVar zInt)] [])
          (mkMap [(mkElemVar xInt, mkInt 0), (mkInt 1, mkInt 2)] [])
          [(inject yInt, mkInt 0), (inject zInt, mkInt 2)]
      , doesn'tMatch
          "x:Int |-> y:Int doesn't match x:Int |-> 0  1 |-> 2"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [])
          (mkMap [(mkElemVar xInt, mkInt 0), (mkInt 1, mkInt 2)] [])
      , doesn'tMatch
          "x:Int |-> y:Int  1 |-> 2 doesn't match x:Int |-> 0"
          (mkMap [(mkElemVar xInt, mkElemVar yInt), (mkInt 1, mkInt 2)] [])
          (mkMap [(mkElemVar xInt, mkInt 0)] [])
      , matches
          "m:Map matches x:Int |-> 0"
          (mkMap [] [mkElemVar mMap])
          (mkMap [(mkElemVar xInt, mkInt 0)] [])
          [(inject mMap, mkMap [(mkElemVar xInt, mkInt 0)] [])]
      , matches
          "x:Int |-> y:Int  m:Map matches x:Int |-> 0"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkElemVar xInt, mkInt 0)] [])
          [(inject yInt, mkInt 0), (inject mMap, mkMap [] [])]
      , matches
          "x:Int |-> y:Int 1 -> z:Int  m:Map matches x:Int |-> 0  1 -> 2"
          ( mkMap
              [(mkElemVar xInt, mkElemVar yInt), (mkInt 1, mkElemVar zInt)]
              [mkElemVar mMap]
          )
          ( mkMap
              [(mkElemVar xInt, mkInt 0), (mkInt 1, mkInt 2)]
              []
          )
          [ (inject yInt, mkInt 0)
          , (inject zInt, mkInt 2)
          , (inject mMap, mkMap [] [])
          ]
      , matches
          "x:Int |-> y:Int  m:Map matches x:Int |-> 0  1 |-> 2"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkElemVar xInt, mkInt 0), (mkInt 1, mkInt 2)] [])
          [ (inject yInt, mkInt 0)
          , (inject mMap, mkMap [(mkInt 1, mkInt 2)] [])
          ]
      , matches
          "1 |-> y:Int  m:Map matches x:Int |-> 0  1 |-> 2"
          (mkMap [(mkInt 1, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkElemVar xInt, mkInt 0), (mkInt 1, mkInt 2)] [])
          [ (inject yInt, mkInt 2)
          , (inject mMap, mkMap [(mkElemVar xInt, mkInt 0)] [])
          ]
      , doesn'tMatch
          "x:Int |-> y:Int  1 |-> 2   m:Map doesn't match x:Int |-> 0"
          ( mkMap
              [(mkElemVar xInt, mkElemVar yInt), (mkInt 1, mkInt 2)]
              [mkElemVar mMap]
          )
          ( mkMap
              [(mkElemVar xInt, mkInt 0)]
              []
          )
      , matches
          "1 |-> y:Int  m:Map matches 1 |-> 2  n:Map"
          (mkMap [(mkInt 1, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkInt 1, mkInt 2)] [mkElemVar nMap])
          [ (inject yInt, mkInt 2)
          , (inject mMap, mkElemVar nMap)
          ]
      , matches
          "x:Int |-> y:Int  m:Map matches x:Int |-> 0  n:Map"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkElemVar xInt, mkInt 0)] [mkElemVar nMap])
          [ (inject yInt, mkInt 0)
          , (inject mMap, mkElemVar nMap)
          ]
      , matchesP
          "x:Int |-> y:Int  m:Map matches x:Int |-> 0  1 |-> 2  n:Map"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap])
          ( mkMap
              [ (mkElemVar xInt, mkInt 0)
              , (mkInt 1, mkInt 2)
              ]
              [mkElemVar nMap]
          )
          (makeCeilPredicate (mkMap [(mkInt 1, mkInt 2)] [mkElemVar nMap]))
          [ (inject yInt, mkInt 0)
          , (inject mMap, mkMap [(mkInt 1, mkInt 2)] [mkElemVar nMap])
          ]
      , matchesP
          "1 |-> y:Int  m:Map matches x:Int |-> 0  1 |-> 2  n:Map"
          (mkMap [(mkInt 1, mkElemVar yInt)] [mkElemVar mMap])
          ( mkMap
              [ (mkElemVar xInt, mkInt 0)
              , (mkInt 1, mkInt 2)
              ]
              [mkElemVar nMap]
          )
          ( makeCeilPredicate
              (mkMap [(mkElemVar xInt, mkInt 0)] [mkElemVar nMap])
          )
          [ (inject yInt, mkInt 2)
          , (inject mMap, mkMap [(mkElemVar xInt, mkInt 0)] [mkElemVar nMap])
          ]
      , matches
          "x:Int |-> y:Int  m matches 0 |-> 1"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkInt 0, mkInt 1)] [])
          [ (inject xInt, mkInt 0)
          , (inject yInt, mkInt 1)
          , (inject mMap, mkMap [] [])
          ]
      , matchesMulti
          "x:Int |-> y:Int  m:Map matches 0 |-> 1  2 |-> 3"
          (mkMap [(mkElemVar xInt, mkElemVar yInt)] [mkElemVar mMap])
          (mkMap [(mkInt 0, mkInt 1), (mkInt 2, mkInt 3)] [])
          [
              [ (inject xInt, mkInt 0)
              , (inject yInt, mkInt 1)
              , (inject mMap, mkMap [(mkInt 2, mkInt 3)] [])
              ]
          ,
              [ (inject xInt, mkInt 2)
              , (inject yInt, mkInt 3)
              , (inject mMap, mkMap [(mkInt 0, mkInt 1)] [])
              ]
          ]
      ]
  
  test_matcherOverloading :: [TestTree]
  test_matcherOverloading =
      [ testGroup
          "Overloading" -- most overloading tests are in AndTerms
          [ matches
              "direct overload, left side"
              (Mock.topOverload (Mock.sortInjectionOtherToTop Mock.aOtherSort))
              (Mock.sortInjectionOtherToTop (Mock.otherOverload Mock.aOtherSort))
              []
          , matches
              "direct overload, right side"
              (Mock.sortInjectionOtherToTop (Mock.otherOverload Mock.aOtherSort))
              (Mock.topOverload (Mock.sortInjectionOtherToTop Mock.aOtherSort))
              []
          , matches
              "overload, both sides, unifiable"
              ( Mock.sortInjectionOtherToTop
                  ( Mock.otherOverload
                      (Mock.sortInjectionSubSubToOther Mock.aSubSubsort)
                  )
              )
              ( Mock.sortInjectionSubToTop
                  ( Mock.subOverload
                      (Mock.sortInjectionSubSubToSub Mock.aSubSubsort)
                  )
              )
              []
          , doesn'tMatch
              "overload vs other constructor"
              (Mock.topOverload (Mock.sortInjectionOtherToTop Mock.aOtherSort))
              (Mock.sortInjectionOtherToTop Mock.aOtherSort)
          , doesn'tMatch
              "overload, both sides, not unifiable"
              ( Mock.sortInjectionOtherToOtherTop
                  ( Mock.otherOverload
                      (Mock.sortInjectionSubSubToOther Mock.aSubSubsort)
                  )
              )
              ( Mock.sortInjectionSubToOtherTop
                  ( Mock.subOverload
                      (Mock.sortInjectionSubSubToSub Mock.aSubSubsort)
                  )
              )
          ]
      ]
  
  xInt, yInt, zInt, mMap, nMap :: ElementVariable RewritingVariableName
  mMap = configElementVariableFromId (testId "mMap") Mock.mapSort
  nMap = configElementVariableFromId (testId "nMap") Mock.mapSort
  xInt = configElementVariableFromId (testId "xInt") Mock.intSort
  yInt = configElementVariableFromId (testId "yInt") Mock.intSort
  zInt = configElementVariableFromId (testId "zInt") Mock.intSort
  
  mkInt :: Integer -> TermLike variable
  mkInt = Mock.builtinInt
  
  mkMap ::
      [(TermLike RewritingVariableName, TermLike RewritingVariableName)] ->
      [TermLike RewritingVariableName] ->
      TermLike RewritingVariableName
  mkMap = Mock.framedMap
  
  matchDefinition ::
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      IO MatchResult
  matchDefinition = match
  
  matchSimplification ::
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      IO MatchResult
  matchSimplification = matchDefinition
  
  type MatchResult =
      Either
          Text
          ( Predicate RewritingVariableName
          , Map.Map
              (SomeVariableName RewritingVariableName)
              (TermLike RewritingVariableName)
          )
  
  mkMatchResult ::
      ( Predicate RewritingVariableName
      , Map
          (SomeVariable RewritingVariableName)
          (TermLike RewritingVariableName)
      ) ->
      MatchResult
  mkMatchResult (predicate, substitution) =
      Right (predicate, Map.mapKeys variableName substitution)
  
  match ::
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      IO MatchResult
  match first second =
      testRunSimplifier Mock.env matchResult
    where
      matchResult :: Simplifier MatchResult
      matchResult = patternMatch SideCondition.top first second
  
  withMatch ::
      (MatchResult -> Assertion) ->
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      TestTree
  withMatch check comment term1 term2 =
      testCase comment $ do
          actual <- match term1 term2
          check actual
  
  doesn'tMatch ::
      HasCallStack =>
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      TestTree
  doesn'tMatch = withMatch (assertBool "" . isLeft)
  
  type MatchSubstitution =
      [(SomeVariable RewritingVariableName, TermLike RewritingVariableName)]
  
  matches ::
      HasCallStack =>
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      MatchSubstitution ->
      TestTree
  matches comment term1 term2 substs =
      matchesAux
          comment
          term1
          term2
          (mkMatchResult (makeTruePredicate, Map.fromList substs))
  
  -- Matches one of the expected results
  matchesMulti ::
      HasCallStack =>
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      [MatchSubstitution] ->
      TestTree
  matchesMulti comment term1 term2 substs =
      matchesAuxMulti
          comment
          term1
          term2
          (mkMatchResult' <$> substs)
    where
      mkMatchResult' subst =
          mkMatchResult (makeTruePredicate, Map.fromList subst)
  
  matchesP ::
      HasCallStack =>
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      Predicate RewritingVariableName ->
      MatchSubstitution ->
      TestTree
  matchesP comment term1 term2 predicate substs =
      matchesAux
          comment
          term1
          term2
          (mkMatchResult (predicate, Map.fromList substs))
  
  matchesAux ::
      HasCallStack =>
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      MatchResult ->
      TestTree
  matchesAux comment term1 term2 expect =
      withMatch check comment term1 term2
    where
      check actual = assertEqual "" expect actual
  
  matchesAuxMulti ::
      HasCallStack =>
      TestName ->
      TermLike RewritingVariableName ->
      TermLike RewritingVariableName ->
      [MatchResult] ->
      TestTree
  matchesAuxMulti comment term1 term2 expect =
      withMatch check comment term1 term2
    where
      check actual =
          assertBool
              "Is one of expected results."
              (actual `elem` expect)
  