Language/Symantic/Compiling/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.Compiling.Int 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_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 Consts_of_Iface (Proxy Int) = Proxy Int ': Consts_imported_by Int
  26 type instance Consts_imported_by 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 Const_from Text cs => Const_from Text (Proxy Int ': cs) where
  46         const_from "Int" k = k (ConstZ kind)
  47         const_from s k = const_from s $ k . ConstS
  48 instance Show_Const cs => Show_Const (Proxy Int ': cs) where
  49         show_const ConstZ{} = "Int"
  50         show_const (ConstS c) = show_const c
  51
  52 instance -- Proj_ConC
  53  ( Proj_Const cs Int
  54  , Proj_Consts cs (Consts_imported_by Int)
  55  ) => Proj_ConC cs (Proxy Int) where
  56         proj_conC _ (TyConst q :$ TyConst c)
  57          | Just Refl <- eq_skind (kind_of_const c) SKiType
  58          , Just Refl <- proj_const c (Proxy::Proxy Int)
  59          = case () of
  60                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
  61                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
  62                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
  63                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
  64                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
  65                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
  66                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
  67                    | Just Refl <- proj_const q (Proxy::Proxy Show)     -> Just Con
  68                  _ -> Nothing
  69         proj_conC _c _q = Nothing
  70 data instance TokenT meta (ts::[*]) (Proxy Int)
  71  = Token_Term_Int Int
  72 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Int))
  73 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Int))
  74 instance -- Term_fromI
  75  Inj_Const (Consts_of_Ifaces is) Int =>
  76  Term_fromI is (Proxy Int) where
  77         term_fromI tok _ctx k =
  78                 case tok of
  79                  Token_Term_Int i -> k (ty @Int) $ TermLC $ \_c -> int i