Language/Symantic/Compiling/Unit.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for '()'.
   4 module Language.Symantic.Compiling.Unit where
   5
   6 import qualified Data.Function as Fun
   7 import Data.Monoid
   8 import Data.Proxy
   9 import Data.Text (Text)
  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.Term
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming.Trans
  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  ]
  34
  35 instance Sym_Unit HostI where
  36         unit = HostI ()
  37 instance Sym_Unit TextI where
  38         unit = TextI $ \_p _v -> "()"
  39 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where
  40         unit = unit `DupI` unit
  41
  42 instance Const_from Text cs => Const_from Text (Proxy () ': cs) where
  43         const_from "()" k = k (ConstZ kind)
  44         const_from s k = const_from s $ k . ConstS
  45 instance Show_Const cs => Show_Const (Proxy () ': cs) where
  46         show_const ConstZ{} = "()"
  47         show_const (ConstS c) = show_const c
  48
  49 instance -- Proj_ConC
  50  ( Proj_Const cs ()
  51  , Proj_Consts cs (Consts_imported_by ())
  52  ) => Proj_ConC cs (Proxy ()) where
  53         proj_conC _ (TyConst q :$ TyConst c)
  54          | Just Refl <- eq_skind (kind_of_const c) SKiType
  55          , Just Refl <- proj_const c (Proxy::Proxy ())
  56          = case () of
  57                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
  58                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
  59                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
  60                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)   -> Just Con
  61                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
  62                  _ -> Nothing
  63         proj_conC _c _q = Nothing
  64 data instance TokenT meta (ts::[*]) (Proxy ())
  65  = Token_Term_Unit
  66 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy ()))
  67 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy ()))
  68 instance -- Term_fromI
  69  ( Inj_Const (Consts_of_Ifaces is) ()
  70  ) => Term_fromI is (Proxy ()) where
  71         term_fromI tok _ctx k =
  72                 case tok of
  73                  Token_Term_Unit -> k (ty @()) $ TermLC $ Fun.const unit