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

import Prelude (Bounded)
import Prelude hiding (Bounded(..))
import qualified Prelude as Bounded

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

-- * Class 'Sym_Bounded'
type instance Sym (Proxy Bounded) = Sym_Bounded
class Sym_Bounded term where
	minBound :: Bounded a => term a
	maxBound :: Bounded a => term a
	default minBound :: Sym_Bounded (UnT term) => Trans term => Bounded a => term a
	default maxBound :: Sym_Bounded (UnT term) => Trans term => Bounded a => term a
	minBound = trans minBound
	maxBound = trans maxBound

-- Interpreting
instance Sym_Bounded Eval where
	minBound = Eval Bounded.minBound
	maxBound = Eval Bounded.maxBound
instance Sym_Bounded View where
	minBound = view0 "minBound"
	maxBound = view0 "maxBound"
instance (Sym_Bounded r1, Sym_Bounded r2) => Sym_Bounded (Dup r1 r2) where
	minBound = dup0 @Sym_Bounded minBound
	maxBound = dup0 @Sym_Bounded maxBound

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

-- Typing
instance FixityOf Bounded
instance ClassInstancesFor Bounded
instance TypeInstancesFor Bounded

-- Compiling
instance Gram_Term_AtomsFor src ss g Bounded
instance (Source src, Inj_Sym ss Bounded) => Module src ss Bounded where
	module_ _s = [] `moduleWhere`
	 [ "minBound" := teBounded_minBound
	 , "maxBound" := teBounded_maxBound
	 ]

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

-- ** 'Term's
teBounded_minBound, teBounded_maxBound :: TermDef Bounded '[Proxy a] (Bounded a #> a)
teBounded_minBound = Term (tyBounded a0) a0 $ teSym @Bounded $ minBound
teBounded_maxBound = Term (tyBounded a0) a0 $ teSym @Bounded $ maxBound