{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Semigroup'. module Language.Symantic.Lib.Semigroup where import Data.Semigroup (Semigroup) 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