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

import qualified Data.Text as Text

import Language.Symantic
import Language.Symantic.Grammar

-- * Class 'Sym_Integer'
type instance Sym (Proxy Integer) = Sym_Integer
class Sym_Integer term where
	integer :: Integer -> term Integer
	default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
	integer = trans . integer

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

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

-- Typing
instance ClassInstancesFor Integer where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
	 | Just HRefl <- proj_ConstKiTy @_ @Integer z
	 = case () of
		 _ | 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 Integer

-- Compiling
instance
 ( Gram_Source src g
 , Gram_Alt g
 , Gram_AltApp g
 , Gram_Rule g
 , Gram_Comment g
 , Inj_Sym ss Integer
 ) => Gram_Term_AtomsFor src ss g Integer where
	g_term_atomsFor _t =
	 [ rule "teinteger" $
		lexeme $ g_source $
		(\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
		 <$> some (choice $ char <$> ['0'..'9'])
	 ]
instance ModuleFor src ss Integer

-- ** 'Term's
tyInteger :: Source src => Inj_Len vs => Type src vs Integer
tyInteger = tyConst @(K Integer) @Integer

teInteger :: Source src => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i