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

import Control.Monad
import Data.Ord (Ord)
import qualified Data.Ord as Ord
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Kind as Kind
import Prelude hiding (Ord(..))

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Eq (Sym_Eq)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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
	(<=)    :: 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 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

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
	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
	compare = textI_app2  "compare"
	(<)     = textI_infix "<"  (Precedence 4)
	(<=)    = textI_infix "<=" (Precedence 4)
	(>)     = textI_infix ">"  (Precedence 4)
	(>=)    = textI_infix ">=" (Precedence 4)
	min     = textI_app2  "min"
	max     = textI_app2  "max"
instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
	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 Const_from Text cs => Const_from Text (Proxy Ord ': cs) where
	const_from "Ord" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
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_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 -- Term_fromI
 ( 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)
 , Term_from is
 ) => Term_fromI is (Proxy Ord) where
	term_fromI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy Ord)
	 -> Term_fromT meta ctx ret is ls (Proxy Ord ': rs)
	term_fromI 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 (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
			term_from tok_a ctx $ \ty_a (TermLC x) ->
			check_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
			k (ty_a ~> ty_res) $ TermLC $
			 \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
			term_from tok_a ctx $ \ty_a (TermLC x) ->
			check_con (At (Just tok_a) (ty @Ord :$ ty_a)) $ \Con ->
			k (ty_a ~> ty_a) $ TermLC $
			 \c -> lam $ \y -> op (x c) y