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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Bounded'.
   4 module Language.Symantic.Lib.Bounded where
   5
   6 import Data.Proxy
   7 import Data.Type.Equality ((:~:)(Refl))
   8 import Prelude as Bounded (Bounded)
   9 import Prelude hiding (Bounded(..))
  10 import qualified Data.Function as Fun
  11 import qualified Prelude as Bounded
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming
  18
  19 -- * Class 'Sym_Bounded'
  20 class Sym_Bounded term where
  21         minBound :: Bounded a => term a
  22         maxBound :: Bounded a => term a
  23         default minBound :: (Trans t term, Bounded a) => t term a
  24         default maxBound :: (Trans t term, Bounded a) => t term a
  25         minBound = trans_lift minBound
  26         maxBound = trans_lift maxBound
  27
  28 type instance Sym_of_Iface (Proxy Bounded) = Sym_Bounded
  29 type instance TyConsts_of_Iface (Proxy Bounded) = Proxy Bounded ': TyConsts_imported_by (Proxy Bounded)
  30 type instance TyConsts_imported_by (Proxy Bounded) = '[]
  31
  32 instance Sym_Bounded HostI where
  33         minBound = HostI Bounded.minBound
  34         maxBound = HostI Bounded.maxBound
  35 instance Sym_Bounded TextI where
  36         minBound = textI0 "minBound"
  37         maxBound = textI0 "maxBound"
  38 instance (Sym_Bounded r1, Sym_Bounded r2) => Sym_Bounded (DupI r1 r2) where
  39         minBound = dupI0 @Sym_Bounded minBound
  40         maxBound = dupI0 @Sym_Bounded maxBound
  41
  42 instance
  43  ( Read_TyNameR TyName cs rs
  44  , Inj_TyConst cs Bounded
  45  ) => Read_TyNameR TyName cs (Proxy Bounded ': rs) where
  46         read_TyNameR _cs (TyName "Bounded") k = k (ty @Bounded)
  47         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  48 instance Show_TyConst cs => Show_TyConst (Proxy Bounded ': cs) where
  49         show_TyConst TyConstZ{} = "Bounded"
  50         show_TyConst (TyConstS c) = show_TyConst c
  51
  52 instance Proj_TyConC cs (Proxy Bounded)
  53 data instance TokenT meta (ts::[*]) (Proxy Bounded)
  54  = Token_Term_Bounded_minBound (EToken meta '[Proxy Token_Type])
  55  | Token_Term_Bounded_maxBound (EToken meta '[Proxy Token_Type])
  56 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Bounded))
  57 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Bounded))
  58
  59 instance -- CompileI
  60  ( Read_TyName TyName cs
  61  , Inj_TyConst        cs Bounded
  62  , Proj_TyCon         cs
  63  , Compile cs is
  64  ) => CompileI cs is (Proxy Bounded) where
  65         compileI tok _ctx k =
  66                 case tok of
  67                  Token_Term_Bounded_minBound tok_ty_a -> bound minBound tok_ty_a
  68                  Token_Term_Bounded_maxBound tok_ty_a -> bound maxBound tok_ty_a
  69                 where
  70                 bound (bnd::forall term a. (Sym_Bounded term, Bounded a) => term a) tok_ty_a =
  71                  -- minBound :: Bounded a => a
  72                  -- maxBound :: Bounded a => a
  73                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
  74                         check_Kind
  75                          (At Nothing SKiType)
  76                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  77                         check_TyCon (At (Just tok_ty_a) (ty @Bounded :$ ty_a)) $ \TyCon ->
  78                         k ty_a $ Term $ Fun.const bnd
  79 instance -- TokenizeT
  80  Inj_Token meta ts Bounded =>
  81  TokenizeT meta ts (Proxy Bounded) where
  82         tokenizeT _t = mempty
  83          { tokenizers_infix = tokenizeTMod []
  84                  [ (TeName "minBound",) ProTok_Term
  85                          { protok_term = \meta -> ProTokPi $ \a ->
  86                                 ProTok $ inj_EToken meta $ Token_Term_Bounded_minBound a
  87                          , protok_fixity = infixN5
  88                          }
  89                  , (TeName "maxBound",) ProTok_Term
  90                          { protok_term = \meta -> ProTokPi $ \a ->
  91                                 ProTok $ inj_EToken meta $ Token_Term_Bounded_maxBound a
  92                          , protok_fixity = infixN5
  93                          }
  94                  ]
  95          }
  96 instance Gram_Term_AtomsT meta ts (Proxy Bounded) g