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

import Control.Applicative ((<*))
import Data.Eq (Eq)
import Data.Function (($))
import Data.Functor ((<$))
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid)
import Data.Ord (Ord)
import Prelude (Bounded, Enum)
import Text.Show (Show)

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