{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Negable'.
module Hcompta.LCC.Sym.Negable where

import Language.Symantic
import Language.Symantic.Lib (a0)

import Hcompta.Quantity

-- * Class 'Sym_Negable'
type instance Sym Negable = Sym_Negable
class Sym_Negable term where
	neg :: Negable a => term a -> term a
	default neg :: Sym_Negable (UnT term) => Trans term => Negable a => term a -> term a
	neg = trans1 neg

instance Sym_Negable Eval where
	neg = eval1 quantity_neg
instance Sym_Negable View where
	neg = view1 "neg"
instance (Sym_Negable r1, Sym_Negable r2) => Sym_Negable (Dup r1 r2) where
	neg = dup1 @Sym_Negable neg
instance (Sym_Negable term, Sym_Lambda term) => Sym_Negable (BetaT term)

instance FixityOf Negable
instance ClassInstancesFor Negable
instance TypeInstancesFor Negable
instance Gram_Term_AtomsFor src ss g Negable
instance (Source src, SymInj ss Negable) => ModuleFor src ss Negable where
	moduleFor = ["Negable"] `moduleWhere`
	 [ "-" `withPrefix` 10 := teNegable_neg
	 ]

tyNegable :: Source src => Type src vs a -> Type src vs (Negable a)
tyNegable a = tyConstLen @(K Negable) @Negable (lenVars a) `tyApp` a

teNegable_neg :: TermDef Negable '[Proxy a] (Negable a #> (a -> a))
teNegable_neg = Term (tyNegable a0) (a0 ~> a0) (teSym @Negable (lam1 neg))