]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Enum.hs
Update to lastest symantic-document
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Enum.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Enum'.
4 module Language.Symantic.Lib.Enum where
5
6 import Prelude (Enum)
7 import Prelude hiding (Enum(..))
8 import qualified Prelude
9
10 import Language.Symantic
11 import Language.Symantic.Lib.Function (a0)
12 import Language.Symantic.Lib.Int (tyInt)
13
14 -- * Class 'Sym_Enum'
15 type instance Sym Enum = Sym_Enum
16 class Sym_Enum term where
17 toEnum :: Enum a => term Int -> term a
18 fromEnum :: Enum a => term a -> term Int
19 succ :: Enum a => term a -> term a
20 pred :: Enum a => term a -> term a
21
22 default succ :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a
23 default pred :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term a
24 default toEnum :: Sym_Enum (UnT term) => Trans term => Enum a => term Int -> term a
25 default fromEnum :: Sym_Enum (UnT term) => Trans term => Enum a => term a -> term Int
26
27 toEnum = trans1 toEnum
28 fromEnum = trans1 fromEnum
29 succ = trans1 succ
30 pred = trans1 pred
31
32 -- Interpreting
33 instance Sym_Enum Eval where
34 toEnum = eval1 Prelude.toEnum
35 fromEnum = eval1 Prelude.fromEnum
36 succ = eval1 Prelude.succ
37 pred = eval1 Prelude.pred
38 instance Sym_Enum View where
39 toEnum = view1 "toEnum"
40 fromEnum = view1 "fromEnum"
41 succ = view1 "succ"
42 pred = view1 "pred"
43 instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (Dup r1 r2) where
44 toEnum = dup1 @Sym_Enum toEnum
45 fromEnum = dup1 @Sym_Enum fromEnum
46 succ = dup1 @Sym_Enum succ
47 pred = dup1 @Sym_Enum pred
48
49 -- Transforming
50 instance (Sym_Enum term, Sym_Lambda term) => Sym_Enum (BetaT term)
51
52 -- Typing
53 instance NameTyOf Enum where
54 nameTyOf _c = ["Enum"] `Mod` "Enum"
55 instance FixityOf Enum
56 instance ClassInstancesFor Enum
57 instance TypeInstancesFor Enum
58
59 -- Compiling
60 instance Gram_Term_AtomsFor src ss g Enum
61 instance (Source src, SymInj ss Enum) => ModuleFor src ss Enum where
62 moduleFor = ["Enum"] `moduleWhere`
63 [ "succ" := teEnum_succ
64 , "pred" := teEnum_pred
65 , "toEnum" := teEnum_toEnum
66 , "fromEnum" := teEnum_fromEnum
67 ]
68
69 -- ** 'Type's
70 tyEnum :: Source src => Type src vs a -> Type src vs (Enum a)
71 tyEnum a = tyConstLen @(K Enum) @Enum (lenVars a) `tyApp` a
72
73 -- ** 'Term's
74 teEnum_toEnum :: TermDef Enum '[Proxy a] (Enum a #> (Int -> a))
75 teEnum_toEnum = Term (tyEnum a0) (tyInt ~> a0) $ teSym @Enum $ lam1 toEnum
76
77 teEnum_fromEnum :: TermDef Enum '[Proxy a] (Enum a #> (a -> Int))
78 teEnum_fromEnum = Term (tyEnum a0) (a0 ~> tyInt) $ teSym @Enum $ lam1 fromEnum
79
80 teEnum_succ, teEnum_pred :: TermDef Enum '[Proxy a] (Enum a #> (a -> a))
81 teEnum_succ = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 succ
82 teEnum_pred = Term (tyEnum a0) (a0 ~> a0) $ teSym @Enum $ lam1 pred