]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Var.hs
polish names
[haskell/symantic.git] / Language / Symantic / Type / Var.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE PatternSynonyms #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE ScopedTypeVariables #-}
8 {-# LANGUAGE UndecidableInstances #-}
9 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
10 {-# OPTIONS_GHC -fno-warn-orphans #-}
11 -- | Type variable.
12 module Language.Symantic.Type.Var
13 ( module Language.Symantic.Type.Var
14 , module Language.Symantic.Lib.Data.Peano
15 ) where
16
17 import qualified Data.MonoTraversable as MT
18 import Data.Type.Equality ((:~:)(Refl))
19
20 import Language.Symantic.Lib.Data.Peano
21 import Language.Symantic.Type.Root
22 import Language.Symantic.Type.Type0
23 import Language.Symantic.Type.Type1
24 import Language.Symantic.Type.Constraint
25 import Language.Symantic.Type.Family
26
27 -- * Type 'Var0'
28 newtype Var0 = Var0 EPeano
29 type instance Host0_of EPeano = Var0
30
31 -- | Undefined instance required to build errors.
32 instance Eq Var0
33 -- | Undefined instance required to build errors.
34 instance Ord Var0
35 -- | Undefined instance required to build errors.
36 instance Monoid Var0
37
38 -- * Type 'Var1'
39 newtype Var1 a = Var1 EPeano
40 type instance Host1_of EPeano = Var1
41
42 -- * Type 'Type_Var0'
43 -- | The variable type of kind @*@.
44 type Type_Var0 = Type0 EPeano
45
46 pattern Type_Var0 :: SPeano p -> Type_Var0 root Var0
47 pattern Type_Var0 p = Type0 (EPeano p)
48
49 instance Type1_Eq (Type_Var0 root) where
50 instance Type0_Constraint Eq (Type_Var0 root)
51 instance Type0_Constraint Monoid (Type_Var0 root)
52 instance Type0_Constraint Ord (Type_Var0 root)
53 instance Type0_Constraint Num (Type_Var0 root)
54 instance Type0_Constraint Integral (Type_Var0 root)
55 instance Type0_Constraint MT.MonoFunctor (Type_Var0 root)
56 instance Type0_Family Type_Family_MonoElement (Type_Var0 root)
57 instance String_from_Type (Type_Var0 root) where
58 string_from_type (Type0 (EPeano p)) =
59 "t" ++ show (integral_from_peano p::Integer)
60
61 -- | Inject 'Type_Var0' within a root type.
62 type_var0 :: Type_Root_Lift Type_Var0 root => SPeano p -> root Var0
63 type_var0 = type_root_lift . Type0 . EPeano
64
65 -- * Type 'Type_Var1'
66 -- | The variable type of kind @* -> *@.
67 type Type_Var1 = Type1 EPeano
68
69 pattern Type_Var1 :: SPeano p -> root a -> Type_Var1 root (Var1 a)
70 pattern Type_Var1 p a = Type1 (EPeano p) a
71
72 instance Type0_Constraint Eq (Type_Var1 root)
73 instance Type0_Constraint Ord (Type_Var1 root)
74 instance Type0_Constraint Monoid (Type_Var1 root)
75 instance Type0_Constraint Num (Type_Var1 root)
76 instance Type0_Constraint Integral (Type_Var1 root)
77 instance Type0_Constraint MT.MonoFunctor (Type_Var1 root)
78 instance Type1_Constraint Applicative (Type_Var1 root)
79 instance Type1_Constraint Foldable (Type_Var1 root)
80 instance Type1_Constraint Functor (Type_Var1 root)
81 instance Type1_Constraint Monad (Type_Var1 root)
82 instance Type1_Constraint Traversable (Type_Var1 root)
83 instance Type0_Family Type_Family_MonoElement (Type_Var1 root)
84 instance Type1_Eq (Type_Var1 root) where
85 type1_eq (Type1 p1 _) (Type1 p2 _)
86 | p1 == p2
87 = Just Refl
88 type1_eq _ _ = Nothing
89 instance -- String_from_Type
90 String_from_Type root =>
91 String_from_Type (Type_Var1 root) where
92 string_from_type (Type1 (EPeano p) a) =
93 "t_" ++ show (integral_from_peano p::Integer) ++
94 " " ++ string_from_type a
95
96 -- | Inject 'Type_Var1' within a root type.
97 type_var1 :: Type_Root_Lift Type_Var1 root => SPeano p -> root a -> root (Var1 a)
98 type_var1 p = type_root_lift . Type_Var1 p