Language/Symantic/Compiling/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.Compiling.Unit where
   6
   7 import qualified Data.Function as Fun
   8 import Data.Monoid
   9 import Data.Proxy
  10 import Data.Text (Text)
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding ((&&), not, (||))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling.Term
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming.Trans
  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 Consts_of_Iface (Proxy ()) = Proxy () ': Consts_imported_by ()
  28 type instance Consts_imported_by () =
  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_TypeNameR Text cs rs
  46  , Inj_Const cs ()
  47  ) => Read_TypeNameR Text cs (Proxy () ': rs) where
  48         read_typenameR _cs "()" k = k (ty @())
  49         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  50 instance Show_Const cs => Show_Const (Proxy () ': cs) where
  51         show_const ConstZ{} = "()"
  52         show_const (ConstS c) = show_const c
  53
  54 instance -- Proj_ConC
  55  ( Proj_Const cs ()
  56  , Proj_Consts cs (Consts_imported_by ())
  57  ) => Proj_ConC cs (Proxy ()) where
  58         proj_conC _ (TyConst q :$ TyConst c)
  59          | Just Refl <- eq_skind (kind_of_const c) SKiType
  60          , Just Refl <- proj_const c (Proxy::Proxy ())
  61          = case () of
  62                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
  63                    | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
  64                    | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
  65                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)  -> Just Con
  66                    | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
  67                    | Just Refl <- proj_const q (Proxy::Proxy Show)    -> Just Con
  68                  _ -> Nothing
  69         proj_conC _c _q = Nothing
  70 data instance TokenT meta (ts::[*]) (Proxy ())
  71  = Token_Term_Unit
  72 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy ()))
  73 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy ()))
  74 instance -- CompileI
  75  ( Inj_Const (Consts_of_Ifaces is) ()
  76  ) => CompileI is (Proxy ()) where
  77         compileI tok _ctx k =
  78                 case tok of
  79                  Token_Term_Unit -> k (ty @()) $ TermO $ Fun.const unit