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

import qualified Data.Text as Text

import Language.Symantic

-- * Class 'Sym_Int'
type instance Sym Int = Sym_Int
class Sym_Int term where
	int :: Int -> term Int
	default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
	int = trans . int

-- Interpreting
instance Sym_Int Eval where
	int = Eval
instance Sym_Int View where
	int a = View $ \_p _v ->
		Text.pack (show a)
instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where
	int x = int x `Dup` int x

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

-- Typing
instance ClassInstancesFor Int where
	proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
	 | Just HRefl <- proj_ConstKiTy @_ @Int 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 @Integral q -> Just Dict
		   | Just Refl <- proj_Const @Num      q -> Just Dict
		   | Just Refl <- proj_Const @Ord      q -> Just Dict
		   | Just Refl <- proj_Const @Real     q -> Just Dict
		   | Just Refl <- proj_Const @Show     q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Int

-- Compiling
instance Gram_Term_AtomsFor src ss g Int
instance ModuleFor src ss Int

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

-- ** 'Term's
teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
teInt i = Term noConstraint tyInt $ teSym @Int $ int i