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 qualified Data.Function as Fun
   7 import Prelude as Bounded (Bounded)
   8 import qualified Prelude as Bounded
   9 import Data.Proxy
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Prelude hiding (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 Bounded
  30 type instance TyConsts_imported_by 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 instance -- CompileI
  59  ( Read_TyName TyName cs
  60  , Inj_TyConst        cs Bounded
  61  , Proj_TyCon         cs
  62  , Compile cs is
  63  ) => CompileI cs is (Proxy Bounded) where
  64         compileI tok _ctx k =
  65                 case tok of
  66                  Token_Term_Bounded_minBound tok_ty_a -> bound minBound tok_ty_a
  67                  Token_Term_Bounded_maxBound tok_ty_a -> bound maxBound tok_ty_a
  68                 where
  69                 bound (bnd::forall term a. (Sym_Bounded term, Bounded a) => term a) tok_ty_a =
  70                  -- minBound :: Bounded a => a
  71                  -- maxBound :: Bounded a => a
  72                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
  73                         check_Kind
  74                          (At Nothing SKiType)
  75                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  76                         check_TyCon (At (Just tok_ty_a) (ty @Bounded :$ ty_a)) $ \TyCon ->
  77                         k ty_a $ TermO $ Fun.const bnd
  78 instance -- TokenizeT
  79  Inj_Token meta ts Bounded =>
  80  TokenizeT meta ts (Proxy Bounded) where
  81         tokenizeT _t = mempty
  82          { tokenizers_infix = tokenizeTMod []
  83                  [ (TeName "minBound",) ProTok_Term
  84                          { protok_term = \meta -> ProTokPi $ \a ->
  85                                 ProTok $ inj_EToken meta $ Token_Term_Bounded_minBound a
  86                          , protok_fixity = infixN5
  87                          }
  88                  , (TeName "maxBound",) ProTok_Term
  89                          { protok_term = \meta -> ProTokPi $ \a ->
  90                                 ProTok $ inj_EToken meta $ Token_Term_Bounded_maxBound a
  91                          , protok_fixity = infixN5
  92                          }
  93                  ]
  94          }
  95 instance Gram_Term_AtomsT meta ts (Proxy Bounded) g