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

import Data.Eq (Eq)
import Data.Function (($), (.))
import Data.Functor ((<$>))
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Prelude (Enum, Integer, Integral, Num, Real)
import Text.Show (Show(..))
import Text.Read (read)
import qualified Data.Text as Text

import Language.Symantic
import Language.Symantic.Grammar

-- * Class 'Sym_Integer'
type instance Sym 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 NameTyOf Integer where
        nameTyOf _c = ["Integer"] `Mod` "Integer"
instance ClassInstancesFor Integer where
        proveConstraintFor _ (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
 , SymInj ss Integer
 ) => Gram_Term_AtomsFor src ss g Integer where
        g_term_atomsFor =
         [ rule "teinteger" $
                lexeme $ 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 => LenInj vs => Type src vs Integer
tyInteger = tyConst @(K Integer) @Integer

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