{-# 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 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 NameTyOf Ordering where
        nameTyOf _c = ["Ord"] `Mod` "Ordering"
instance ClassInstancesFor Ordering
instance TypeInstancesFor Ordering

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

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

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

-- * Class 'Sym_Ord'
type instance Sym 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 NameTyOf Ord where
        nameTyOf _c = ["Ord"] `Mod` "Ord"
instance FixityOf Ord
instance ClassInstancesFor Ord where
        proveConstraintFor _ (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, SymInj 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