{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
-- | Symantic for '()'.
module Language.Symantic.Lib.Unit where

import qualified Data.Function as Fun
import Data.Monoid
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((&&), not, (||))

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming

-- * 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 TyConsts_of_Iface (Proxy ()) = Proxy () ': TyConsts_imported_by ()
type instance TyConsts_imported_by () =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Monoid
 , Proxy Ord
 , Proxy Show
 ]

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
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs ()
 ) => Read_TyNameR TyName cs (Proxy () ': rs) where
	read_TyNameR _cs (TyName "()") k = k (ty @())
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy () ': cs) where
	show_TyConst TyConstZ{} = "()"
	show_TyConst (TyConstS c) = show_TyConst c

instance -- Proj_TyConC
 ( Proj_TyConst cs ()
 , Proj_TyConsts cs (TyConsts_imported_by ())
 ) => Proj_TyConC cs (Proxy ()) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @())
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monoid)  -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
		 _ -> Nothing
	proj_TyConC _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 -- CompileI
 ( Inj_TyConst cs ()
 ) => CompileI cs is (Proxy ()) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Unit -> k (ty @()) $ TermO $ Fun.const unit
instance -- TokenizeT
 -- Inj_Token meta ts () =>
 TokenizeT meta ts (Proxy ())
instance -- Gram_Term_AtomsT
 ( Gram_Rule g
 , Gram_Lexer g
 , Gram_Meta meta g
 , Inj_Token meta ts ()
 ) => Gram_Term_AtomsT meta ts (Proxy ()) g where
	gs_term_atomsT _t =
	 [ rule "term_unit" $
		metaG $
		(\meta -> ProTok $ inj_EToken meta $ Token_Term_Unit)
		 <$ symbol "("
		 <* symbol ")"
	 ]