Language/Symantic/Compiling/Integer.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
   4 -- | Symantic for 'Integer'.
   5 module Language.Symantic.Compiling.Integer where
   6
   7 import Data.Proxy
   8 import Data.Text (Text)
   9 import qualified Data.Text as Text
  10 import Data.Type.Equality ((:~:)(Refl))
  11
  12 import Language.Symantic.Parsing
  13 import Language.Symantic.Typing
  14 import Language.Symantic.Compiling.Term
  15 import Language.Symantic.Interpreting
  16 import Language.Symantic.Transforming.Trans
  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 Consts_of_Iface (Proxy Integer) = Proxy Integer ': Consts_imported_by Integer
  26 type instance Consts_imported_by Integer =
  27  [ Proxy Enum
  28  , Proxy Eq
  29  , Proxy Integral
  30  , Proxy Num
  31  , Proxy Ord
  32  , Proxy Real
  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 Const_from Text cs => Const_from Text (Proxy Integer ': cs) where
  44         const_from "Integer" k = k (ConstZ kind)
  45         const_from s k = const_from s $ k . ConstS
  46 instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
  47         show_const ConstZ{} = "Integer"
  48         show_const (ConstS c) = show_const c
  49
  50 instance -- Proj_ConC
  51  ( Proj_Const cs Integer
  52  , Proj_Consts cs (Consts_imported_by Integer)
  53  ) => Proj_ConC cs (Proxy Integer) where
  54         proj_conC _ (TyConst q :$ TyConst c)
  55          | Just Refl <- eq_skind (kind_of_const c) SKiType
  56          , Just Refl <- proj_const c (Proxy::Proxy Integer)
  57          = case () of
  58                  _ | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
  59                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
  60                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
  61                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
  62                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
  63                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
  64                  _ -> Nothing
  65         proj_conC _c _q = Nothing
  66 data instance TokenT meta (ts::[*]) (Proxy Integer)
  67  = Token_Term_Integer Integer
  68 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
  69 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))
  70 instance -- Term_fromI
  71  Inj_Const (Consts_of_Ifaces is) Integer =>
  72  Term_fromI is (Proxy Integer) where
  73         term_fromI tok _ctx k =
  74                 case tok of
  75                  Token_Term_Integer i -> k (ty @Integer) $ TermLC $ \_c -> integer i