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

import Language.Symantic
import Language.Symantic.Grammar

-- * Class 'Sym_Unit'
type instance Sym () = Sym_Unit
class Sym_Unit term where
	unit :: term ()
	default unit :: Sym_Unit (UnT term) => Trans term => term ()
	unit = trans unit

-- Interpreting
instance Sym_Unit Eval where
	unit = Eval ()
instance Sym_Unit View where
	unit = View $ \_p _v -> "()"
instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
	unit = unit `Dup` unit

-- Transforming
instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)

-- Typing
instance NameTyOf () where
	nameTyOf _c = [] `Mod` ""
instance ClassInstancesFor () where
	proveConstraintFor _ (TyConst _ _ q :$ z)
	 | Just HRefl <- proj_ConstKiTy @_ @() z
	 = case () of
		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
		   | Just Refl <- proj_Const @Enum    q -> Just Dict
		   | Just Refl <- proj_Const @Eq      q -> Just Dict
		   | Just Refl <- proj_Const @Monoid  q -> Just Dict
		   | Just Refl <- proj_Const @Ord     q -> Just Dict
		   | Just Refl <- proj_Const @Show    q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor ()

-- Compiling
instance
 ( Gram_Source src g
 , Gram_Rule g
 , Gram_Comment g
 , SymInj ss ()
 ) => Gram_Term_AtomsFor src ss g () where
	g_term_atomsFor =
	 [ rule "teUnit" $
		source $
		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
		 <$ symbol "("
		 <* symbol ")"
	 ]
instance ModuleFor src ss ()

-- ** 'Type's
tyUnit :: Source src => LenInj vs => Type src vs ()
tyUnit = tyConst @(K ()) @()

-- ** 'Term's
teUnit :: TermDef () '[] (() #> ())
teUnit = Term noConstraint tyUnit $ teSym @() $ unit