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

import Data.Ord (Ord)
import Prelude hiding (Ord(..))
import qualified Data.Ord as Ord
import qualified Data.Text as Text

import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Eq (Sym_Eq)

-- * Class 'Sym_Ordering'
type instance Sym (Proxy Ordering) = Sym_Ordering
class Sym_Eq term => Sym_Ordering term where
	ordering :: Ordering -> term Ordering
	default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering
	ordering = trans . ordering

-- Interpreting
instance Sym_Ordering Eval where
	ordering = Eval
instance Sym_Ordering View where
	ordering o = View $ \_p _v ->
		Text.pack (show o)
instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (Dup r1 r2) where
	ordering o = ordering o `Dup` ordering o

-- Transforming
instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)

-- Typing
instance ClassInstancesFor Ordering
instance TypeInstancesFor Ordering

-- Compiling
instance Gram_Term_AtomsFor src ss g Ordering
instance (Source src, Inj_Sym ss Ordering) => ModuleFor src ss Ordering where
	moduleFor = [] `moduleWhere`
	 [ "LT" := teOrdering LT
	 , "EQ" := teOrdering EQ
	 , "GT" := teOrdering GT
	 ]

-- ** 'Type's
tyOrdering :: Source src => Inj_Len vs => Type src vs Ordering
tyOrdering = tyConst @(K Ordering) @Ordering

-- ** 'Term's
teOrdering :: Source src => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o

-- * Class 'Sym_Ord'
type instance Sym (Proxy Ord) = 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  :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Ordering
	default (<)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
	default (<=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
	default (>)      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
	default (>=)     :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term Bool
	default max      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
	default min      :: Sym_Ord (UnT term) => Trans term => Ord a => term a -> term a -> term a
	
	compare  = trans2 compare
	(<)      = trans2 (<)
	(<=)     = trans2 (<=)
	(>)      = trans2 (>)
	(>=)     = trans2 (>=)
	min      = trans2 min
	max      = trans2 max

-- Interpreting
instance Sym_Ord Eval where
	compare  = eval2 Ord.compare
	(<)      = eval2 (Ord.<)
	(<=)     = eval2 (Ord.<=)
	(>)      = eval2 (Ord.>)
	(>=)     = eval2 (Ord.>=)
	min      = eval2 Ord.min
	max      = eval2 Ord.max
instance Sym_Ord View where
	compare  = view2 "compare"
	(<)      = viewInfix "<"  (infixN 4)
	(<=)     = viewInfix "<=" (infixN 4)
	(>)      = viewInfix ">"  (infixN 4)
	(>=)     = viewInfix ">=" (infixN 4)
	min      = view2 "min"
	max      = view2 "max"
instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (Dup r1 r2) where
	compare    = dup2 @Sym_Ord compare
	(<)        = dup2 @Sym_Ord (<)
	(<=)       = dup2 @Sym_Ord (<=)
	(>)        = dup2 @Sym_Ord (>)
	(>=)       = dup2 @Sym_Ord (>=)
	min        = dup2 @Sym_Ord min
	max        = dup2 @Sym_Ord max

-- Transforming
instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)

-- Typing
instance FixityOf Ord
instance ClassInstancesFor Ord where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
	 | Just HRefl <- proj_ConstKiTy @_ @Ordering z
	 = case () of
		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
		   | Just Refl <- proj_Const @Enum    q -> Just Dict
		   | Just Refl <- proj_Const @Eq      q -> Just Dict
		   | Just Refl <- proj_Const @Ord     q -> Just Dict
		   | Just Refl <- proj_Const @Show    q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Ord

-- Compiling
instance Gram_Term_AtomsFor src ss g Ord
instance (Source src, Inj_Sym ss Ord) => ModuleFor src ss Ord where
	moduleFor = ["Ord"] `moduleWhere`
	 [ "compare" := teOrd_compare
	 , "<"  `withInfixN` 4 := teOrd_lt
	 , "<=" `withInfixN` 4 := teOrd_le
	 , ">"  `withInfixN` 4 := teOrd_gt
	 , ">=" `withInfixN` 4 := teOrd_ge
	 ]

-- ** 'Type's
tyOrd :: Source src => Type src vs a -> Type src vs (Ord a)
tyOrd a = tyConstLen @(K Ord) @Ord (lenVars a) `tyApp` a

-- ** 'Term's
teOrd_compare :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Ordering))
teOrd_compare = Term (tyOrd a0) (a0 ~> a0 ~> tyOrdering) $ teSym @Ord $ lam2 compare

teOrd_le, teOrd_lt, teOrd_ge, teOrd_gt :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> Bool))
teOrd_le = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<=)
teOrd_lt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (<)
teOrd_ge = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>=)
teOrd_gt = Term (tyOrd a0) (a0 ~> a0 ~> tyBool) $ teSym @Ord $ lam2 (>)

teOrd_min, teOrd_max :: TermDef Ord '[Proxy a] (Ord a #> (a -> a -> a))
teOrd_min = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 min
teOrd_max = Term (tyOrd a0) (a0 ~> a0 ~> a0) $ teSym @Ord $ lam2 max