]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Unit.hs
Fix comment typo.
[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 qualified Data.Function as Fun
8 import Data.Monoid
9 import Data.Proxy
10 import Data.Type.Equality ((:~:)(Refl))
11 import Prelude hiding ((&&), not, (||))
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
19 -- * Class 'Sym_Unit'
20 class Sym_Unit term where
21 unit :: term ()
22 default unit :: Trans t term => t term ()
23 unit = trans_lift unit
24
25 type instance Sym_of_Iface (Proxy ()) = Sym_Unit
26 type instance TyConsts_of_Iface (Proxy ()) = Proxy () ': TyConsts_imported_by ()
27 type instance TyConsts_imported_by () =
28 [ Proxy Bounded
29 , Proxy Enum
30 , Proxy Eq
31 , Proxy Monoid
32 , Proxy Ord
33 , Proxy Show
34 ]
35
36 instance Sym_Unit HostI where
37 unit = HostI ()
38 instance Sym_Unit TextI where
39 unit = TextI $ \_p _v -> "()"
40 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where
41 unit = unit `DupI` unit
42
43 instance
44 ( Read_TyNameR TyName cs rs
45 , Inj_TyConst cs ()
46 ) => Read_TyNameR TyName cs (Proxy () ': rs) where
47 read_TyNameR _cs (TyName "()") k = k (ty @())
48 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
49 instance Show_TyConst cs => Show_TyConst (Proxy () ': cs) where
50 show_TyConst TyConstZ{} = "()"
51 show_TyConst (TyConstS c) = show_TyConst c
52
53 instance -- Proj_TyConC
54 ( Proj_TyConst cs ()
55 , Proj_TyConsts cs (TyConsts_imported_by ())
56 ) => Proj_TyConC cs (Proxy ()) where
57 proj_TyConC _ (TyConst q :$ TyConst c)
58 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
59 , Just Refl <- proj_TyConst c (Proxy @())
60 = case () of
61 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
62 | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
63 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
64 | Just Refl <- proj_TyConst q (Proxy @Monoid) -> Just TyCon
65 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
66 | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
67 _ -> Nothing
68 proj_TyConC _c _q = Nothing
69 data instance TokenT meta (ts::[*]) (Proxy ())
70 = Token_Term_Unit
71 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy ()))
72 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy ()))
73 instance -- CompileI
74 ( Inj_TyConst (TyConsts_of_Ifaces is) ()
75 ) => CompileI is (Proxy ()) where
76 compileI tok _ctx k =
77 case tok of
78 Token_Term_Unit -> k (ty @()) $ TermO $ Fun.const unit
79 instance -- TokenizeT
80 -- Inj_Token meta ts () =>
81 TokenizeT meta ts (Proxy ())
82 instance -- Gram_Term_AtomsT
83 ( Gram_Rule g
84 , Gram_Lexer g
85 , Gram_Meta meta g
86 , Inj_Token meta ts ()
87 ) => Gram_Term_AtomsT meta ts (Proxy ()) g where
88 term_atomsT _t =
89 [ rule "term_unit" $
90 metaG $
91 (\meta -> ProTok $ inj_EToken meta $ Token_Term_Unit)
92 <$ symbol "("
93 <* symbol ")"
94 ]