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 Consts_of_Iface (Proxy ()) = Proxy () ': Consts_imported_by ()
  27 type instance Consts_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_TypeNameR Type_Name cs rs
  45  , Inj_Const cs ()
  46  ) => Read_TypeNameR Type_Name cs (Proxy () ': rs) where
  47         read_typenameR _cs (Type_Name "()") k = k (ty @())
  48         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  49 instance Show_Const cs => Show_Const (Proxy () ': cs) where
  50         show_const ConstZ{} = "()"
  51         show_const (ConstS c) = show_const c
  52
  53 instance -- Proj_ConC
  54  ( Proj_Const cs ()
  55  , Proj_Consts cs (Consts_imported_by ())
  56  ) => Proj_ConC cs (Proxy ()) where
  57         proj_conC _ (TyConst q :$ TyConst c)
  58          | Just Refl <- eq_skind (kind_of_const c) SKiType
  59          , Just Refl <- proj_const c (Proxy @())
  60          = case () of
  61                  _ | Just Refl <- proj_const q (Proxy @Bounded) -> Just Con
  62                    | Just Refl <- proj_const q (Proxy @Enum)    -> Just Con
  63                    | Just Refl <- proj_const q (Proxy @Eq)      -> Just Con
  64                    | Just Refl <- proj_const q (Proxy @Monoid)  -> Just Con
  65                    | Just Refl <- proj_const q (Proxy @Ord)     -> Just Con
  66                    | Just Refl <- proj_const q (Proxy @Show)    -> Just Con
  67                  _ -> Nothing
  68         proj_conC _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_Const (Consts_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          ]