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 @()) $ TermO $ 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 -> ProTok $ inj_EToken meta $ Token_Term_Unit)
  96                  <$ symbol "("
  97                  <* symbol ")"
  98          ]