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

import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Int (Int)
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Prelude (Bounded, Enum, Integral, Num, Real)
import Text.Show (Show(..))
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 NameTyOf Int where
        nameTyOf _c = ["Int"] `Mod` "Int"
instance ClassInstancesFor Int where
        proveConstraintFor _c (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