Cospan.hs

{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Props.Cospan where

import Data.Foldable (toList)
import Data.Maybe (isJust)
import Data.Typeable ((:~:) (..))
import Test.Tasty (TestTree, testGroup)
import Prelude (Bool (..), Maybe (..), pure, zip, ($), (&&), (++), (<$>), (<*>), (||))

import Proarrow.Category.Instance.Cospan (COSPAN (..), Cospan (..))
import Proarrow.Category.Instance.FinSet (FINSET (..), findIso, unFinSet)
import Proarrow.Core (CAT, CategoryOf (..), UN, (//), (\\))

import Proarrow.Testing
  ( GenTotal (..)
  , Some (..)
  , Testable (..)
  , TestableProfunctor
  , TestableType (..)
  , TestingEqShow (..)
  , mapSome
  , pattern GenNonEmpty
  )
import Proarrow.Testing.Laws
import Props.FinSet (eqFinSet)

test :: TestTree
test =
  testGroup
    "Cospan(FinSet)"
    [ testCategory @(COSPAN FINSET)
    , testDagger @(COSPAN FINSET)
    , testMonoidal_ @(COSPAN FINSET)
    , testSymMonoidal_ @(COSPAN FINSET)
    , testClosed_ @(COSPAN FINSET)
    , testStarAutonomous_ @(COSPAN FINSET)
    , testCompactClosed_ @(COSPAN FINSET)
    , testCopyDiscard_ @(COSPAN FINSET)
    , testHypergraph_ @(COSPAN FINSET)
    ]

-- instance (Testable k, HasPushouts k, TestObIsOb k) => Testable (COSPAN k) where
instance Testable (COSPAN FINSET) where
  type TestOb a = Ob a
  showOb @a = showOb @_ @(UN CS a)
  genSome = mapSome CS <$> genSome
  genSomeSmall = mapSome CS <$> genSomeSmall

-- instance (Ob a, Ob b, Testable k, TestObIsOb k) => TestingEqShow (Cospan a (b :: COSPAN k)) where
instance (Ob a, Ob b) => TestingEqShow (Cospan a (b :: COSPAN FINSET)) where
  eqP (Cospan @c1 l1 r1) (Cospan @c2 l2 r2) =
    l1 //
      l2 //
        case eqFinSet @c1 @c2 of
          Just Refl -> do
            eql <- eqP l1 l2
            eqr <- eqP r1 r2
            -- Both legs map *into* the apex, so a relabelling has to satisfy every constraint the
            -- two leg pairs impose at once, which takes an actual search. Span's legs map out, so
            -- it can settle the question by comparing multisets (see "Props.Span").
            let hasIso =
                  isJust
                    ( findIso @(UN FS c1)
                        (zip (toList (unFinSet l1)) (toList (unFinSet l2)) ++ zip (toList (unFinSet r1)) (toList (unFinSet r2)))
                    )
            pure $ (eql && eqr) || hasIso
          Nothing -> pure False
  showP (Cospan @c l r) = "Cospan @(" ++ showOb @_ @c ++ ") (" ++ showP l ++ ") (" ++ showP r ++ ")" \\ l

-- instance (TestOb a, TestOb b, Testable k, TestObIsOb k) => TestableType (Cospan a (b :: COSPAN k)) where
instance (TestOb a, TestOb b) => TestableType (Cospan a (b :: COSPAN FINSET)) where
  gen = GenNonEmpty loop
    where
      loop = do
        Some @c <- genSome @_
        case (gen @(UN CS a ~> c), gen @(UN CS b ~> c)) of
          (GenEmpty _, _) -> loop
          (_, GenEmpty _) -> loop
          (GenNonEmpty l, GenNonEmpty r) -> Cospan <$> l <*> r

instance TestableProfunctor (Cospan :: CAT (COSPAN FINSET))