{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
-- | Symantic for 'Integer'.
module Language.Symantic.Compiling.Integer where

import qualified Data.Function as Fun
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Integer'
class Sym_Integer term where
	integer :: Integer -> term Integer
	default integer :: Trans t term => Integer -> t term Integer
	integer = trans_lift . integer

type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
type instance Consts_of_Iface (Proxy Integer) = Proxy Integer ': Consts_imported_by Integer
type instance Consts_imported_by Integer =
 [ Proxy Enum
 , Proxy Eq
 , Proxy Integral
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 ]

instance Sym_Integer HostI where
	integer = HostI
instance Sym_Integer TextI where
	integer a = TextI $ \_p _v ->
		Text.pack (show a)
instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
	integer x = integer x `DupI` integer x

instance Const_from Text cs => Const_from Text (Proxy Integer ': cs) where
	const_from "Integer" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
	show_const ConstZ{} = "Integer"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs Integer
 , Proj_Consts cs (Consts_imported_by Integer)
 ) => Proj_ConC cs (Proxy Integer) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy Integer)
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Integer
 , Show_Const (Consts_of_Ifaces is)
 ) => Term_fromI is (Proxy Integer) ast where
	term_fromI ast _ctx k =
		case ast_lexem ast of
		 "integer" -> integer_from
		 _ -> Left $ Error_Term_unsupported
		where
		integer_from =
			let ty = tyInteger in
			from_lex (Text.pack $ show_type ty) ast $ \(i::Integer) as ->
			k as ty $ TermLC $ Fun.const $ integer i

-- | The 'Integer' 'Type'
tyInteger :: Inj_Const cs Integer => Type cs Integer
tyInteger = TyConst inj_const

sym_Integer :: Proxy Sym_Integer
sym_Integer = Proxy

syInteger :: IsString a => Syntax a
syInteger = Syntax "Integer" []