1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Enum'.
4 module Language.Symantic.Lib.Enum where
6 import Control.Monad (liftM)
7 import qualified Data.Function as Fun
9 import Data.Type.Equality ((:~:)(Refl))
10 import qualified Prelude
11 import Prelude hiding (Enum(..))
14 import Language.Symantic.Parsing
15 import Language.Symantic.Typing
16 import Language.Symantic.Compiling
17 import Language.Symantic.Interpreting
18 import Language.Symantic.Transforming
19 import Language.Symantic.Lib.Lambda
22 class Sym_Enum term where
23 toEnum :: Enum a => term Int -> term a
24 fromEnum :: Enum a => term a -> term Int
25 succ :: Enum a => term a -> term a
26 pred :: Enum a => term a -> term a
28 default succ :: (Trans t term, Enum a) => t term a -> t term a
29 default pred :: (Trans t term, Enum a) => t term a -> t term a
30 default toEnum :: (Trans t term, Enum a) => t term Int -> t term a
31 default fromEnum :: (Trans t term, Enum a) => t term a -> t term Int
33 toEnum = trans_map1 toEnum
34 fromEnum = trans_map1 fromEnum
35 succ = trans_map1 succ
36 pred = trans_map1 pred
38 type instance Sym_of_Iface (Proxy Enum) = Sym_Enum
39 type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_imported_by Enum
40 type instance TyConsts_imported_by Enum =
44 instance Sym_Enum HostI where
45 toEnum = liftM Prelude.toEnum
46 fromEnum = liftM Prelude.fromEnum
47 succ = liftM Prelude.succ
48 pred = liftM Prelude.pred
49 instance Sym_Enum TextI where
50 toEnum = textI1 "toEnum"
51 fromEnum = textI1 "fromEnum"
54 instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (DupI r1 r2) where
55 toEnum = dupI1 @Sym_Enum toEnum
56 fromEnum = dupI1 @Sym_Enum fromEnum
57 succ = dupI1 @Sym_Enum succ
58 pred = dupI1 @Sym_Enum pred
61 ( Read_TyNameR TyName cs rs
63 ) => Read_TyNameR TyName cs (Proxy Enum ': rs) where
64 read_TyNameR _cs (TyName "Enum") k = k (ty @Enum)
65 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
66 instance Show_TyConst cs => Show_TyConst (Proxy Enum ': cs) where
67 show_TyConst TyConstZ{} = "Enum"
68 show_TyConst (TyConstS c) = show_TyConst c
70 instance Proj_TyConC cs (Proxy Enum)
71 data instance TokenT meta (ts::[*]) (Proxy Enum)
72 = Token_Term_Enum_fromEnum (EToken meta ts)
73 | Token_Term_Enum_toEnum (EToken meta '[Proxy Token_Type])
74 | Token_Term_Enum_succ (EToken meta ts)
75 | Token_Term_Enum_pred (EToken meta ts)
76 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Enum))
77 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Enum))
79 ( Read_TyName TyName cs
85 ) => CompileI cs is (Proxy Enum) where
88 Token_Term_Enum_toEnum tok_ty_a ->
89 -- toEnum :: Enum a => Int -> a
90 compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
93 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
94 check_TyCon (At (Just tok_ty_a) (ty @Enum :$ ty_a)) $ \TyCon ->
95 k (ty @Int ~> ty_a) $ TermO $
96 Fun.const $ lam toEnum
97 Token_Term_Enum_fromEnum tok_a ->
98 -- fromEnum :: Enum a => a -> Int
99 compileO tok_a ctx $ \ty_a (TermO a) ->
100 check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
101 k (ty @Int) $ TermO $
103 Token_Term_Enum_succ tok_a -> op1_from tok_a succ
104 Token_Term_Enum_pred tok_a -> op1_from tok_a pred
107 (op::forall term a. (Sym_Enum term, Enum a)
108 => term a -> term a) =
109 -- succ :: Enum a => a -> a
110 -- pred :: Enum a => a -> a
111 compileO tok_a ctx $ \ty_a (TermO x) ->
112 check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
115 instance -- TokenizeT
116 Inj_Token meta ts Enum =>
117 TokenizeT meta ts (Proxy Enum) where
118 tokenizeT _t = mempty
119 { tokenizers_infix = tokenizeTMod []
120 [ tokenize1 "succ" infixN5 Token_Term_Enum_succ
121 , tokenize1 "pred" infixN5 Token_Term_Enum_pred
122 , (TeName "toEnum",) ProTok_Term
123 { protok_term = \meta -> ProTokPi $ \a ->
124 ProTok $ inj_EToken meta $ Token_Term_Enum_toEnum a
125 , protok_fixity = infixN5
127 , tokenize1 "fromEnum" infixN5 Token_Term_Enum_fromEnum
130 instance Gram_Term_AtomsT meta ts (Proxy Enum) g