{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
-- | Symantic for 'Unit'.
module Hcompta.LCC.Sym.Unit where

-- import Data.Decimal (Decimal)
import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Text.Show (Show(..))
import qualified Data.Text as Text
import qualified Language.Symantic.Typing as Sym

import Hcompta.LCC.Amount

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans
import qualified Language.Symantic.Lib as Sym

-- * Class 'Sym_Unit'
class Sym_Unit term where
	unit :: Unit -> term Unit
	default unit :: Trans t term => Unit -> t term Unit
	unit = trans_lift . unit

type instance Sym_of_Iface (Proxy Unit) = Sym_Unit
type instance TyConsts_of_Iface (Proxy Unit) = Proxy Unit ': TyConsts_imported_by (Proxy Unit)
type instance TyConsts_imported_by (Proxy Unit) =
 [ Proxy Eq
 , Proxy Ord
 , Proxy Show
 ]

instance Sym_Unit HostI where
	unit = HostI
instance Sym_Unit TextI where
	unit a = TextI $ \_p _v ->
		Text.pack (show a)
instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where
	unit x = unit x `DupI` unit x

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Unit
 ) => Read_TyNameR TyName cs (Proxy Unit ': rs) where
	read_TyNameR _cs (TyName "Unit") k = k (ty @Unit)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Unit ': cs) where
	show_TyConst TyConstZ{} = "Unit"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyFamC cs Sym.TyFam_MonoElement Unit

instance -- Proj_TyConC
 ( Proj_TyConst cs Unit
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Unit))
 ) => Proj_TyConC cs (Proxy Unit) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Unit)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)   -> 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 Unit)
 = Token_Term_Unit Unit
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Unit))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Unit))

instance -- CompileI
 Inj_TyConst cs Unit =>
 CompileI cs is (Proxy Unit) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Unit i -> k (ty @Unit) $ TermO $ \_c -> unit i
instance -- TokenizeT
 -- Inj_Token meta ts Unit =>
 TokenizeT meta ts (Proxy Unit)
instance Gram_Term_AtomsT meta ts (Proxy Unit) g