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

import Prelude (Enum)
import Prelude hiding (Enum(..))
import qualified Prelude

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

-- * Class 'Sym_Enum'
type instance Sym Enum = Sym_Enum
class Sym_Enum term where
	toEnum   :: Enum a => term Int -> term a
	fromEnum :: Enum a => term a -> term Int
	succ     :: Enum a => term a -> term a
	pred     :: Enum a => term a -> term a
	
	default succ     :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a
	default pred     :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a
	default toEnum   :: Sym_Enum (UnT term) => Trans term => Enum a => term Int -> term a
	default fromEnum :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term Int
	
	toEnum   = trans1 toEnum
	fromEnum = trans1 fromEnum
	succ     = trans1 succ
	pred     = trans1 pred

-- Interpreting
instance Sym_Enum Eval where
	toEnum   = eval1 Prelude.toEnum
	fromEnum = eval1 Prelude.fromEnum
	succ     = eval1 Prelude.succ
	pred     = eval1 Prelude.pred
instance Sym_Enum View where
	toEnum   = view1 "toEnum"
	fromEnum = view1 "fromEnum"
	succ     = view1 "succ"
	pred     = view1 "pred"
instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (Dup r1 r2) where
	toEnum   = dup1 @Sym_Enum toEnum
	fromEnum = dup1 @Sym_Enum fromEnum
	succ     = dup1 @Sym_Enum succ
	pred     = dup1 @Sym_Enum pred

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

-- Typing
instance NameTyOf Enum where
	nameTyOf _c = ["Enum"] `Mod` "Enum"
instance FixityOf Enum
instance ClassInstancesFor Enum
instance TypeInstancesFor Enum

-- Compiling
instance Gram_Term_AtomsFor src ss g Enum
instance (Source src, SymInj ss Enum) => ModuleFor src ss Enum where
	moduleFor = ["Enum"] `moduleWhere`
	 [ "succ"     := teEnum_succ
	 , "pred"     := teEnum_pred
	 , "toEnum"   := teEnum_toEnum
	 , "fromEnum" := teEnum_fromEnum
	 ]

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

-- ** 'Term's
teEnum_toEnum :: TermDef Enum '[Proxy a] (Enum a #> (Int -> a))
teEnum_toEnum = Term (tyEnum a0) (tyInt ~> a0) $ teSym @Enum $ lam1 toEnum

teEnum_fromEnum :: TermDef Enum '[Proxy a] (Enum a #> (a -> Int))
teEnum_fromEnum = Term (tyEnum a0) (a0 ~> tyInt) $ teSym @Enum $ lam1 fromEnum

teEnum_succ, teEnum_pred :: TermDef Enum '[Proxy a] (Enum a #> (a -> a))
teEnum_succ = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 succ
teEnum_pred = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 pred