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

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

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)

-- * 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 Ord
type instance TyConsts_of_Iface (Proxy Ordering) = Proxy Ordering ': TyConsts_imported_by Ordering
type instance TyConsts_imported_by Ord = '[]
type instance TyConsts_imported_by 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_TyConC cs (Proxy Ord)
instance -- Proj_TyConC
 ( Proj_TyConst cs Ordering
 , Proj_TyConsts cs (TyConsts_imported_by 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 (TyConsts_of_Ifaces is) Bool
 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
 , Inj_TyConst (TyConsts_of_Ifaces is) Ord
 , Inj_TyConst (TyConsts_of_Ifaces is) Ordering
 , Proj_TyCon (TyConsts_of_Ifaces is)
 , Compile is
 ) => CompileI is (Proxy Ord) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy Ord)
	 -> CompileT meta ctx ret 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 (TyConsts_of_Ifaces is) (res::Kind.Type)
		 -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
		 -> Either (Error_Term meta 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
			compileO tok_a ctx $ \ty_a (TermO x) ->
			check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_res) $ TermO $
			 \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
			compileO tok_a ctx $ \ty_a (TermO x) ->
			check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty_a) $ TermO $
			 \c -> lam $ \y -> op (x c) y
instance -- CompileI
 ( Inj_TyConst (TyConsts_of_Ifaces is) Ordering
 ) => CompileI is (Proxy Ordering) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Ordering o -> k (ty @Ordering) $ TermO $ \_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