symantic-lib/Language/Symantic/Lib/Enum.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Enum'.
   4 module Language.Symantic.Lib.Enum where
   5
   6 import Control.Monad (liftM)
   7 import Data.Proxy
   8 import Data.Type.Equality ((:~:)(Refl))
   9 import Prelude (Enum)
  10 import Prelude hiding (Enum(..))
  11 import qualified Data.Function as Fun
  12 import qualified Prelude
  13
  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
  20
  21 -- * Class 'Sym_Enum'
  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
  27
  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
  32
  33         toEnum   = trans_map1 toEnum
  34         fromEnum = trans_map1 fromEnum
  35         succ     = trans_map1 succ
  36         pred     = trans_map1 pred
  37
  38 type instance Sym_of_Iface (Proxy Enum) = Sym_Enum
  39 type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_imported_by (Proxy Enum)
  40 type instance TyConsts_imported_by (Proxy Enum) =
  41  '[ Proxy Int
  42  ]
  43
  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"
  52         succ     = textI1 "succ"
  53         pred     = textI1 "pred"
  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
  59
  60 instance
  61  ( Read_TyNameR TyName cs rs
  62  , Inj_TyConst cs Enum
  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
  69
  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))
  78
  79 instance -- CompileI
  80  ( Read_TyName TyName cs
  81  , Inj_TyConst        cs Enum
  82  , Inj_TyConst        cs (->)
  83  , Inj_TyConst        cs Int
  84  , Proj_TyCon         cs
  85  , Compile cs is
  86  ) => CompileI cs is (Proxy Enum) where
  87         compileI tok ctx k =
  88                 case tok of
  89                  Token_Term_Enum_toEnum tok_ty_a ->
  90                         -- toEnum :: Enum a => Int -> a
  91                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
  92                         check_Kind
  93                          (At Nothing SKiType)
  94                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  95                         check_TyCon (At (Just tok_ty_a) (ty @Enum :$ ty_a)) $ \TyCon ->
  96                         k (ty @Int ~> ty_a) $ Term $
  97                                 Fun.const $ lam toEnum
  98                  Token_Term_Enum_fromEnum tok_a ->
  99                         -- fromEnum :: Enum a => a -> Int
 100                         compile tok_a ctx $ \ty_a (Term a) ->
 101                         check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
 102                         k (ty @Int) $ Term $
 103                                 \c -> fromEnum (a c)
 104                  Token_Term_Enum_succ tok_a -> op1_from tok_a succ
 105                  Token_Term_Enum_pred tok_a -> op1_from tok_a pred
 106                 where
 107                 op1_from tok_a
 108                  (op::forall term a. (Sym_Enum term, Enum a)
 109                          => term a -> term a) =
 110                  -- succ :: Enum a => a -> a
 111                  -- pred :: Enum a => a -> a
 112                         compile tok_a ctx $ \ty_a (Term x) ->
 113                         check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
 114                         k ty_a $ Term $
 115                          \c -> op (x c)
 116 instance -- TokenizeT
 117  Inj_Token meta ts Enum =>
 118  TokenizeT meta ts (Proxy Enum) where
 119         tokenizeT _t = mempty
 120          { tokenizers_infix = tokenizeTMod []
 121                  [ tokenize1 "succ" infixN5 Token_Term_Enum_succ
 122                  , tokenize1 "pred" infixN5 Token_Term_Enum_pred
 123                  , (TeName "toEnum",) ProTok_Term
 124                          { protok_term = \meta -> ProTokPi $ \a ->
 125                                 ProTokTe $ inj_EToken meta $ Token_Term_Enum_toEnum a
 126                          , protok_fixity = infixN5
 127                          }
 128                  , tokenize1 "fromEnum" infixN5 Token_Term_Enum_fromEnum
 129                  ]
 130          }
 131 instance Gram_Term_AtomsT meta ts (Proxy Enum) g