-- | Symantic for 'Enum'.
module Language.Symantic.Lib.Enum where
-import Control.Monad (liftM)
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude (Enum)
import Prelude hiding (Enum(..))
-import qualified Data.Function as Fun
import qualified Prelude
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0)
+import Language.Symantic.Lib.Int (tyInt)
-- * Class 'Sym_Enum'
+type instance Sym Enum = Sym_Enum
class Sym_Enum term where
toEnum :: Enum a => term Int -> term a
fromEnum :: Enum a => term a -> term Int
succ :: Enum a => term a -> term a
pred :: Enum a => term a -> term a
- default succ :: (Trans t term, Enum a) => t term a -> t term a
- default pred :: (Trans t term, Enum a) => t term a -> t term a
- default toEnum :: (Trans t term, Enum a) => t term Int -> t term a
- default fromEnum :: (Trans t term, Enum a) => t term a -> t term Int
+ default succ :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a
+ default pred :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a
+ default toEnum :: Sym_Enum (UnT term) => Trans term => Enum a => term Int -> term a
+ default fromEnum :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term Int
- toEnum = trans_map1 toEnum
- fromEnum = trans_map1 fromEnum
- succ = trans_map1 succ
- pred = trans_map1 pred
+ toEnum = trans1 toEnum
+ fromEnum = trans1 fromEnum
+ succ = trans1 succ
+ pred = trans1 pred
-type instance Sym_of_Iface (Proxy Enum) = Sym_Enum
-type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_imported_by (Proxy Enum)
-type instance TyConsts_imported_by (Proxy Enum) =
- '[ Proxy Int
- ]
+-- Interpreting
+instance Sym_Enum Eval where
+ toEnum = eval1 Prelude.toEnum
+ fromEnum = eval1 Prelude.fromEnum
+ succ = eval1 Prelude.succ
+ pred = eval1 Prelude.pred
+instance Sym_Enum View where
+ toEnum = view1 "toEnum"
+ fromEnum = view1 "fromEnum"
+ succ = view1 "succ"
+ pred = view1 "pred"
+instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (Dup r1 r2) where
+ toEnum = dup1 @Sym_Enum toEnum
+ fromEnum = dup1 @Sym_Enum fromEnum
+ succ = dup1 @Sym_Enum succ
+ pred = dup1 @Sym_Enum pred
-instance Sym_Enum HostI where
- toEnum = liftM Prelude.toEnum
- fromEnum = liftM Prelude.fromEnum
- succ = liftM Prelude.succ
- pred = liftM Prelude.pred
-instance Sym_Enum TextI where
- toEnum = textI1 "toEnum"
- fromEnum = textI1 "fromEnum"
- succ = textI1 "succ"
- pred = textI1 "pred"
-instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (DupI r1 r2) where
- toEnum = dupI1 @Sym_Enum toEnum
- fromEnum = dupI1 @Sym_Enum fromEnum
- succ = dupI1 @Sym_Enum succ
- pred = dupI1 @Sym_Enum pred
+-- Transforming
+instance (Sym_Enum term, Sym_Lambda term) => Sym_Enum (BetaT term)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Enum
- ) => Read_TyNameR TyName cs (Proxy Enum ': rs) where
- read_TyNameR _cs (TyName "Enum") k = k (ty @Enum)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Enum ': cs) where
- show_TyConst TyConstZ{} = "Enum"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Typing
+instance NameTyOf Enum where
+ nameTyOf _c = ["Enum"] `Mod` "Enum"
+instance FixityOf Enum
+instance ClassInstancesFor Enum
+instance TypeInstancesFor Enum
-instance Proj_TyConC cs (Proxy Enum)
-data instance TokenT meta (ts::[*]) (Proxy Enum)
- = Token_Term_Enum_fromEnum (EToken meta ts)
- | Token_Term_Enum_toEnum (EToken meta '[Proxy Token_Type])
- | Token_Term_Enum_succ (EToken meta ts)
- | Token_Term_Enum_pred (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Enum))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Enum))
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Enum
+instance (Source src, SymInj ss Enum) => ModuleFor src ss Enum where
+ moduleFor = ["Enum"] `moduleWhere`
+ [ "succ" := teEnum_succ
+ , "pred" := teEnum_pred
+ , "toEnum" := teEnum_toEnum
+ , "fromEnum" := teEnum_fromEnum
+ ]
-instance -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs Enum
- , Inj_TyConst cs (->)
- , Inj_TyConst cs Int
- , Proj_TyCon cs
- , Compile cs is
- ) => CompileI cs is (Proxy Enum) where
- compileI tok ctx k =
- case tok of
- Token_Term_Enum_toEnum tok_ty_a ->
- -- toEnum :: Enum a => Int -> 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 @Enum :$ ty_a)) $ \TyCon ->
- k (ty @Int ~> ty_a) $ Term $
- Fun.const $ lam toEnum
- Token_Term_Enum_fromEnum tok_a ->
- -- fromEnum :: Enum a => a -> Int
- compile tok_a ctx $ \ty_a (Term a) ->
- check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
- k (ty @Int) $ Term $
- \c -> fromEnum (a c)
- Token_Term_Enum_succ tok_a -> op1_from tok_a succ
- Token_Term_Enum_pred tok_a -> op1_from tok_a pred
- where
- op1_from tok_a
- (op::forall term a. (Sym_Enum term, Enum a)
- => term a -> term a) =
- -- succ :: Enum a => a -> a
- -- pred :: Enum a => a -> a
- compile tok_a ctx $ \ty_a (Term x) ->
- check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
- k ty_a $ Term $
- \c -> op (x c)
-instance -- TokenizeT
- Inj_Token meta ts Enum =>
- TokenizeT meta ts (Proxy Enum) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize1 "succ" infixN5 Token_Term_Enum_succ
- , tokenize1 "pred" infixN5 Token_Term_Enum_pred
- , (TeName "toEnum",) ProTok_Term
- { protok_term = \meta -> ProTokPi $ \a ->
- ProTok $ inj_EToken meta $ Token_Term_Enum_toEnum a
- , protok_fixity = infixN5
- }
- , tokenize1 "fromEnum" infixN5 Token_Term_Enum_fromEnum
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Enum) g
+-- ** 'Type's
+tyEnum :: Source src => Type src vs a -> Type src vs (Enum a)
+tyEnum a = tyConstLen @(K Enum) @Enum (lenVars a) `tyApp` a
+
+-- ** 'Term's
+teEnum_toEnum :: TermDef Enum '[Proxy a] (Enum a #> (Int -> a))
+teEnum_toEnum = Term (tyEnum a0) (tyInt ~> a0) $ teSym @Enum $ lam1 toEnum
+
+teEnum_fromEnum :: TermDef Enum '[Proxy a] (Enum a #> (a -> Int))
+teEnum_fromEnum = Term (tyEnum a0) (a0 ~> tyInt) $ teSym @Enum $ lam1 fromEnum
+
+teEnum_succ, teEnum_pred :: TermDef Enum '[Proxy a] (Enum a #> (a -> a))
+teEnum_succ = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 succ
+teEnum_pred = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 pred
sourcephile / git / haskell / symantic.git / blobdiff