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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
   4 -- | Symantic for 'Integer'.
   5 module Language.Symantic.Lib.Integer where
   6
   7 import Data.Proxy
   8 import Data.Type.Equality ((:~:)(Refl))
   9 import qualified Data.Text as Text
  10
  11 import Language.Symantic.Parsing
  12 import Language.Symantic.Typing
  13 import Language.Symantic.Compiling
  14 import Language.Symantic.Interpreting
  15 import Language.Symantic.Transforming
  16 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
  17
  18 -- * Class 'Sym_Integer'
  19 class Sym_Integer term where
  20         integer :: Integer -> term Integer
  21         default integer :: Trans t term => Integer -> t term Integer
  22         integer = trans_lift . integer
  23
  24 type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
  25 type instance TyConsts_of_Iface (Proxy Integer) = Proxy Integer ': TyConsts_imported_by (Proxy Integer)
  26 type instance TyConsts_imported_by (Proxy Integer) =
  27  [ Proxy Enum
  28  , Proxy Eq
  29  , Proxy Integral
  30  , Proxy Num
  31  , Proxy Ord
  32  , Proxy Real
  33  , Proxy Show
  34  ]
  35
  36 instance Sym_Integer HostI where
  37         integer = HostI
  38 instance Sym_Integer TextI where
  39         integer a = TextI $ \_p _v ->
  40                 Text.pack (show a)
  41 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
  42         integer x = integer x `DupI` integer x
  43
  44 instance
  45  ( Read_TyNameR TyName cs rs
  46  , Inj_TyConst cs Integer
  47  ) => Read_TyNameR TyName cs (Proxy Integer ': rs) where
  48         read_TyNameR _cs (TyName "Integer") k = k (ty @Integer)
  49         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  50 instance Show_TyConst cs => Show_TyConst (Proxy Integer ': cs) where
  51         show_TyConst TyConstZ{} = "Integer"
  52         show_TyConst (TyConstS c) = show_TyConst c
  53
  54 instance Proj_TyFamC cs TyFam_MonoElement Integer
  55
  56 instance -- Proj_TyConC
  57  ( Proj_TyConst cs Integer
  58  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Integer))
  59  ) => Proj_TyConC cs (Proxy Integer) where
  60         proj_TyConC _ (TyConst q :$ TyConst c)
  61          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
  62          , Just Refl <- proj_TyConst c (Proxy @Integer)
  63          = case () of
  64                  _ | Just Refl <- proj_TyConst q (Proxy @Enum)     -> Just TyCon
  65                    | Just Refl <- proj_TyConst q (Proxy @Eq)       -> Just TyCon
  66                    | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
  67                    | Just Refl <- proj_TyConst q (Proxy @Num)      -> Just TyCon
  68                    | Just Refl <- proj_TyConst q (Proxy @Ord)      -> Just TyCon
  69                    | Just Refl <- proj_TyConst q (Proxy @Real)     -> Just TyCon
  70                    | Just Refl <- proj_TyConst q (Proxy @Show)     -> Just TyCon
  71                  _ -> Nothing
  72         proj_TyConC _c _q = Nothing
  73 data instance TokenT meta (ts::[*]) (Proxy Integer)
  74  = Token_Term_Integer Integer
  75 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
  76 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))
  77
  78 instance -- CompileI
  79  Inj_TyConst cs Integer =>
  80  CompileI cs is (Proxy Integer) where
  81         compileI tok _ctx k =
  82                 case tok of
  83                  Token_Term_Integer i -> k (ty @Integer) $ Term $ \_c -> integer i
  84 instance -- TokenizeT
  85  -- Inj_Token meta ts Integer =>
  86  TokenizeT meta ts (Proxy Integer)
  87 instance -- Gram_Term_AtomsT
  88  ( Alt g
  89  , Alter g
  90  , Gram_Rule g
  91  , Gram_Lexer g
  92  , Gram_Meta meta g
  93  , Inj_Token meta ts Integer
  94  ) => Gram_Term_AtomsT meta ts (Proxy Integer) g where
  95         gs_term_atomsT _t =
  96          [ rule "term_integer" $
  97                 lexeme $ metaG $
  98                 (\i meta -> ProTokTe $ inj_EToken meta $ Token_Term_Integer $ read i)
  99                  <$> some (choice $ char <$> ['0'..'9'])
 100          ]