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

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

import Language.Symantic

import Hcompta.LCC.Amount

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

instance Sym_Unit Eval where
	unit = Eval
instance Sym_Unit View where
	unit (Unit u) = View $ \_p _v -> u
instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
	unit x = unit x `Dup` unit x
instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)

instance ClassInstancesFor Unit where
	proveConstraintFor _c (TyApp _ (TyConst _ _ q) c)
	 | Just HRefl <- proj_ConstKiTy @(K Unit) @Unit c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq   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 Unit
instance Gram_Term_AtomsFor src ss g Unit
instance (Source src, SymInj ss Unit) => ModuleFor src ss Unit where
	moduleFor = ["Unit"] `moduleWhere`
	 [
	 ]

tyUnit :: Source src => LenInj vs => Type src vs Unit
tyUnit = tyConst @(K Unit) @Unit

teUnit :: Source src => SymInj ss Unit => Unit -> Term src ss ts '[] (() #> Unit)
teUnit a = Term noConstraint tyUnit $ teSym @Unit $ unit a