{-# 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 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