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 qualified Data.Text as Text
   9 import Data.Type.Equality ((:~:)(Refl))
  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
  17 -- * Class 'Sym_Integer'
  18 class Sym_Integer term where
  19         integer :: Integer -> term Integer
  20         default integer :: Trans t term => Integer -> t term Integer
  21         integer = trans_lift . integer
  22
  23 type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
  24 type instance Consts_of_Iface (Proxy Integer) = Proxy Integer ': Consts_imported_by Integer
  25 type instance Consts_imported_by Integer =
  26  [ Proxy Enum
  27  , Proxy Eq
  28  , Proxy Integral
  29  , Proxy Num
  30  , Proxy Ord
  31  , Proxy Real
  32  , Proxy Show
  33  ]
  34
  35 instance Sym_Integer HostI where
  36         integer = HostI
  37 instance Sym_Integer TextI where
  38         integer a = TextI $ \_p _v ->
  39                 Text.pack (show a)
  40 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
  41         integer x = integer x `DupI` integer x
  42
  43 instance
  44  ( Read_TypeNameR Type_Name cs rs
  45  , Inj_Const cs Integer
  46  ) => Read_TypeNameR Type_Name cs (Proxy Integer ': rs) where
  47         read_typenameR _cs (Type_Name "Integer") k = k (ty @Integer)
  48         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  49 instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
  50         show_const ConstZ{} = "Integer"
  51         show_const (ConstS c) = show_const c
  52
  53 instance -- Proj_ConC
  54  ( Proj_Const cs Integer
  55  , Proj_Consts cs (Consts_imported_by Integer)
  56  ) => Proj_ConC cs (Proxy Integer) where
  57         proj_conC _ (TyConst q :$ TyConst c)
  58          | Just Refl <- eq_skind (kind_of_const c) SKiType
  59          , Just Refl <- proj_const c (Proxy @Integer)
  60          = case () of
  61                  _ | Just Refl <- proj_const q (Proxy @Enum)     -> Just Con
  62                    | Just Refl <- proj_const q (Proxy @Eq)       -> Just Con
  63                    | Just Refl <- proj_const q (Proxy @Integral) -> Just Con
  64                    | Just Refl <- proj_const q (Proxy @Num)      -> Just Con
  65                    | Just Refl <- proj_const q (Proxy @Ord)      -> Just Con
  66                    | Just Refl <- proj_const q (Proxy @Real)     -> Just Con
  67                    | Just Refl <- proj_const q (Proxy @Show)     -> Just Con
  68                  _ -> Nothing
  69         proj_conC _c _q = Nothing
  70 data instance TokenT meta (ts::[*]) (Proxy Integer)
  71  = Token_Term_Integer Integer
  72 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
  73 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))
  74 instance -- CompileI
  75  Inj_Const (Consts_of_Ifaces is) Integer =>
  76  CompileI is (Proxy Integer) where
  77         compileI tok _ctx k =
  78                 case tok of
  79                  Token_Term_Integer i -> k (ty @Integer) $ TermO $ \_c -> integer i
  80 instance -- TokenizeT
  81  -- Inj_Token meta ts Integer =>
  82  TokenizeT meta ts (Proxy Integer)
  83 instance -- Gram_Term_AtomsT
  84  ( Alt g
  85  , Alter g
  86  , Gram_Rule g
  87  , Gram_Lexer g
  88  , Gram_Meta meta g
  89  , Inj_Token meta ts Integer
  90  ) => Gram_Term_AtomsT meta ts (Proxy Integer) g where
  91         term_atomsT _t =
  92          [ rule "term_integer" $
  93                 lexeme $ metaG $
  94                 (\i meta -> ProTok $ inj_etoken meta $ Token_Term_Integer $ read i)
  95                  <$> some (choice $ char <$> ['0'..'9'])
  96          ]