]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Var.hs
init
[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 Data.Type.Equality ((:~:)(Refl))
18 import Language.Symantic.Type.Common
19 import Language.Symantic.Lib.Data.Peano
20
21 -- * Type 'Var0'
22 newtype Var0 = Var0 EPeano
23 type instance Host_of EPeano = Var0
24
25 -- | Undefined instance required to build errors.
26 instance Eq Var0
27 -- | Undefined instance required to build errors.
28 instance Ord Var0
29
30 -- * Type 'Var1'
31 newtype Var1 a = Var1 EPeano
32 type instance Host1_of EPeano = Var1
33
34 -- * Type 'Type_Var0'
35 -- | The variable type of kind @*@.
36 type Type_Var0 = Type_Type0 EPeano
37
38 pattern Type_Var0 :: SPeano p -> Type_Var0 root Var0
39 pattern Type_Var0 p = Type_Type0 (EPeano p)
40
41 instance Eq_Type1 (Type_Var0 root) where
42 instance -- String_from_Type
43 String_from_Type (Type_Var0 root) where
44 string_from_type (Type_Type0 (EPeano p)) =
45 "t" ++ show (integral_from_peano p::Integer)
46 instance Constraint_Type Eq (Type_Var0 root) where
47 constraint_type _c Type_Type0{} = Just Dict
48
49 -- | Inject 'Type_Var0' within a root type.
50 type_var0 :: Lift_Type_Root Type_Var0 root => SPeano p -> root Var0
51 type_var0 = lift_type_root . Type_Type0 . EPeano
52
53 -- * Type 'Type_Var1'
54 -- | The variable type of kind @* -> *@.
55 type Type_Var1 = Type_Type1 EPeano
56 instance Constraint_Type Eq (Type_Var1 root)
57
58 pattern Type_Var1 :: SPeano p -> root a -> Type_Var1 root (Var1 a)
59 pattern Type_Var1 p a = Type_Type1 (EPeano p) a
60
61 instance Eq_Type1 (Type_Var1 root) where
62 eq_type1 (Type_Type1 p1 _) (Type_Type1 p2 _)
63 | p1 == p2
64 = Just Refl
65 eq_type1 _ _ = Nothing
66 instance -- String_from_Type
67 String_from_Type root =>
68 String_from_Type (Type_Var1 root) where
69 string_from_type (Type_Type1 (EPeano p) a) =
70 "t_" ++ show (integral_from_peano p::Integer) ++
71 " " ++ string_from_type a
72
73 -- | Inject 'Type_Var1' within a root type.
74 type_var1 :: Lift_Type_Root Type_Var1 root => SPeano p -> root a -> root (Var1 a)
75 type_var1 p = lift_type_root . Type_Var1 p