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

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

import Hcompta.Quantity

-- * Class 'Sym_Subable'
type instance Sym (Proxy Subable) = Sym_Subable
class Sym_Subable term where
	(-) :: Subable a => term a -> term a -> term a; infixl 6 -
	default (-) :: Sym_Subable (UnT term) => Trans term => Subable a => term a -> term a -> term a
	(-) = trans2 (-)

instance Sym_Subable Eval where
	(-) = eval2 quantity_sub
instance Sym_Subable View where
	(-) = viewInfix "-" (infixB SideL 6)
instance (Sym_Subable r1, Sym_Subable r2) => Sym_Subable (Dup r1 r2) where
	(-) = dup2 @Sym_Subable (-)
instance (Sym_Subable term, Sym_Lambda term) => Sym_Subable (BetaT term)

instance FixityOf Subable
instance ClassInstancesFor Subable
instance TypeInstancesFor Subable
instance Gram_Term_AtomsFor src ss g Subable
instance (Source src, Inj_Sym ss Subable) => ModuleFor src ss Subable where
	moduleFor _s = ["Subable"] `moduleWhere`
	 [ "-" `withInfixB` (SideL, 6) := teSubable_sub
	 ]

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

teSubable_sub :: TermDef Subable '[Proxy a] (Subable a #> (a -> a -> a))
teSubable_sub = Term (tySubable a0) (a0 ~> a0 ~> a0) (teSym @Subable (lam2 (-)))