]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Unit.hs
Try to implement polymorphic types.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Unit.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
4 -- | Symantic for '()'.
5 module Language.Symantic.Lib.Unit where
6
7 import Data.Monoid
8 import Data.Proxy
9 import Data.Type.Equality ((:~:)(Refl))
10 import Prelude hiding ((&&), not, (||))
11 import qualified Data.Function as Fun
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming
18 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
19
20 -- * Class 'Sym_Unit'
21 class Sym_Unit term where
22 unit :: term ()
23 default unit :: Trans t term => t term ()
24 unit = trans_lift unit
25
26 type instance Sym_of_Iface (Proxy ()) = Sym_Unit
27 type instance TyConsts_of_Iface (Proxy ()) = Proxy () ': TyConsts_imported_by (Proxy ())
28 type instance TyConsts_imported_by (Proxy ()) =
29 [ Proxy Bounded
30 , Proxy Enum
31 , Proxy Eq
32 , Proxy Monoid
33 , Proxy Ord
34 , Proxy Show
35 ]
36
37 instance Sym_Unit HostI where
38 unit = HostI ()
39 instance Sym_Unit TextI where
40 unit = TextI $ \_p _v -> "()"
41 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where
42 unit = unit `DupI` unit
43
44 instance
45 ( Read_TyNameR TyName cs rs
46 , Inj_TyConst cs ()
47 ) => Read_TyNameR TyName cs (Proxy () ': rs) where
48 read_TyNameR _cs (TyName "()") k = k (ty @())
49 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
50 instance Show_TyConst cs => Show_TyConst (Proxy () ': cs) where
51 show_TyConst TyConstZ{} = "()"
52 show_TyConst (TyConstS c) = show_TyConst c
53
54 instance Proj_TyFamC cs TyFam_MonoElement ()
55
56 instance -- Proj_TyConC
57 ( Proj_TyConst cs ()
58 , Proj_TyConsts cs (TyConsts_imported_by (Proxy ()))
59 ) => Proj_TyConC cs (Proxy ()) where
60 proj_TyConC _ (TyConst q :$ TyConst c)
61 | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
62 , Just Refl <- proj_TyConst c (Proxy @())
63 = case () of
64 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
65 | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
66 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
67 | Just Refl <- proj_TyConst q (Proxy @Monoid) -> Just TyCon
68 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
69 | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
70 _ -> Nothing
71 proj_TyConC _c _q = Nothing
72 data instance TokenT meta (ts::[*]) (Proxy ())
73 = Token_Term_Unit
74 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy ()))
75 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy ()))
76
77 instance -- CompileI
78 ( Inj_TyConst cs ()
79 ) => CompileI cs is (Proxy ()) where
80 compileI tok _ctx k =
81 case tok of
82 Token_Term_Unit -> k (ty @()) $ Term $ Fun.const unit
83 instance -- TokenizeT
84 -- Inj_Token meta ts () =>
85 TokenizeT meta ts (Proxy ())
86 instance -- Gram_Term_AtomsT
87 ( Gram_Rule g
88 , Gram_Lexer g
89 , Gram_Meta meta g
90 , Inj_Token meta ts ()
91 ) => Gram_Term_AtomsT meta ts (Proxy ()) g where
92 gs_term_atomsT _t =
93 [ rule "term_unit" $
94 metaG $
95 (\meta -> ProTokTe $ inj_EToken meta $ Token_Term_Unit)
96 <$ symbol "("
97 <* symbol ")"
98 ]