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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   4 -- | Symantic for 'Int'.
   5 module Language.Symantic.Lib.Int 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_Int'
  19 class Sym_Int term where
  20         int :: Int -> term Int
  21         default int :: Trans t term => Int -> t term Int
  22         int = trans_lift . int
  23
  24 type instance Sym_of_Iface (Proxy Int) = Sym_Int
  25 type instance TyConsts_of_Iface (Proxy Int) = Proxy Int ': TyConsts_imported_by (Proxy Int)
  26 type instance TyConsts_imported_by (Proxy Int) =
  27  [ Proxy Bounded
  28  , Proxy Enum
  29  , Proxy Eq
  30  , Proxy Integral
  31  , Proxy Num
  32  , Proxy Ord
  33  , Proxy Real
  34  , Proxy Show
  35  ]
  36
  37 instance Sym_Int HostI where
  38         int = HostI
  39 instance Sym_Int TextI where
  40         int a = TextI $ \_p _v ->
  41                 Text.pack (show a)
  42 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (DupI r1 r2) where
  43         int x = int x `DupI` int x
  44
  45 instance
  46  ( Read_TyNameR TyName cs rs
  47  , Inj_TyConst cs Int
  48  ) => Read_TyNameR TyName cs (Proxy Int ': rs) where
  49         read_TyNameR _cs (TyName "Int") k = k (ty @Int)
  50         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  51 instance Show_TyConst cs => Show_TyConst (Proxy Int ': cs) where
  52         show_TyConst TyConstZ{} = "Int"
  53         show_TyConst (TyConstS c) = show_TyConst c
  54
  55 instance Proj_TyFamC cs TyFam_MonoElement Int
  56
  57 instance -- Proj_TyConC
  58  ( Proj_TyConst cs Int
  59  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Int))
  60  ) => Proj_TyConC cs (Proxy Int) where
  61         proj_TyConC _ (TyConst q :$ TyConst c)
  62          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
  63          , Just Refl <- proj_TyConst c (Proxy @Int)
  64          = case () of
  65                  _ | Just Refl <- proj_TyConst q (Proxy @Bounded)  -> Just TyCon
  66                    | Just Refl <- proj_TyConst q (Proxy @Enum)     -> Just TyCon
  67                    | Just Refl <- proj_TyConst q (Proxy @Eq)       -> Just TyCon
  68                    | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
  69                    | Just Refl <- proj_TyConst q (Proxy @Num)      -> Just TyCon
  70                    | Just Refl <- proj_TyConst q (Proxy @Ord)      -> Just TyCon
  71                    | Just Refl <- proj_TyConst q (Proxy @Real)     -> Just TyCon
  72                    | Just Refl <- proj_TyConst q (Proxy @Show)     -> Just TyCon
  73                  _ -> Nothing
  74         proj_TyConC _c _q = Nothing
  75 data instance TokenT meta (ts::[*]) (Proxy Int)
  76  = Token_Term_Int Int
  77 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Int))
  78 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Int))
  79
  80 instance -- CompileI
  81  Inj_TyConst cs Int =>
  82  CompileI cs is (Proxy Int) where
  83         compileI tok _ctx k =
  84                 case tok of
  85                  Token_Term_Int i -> k (ty @Int) $ TermO $ \_c -> int i
  86 instance TokenizeT meta ts (Proxy Int)
  87 instance Gram_Term_AtomsT meta ts (Proxy Int) g