-- | Symantic for 'Bounded'.
module Language.Symantic.Lib.Bounded where
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
-import Prelude as Bounded (Bounded)
+import Prelude (Bounded)
import Prelude hiding (Bounded(..))
-import qualified Data.Function as Fun
import qualified Prelude as Bounded
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0)
-- * Class 'Sym_Bounded'
+type instance Sym Bounded = Sym_Bounded
class Sym_Bounded term where
minBound :: Bounded a => term a
maxBound :: Bounded a => term a
- default minBound :: (Trans t term, Bounded a) => t term a
- default maxBound :: (Trans t term, Bounded a) => t term a
- minBound = trans_lift minBound
- maxBound = trans_lift maxBound
-
-type instance Sym_of_Iface (Proxy Bounded) = Sym_Bounded
-type instance TyConsts_of_Iface (Proxy Bounded) = Proxy Bounded ': TyConsts_imported_by (Proxy Bounded)
-type instance TyConsts_imported_by (Proxy Bounded) = '[]
-
-instance Sym_Bounded HostI where
- minBound = HostI Bounded.minBound
- maxBound = HostI Bounded.maxBound
-instance Sym_Bounded TextI where
- minBound = textI0 "minBound"
- maxBound = textI0 "maxBound"
-instance (Sym_Bounded r1, Sym_Bounded r2) => Sym_Bounded (DupI r1 r2) where
- minBound = dupI0 @Sym_Bounded minBound
- maxBound = dupI0 @Sym_Bounded maxBound
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Bounded
- ) => Read_TyNameR TyName cs (Proxy Bounded ': rs) where
- read_TyNameR _cs (TyName "Bounded") k = k (ty @Bounded)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Bounded ': cs) where
- show_TyConst TyConstZ{} = "Bounded"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance Proj_TyConC cs (Proxy Bounded)
-data instance TokenT meta (ts::[*]) (Proxy Bounded)
- = Token_Term_Bounded_minBound (EToken meta '[Proxy Token_Type])
- | Token_Term_Bounded_maxBound (EToken meta '[Proxy Token_Type])
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Bounded))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Bounded))
-
-instance -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs Bounded
- , Proj_TyCon cs
- , Compile cs is
- ) => CompileI cs is (Proxy Bounded) where
- compileI tok _ctx k =
- case tok of
- Token_Term_Bounded_minBound tok_ty_a -> bound minBound tok_ty_a
- Token_Term_Bounded_maxBound tok_ty_a -> bound maxBound tok_ty_a
- where
- bound (bnd::forall term a. (Sym_Bounded term, Bounded a) => term a) tok_ty_a =
- -- minBound :: Bounded a => a
- -- maxBound :: Bounded a => a
- compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
- check_TyCon (At (Just tok_ty_a) (ty @Bounded :$ ty_a)) $ \TyCon ->
- k ty_a $ Term $ Fun.const bnd
-instance -- TokenizeT
- Inj_Token meta ts Bounded =>
- TokenizeT meta ts (Proxy Bounded) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ (TeName "minBound",) ProTok_Term
- { protok_term = \meta -> ProTokPi $ \a ->
- ProTokTe $ inj_EToken meta $ Token_Term_Bounded_minBound a
- , protok_fixity = infixN5
- }
- , (TeName "maxBound",) ProTok_Term
- { protok_term = \meta -> ProTokPi $ \a ->
- ProTokTe $ inj_EToken meta $ Token_Term_Bounded_maxBound a
- , protok_fixity = infixN5
- }
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Bounded) g
+ default minBound :: Sym_Bounded (UnT term) => Trans term => Bounded a => term a
+ default maxBound :: Sym_Bounded (UnT term) => Trans term => Bounded a => term a
+ minBound = trans minBound
+ maxBound = trans maxBound
+
+-- Interpreting
+instance Sym_Bounded Eval where
+ minBound = Eval Bounded.minBound
+ maxBound = Eval Bounded.maxBound
+instance Sym_Bounded View where
+ minBound = view0 "minBound"
+ maxBound = view0 "maxBound"
+instance (Sym_Bounded r1, Sym_Bounded r2) => Sym_Bounded (Dup r1 r2) where
+ minBound = dup0 @Sym_Bounded minBound
+ maxBound = dup0 @Sym_Bounded maxBound
+
+-- Transforming
+instance (Sym_Lambda term, Sym_Bounded term) => Sym_Bounded (BetaT term)
+
+-- Typing
+instance NameTyOf Bounded where
+ nameTyOf _c = ["Bounded"] `Mod` "Bounded"
+instance FixityOf Bounded
+instance ClassInstancesFor Bounded
+instance TypeInstancesFor Bounded
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Bounded
+instance (Source src, SymInj ss Bounded) => ModuleFor src ss Bounded where
+ moduleFor = ["Bounded"] `moduleWhere`
+ [ "minBound" := teBounded_minBound
+ , "maxBound" := teBounded_maxBound
+ ]
+
+-- ** 'Type's
+tyBounded :: Source src => Type src vs a -> Type src vs (Bounded a)
+tyBounded a = tyConstLen @(K Bounded) @Bounded (lenVars a) `tyApp` a
+
+-- ** 'Term's
+teBounded_minBound, teBounded_maxBound :: TermDef Bounded '[Proxy a] (Bounded a #> a)
+teBounded_minBound = Term (tyBounded a0) a0 $ teSym @Bounded $ minBound
+teBounded_maxBound = Term (tyBounded a0) a0 $ teSym @Bounded $ maxBound
sourcephile / git / haskell / symantic.git / blobdiff