{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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.String (IsString)
import Data.Text (Text)
import qualified Data.Kind as Kind
import Prelude hiding (Ord(..))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Bool
import Language.Symantic.Compiling.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 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 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
 Proj_ConC cs (Proxy Ord)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , 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 ast
 ) => Term_fromI is (Proxy Ord) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy Ord ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "compare" -> test2_from compare tyOrdering
		 "<="      -> test2_from (<=)    tyBool
		 "<"       -> test2_from (<)     tyBool
		 ">="      -> test2_from (>=)    tyBool
		 ">"       -> test2_from (>)     tyBool
		 "min"     -> op2_from min
		 "max"     -> op2_from max
		 _ -> Left $ Error_Term_unsupported
		where
		test2_from
		 :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
		 -> Type (Consts_of_Ifaces is) (res::Kind.Type)
		 -> Either (Error_Term is ast) ret
		test2_from op ty_res =
			from_ast1 ast $ \ast_x as ->
			term_from ast_x ctx $ \ty_x (TermLC x) ->
			check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
			k as (ty_x ~> ty_res) $ TermLC $
			 \c -> lam $ op (x c)
		op2_from
		 :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term a)
		 -> Either (Error_Term is ast) ret
		op2_from op =
			from_ast1 ast $ \ast_x as ->
			term_from ast_x ctx $ \ty_x (TermLC x) ->
			check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
			k as (ty_x ~> ty_x) $ TermLC $
			 \c -> lam $ op (x c)

-- | The 'Ord' 'Type'
tyOrd :: Inj_Const cs Ord => Type cs Ord
tyOrd = TyConst inj_const

-- | The 'Ordering' 'Type'
tyOrdering :: Inj_Const cs Ordering => Type cs Ordering
tyOrdering = TyConst inj_const

sym_Ord :: Proxy Sym_Ord
sym_Ord = Proxy

syOrd :: IsString a => [Syntax a] -> Syntax a
syOrd = Syntax "Ord"