{-# 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 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
	ordering :: Ordering -> term Ordering
	compare  :: Ord a => term a -> term a -> term Ordering
	(<)      :: Ord a => term a -> term a -> term Bool
	(<=)     :: Ord a => term a -> term a -> term Bool
	(>)      :: Ord a => term a -> term a -> term Bool
	(>=)     :: Ord a => term a -> term a -> term Bool
	max      :: Ord a => term a -> term a -> term a
	min      :: Ord a => term a -> term a -> term a
	
	default ordering :: Trans t term => Ordering -> t term Ordering
	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
	
	ordering = trans_lift . ordering
	compare  = trans_map2 compare
	(<)      = trans_map2 (<)
	(<=)     = trans_map2 (<=)
	(>)      = trans_map2 (>)
	(>=)     = trans_map2 (>=)
	min      = trans_map2 min
	max      = trans_map2 max

infix 4 <
infix 4 <=
infix 4 >
infix 4 >=

type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
type instance Consts_of_Iface (Proxy Ord) = Proxy Ord ': Consts_imported_by Ord
type instance Consts_imported_by Ord = '[]

instance Sym_Ord HostI where
	ordering = HostI
	compare  = liftM2 Ord.compare
	(<)      = liftM2 (Ord.<)
	(<=)     = liftM2 (Ord.<=)
	(>)      = liftM2 (Ord.>)
	(>=)     = liftM2 (Ord.>=)
	min      = liftM2 Ord.min
	max      = liftM2 Ord.max
instance Sym_Ord TextI where
	ordering o = TextI $ \_p _v ->
		Text.pack (show o)
	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_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
	ordering o = ordering o `DupI` ordering o
	compare    = dupI2 (Proxy @Sym_Ord) compare
	(<)        = dupI2 (Proxy @Sym_Ord) (<)
	(<=)       = dupI2 (Proxy @Sym_Ord) (<=)
	(>)        = dupI2 (Proxy @Sym_Ord) (>)
	(>=)       = dupI2 (Proxy @Sym_Ord) (>=)
	min        = dupI2 (Proxy @Sym_Ord) min
	max        = dupI2 (Proxy @Sym_Ord) max

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs Ord
 ) => Read_TypeNameR Type_Name cs (Proxy Ord ': rs) where
	read_typenameR _cs (Type_Name "Ord") k = k (ty @Ord)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
	show_const ConstZ{} = "Ord"
	show_const (ConstS c) = show_const c

instance Proj_ConC cs (Proxy Ord)
data instance TokenT meta (ts::[*]) (Proxy Ord)
 = Token_Term_Ordering    Ordering
 | 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)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
instance -- CompileI
 ( Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Ord
 , Inj_Const (Consts_of_Ifaces is) Ordering
 , Proj_Con (Consts_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_Ordering o -> k (ty @Ordering) $ TermO $ \_c -> ordering o
		 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 (Consts_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_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
			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_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
			k (ty_a ~> ty_a) $ TermO $
			 \c -> lam $ \y -> op (x c) y
instance -- TokenizeT
 Inj_Token meta ts Ord =>
 TokenizeT meta ts (Proxy Ord) 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
		 , 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 Gram_Term_AtomsT meta ts (Proxy Ord) g