{-# LANGUAGE Safe #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}

module Logic.Theory.Semigroup (
  type (<>) (),
  (<>),
  type NonEmptyConcat (),
  sconcat,
) where

import Data.List.NonEmpty qualified as NonEmpty
import Data.Semigroup qualified as Semigroup
import Logic.Kernel
import Logic.Theory.Arithmetic
import Logic.Theory.List
import Logic.Theory.Ord

data (<>) aN bN = AppendAxiom
type role (<>) nominal nominal

data NonEmptyConcat aN = NonEmptyConcatAxiom
type role NonEmptyConcat nominal

(<>) :: Semigroup.Semigroup a => aN ::: a -> bN ::: a -> (<>) aN bN ::: a
(<>) (Named x) (Named y) = AppendAxiom ... (x Semigroup.<> y)

sconcat :: Semigroup.Semigroup a => aN ::: [a] / Zero < ListLength aN -> NonEmptyConcat aN ::: a
sconcat (Named xs) = NonEmptyConcatAxiom ... Semigroup.sconcat (NonEmpty.fromList xs)