{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Enum'. module Language.Symantic.Lib.Enum where import Control.Monad (liftM) import Data.Proxy import Data.Type.Equality ((:~:)(Refl)) import Prelude (Enum) import Prelude hiding (Enum(..)) import qualified Data.Function as Fun import qualified Prelude import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling import Language.Symantic.Interpreting import Language.Symantic.Transforming import Language.Symantic.Lib.Lambda -- * Class '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 :: (Trans t term, Enum a) => t term a -> t term a default pred :: (Trans t term, Enum a) => t term a -> t term a default toEnum :: (Trans t term, Enum a) => t term Int -> t term a default fromEnum :: (Trans t term, Enum a) => t term a -> t term Int toEnum = trans_map1 toEnum fromEnum = trans_map1 fromEnum succ = trans_map1 succ pred = trans_map1 pred type instance Sym_of_Iface (Proxy Enum) = Sym_Enum type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_imported_by (Proxy Enum) type instance TyConsts_imported_by (Proxy Enum) = '[ Proxy Int ] instance Sym_Enum HostI where toEnum = liftM Prelude.toEnum fromEnum = liftM Prelude.fromEnum succ = liftM Prelude.succ pred = liftM Prelude.pred instance Sym_Enum TextI where toEnum = textI1 "toEnum" fromEnum = textI1 "fromEnum" succ = textI1 "succ" pred = textI1 "pred" instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (DupI r1 r2) where toEnum = dupI1 @Sym_Enum toEnum fromEnum = dupI1 @Sym_Enum fromEnum succ = dupI1 @Sym_Enum succ pred = dupI1 @Sym_Enum pred instance ( Read_TyNameR TyName cs rs , Inj_TyConst cs Enum ) => Read_TyNameR TyName cs (Proxy Enum ': rs) where read_TyNameR _cs (TyName "Enum") k = k (ty @Enum) read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k instance Show_TyConst cs => Show_TyConst (Proxy Enum ': cs) where show_TyConst TyConstZ{} = "Enum" show_TyConst (TyConstS c) = show_TyConst c instance Proj_TyConC cs (Proxy Enum) data instance TokenT meta (ts::[*]) (Proxy Enum) = Token_Term_Enum_fromEnum (EToken meta ts) | Token_Term_Enum_toEnum (EToken meta '[Proxy Token_Type]) | Token_Term_Enum_succ (EToken meta ts) | Token_Term_Enum_pred (EToken meta ts) deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Enum)) deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Enum)) instance -- CompileI ( Read_TyName TyName cs , Inj_TyConst cs Enum , Inj_TyConst cs (->) , Inj_TyConst cs Int , Proj_TyCon cs , Compile cs is ) => CompileI cs is (Proxy Enum) where compileI tok ctx k = case tok of Token_Term_Enum_toEnum tok_ty_a -> -- toEnum :: Enum a => Int -> a compile_Type tok_ty_a $ \(ty_a::Type cs a) -> check_Kind (At Nothing SKiType) (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl -> check_TyCon (At (Just tok_ty_a) (ty @Enum :$ ty_a)) $ \TyCon -> k (ty @Int ~> ty_a) $ Term $ Fun.const $ lam toEnum Token_Term_Enum_fromEnum tok_a -> -- fromEnum :: Enum a => a -> Int compile tok_a ctx $ \ty_a (Term a) -> check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon -> k (ty @Int) $ Term $ \c -> fromEnum (a c) Token_Term_Enum_succ tok_a -> op1_from tok_a succ Token_Term_Enum_pred tok_a -> op1_from tok_a pred where op1_from tok_a (op::forall term a. (Sym_Enum term, Enum a) => term a -> term a) = -- succ :: Enum a => a -> a -- pred :: Enum a => a -> a compile tok_a ctx $ \ty_a (Term x) -> check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon -> k ty_a $ Term $ \c -> op (x c) instance -- TokenizeT Inj_Token meta ts Enum => TokenizeT meta ts (Proxy Enum) where tokenizeT _t = mempty { tokenizers_infix = tokenizeTMod [] [ tokenize1 "succ" infixN5 Token_Term_Enum_succ , tokenize1 "pred" infixN5 Token_Term_Enum_pred , (TeName "toEnum",) ProTok_Term { protok_term = \meta -> ProTokPi $ \a -> ProTokTe $ inj_EToken meta $ Token_Term_Enum_toEnum a , protok_fixity = infixN5 } , tokenize1 "fromEnum" infixN5 Token_Term_Enum_fromEnum ] } instance Gram_Term_AtomsT meta ts (Proxy Enum) g