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

import Control.Monad
import Data.Ord (Ord)
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Ord(..))
import qualified Data.Kind as Kind
import qualified Data.Ord as Ord
import qualified Data.Text as Text

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda
import Language.Symantic.Lib.Eq (Sym_Eq)
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)

-- * Class 'Sym_Ord'
class Sym_Eq term => Sym_Ord term where
	compare  :: Ord a => term a -> term a -> term Ordering
	(<)      :: Ord a => term a -> term a -> term Bool; infix 4 <
	(<=)     :: Ord a => term a -> term a -> term Bool; infix 4 <=
	(>)      :: Ord a => term a -> term a -> term Bool; infix 4 >
	(>=)     :: Ord a => term a -> term a -> term Bool; infix 4 >=
	max      :: Ord a => term a -> term a -> term a
	min      :: Ord a => term a -> term a -> term a
	
	default compare  :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
	default (<)      :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default (<=)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default (>)      :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default (>=)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default max      :: (Trans t term, Ord a) => t term a -> t term a -> t term a
	default min      :: (Trans t term, Ord a) => t term a -> t term a -> t term a
	
	compare  = trans_map2 compare
	(<)      = trans_map2 (<)
	(<=)     = trans_map2 (<=)
	(>)      = trans_map2 (>)
	(>=)     = trans_map2 (>=)
	min      = trans_map2 min
	max      = trans_map2 max

-- * Class 'Sym_Ordering'
class Sym_Eq term => Sym_Ordering term where
	ordering :: Ordering -> term Ordering
	default ordering :: Trans t term => Ordering -> t term Ordering
	ordering = trans_lift . ordering

type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
type instance Sym_of_Iface (Proxy Ordering) = Sym_Ordering
type instance TyConsts_of_Iface (Proxy Ord) = Proxy Ord ': TyConsts_imported_by (Proxy Ord)
type instance TyConsts_of_Iface (Proxy Ordering) = Proxy Ordering ': TyConsts_imported_by (Proxy Ordering)
type instance TyConsts_imported_by (Proxy Ord) =
 [ Proxy Bool
 , Proxy Ordering
 ]
type instance TyConsts_imported_by (Proxy Ordering) =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Ord
 , Proxy Show
 ]

instance Sym_Ord HostI where
	compare  = liftM2 Ord.compare
	(<)      = liftM2 (Ord.<)
	(<=)     = liftM2 (Ord.<=)
	(>)      = liftM2 (Ord.>)
	(>=)     = liftM2 (Ord.>=)
	min      = liftM2 Ord.min
	max      = liftM2 Ord.max
instance Sym_Ordering HostI where
	ordering = HostI
instance Sym_Ord TextI where
	compare  = textI2 "compare"
	(<)      = textI_infix "<"  (infixN 4)
	(<=)     = textI_infix "<=" (infixN 4)
	(>)      = textI_infix ">"  (infixN 4)
	(>=)     = textI_infix ">=" (infixN 4)
	min      = textI2 "min"
	max      = textI2 "max"
instance Sym_Ordering TextI where
	ordering o = TextI $ \_p _v ->
		Text.pack (show o)
instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
	compare    = dupI2 @Sym_Ord compare
	(<)        = dupI2 @Sym_Ord (<)
	(<=)       = dupI2 @Sym_Ord (<=)
	(>)        = dupI2 @Sym_Ord (>)
	(>=)       = dupI2 @Sym_Ord (>=)
	min        = dupI2 @Sym_Ord min
	max        = dupI2 @Sym_Ord max
instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (DupI r1 r2) where
	ordering o = ordering o `DupI` ordering o

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Ord
 ) => Read_TyNameR TyName cs (Proxy Ord ': rs) where
	read_TyNameR _cs (TyName "Ord") k = k (ty @Ord)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Ordering
 ) => Read_TyNameR TyName cs (Proxy Ordering ': rs) where
	read_TyNameR _cs (TyName "Ordering") k = k (ty @Ordering)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Ord ': cs) where
	show_TyConst TyConstZ{} = "Ord"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy Ordering ': cs) where
	show_TyConst TyConstZ{} = "Ordering"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyFamC cs TyFam_MonoElement Ordering

instance Proj_TyConC cs (Proxy Ord)
instance -- Proj_TyConC
 ( Proj_TyConst cs Ordering
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Ordering))
 ) => Proj_TyConC cs (Proxy Ordering) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Ordering)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Ord)
 = Token_Term_Ord_compare (EToken meta ts)
 | Token_Term_Ord_le      (EToken meta ts)
 | Token_Term_Ord_lt      (EToken meta ts)
 | Token_Term_Ord_ge      (EToken meta ts)
 | Token_Term_Ord_gt      (EToken meta ts)
 | Token_Term_Ord_min     (EToken meta ts)
 | Token_Term_Ord_max     (EToken meta ts)
data instance TokenT meta (ts::[*]) (Proxy Ordering)
 = Token_Term_Ordering Ordering
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ordering))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ordering))

instance -- CompileI
 ( Inj_TyConst cs Bool
 , Inj_TyConst cs (->)
 , Inj_TyConst cs Ord
 , Inj_TyConst cs Ordering
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Ord) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy Ord)
	 -> Compiler meta ctx ret cs is ls (Proxy Ord ': rs)
	compileI tok ctx k =
		case tok of
		 Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare
		 Token_Term_Ord_le      tok_a -> compare_from tok_a (ty @Bool) (<=)
		 Token_Term_Ord_lt      tok_a -> compare_from tok_a (ty @Bool) (<)
		 Token_Term_Ord_ge      tok_a -> compare_from tok_a (ty @Bool) (>=)
		 Token_Term_Ord_gt      tok_a -> compare_from tok_a (ty @Bool) (>)
		 Token_Term_Ord_min     tok_a -> op2_from tok_a min
		 Token_Term_Ord_max     tok_a -> op2_from tok_a max
		where
		compare_from
		 :: EToken meta is
		 -> Type cs (res::Kind.Type)
		 -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
		 -> Either (Error_Term meta cs is) ret
		compare_from tok_a ty_res op =
		 -- compare :: Ord a => a -> a -> Ordering
		 -- (<=)    :: Ord a => a -> a -> Bool
		 -- (<)     :: Ord a => a -> a -> Bool
		 -- (>=)    :: Ord a => a -> a -> Bool
		 -- (>)     :: Ord a => a -> a -> Bool
			compile tok_a ctx $ \ty_a (Term x) ->
			check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_res) $ Term $
			 \c -> lam $ op (x c)
		op2_from tok_a
		 (op::forall term a. (Sym_Ord term, Ord a)
			 => term a -> term a -> term a) =
		 -- min :: Ord a => a -> a -> a
		 -- max :: Ord a => a -> a -> a
			compile tok_a ctx $ \ty_a (Term x) ->
			check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_a) $ Term $
			 \c -> lam $ \y -> op (x c) y
instance -- CompileI
 ( Inj_TyConst cs Ordering
 ) => CompileI cs is (Proxy Ordering) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Ordering o -> k (ty @Ordering) $ Term $ \_c -> ordering o
instance -- TokenizeT
 Inj_Token meta ts Ord =>
 TokenizeT meta ts (Proxy Ord) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "compare" infixN5 Token_Term_Ord_compare
		 , tokenize1 "<"  (infixN 4) Token_Term_Ord_lt
		 , tokenize1 "<=" (infixN 4) Token_Term_Ord_le
		 , tokenize1 ">"  (infixN 4) Token_Term_Ord_gt
		 , tokenize1 ">=" (infixN 4) Token_Term_Ord_ge
		 ]
	 }
instance -- TokenizeT
 Inj_Token meta ts Ordering =>
 TokenizeT meta ts (Proxy Ordering) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize0 "LT" infixN5 $ Token_Term_Ordering LT
		 , tokenize0 "EQ" infixN5 $ Token_Term_Ordering EQ
		 , tokenize0 "GT" infixN5 $ Token_Term_Ordering GT
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Ordering) g
instance Gram_Term_AtomsT meta ts (Proxy Ord) g