{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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
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
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
instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
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
instance Gram_Term_AtomsFor src ss g Int
instance ModuleFor src ss Int
tyInt :: Source src => LenInj vs => Type src vs Int
tyInt = tyConst @(K Int) @Int
teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
teInt i = Term noConstraint tyInt $ teSym @Int $ int i