{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for '()'. module Language.Symantic.Compiling.Unit where import qualified Data.Function as Fun import Data.Monoid import Data.Proxy import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding ((&&), not, (||)) import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class 'Sym_Unit' class Sym_Unit term where unit :: term () default unit :: Trans t term => t term () unit = trans_lift unit type instance Sym_of_Iface (Proxy ()) = Sym_Unit type instance Consts_of_Iface (Proxy ()) = Proxy () ': Consts_imported_by () type instance Consts_imported_by () = [ Proxy Bounded , Proxy Enum , Proxy Eq , Proxy Monoid , Proxy Ord ] instance Sym_Unit HostI where unit = HostI () instance Sym_Unit TextI where unit = TextI $ \_p _v -> "()" instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where unit = unit `DupI` unit instance Const_from Text cs => Const_from Text (Proxy () ': cs) where const_from "()" k = k (ConstZ kind) const_from s k = const_from s $ k . ConstS instance Show_Const cs => Show_Const (Proxy () ': cs) where show_const ConstZ{} = "()" show_const (ConstS c) = show_const c instance -- Proj_ConC ( Proj_Const cs () , Proj_Consts cs (Consts_imported_by ()) ) => Proj_ConC cs (Proxy ()) where proj_conC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_const c) SKiType , Just Refl <- proj_const c (Proxy::Proxy ()) = case () of _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Ord) -> Just Con _ -> Nothing proj_conC _c _q = Nothing data instance TokenT meta (ts::[*]) (Proxy ()) = Token_Term_Unit deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy ())) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy ())) instance -- Term_fromI ( Inj_Const (Consts_of_Ifaces is) () ) => Term_fromI is (Proxy ()) where term_fromI tok _ctx k = case tok of Token_Term_Unit -> k (ty @()) $ TermLC $ Fun.const unit