{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Semigroup'.
module Language.Symantic.Lib.Semigroup where

import Data.Function (($))
import Data.Semigroup (Semigroup)
import Prelude (Integral)
import qualified Data.Semigroup as Semigroup

import Language.Symantic
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.Integral (tyIntegral)

-- * Class 'Sym_Semigroup'
type instance Sym Semigroup = Sym_Semigroup
class Sym_Semigroup term where
        (<>)   :: Semigroup a => term a -> term a -> term a
        stimes :: (Semigroup a, Integral b) => term b -> term a -> term a
        -- sconcat :: NonEmpty a -> a
        default (<>)   :: Sym_Semigroup (UnT term) => Trans term => Semigroup a => term a -> term a -> term a
        default stimes :: Sym_Semigroup (UnT term) => Trans term => Semigroup a => Integral b => term b -> term a -> term a
        (<>)   = trans2 (<>)
        stimes = trans2 stimes

-- Interpreting
instance Sym_Semigroup Eval where
        (<>)   = eval2 (Semigroup.<>)
        stimes = eval2 Semigroup.stimes
instance Sym_Semigroup View where
        (<>)   = viewInfix "-" (infixR 6)
        stimes = view2 "stimes"
instance (Sym_Semigroup r1, Sym_Semigroup r2) => Sym_Semigroup (Dup r1 r2) where
        (<>)   = dup2 @Sym_Semigroup (<>)
        stimes = dup2 @Sym_Semigroup stimes

-- Transforming
instance (Sym_Semigroup term, Sym_Lambda term) => Sym_Semigroup (BetaT term)

-- Typing
instance NameTyOf Semigroup where
        nameTyOf _c = ["Semigroup"] `Mod` "Semigroup"
instance FixityOf Semigroup
instance ClassInstancesFor Semigroup
instance TypeInstancesFor Semigroup

-- Compiling
instance Gram_Term_AtomsFor src ss g Semigroup
instance (Source src, SymInj ss Semigroup) => ModuleFor src ss Semigroup where
        moduleFor = ["Semigroup"] `moduleWhere`
         [ "<>" `withInfixR` 6 := teSemigroup_sappend
         , "stimes" := teSemigroup_stimes
         ]

-- ** 'Type's
tySemigroup :: Source src => Type src vs a -> Type src vs (Semigroup a)
tySemigroup a = tyConstLen @(K Semigroup) @Semigroup (lenVars a) `tyApp` a

-- ** 'Term's
teSemigroup_sappend :: TermDef Semigroup '[Proxy a] (Semigroup a #> (a -> a -> a))
teSemigroup_sappend = Term (tySemigroup a0) (a0 ~> a0 ~> a0) $ teSym @Semigroup $ lam2 (<>)

teSemigroup_stimes :: TermDef Semigroup '[Proxy a, Proxy b] (Semigroup a # Integral b #> (b -> a -> a))
teSemigroup_stimes = Term (tySemigroup a0 # tyIntegral b1) (b1 ~> a0 ~> a0) $ teSym @Semigroup $ lam2 stimes