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 qualified Data.Function as Fun
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import qualified Prelude
  11 import Prelude hiding (Enum(..))
  12 import Prelude (Enum)
  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 Enum
  40 type instance TyConsts_imported_by 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 instance -- CompileI
  79  ( Read_TyName TyName cs
  80  , Inj_TyConst        cs Enum
  81  , Inj_TyConst        cs (->)
  82  , Inj_TyConst        cs Int
  83  , Proj_TyCon         cs
  84  , Compile cs is
  85  ) => CompileI cs is (Proxy Enum) where
  86         compileI tok ctx k =
  87                 case tok of
  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) ->
  91                         check_Kind
  92                          (At Nothing SKiType)
  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 $
 102                                 \c -> fromEnum (a c)
 103                  Token_Term_Enum_succ tok_a -> op1_from tok_a succ
 104                  Token_Term_Enum_pred tok_a -> op1_from tok_a pred
 105                 where
 106                 op1_from tok_a
 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 ->
 113                         k ty_a $ TermO $
 114                          \c -> op (x c)
 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
 126                          }
 127                  , tokenize1 "fromEnum" infixN5 Token_Term_Enum_fromEnum
 128                  ]
 129          }
 130 instance Gram_Term_AtomsT meta ts (Proxy Enum) g