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

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

import Hcompta.Quantity as H hiding (zero)
import qualified Hcompta.Quantity as H

-- * Class 'Sym_Zeroable'
type instance Sym Zeroable = Sym_Zeroable
class Sym_Zeroable term where
	zero :: Zeroable a => term a
	default zero :: Sym_Zeroable (UnT term) => Trans term => Zeroable a => term a
	zero = trans zero

instance Sym_Zeroable Eval where
	zero = Eval H.zero
instance Sym_Zeroable View where
	zero = view0 "zero"
instance (Sym_Zeroable r1, Sym_Zeroable r2) => Sym_Zeroable (Dup r1 r2) where
	zero = dup0 @Sym_Zeroable zero
instance (Sym_Zeroable term, Sym_Lambda term) => Sym_Zeroable (BetaT term)

instance NameTyOf Zeroable where
	nameTyOf _c = ["Zeroable"] `Mod` "Zeroable"
instance FixityOf Zeroable
instance ClassInstancesFor Zeroable
instance TypeInstancesFor Zeroable
instance Gram_Term_AtomsFor src ss g Zeroable
instance (Source src, SymInj ss Zeroable) => ModuleFor src ss Zeroable where
	moduleFor = ["Zeroable"] `moduleWhere`
	 [ "zero" := teZeroable_zero
	 ]

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

teZeroable_zero :: TermDef Zeroable '[Proxy a] (Zeroable a #> a)
teZeroable_zero = Term (tyZeroable a0) a0 (teSym @Zeroable zero)